feat(graph-iso): prove and adopt the structured search

[kim-em]

The structured engine now drives the public canonicalization, certification, generator and orbit APIs. Its complete key and generator-completeness theorems follow from actual generic-recursion calls and proved local rules, without legacy traversal correctness assumptions. Empty-graph certification and the public theorem statements are preserved.

The engine takes Nauty/Search/Search.lean and retains its nauty correspondence table. This removes the literal traversal, Nauty/Correct/, the old incumbent/closure proof, and recursive reach proof. Reusable primitive-state and reference/stabilizer mathematics remain in Search/State, Invariant, and Generation. The direct hot loop retains its proved equality with the policy recursion. Canonicalization does not import the full generation proof.

Validation:

• Both libraries, registered tests, conformance and HexManual: successful build after rebasing onto current main.
• All 6,233 fixture records unchanged byte for byte; nauty agrees on those and the 32,798-case campaign. Full wrapper twin passes. Negative oracle controls reject altered rows, labels and node counts.
• Axiom guards cover engine and public correctness; dependency audit finds no legacy traversal proof. No added sorry, axiom, or native_decide.
• Chungus2 cactus data, manifest, figures and tactic timings committed under 4fa1958f160d; freshness and the existing 0.2 exponent check pass.
• All 98 benchmark node counts match the spike. Current/archive engine-time geometric mean is 1.0012 (worst instance 1.0243), comparing one current run with the archived three-run median.
• A temporary newest-32-pair filter changes a normal-root traversal from 168 to 712 nodes, preserving key and 11 generators with local proof changes. This demonstrates locality parity with the legacy proof, not an exclusive advantage or speedup. Production retains the original full scan.

The dependency checker now includes import all edges in build reachability, with a regression test; sealed-import restrictions are unchanged. The library umbrella also includes the standalone trace proof, and the policy entry point includes the first-root proof.

Optimization scope: changes inside policy operations have local obligations; changes to recursion shape must maintain direct/generic agreement and may require new return and generation arguments. The primitive SearchSt view remains a maintenance cost.

Proof structure and validation details: reports/hex-graph-iso-obligations.md; locality evidence: reports/hex-graph-iso-locality.md.

Closes #10043.

[kim-em]

The independent Opus review found no correctness defect or vacuous assumption in the completed engine/generic equivalence, checked-admission, reachability, exhaustive-policy, or local leaf-maximum proofs. Its medium findings concern the still-missing whole-search coverage argument.

Implemented follow-up:

• pruneReturn_target proves the arithmetic split between a target at or above eqlevCanon and the cheap-boundary target.
• Comparison.prune_witness and Comparison.prune_result give actual code-prune exits a Generic.Result carrying semantic ancestor coverage. The witness uses cs.take (t + 1): the review's sample cs.take t loses the first unequal code when t = eqlevCanon, so that proposed statement was not used.
• SubtreeOk.node_key and SubtreeOk.path_key prove that any complete selected descent in a small-cell subtree realizes its entire specification key, including codes. The underlying child-key theorem is now outside Correct/.
• Removed the redundant positive-size premise from Trivial.Complete, documented its immediate-parent stack discipline, clarified that generic sweep entries may represent vertices or offsets, and removed the dummy empty graph context in the depth proof.

The review's proposed stack redesign is unnecessary for the exhaustive instance: recover_child and node_eq establish the current balance and immediate-parent return. The generic module contains the executable recursion, so keeping the direct engine's reducible Exit/Leaf aliases there does not introduce a dependency on proof modules. The matching engine/legacy result names remain namespace-qualified during the migration; their public replacement and deletion must be atomic once maximum soundness is available.

Still unresolved: the full pruning invariant (AutosOk/PairOk, orbit witnesses, and frozen ancestor frames), binding path codes to those frames through the actual recursion, and composing all cheap and automorphism returns into whole-search coverage. Checked automorphism validity alone does not establish the ancestor stabilization needed by the pair ledger. Consequently the public search switch and legacy deletions are not ready, and this PR remains a draft rather than claiming #10043 is complete.

[kim-em]

Follow-up to the independent Opus review:

• Extracted FixedCells, LocalAutos, PathStab, and the reusable PathOk transitions into Invariant/PathStab.lean. The legacy root initializer remains with the literal search. NodePre, SweepPre, and FirstPre now carry current-partition stabilization; the initial state and both actual call paths establish it. SweepPre.local_pairs combines this path evidence with the root ledger at the consuming partition.
• Proved node_fixed through Generic.CallPolicy, including first-path and off-path calls, nonlocal exits, and fuel exhaustion. Target-cell singleton evidence proves the chosen vertex fresh, and child cleanup restores the exact parent fixed set before recovery. This supplies the missing premise of the path-stabilization return transition.
• Added WorkspaceOk to the persistent and first-entry invariants. Explicit/implicit admissions preserve positive capacity and the array bound, and the actual first descent establishes the invariant.
• Added Covers.keysMax, Result.node, and witness implication transport. The saved first-reference history now records its actual code array contents; FirstRef.code_eq connects those contents to the semantic comparison codes, and pathKey_codes identifies the key's real-code prefix.
• The claim that colour stabilization had no consumer was incorrect: PairsOk.admit consumes it for every explicit admission. A separate public colour/IsIso bridge was optional, and main now supplies its own AutTrace bridge through feat(graph-iso): prove full automorphism generation and exact group order #10108. I did not reorder CheapOk's existing array arguments: the explicit instantiations are correct, and that stylistic change is not needed for correctness.

