Finding Superaxioms

[From EdP]
In[]:=
PruneSubgraph[graph_,subgraph_]:=Module[{subBranches,branches,prunecheck,prunable},​​subBranches=Sort[Tally[Last/@Union[EdgeList[subgraph]]]];​​branches=Tally[Last/@Union[EdgeList[graph]]];​​prunecheck=Sort[Select[branches,MemberQ[First/@subBranches,#[[1]]]&]];​​prunable=Table[If[prunecheck[[n,2]]==subBranches[[n,2]],prunecheck[[n,1]],Sequence@@{}],{n,1,Length[prunecheck]}];​​If[Length[prunable]0,"Same graph",​​Graph[Select[EdgeList[graph],Not[MemberQ[prunable,First[#]]]&]]]]
In[]:=
With[{g=Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"12]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"9|>Red}]]
Out[]=
In[]:=
With[{g=PruneSubgraph[Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"12]],Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"9]]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"9|>Red}]]
Out[]=
In[]:=
Total[Length[VertexOutComponent[euc,#]]&/@VertexList[euc]]
Out[]=
25852
[[ Need tradeoff between number of axioms and reduction of this number ]]
In[]:=
ResourceFunction["ParallelMapMonitored"][#(If[!GraphQ[#],0,VertexCount[euc]-VertexCount[#]]&[PruneSubgraph[euc,Subgraph[euc,VertexOutComponent[euc,#]]]])&,VertexList[euc]]
Out[]=
In[]:=
ListLinePlot[%]
Out[]=
$Aborted
In[]:=
ListLinePlot[Values[%%]]
Out[]=
100
200
300
400
2
4
6
8
10

The above seems to be WRONG...

Instead, for any given theorem, stop if one reaches the superaxiom before the axioms

In[]:=
With[{g=Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"9,2]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyleLightBlue]]
Out[]=
In[]:=
With[{g=Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"9,2]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"2|>Red}]]
Out[]=
In[]:=
With[{g=GraphDifference[Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"9,2]],Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"2,2]]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"2|>Red}]]
Out[]=
In[]:=
With[{g=Subgraph[euc,VertexOutComponent[euc,"Book"2,"Theorem"9,2]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"2|>Red}]]
Out[]=

Another Definition

[[ Need tradeoff between number of axioms and reduction of this number ]]

Does the wrong thing for lower-numbered theorems....