theorem Hex.GraphIso.Nauty.Sparse.compare_same {n : Nat} (level code : Nat) (st : State n) : (compareCodes level code st).allsamelevel = st.allsamelevel

theorem Hex.GraphIso.Nauty.Sparse.target_same {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (chooseTarget first g tcLevel level numcells st).snd.snd.snd.allsamelevel = st.allsamelevel

theorem Hex.GraphIso.Nauty.Sparse.classify_same {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : (classify g level numcells st).snd.allsamelevel = st.allsamelevel

theorem Hex.GraphIso.Nauty.Sparse.leafExit_same {n : Nat} (leaf : Leaf) (level : Nat) (st : State n) : (leafExit leaf level st).snd.allsamelevel = st.allsamelevel

theorem Hex.GraphIso.Nauty.Sparse.recover_same {n : Nat} (inf level : Nat) (st : State n) : (recoverLevels level (recoverPtn inf level st)).allsamelevel = st.allsamelevel

theorem Hex.GraphIso.Nauty.Sparse.firstFloor {n : Nat} (g : Graph n) (inf tcLevel bound : Nat) : Generic.BoundedPolicy g inf tcLevel bound fun (st : State n) => bound ≤ st.allsamelevel ∧ bound ≤ st.eqlevFirst

Native calls below an ancestor retain its lower bounds on first-code agreement and the all-same boundary, including cached target dispatch.

theorem Hex.GraphIso.Nauty.Sparse.firstPath_floor {n : Nat} {g : Graph n} {inf tcLevel fuel level numcells last : Nat} {st leaf : State n} (path : Generic.FirstPath g tcLevel fuel level numcells st last leaf) : level ≤ (Generic.node true g inf tcLevel fuel level numcells st).snd.allsamelevel ∧ level ≤ (Generic.node true g inf tcLevel fuel level numcells st).snd.eqlevFirst

The actual first terminal installs both boundaries at its depth; every enclosing first call retains the bounds at its own entry level.