The fixed ancestor code binding, cheap/automorphism unwind coverage, short-prune fix-test receipt, and whole-engine maximum remain unfinished. Witness implication transport alone does not establish the missing frozen-frame binding. The public search migration and legacy deletion are still gated on those proofs. The new public generation-completeness dependency from #10108 is documented separately on #10043; it also needs a transfer that canonical-key equality does not supply.

[kim-em]

Follow-up to the independent Opus comparison review:

• The full-window carrier lemma is now named SweepPre.window_carriers. FilterCover.lean instead proves long-filter coverage for an arbitrary mutable live subset using ChildCover.filterDesc, the actual pair-drop theorem, and vertex-indexed specification keys. It carries earlier coverage through incumbent growth, cursor advancement, and parent recovery. The short-filter counterpart retains the receiving fix-test premise explicitly; integrating that producer and these lemmas into the whole maximum contract remains unfinished.
• recover_filters proves both filters read the same workspace before and after recovery. pruneReturn_short and leafExit_cheap_short derive implicit admission from the actual short flag. Generic.ShortPolicy instantiates the common recursion to transport leaf-emission properties. Its nauty instance supplies node_origin and sweep_origin; LeafReturn.admission identifies the newest pair at a returned state using capacity supplied there.
• Factored the executable post-child control into Generic.advance and Generic.resume. Reach, fuel, fixed-point, safety, comparison, and short-return contracts now state their local theorems over those operations. The direct-engine equality still builds.
• Moved Comparison.prepare into its sole consumer, CodeCalls.lean, and removed the comparison import from Prepared.lean; pared the safety imports accordingly.
• I disagree that discarding the explicit Grows result loses the first-leaf lower bound: ReturnCodes.lower already states keyLe (incKey ctx fs st.firstlab) (incKey ctx bs st.canonlab) and survives firstPath_codes and the real root initializer. No redundant induction was added for that bound.

The remaining coverage contract will retain frozen ancestor information separately from the settled comparison receipt. The draft remains incomplete and is not ready to merge.

[kim-em]

Addressed the fifth Opus review's concrete findings:

• Short-return admission now uses the receiving state's fields and proves the return target is at most noncheaplevel - 1 for implicit pairs, or equals gcaCanon for explicit pairs.
• The implicit fix test is proved for an actual returned child, using its partition effect, restored fixed points, and frozen singleton cells. It does not assume the conclusion as a filter precondition.
• Removed unused workspace wrappers, renamed the new coverage relation to CellCover, aligned short-return binder order with the executable operations, and added cursor exhaustion and representative-skip rules.
• Added canonical-ancestor bounds to actual node and sweep preconditions. CanonOut now tracks reference installations and both ancestor bounds through the common recursion; canon_old identifies the retained parent reference on an upward return, and canon_guide/canon_locate connect it to covered ancestor children.

The review found no correctness defect in the original short-return origin or mutable coverage proofs. Its remaining integration concerns are still applicable: the explicit pair's receiving fix test, actual first-path orbit-skip justification, and the whole-engine maximum are unfinished. The new guide restoration consumes child coverage as the intended induction hypothesis; it does not itself establish whole-search coverage. The PR remains a draft.

[kim-em]

Addressed the canonical-reference review in the short-filter batch:

• The generic sweep now proves its unconditional strict unwind bound through SoundPolicy. Both actual node branches have strict bounds, and child_target identifies a received child target with the parent level.
• Canonical-reference transport and pair validity now have partition-based entry points that apply before any sibling has returned. child_canon_guide includes both first-child and fixed-point cleanup; first_return_pair proves validity after the actual leftmost child's cleanup without a later-sibling precondition.
• Short-return provenance retains the actual classifier. LeafReturn.admission transports its scatter relation and recorded generator; return_pair derives local validity for both explicit and implicit pairs. SweepPre.return_cover applies that result to the actual short filter. The obsolete, weaker short_admission wrapper is removed.
• CanonGuide.mem proves membership in the original target window, which can contain vertices removed from the mutable target set.
• Shared canonical-control lemmas replace the duplicate admission, prune, and recovery proofs. FixedCells.ofSearchOut delegates to ofEffect. Result imports the new proof layer without publicly re-exporting it.
• All new proof modules are committed and reached by the library build. The small-cell shape is also carried by the actual node and sweep preconditions, including first-child recovery.

The dummy target-level argument remains in the policy-independent child proof, consistent with the other local-policy instantiations. No executable behavior was changed. The whole-engine maximum, nonlocal coverage witnesses, first-path orbit coverage, generation completeness transfer, public migration, and deletions remain unfinished; the PR remains a draft.