# v0.9 graph-semantics and correctness design Status: released Baseline release: v0.8.0 Released version: v0.9.0 ## Purpose v0.9 strengthens the public finite-graph layer before attempting a faster proof-net correctness checker. The existing `Graph.isTree` implementation and its exact `isTree_iff_isTree` theorem remain the trusted reference behavior. The new work must preserve undirected multigraph edge occurrences rather than silently collapsing parallel stored edges. ## Completed first increment `Graph.Acyclic` means that every `Graph.EdgeSimpleCycle` yields `False`. `EdgeSimpleCycle` tracks exact list indices, so two parallel stored edges can form a genuine cycle of length two. The kernel now checks: - `acyclic_iff_not_nonempty_edgeSimpleCycle`; - `IsTree.no_edgeSimpleCycle`; - the public wrapper `IsTree.acyclic`; - exact transport of directed edge occurrences, edge-aware walks, and simple cycles through every bounded bijective vertex renaming; - `Acyclic.reindex` and the bidirectional `acyclic_reindex_iff`; - a cyclic-triangle negative regression and a checked-tree positive regression, plus a length-two parallel-edge cycle and nontrivial reindexing regressions. `IsTree.acyclic` is included in the generated public API and the exact axiom audit. It currently depends on exactly `[propext, Classical.choice, Quot.sound]`, matching the existing public MLL graph/sequentialization boundary. The two public acyclicity-transport theorems require exactly `[propext, Quot.sound]` and do not introduce `Classical.choice`. ## Completed converse The kernel now checks: ```lean graph.Bounded ∧ graph.Connected ∧ graph.Acyclic → graph.IsTree ``` The proof does not retain `edges.length + 1 = vertexCount` as a redundant premise. It constructs the graph of shortest-path parent edges, proves that graph is a spanning `IsTree`, and lifts its simple paths back into the ambient multigraph with exact edge provenance. Any ambient edge outside the parent graph closes one of those paths into an `EdgeSimpleCycle`. Acyclicity also rules out duplicate stored edge values at distinct indices, because two such occurrences form a length-two cycle. These facts give the upper forest bound: ```lean graph.edges.length + 1 ≤ graph.vertexCount ``` Connectedness supplies the opposite inequality through `Connected.vertexCount_le_edges_add_one`, yielding the public exact theorem: ```lean graph.IsTree ↔ graph.Bounded ∧ graph.Connected ∧ graph.Acyclic ``` Both new public theorems are included in the generated API and exact trust audit. They depend on exactly `[propext, Classical.choice, Quot.sound]`. ## Completed certified reference decision `Graph.isEdgeSimpleCycleTraversal` validates one nonempty directed-edge sequence by checking ordered closure, duplicate-free stored edge indices, and duplicate-free source vertices. Lean proves both directions between accepted sequences and `EdgeSimpleCycle`. `Graph.edgeSimpleCycleTraversalCandidates` exhaustively enumerates directed edge sequences of lengths one through `edges.length`. Since every exact simple cycle has at most that many stored edge occurrences, the resulting `Graph.hasEdgeSimpleCycle` is complete. The kernel now checks: ```lean graph.hasEdgeSimpleCycle = true ↔ Nonempty graph.EdgeSimpleCycle graph.isAcyclic = true ↔ graph.Acyclic ``` The candidate family is exponential. It is a transparent executable specification oracle, not the planned optimized implementation. Combining the decision theorem with the completed forest converse gives a second tree path: ```lean graph.isTreeViaAcyclic = true ↔ graph.IsTree graph.isTreeViaAcyclic = graph.isTree ``` The regression boundary includes self-loops, equal parallel stored edges, oppositely oriented parallel stored edges, a triangle, a disconnected forest, and a tree. Six new public theorems are locked in the exact axiom audit; the traversal-level pair depends on `[propext, Quot.sound]`, while the four global decision/tree theorems depend on `[propext, Classical.choice, Quot.sound]`. ## Optimized-checker plan The first non-enumerative proof-net component is now kernel checked: ```lean Certificate.verifyDerivation? : Certificate → CutFreeDerivation → Option (DerivationVerificationResult certificate) ``` It does not evaluate the all-switchings checker on the input. It checks structural well-formedness, independently infers and desequentializes the submitted derivation, and compares the result through the non-factorial intrinsic canonical code. A successful value carries an accepted output and an exact `ProofNetEquivalent` proof. The completeness theorem covers every structurally well-formed input when the supplied derivation desequentializes to an equivalent net. The automatic layer is now also kernel checked. `reconstructDerivation?` first runs a structure-guided inverse-rule path: it recursively tries the executable terminal-par peel and splitting-tensor partition candidates, aligns repeated boundary occurrences by formula-tree/axiom profiles, composes the complete derivation, and then calls `verifyDerivation?` once. If that heuristic result is absent or rejected, the proved recursively verified exhaustive path remains the fallback. Neither executable path contains a `Certificate.check` call. Lean proves: ```lean input.check = true → ∃ result, input.reconstructDerivation? = some result input.reconstructsDerivation = input.check ``` Successful reconstruction therefore produces a formula-valid cut-free derivation, an accepted desequentialization, and exact `ProofNetEquivalent` identity. The reference checker occurs only in the statement/proof of completeness, not in the runtime search. The current search is not a linear-time contraction algorithm. The fast path does not eagerly materialize the exhaustive repeated-label fallback, but the fallback can still backtrack over terminal links and enumerate formula-compatible boundary orders. Remaining qualification work is: 1. prove or enforce a user-facing worst-case resource bound for fallback backtracking and repeated-label order search; 2. state only the complexity bound actually proved or measured; 3. retain `Graph.isTree`, `Graph.isAcyclic`, and all-switchings enumeration as specification oracles. The colored-cycle development proves, under structural well-formedness, that `CuspAcyclic` is equivalent to exact occurrence-aware acyclicity of every switching. A finite maximal-forest theorem now also proves the connectedness/tree component: every switching retains the same edge count, so one connected all-left reference switching suffices. Lean proves the compact factoring `check = true ↔ StructurallyWellFormed ∧ CuspAcyclic ∧ ReferenceSwitchingConnected`. `compactCheck` executes this criterion without enumerating switchings and is proved Boolean-equal to `check`. Its `isCuspAcyclic` phase still enumerates exact cycle traversals. The next algorithmic layer now exists in initial form. `unificationFastCheck` implements eager axiom/start, par/forward, and tensor/unify token rules while carrying partial derivation components. A candidate must pass `verifyDerivation?`, so its soundness is kernel checked. `unificationCheck` combines that fast path with the already complete checker-free reconstruction fallback and is proved Boolean-equal to `check`. It never enumerates switching graphs. The pure fast path is not yet proved complete, and eager repeated scans plus the exhaustive miss fallback do not inherit Guerrini's linear bound. See [guerrini-unification-audit.md](guerrini-unification-audit.md). The public fail-closed boundary is now `reconstructDerivationWithinLimits`. It rejects inputs above explicit formula, link, or conclusion ceilings before search and never invokes the exhaustive fallback. The qualified default is 128/96/24, matching the adversarial qualification envelope with headroom. Its `noCandidate` and `candidateVerificationFailed` errors are not logical rejection; Lean proves only the safe direction that every bounded success is sound, reference-accepted, and accepted by the complete unbounded decision. A step-count or external deadline contract remains separate work. The frozen v0.2-shaped 1,000-case runtime audit is complete: checker-free reconstruction agreed with the reference on 250 positives and 750 deterministic malformed mutations, completing in 2,798 ms on the recorded Windows run under a 15-second CI budget. After adding a fail-fast structural gate, the current recorded run completed in 413 ms. This is differential qualification, not the complexity proof still listed above. The separate adversarial stress executable covers 18 right-skewed, balanced tensor, balanced par, and alternating identity nets with one repeated internal atom, including repeated-boundary expansion, reversed link storage, and inputs through 126 formula occurrences and 22 conclusions. The recorded Windows run completed in 34,416 ms under a 45-second CI budget. Before the fast-path change, right-tensor depth 8 and balanced depth 4 exceeded bounded exploratory timeouts. This bounded before/after regression is not an asymptotic claim. The new reconstruction and hybrid-unification theorems are exact alternative correctness decisions, but they do not prove a linear-time proof-net criterion. The deterministic unification tier now has its own source mapping, soundness theorem, 1,500-case differential gate, main benchmark counter, and adversarial stress coverage. Its completeness, worklist invariant, and complexity theorem remain separate requirements before any linear production claim.