theorem
Hex.GraphIso.Nauty.Max.NodeInput.reference_tree
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel false f bs fs parents)
:
Generation.TreeOk ctx f.level (SearchState.refined ctx f.level f.numcells f.entry)
The actual off-path input supplies the complete mathematical tree invariant after refinement.
theorem
Hex.GraphIso.Nauty.Max.Loop.reference_prepare
{n : Nat}
{ctx : Ctx n}
{tcLevel tc : Nat}
{f : Frame n}
{targets : List Nat}
{key : Key n}
(ht : Generation.TreeOk ctx f.level (SearchState.refined ctx f.level f.numcells f.entry))
(hm : Generation.Matches ctx f.level f.entry (tc :: targets) key)
(hp : Generation.HasLeaf ctx tcLevel f.level (SearchState.refined ctx f.level f.numcells f.entry) (tc :: targets) key)
(heq : f.entry.eqlevFirst = f.level - 1)
(hn : (SearchState.refined ctx f.level f.numcells f.entry).numcells < n)
:
have l := { node := f, first := false };
have p := prepare ctx tcLevel l;
have rs := SearchState.refined ctx f.level f.numcells f.entry;
have mt := specMaketargetcell ctx rs.lab rs.ptn f.level tcLevel;
(have q := prepareOther ctx tcLevel f.level f.numcells f.entry;
(classify ctx f.level q.fst q.snd.snd.snd.snd.snd).fst = Generic.Leaf.internal) ∧ p.snd.fst = Int.ofNat mt.fst ∧ p.snd.snd.fst = mt.snd.fst ∧ p.snd.snd.snd.fst = mt.snd.snd ∧ p.snd.snd.snd.snd.eqlevFirst = f.level ∧ SearchState.reference p.snd.snd.snd.snd = SearchState.reference f.entry ∧ p.snd.snd.snd.snd.allsamelevel = f.entry.allsamelevel ∧ p.snd.snd.snd.snd.gcaFirst = f.entry.gcaFirst ∧ p.snd.snd.snd.snd.gcaCanon = f.entry.gcaCanon
A matching internal node prepares exactly the specification target and retains first-reference agreement, regardless of the canonical comparison.