# v0.10 unification completeness design Status: active development Baseline release: v0.9.0 ## Purpose v0.10 targets the exact gap intentionally left by v0.9: prove that the pure event-driven token-unification path succeeds on every correct unit-free, cut-free MLL certificate, without appealing to recursive inverse-rule reconstruction. Complexity claims remain a later layer. A universal completeness theorem must not be inferred from the existing 7,200-case counterexample search. ## Formal layers ### 1. Independent rule semantics Define a proof-irrelevant marking/partition state and an inductive one-step relation with exactly three rules: - axiom/start assigns one fresh token to both unmarked axiom conclusions; - par/forward marks a conclusion when its two premises have the same current representative; - tensor/unify marks a conclusion and merges two distinct premise classes. The relation must state freshness, range, and occurrence bounds without referring to the executable scan or worklist functions. Prove that every executable firing refines one semantic step. Separately retain the existing derivation-component invariant so every fired token class denotes a genuine partial cut-free derivation. The abstract relation uses a fixed `Nat` carrier and an allocated initial segment. Allocating token `tokenCount` therefore preserves the global thread equivalence and separately proves that this carrier element was isolated from all previously allocated tokens. Defining the extension only on the enlarged initial segment is invalid here because it would violate reflexivity outside that segment. ### 2. Scheduler coverage State an invariant connecting every unmarked connective to one of: - idle because at least one premise is unmarked; - queued because a premise was newly marked; - waiting par because both premises are marked with distinct classes; - permanent tensor deadlock because both premises have the same class; - already fired. Prove initial connective enqueues establish the invariant, marking a conclusion enqueues all newly affected consumers, and every tensor merge requeues all pars whose representatives may have changed. This theorem is about absence of missed enabled work, not proof-net correctness. ### 3. Fuel sufficiency Prove bounds for successful enqueue sources: - at most one initial enqueue per connective; - at most one distinct dependency enqueue per successful firing, because structural linear ownership makes every premise-consumer bucket constant; - at most one submitted-link carrier of waiting-par requeues per successful tensor firing. Use queue deduplication and single-firing of connective conclusions to show that the existing `n(n+4)+1` fuel reaches an empty queue rather than merely stopping the recursive evaluator. ### 4. Correct-state progress Connect the independent marking semantics to the already proved switching criterion. For a structurally well-formed correct certificate, prove that a quiescent nonfinal state cannot contain a tensor deadlock and cannot contain only waiting/idle links. Therefore scheduler quiescence implies total marking and one token class. Combine this with the existing independent derivation verifier to prove: ```text Certificate.unificationWorklistFastCheck = Certificate.check ``` Only after this theorem is checked may the recursive reconstruction fallback be removed from the logical decision. ### 5. Sequential linear implementation Pure completeness does not imply Guerrini's linear-time theorem. Replace eager all-axiom starts and flat waiting requeues with the Figures 7--8 stack: - build later-state start selection around the now-kernel-checked bounded/tagged `NEXTAXIOM`. Per-call trace/tag invariants, exact oriented source-left routes, and touched-set disjointness for successive calls that strictly thread `first.tags` are already proved. Initial/local totality is proved under rank-scoped freshness with fuel greater than the start complexity. It does not establish freshness for a later Figure-7 `new` call or totality of the carrier-size wrapper. Since any success tags complexity-zero axiom endpoints, this global low-rank predicate cannot be threaded to a second call; introduce a route-local scheduler invariant; - retain the now-kernel-checked first delayed state slice: `RawTokenAge` is discovery order rather than a representative, `SigmaAgePartition` encodes strictly increasing raw-age boundaries below the horizon, and fixed-capacity waiting storage distinguishes out-of-bounds, undefined `⊥`, and initialized empty `∅`. Strict empty `init` leaves `W(0)` undefined. The printed Figure-7 `new` writes the fresh top even though the prose defines `W` on inactive boundaries and `unify` reads the old predecessor. Keep `newEnqueue?` only as a literal source-audit helper. Production `operationalNewEnqueue?` initializes the old active boundary, leaves the fresh top undefined, and preserves the kernel-checked `OperationalWaitingDomain` stating that initialized allocated cells are exactly `sigma.dropLast`. This is the project's operational interpretation, not an author-confirmed erratum; - the production bridge implements initial and fully tag-threaded typed later reservations, proves the narrow `RealizesSigma` relation between delayed and production state, threads the complete output tags, and preserves `ReservationInvariant`, including `OperationalWaitingDomain`. The local Figure-7 pipeline also synchronizes pop-before-mark, raw-age marking, tensor-mate selection, post-mark `NEXTAXIOM`, and operational `new`. These preservation theorems alone do not characterize reachability or prove later-state search totality. The separate `InitNewHistory` now records exact empty/init/new executions and proves tag provenance, global submitted-slot non-reuse, and reservation-count alignment. Exact local `concl`/`nop`/`wait` transitions now sit outside that history; `wait` performs one raw-age-to-boundary initialized-cell cons without an ownership claim; - then formalize ready/waiting payload ownership, the executable `forward`/`unify` transitions, and full-history integration of the now-local `concl`/`nop`/`wait` rules, preserving the operational waiting domain, queue provenance, and a full-rule reachable state invariant; - keep the existing `dynamicStartWithFuel?` as an independent eager Figure-5 refinement only. Figures 7–8 `init`/`new` delay endpoint marking by pushing endpoints into `R`; - state scheduler guards over raw assigned token ages, not their union-find representatives; - prove the special ordered union-find representation correct; - count every vertex visit, queue/stack operation, representative operation, and final verification cost. The library may claim Guerrini-style whole-program linearity only after this separate cost theorem is kernel checked for the actual executable. ### Rejected flat-scheduler invariant and proof-plan split The current flat eager scheduler cannot be assigned the Figure-7 token-age/LIFO invariant. A stable accepted certificate with three axioms and two tensors starts token ages 0, 1, and 2 in submitted link order. Because the initial connective queue is reversed, its first tensor firing joins ages 0 and 2; the complete worklist run succeeds in two attempts with zero waiting requeues and two firings. The counters are only the public regression receipt: the noncontiguous class follows from the fixed links plus the eager-start and reverse-queue definitions. Similarly, `tagSchedulerFamily.step` numbers a selected dependency-cycle segment rather than worklist time or token age. The terminal order `firstTag → lastTag → anchor → outerLast` gives separated endpoint pairs, and ordinary laminarity permits them as siblings. It cannot by itself establish that the alleged outer pair is an operational ancestor containing the inner pair. The v0.10 proof plan therefore splits. Two initially plausible confluence relations are already too fine: exact concrete-state confluence fails on a derivation-generated correct certificate, and structural-only confluence fails on a structurally well-formed certificate. Current flat-worklist completeness may instead be pursued by proving that `ResidualParsingWitness` is preserved by every successful competing firing, or by a local-confluence theorem modulo the candidate observation ```text (marked occurrence domain, occurrence-thread partition). ``` The two exploratory counterexamples use the following exact incidence lists (atomic occurrences are paired by the displayed axioms and the remaining occurrences are the displayed tensor conclusions): ```text correct, exact-state counterexample axiom 0 1 axiom 2 3 axiom 4 5 tensor 0 2 6 tensor 1 4 7 conclusions [7, 6, 3, 5] structural-only counterexample axiom 0 1 axiom 2 3 tensor 0 2 4 tensor 1 3 5 conclusions [4, 5] ``` In the first certificate both tensor orders terminate successfully but retain different raw union/derivation construction histories; in the second, whichever tensor fires first disables the other. These fixtures are recorded here as counterexample inputs, not as a committed executable regression. An uncommitted exploratory local audit of 80 derivation-generated correct certificates visited 2,734 reachable quotient states and 7,148 enabled critical pairs, with 0 disabled pairs and 0 quotient non-diamonds. No committed script or artifact currently reproduces those counts, so they are not a release or CI gate. This is not a local-diamond, confluence, progress, pure-worklist-completeness, or complexity theorem. Guerrini-style linearity instead requires extending the separate bounded/tagged `NEXTAXIOM` checkpoint through the proved initial production bridge and faithful full `R`/`W` token-age sequencing; the independent raw-age `σ`/waiting state plus one reservation is still only the first slice. Neither route changes the already complete general checker-accepted sequentialization theorem. Canonicalization likewise remains exact only for `ProofNetEquivalent`, which preserves ordered conclusions; it is not arbitrary unlabeled graph isomorphism. ## Release gates - [x] independent proof-irrelevant marking state and Figure-5 step relation; - [x] raw token identity separated from semantic thread equivalence; - [x] executable-to-abstract state map under an explicit bounds contract; - [x] representative-range validity made an explicit abstraction precondition; - [x] executable mark-array/domain alignment made an explicit precondition; - [x] representative idempotence made explicit and conclusion marking proved to preserve the abstraction contract; - [x] concrete conclusion marking proved to refine the independent forward rule under the exact par guards; - [x] representative lookups connected back to allocated raw marks and their semantic thread without additional axioms; - [x] fixed-carrier fresh-token semantics proved globally equivalent, with the newly exposed token isolated from every previously allocated token; - [x] identity-parent start preservation and exact abstract `start` refinement for the real `startAxiom?` execution path; - [x] successful real `firePar?` execution, including component construction, proved to refine one independent forward step; - [x] `MergeExtension` proved to preserve equivalence; - [x] cyclic-parent counterexample recorded during development and excluded by an ordered-forest invariant; - [x] ordered parents proved to imply representative range, sufficient-fuel stability, and representative idempotence; - [x] ordered parents preserved through axiom initialization, par/tensor firings, eager passes, and saturation prefixes; - [x] tensor guards factored into `unifyTokens?`, with concrete `mergeConclusion` bounds/forest preservation and real-firing observation equivalence; - [x] exact representative-update theorem equating `mergeConclusion` with `MergeExtension` on the full fixed carrier; - [x] eager connective firing, pass, and finite-saturation abstraction preservation plus independent execution refinement; - [x] whole successful initialization-plus-saturation reachable-state execution theorem from the empty marking; - [x] partial-derivation formula/frontier invariant for axiom, par, tensor, complete passes, saturation prefixes, and the whole successful eager run; - [ ] scheduler coverage invariant; - [x] operational queued/fired/idle/waiting/deadlock classification and initial-connective coverage; - [x] exact no-missed-dependency direction for the precomputed consumer table; - [x] sound deduplication flags plus coverage preservation for ordinary enqueues, dependency fan-out, waiting registration, and full waiting-par requeue; - [x] bounded queue/waiting registries, sound waiting deduplication, and pop preservation after clearing the exact head flag; - [x] pending-link premise/frontier coverage stated without incorrectly requiring consumed marked occurrences to remain exposed, plus exact one- and two-occurrence frontier-picker totality; - [x] guard-ready par/tensor component construction proved total under that invariant, and the processed popped connective reclassified as fired, idle, registered waiting, or tensor-deadlocked; - [x] every worklist processing branch proved to preserve the executable abstraction contract, ordered union-find forest, and live-component formula consistency; - [x] structural ownership proved to make every premise parent and every compound producer unique; - [x] exact frontier transport proved for successful par and tensor firings, including tensor representative changes and the newly created conclusion frontier; - [x] pending-premise coverage proved across every axiom start, every pop-and-process core branch, and the complete fuel-bounded production worklist run; - [x] canonical empty initialization proved to establish the bundled abstraction, ordered-parent, component/formula, and pending-frontier invariants used by the production worklist; - [x] atomic pop-and-process coverage proved for a submitted connective head: pop preserves every other classification, par/tensor firing transports it through exact consumer fan-out, tensor union preserves old shared-token classes, and processed-head reclassification restores full coverage; - [x] reverse consumer-table provenance proved for dependency fan-out; queue provenance and waiting-par provenance make every popped head a real connective; the bundled core, scheduler, flag, carrier, and provenance invariant is preserved through every finite production worklist run; - [x] exact queue/waiting membership-to-flag completeness and duplicate-free registries preserved through enqueue, registration, requeue, pop, processing, and every finite run; both registry lengths are bounded by the submitted-link carrier; - [x] exact transition and finite-run enqueue accounting, culminating in `linkAttempts + residual queue length = initial + dependency + waiting-requeue insertions` from canonical initialization; - [x] cumulative enqueue-source bounds and worklist fuel sufficiency: - [x] every successful dependency fan-out inserts at most one distinct link; - [x] proof-only firing history is duplicate-free, submitted, marked, and exactly counted, hence successful firings are bounded by the link carrier; - [x] each full waiting requeue inserts at most the old registry length, and the production invariant bounds that registry by the link carrier; - [x] initial, dependency, and waiting sources fit `n(n+4)+1`; - [x] any residual queue implies exact fuel exhaustion, so source bounds plus insertion/pop conservation prove the canonical final queue is empty; - [ ] correct-quiescent-state progress theorem; - [x] combine canonical queue exhaustion with scheduler coverage so every submitted but unfired connective yields an exact idle-premise, distinct-thread waiting-par, or same-thread tensor-deadlock witness; - [x] choose an unassigned conclusion of least formula complexity, recover its concrete submitted source link, and use strict premise complexity to rule out the idle-premise case; - [x] prove semantic-thread connectivity in the active all-left reference subgraph and use declarative reference-switching acyclicity to rule out same-thread tensor deadlock in a nonfinal reachable state; - [x] prove reachable markings causally closed, prove every active retained edge stays inside one token class, and derive exact equivalence between active-reference connectivity and union-find thread equality; - [x] strengthen the remaining waiting-par witness with a proof that its two marked premises have no active reference walk between them; - [x] prove occurrence-aware tree-edge exchange, flip exactly the submitted par occurrence, and obtain a reference simple path between its premises which avoids the par conclusion; - [x] turn active-component separation along that path into a concrete unmarked internal occurrence, distinct from both marked premises and the waiting par conclusion; - [x] expose an exact retained reference-edge occurrence directed from a marked path vertex into an unmarked target; - [x] select the first such frontier, retain its entirely active prefix, and prove that its source carries the waiting par's left-premise token; - [x] read the path backward to select the last inactive frontier, identify its marked target with the right-premise token, and derive one exact ordered decomposition with two distinct boundary occurrences; - [x] classify that boundary by an exact submitted-link lookup, excluding axiom and reverse-connective cases and retaining a forward par/tensor premise-to-conclusion occurrence; - [x] derive the classified frontier connective's local scheduler status: par omitted-premise/unassigned or registered/distinct-token, and tensor opposite-premise/unassigned after deadlock exclusion; - [x] derive that same local scheduler classification at the reverse-oriented right frontier; - [x] cut at the first unmarked-to-marked reentry, proving every intervening traversed occurrence has unmarked endpoints and retaining the exact local scheduler classifications at both boundary orientations; - [x] retain the globally minimum-complexity unassigned waiting conclusion and normalize both boundary classifications: each boundary target is strictly above that minimum or the boundary is an exact registered distinct-thread par; - [x] prove by strong induction that every unassigned occurrence reaches a concrete registered waiting par through strict formula-complexity descent, and retain such non-increasing chase endpoints for both orientations of the exact first inactive block; - [x] generalize the path/frontier/chase construction to every registered waiting par, prove that every dependency endpoint lies in the finite formula carrier, and prove that a dependency iteration of `formulas.size + 1` occurrences repeats a waiting conclusion while retaining every adjacent dependency witness; - [x] extract one concrete nonempty closed dependency segment with `earlier < later ≤ formulas.size`, equal endpoint conclusions, every vertex registered as waiting, and the full witness for every interval edge; - [x] retain every exact source-connective/premise step in the formula-descent chase inside each dependency, prove path composition and non-increasing endpoint complexity, and prove strict decrease for every nontrivial chase; - [x] lift every formula-premise descent step to its exact full occurrence-graph backward edge, compose nontrivial chases into vertex-simple internally cusp-free paths, retain unassigned evidence for every visited occurrence, retain the occurrence-exact lifted frontier, and exclude immediate frontier reversal by the first tail edge; - [x] classify the deterministic mask at the exact lifted full-edge index, transport the corresponding par/unique incidence colors, use structural typing and unique producer ownership to synchronize the first formula tail, propositionally bind the classified frontier and tail head to the actual last/first occurrences in the composed segment, and classify every nontrivial frontier/tail transition as a genuine par cusp or tensor-colored free turn; - [x] package every dependency as an exact composable complete-graph segment from its source waiting conclusion to its target, using the reversed source-par incidence, retained reference-prefix lift, and all-backward formula tail; - [x] concatenate the selected finite family into a genuinely nonempty closed occurrence-aware `fullGraph` walk with propositionally equal start/end conclusions; - [x] define exact-occurrence `Graph.EdgeWalk.NoImmediateReverse`, prove its duplicate-key, constant-orientation, and append rules, and prove every individual dependency segment internally nonbacktracking across all four internal regions/junctions; - [x] prove every immediate reversal at an adjacent dependency-segment junction forces the preceding dependency's formula chase to be reflexive; - [x] bind that reversal to the exact retained-frontier/full-edge occurrence and the next waiting par's source incidence, then cancel one such exact reverse pair while preserving endpoints, every remaining occurrence, and the nesting witness; - [x] iterate exact-occurrence cancellation over internal and cyclic closing junctions, preserve endpoints and surviving occurrences, and derive the exhaustive empty-or-cyclically-nonbacktracking closed normal form; - [x] retain a proof-relevant tree of every internal and rotated closing cancellation, and prove that an empty normal form contains the exact-index reverse of every represented directed-edge value in the original dependency obstruction (membership, not yet a positional bijection); - [x] propagate all-left reference retention for every forward occurrence through the concatenated dependency walk, and deduce that every original edge index is retained in the empty-normal-form branch; - [x] expose the deterministic reference switching's `IsTree` theorem and transport the empty branch's original nonempty closed exact-occurrence walk into that reference graph; retain the nested-backtracking possibility explicitly rather than treating a closed tree walk as an immediate contradiction; - [x] preserve exact compacted indices, stored edge values, orientations, and cyclic nonbacktracking through arbitrary occurrence masks; expose every valid switching of a correct certificate as a tree; prove a par-pair-sparse nonempty normal form impossible; and extract a concrete surviving left/right par pair whose omitted right occurrence is necessarily backward; - [x] prove cyclically nonbacktracking traversals are fixed points of the proof-relevant normalization; when a nonempty traversal normalizes to empty, extract an exact internal or closing cancellation site in the original representation; and prove that an internal cancellation in the append of two individually nonbacktracking pieces must cross their unique junction; - [x] preserve the full indexed dependency-segment decomposition through the empty branch, localize its exact cancellation site to an adjacent or cyclic segment junction, and prove that the junction is the preceding dependency's exact retained reflexive end and the following waiting par's stored left incidence; - [x] choose the first repeated waiting conclusion, preserve injectivity of all earlier chain positions, and prove that the empty-branch family is a simple dependency cycle with at least two distinct waiting-par nodes; - [x] retain the exact first marked-to-unmarked frontier and its assigned prefix in every dependency, prove that a frontier entering a registered waiting par has a reflexive formula chase, pair every source reverse with the unique cyclic predecessor's last occurrence, and conclude that every segment in the fully cancelling simple cycle ends at its reflexive frontier; - [x] preserve the occurrence-indexed full-segment decomposition through the finite family, remove each exact source/frontier pair to obtain the deterministic residual core, prove its endpoints share one live token, chain it to the cyclic successor, and prove every residual-core edge has both endpoints assigned before the first inactive frontier; - [x] prove each residual core is nonempty by combining exact par-target annotations, structural one-parent ownership, and injectivity of the at-least-two-node dependency cycle; - [x] inherit no-immediate-reverse from each containing dependency segment and record nonemptiness plus internal reduction in the deterministic active residual-core family; - [x] compose that deterministic family into a nonempty closed full-graph walk based at the first residual source premise; - [x] prove all core-only occurrences reference-kept, rule out a nonempty cyclically nonbacktracking normal form in the reference switching tree, and localize the forced empty-normal-form cancellation to a cyclic junction between two nonempty internally reduced cores; - [x] turn that cyclic list junction into an exact in-bounds dependency index, reconcile the cyclic successor's concrete segment/source witness, and expose the strict two-layer occurrence word `inner, outer, outer.reverse, inner.reverse` across the two consecutive dependency segments; exact segment nonbacktracking rules out a degenerate inner/outer pair; - [x] preserve both original full-segment witnesses at the indexed strict nesting, align each `core ++ frontier` with its exact retained reference prefix by compacted index, edge, orientation, and target, and transport the inner reversal to the actual head of the successor reference-prefix walk; - [x] replace every reflexive dependency by the complementary exact backward-right-par/reversed-strict-suffix path, prove that path vertex-simple and nonempty, and prove it avoids the target waiting par's exact retained left occurrence; - [x] compose the simultaneous flips around the simple dependency cycle and prove the flattened walk closed, nonempty, and cyclically nonbacktracking, with every forward occurrence retained by the all-left reference switching; - [x] prove every flipped segment internally cusp-free and use exact target-left avoidance plus reference-switching occurrence uniqueness to exclude cusps at every adjacent and cyclic closing segment junction; - [x] prove that a reference-omitted occurrence in a flipped segment is uniquely its head, exclude the source par's retained left incidence from that same vertex-simple segment, and localize the unavoidable concrete par-pair conflict to two distinct indexed flipped segments; - [x] use first-repeat prefix injectivity to prove that the conflict conclusion is a non-start vertex reached in the distinct holder segment's target list, with exact retained-left and omitted-right edge/mask facts; - [x] split the holder segment at the conflict conclusion into incoming and outgoing vertex-simple paths, prove the incoming side nonempty, assign the retained-left occurrence to its orientation-correct side, and prove the paths meet only at the conclusion; - [x] order the two indexed conflict segments by an exact before/middle/after decomposition and cut the cyclic family at the shared conclusion into two closed full-graph arcs; prove the first arc nonempty, place omitted-right in it, assign retained-left to one of the two, and cover the original flipped occurrences up to cyclic rotation; - [x] retain an exact rotation witness and transport internal cusp-freedom to the rotated concatenation and each closed arc separately; - [x] bind the retained-left orientation to the exact chord boundary: forward retained-left is the incoming path's last edge and forms a par cusp with the omitted-right first-arc head, while backward retained-left is the outgoing path's first edge and the nonempty second arc's head; - [x] classify the backward chord-closing turn: prove the second arc closing-cusp-free, cyclically nonbacktracking, nonempty, and strictly shorter than the original flipped walk; - [x] transport pointwise scheduler provenance and forward reference retention to the shorter second arc, re-extract its backward-right par obstruction, and locate that recursive chord at two distinct classified scheduler segments with the shared conclusion at one segment's start and internally in the other; - [x] package an arbitrary recursively cut closed subarc with internal and closing cusp-freedom, forward reference retention, pointwise indexed scheduler provenance, and its scheduler-located par obstruction; rotate omitted-right to the head and prove that a backward retained-left produces a strictly shorter state with every invariant preserved, while recording the exact rotation and contiguous smaller interval as a proof-relevant cyclic-interval descent step; - [x] close the backward recursion by traversal-length well-foundedness and prove that every initial fully reflexive flipped dependency family reaches a terminal forward retained-left par-cusp interval with a complete interval trace back to the original family, without ordinary loop erasure; - [x] strengthen that terminal object with the exact complementary cyclic interval; prove the complement nonempty, closed, internally cusp-free, and strictly shorter, and prove that every closing cusp on it is the exact last/first reversal rather than a second nontrivial par cusp; - [x] strip exact first/last reverse shells proof-relevantly while retaining the exact positional context and length equation; transport the normalized core's occurrence-indexed scheduler provenance, recurse through every cusp-free nonempty core by strict cyclic-interval descent, and reduce the nesting argument to an empty shell core or a scheduler-located nontrivial closing-par core; - [x] make the terminal obstruction position-aware in both coordinate systems: retain exact before/middle/after decompositions inside the current cyclic interval and inside the indexed scheduler-segment family, bind the terminal cusp head/last/conclusion to that same witness, and remove independently selectable duplicate witnesses from the terminal base; - [x] define coordinate-exact scheduler occurrences carrying segment step, in-segment offset, and edge value; prove the tagged family erases to the original flattened traversal, is duplicate-free, and supports exact segment/offset lookup; project each positioned par obstruction to its exact right-head and left-offset scheduler tags; prove tagged cyclic cuts and descent traces erase to their edge-level counterparts; - [x] refactor the cyclic scheduler state and full backward-chord recursion to carry tags from the initial family: invert every surviving tag to its exact source lookup, recompute the next obstruction on retained coordinates, and reach the terminal forward cusp with a complete tagged state-and-interval descent; - [x] define coordinate-exact reverse-shell normalization, prove that its two endpoint coordinate lists erase to reverse traversals, and turn it into an exact tagged cyclic descent; - [x] bind the terminal generator, arc, complement, derived strict cut, closed complement walk, source-fixed reverse-shell normalization, and nested trace in one indexed tagged witness, so every later argument refers to the same visits even when edge values repeat; remove the terminal path's first generic `CyclicIntervalCut` positional lift; - [ ] exclude the finite terminal bases by exact local geometry and the scheduler-order contradiction: - [x] in an empty core, pair every exact visit with a distinct reverse-valued visit from a different scheduler step; - [x] retain the complement's exact closed-walk/cusp-free witnesses, prove every empty-core edge reference-kept, transport the nonempty complement into the reference-switching tree, and exclude every flipped-segment head from that complement; - [x] select a concrete reverse pair, orient it by strict scheduler-step order, and retain the exact before/middle/after segment decomposition; - [x] invert every positive offset to the concrete omitted-head/retained- suffix decomposition and retain the suffix walk to its segment target; - [x] expose the coordinate-exact head-skipping reverse chord: the zero-offset heads of both ordered endpoint segments occur in the initial tagged scheduler family and are absent from the empty-core complement; - [x] classify both chord endpoints by their exact scheduler source, complete reference-kept suffix walk to the next scheduler conclusion, and the exact retained-left occurrence of that target waiting par avoided by the whole segment; connect this terminal outcome to the global fully reflexive dependency-cycle extraction; - [x] transport both selected suffixes to the deterministic reference switching with exact compacted indices and orientations, and prove that their selected occurrences remain an exact reverse pair; - [x] split the empty reverse shell into nonempty opening and closing coordinate halves, transport each half to a reference walk through one midpoint, and prove the complete retained closing traversal is exactly the reverse of the retained opening traversal; - [x] exclude the empty shell directly: the last opening occurrence is followed at the midpoint by its exact reverse, forcing a cusp contrary to the inherited cusp-free complement; - [x] retain the surviving closing-par core's exact first and last scheduler tags, invert them to their source segment/offset lookups, and prove the forward last incidence reference-kept; - [x] bind those exact first/last tags to the same positioned par link and the same reverse-shell normalization core, retain the closed core as `first :: middle ++ [last]`, prove the endpoint steps distinct and `chainAt (last.step + 1)` different from the shared conclusion, and exclude both same-segment and segment-boundary coordinate adjacency of the artificial closing seam; - [x] retain a state-and-interval ancestry through every backward search, terminal complement, reverse-shell normalization, and recursive nesting step, with a projection to the older `CyclicIntervalDescent`; - [x] replace every bare backward-search cut with an explicit semantic step sharing the exact positioned right/left tags, both cyclic decompositions, backward orientation, retained suffix, and strict cut; - [x] bind each nesting complement, its derived strict cut, closed walk, reverse-shell normalization, and recursive trace to the exact indexed terminal forward-cusp split that generated it; - [x] assemble the exact terminal base, data-indexed global ancestry, closing outcome, and normalized endpoint split into one package with common base/complement-base/complement/normalized-core indices; - [x] lift the hidden `SchedulerTaggedTerminalComplementStepAt` frame into a seam-specific indexed object, or destruct and thread the same existential wrapper exactly once, without reselecting its arc, rotations, link split, occurrences, scheduler coordinates, or segments; - [x] replay the artificial closing seam outward through the exact terminal, backward, reverse-shell, nesting, and global-ancestry frames as a boundary cursor, from a boundary-zero empty-gap seed to a nonempty accumulated candidate gap in the initial tagged family; - [x] prove pointwise gap containment and preservation of every incoming gap occurrence through the replay, and transport the same terminal omitted arc's zero-offset backward head into the initial tagged family with its exact right-par incidence, omitted reference entry, classified segment, waiting-dependency semantics, and source conclusion; - [x] enrich that same stored replay with an occurrence-position endpoint zipper whose `gap` is the complete complementary arc between the fixed first and last tagged endpoint occurrences, without identifying it with the weaker candidate cursor gap; - [x] derive nonemptiness of every scheduler segment from the indexed flipped traversals and prove the initial-family exact gap nonempty: otherwise empty exact gap would imply the scheduler-coordinate adjacency already excluded by the closing endpoint witness; - [x] retain the first exact empty-to-nonempty gap-opening frame with its original replay index, nonempty `rightContext ++ leftContext` insertion, and explicit gap-splice branch; split the replay at one shared Type-valued base zipper and classify the opening as terminal or ancestry, with the ancestry branch carrying a proof that every terminal gap stayed empty; - [x] construct the canonical endpoint replay of the fixed terminal step and prove that it always first-opens there: the reverse-shell frame opens first when `closing ++ opening` is nonempty, and otherwise the nonempty omitted arc opens in the second frame; - [x] retain in that construction the exact reverse-shell equation, the omitted-right zero-offset backward anchor, the forward retained-left last occurrence of the outer terminal arc, and the canonical base gap `closing ++ taggedArc ++ opening`; - [x] retain the erased outer `taggedArc` as a closed `EdgeWalk` at the complement base and a `CuspFreeTraversal`, together with its exact cyclic closing cusp from the outer last occurrence to the anchor and the non-reverse endpoint fact; - [x] prove endpoint-gap sublist and membership monotonicity and transport the complete outer `taggedArc` in its original linear order through global ancestry to the initial tagged-family gap, retaining its omitted-right head and outer retained-left last occurrence; - [x] prove the generic ordered-decomposition lemma for a retained sublist with specified `head?` and `getLast?`, and apply it to exhibit the initial exact gap as `g0 ++ anchor :: g1 ++ outerLast :: g2` and the initial family as `CyclicFourPointDisplayAt firstTag lastTag anchor outerLast`; - [x] specialize to the complete initial `tagSchedulerFamily flippedSegments`: use its exact-coordinate `Nodup` to prove `[firstTag, lastTag, anchor, outerLast].Nodup`, while preserving the boundary that erased edge values and vertices may still repeat; - [x] retain the same outer positioned terminal choice in the endpoint replay, lift both the inner normalized closing witness and that outer witness through exact ancestry membership into the complete initial family, and return both with the four-point display and four-tag `Nodup` fact from one specialized theorem; - [x] audit and reject a generic contiguous token-age/proper-nesting/LIFO invariant for the actual flat scheduler. The stable small accepted regression first merges ages 0 and 2, and ordinary laminarity permits the separated order `firstTag → lastTag → anchor → outerLast` as sibling intervals. `tagSchedulerFamily.step` is a dependency-segment index, not firing age; - [x] reject exact concrete-state confluence on a derivation-generated correct certificate and reject structural-only confluence on a structurally well-formed certificate; - [x] record an uncommitted exploratory local audit of the candidate marked-domain/occurrence-thread quotient on 80 derivation-generated correct certificates: 2,734 reachable quotient states, 7,148 enabled critical pairs, 0 disabled pairs, and 0 quotient non-diamonds. No committed reproducer exists, so this is neither a release/CI gate nor a theorem; - [ ] prove preservation of `ResidualParsingWitness` under an arbitrary successful firing, or a local-confluence theorem at that quotient, and use it to exclude the tagged nontrivial closing-par base and discharge the remaining path-exposed waiting-par obstruction; - [ ] pure worklist completeness and equality with `check`; - [ ] fallback removal from the exact worklist decision; - [x] bounded/tagged `NEXTAXIOM` checkpoint: - [x] build a reusable source-incidence index and prove exact submitted-link origin for every stored entry; - [x] prove structural singleton lookup for every in-bounds occurrence. `SourceIndex.Sound` alone is only provenance: the index deliberately records both endpoints of a malformed self-axiom in one bucket, whose multiplicity structural well-formedness excludes; - [x] retain exact submitted axiom index/endpoints, final tags, and trace on success, with tag-array size preservation, old-true-tag monotonicity, trace `Nodup`, input-false/output-true trace and endpoint tagging, input-unmarked endpoint proofs, and `trace.length ≤ fuel`; - [x] define the touched carrier as trace plus endpoints and prove successive touched carriers disjoint when the second successful call uses exactly `first.tags`; reset or replaced tags are outside the theorem; - [x] prove dynamic start refines Figure 5 under `OrderedParents` and test zero fuel, out-of-bounds, tagged and marked starts, missing and ambiguous sources, threaded-result-tags repeat rejection, and dynamic allocation; - [x] prove every successful search has an exact oriented submitted source-left route to the endpoint actually reached; lock the stored-right orientation by regression; - [x] prove local totality under `SearchClearThrough` with fuel greater than the start complexity, plus the full-initial-carrier `complexity + 1` corollary and a depth-two exact rank/fuel boundary regression; - [ ] later-state `NEXTAXIOM` selection and preservation of its freshness premise; carrier-size-wrapper totality is not yet established; - [ ] replace global low-rank freshness with a route-local invariant that survives previously tagged axiom endpoints; - [ ] prove a formula-complexity/carrier bound before exposing a `nextAxiom?` totality corollary; - [ ] weaken the local theorem from full `Abstractable` to its actual mark-slot-readiness dependency when API reuse warrants it; - [ ] faithful `σ`/`R`/`W` state and token-age sequencing: - [x] prove the first independent `SigmaAgePartition`/waiting-state layer: strictly increasing `σ` boundaries partition raw discovery ages; out-of-bounds/undefined/initialized-empty remain distinct, and strict empty `init` establishes `OperationalWaitingDomain`; - [x] retain the printed fresh-cell `newEnqueue?` only as a source-audit helper, and prove that production `operationalNewEnqueue?` instead initializes the old active boundary, leaves the fresh top undefined, and preserves `WellShaped` plus `OperationalWaitingDomain`; - [x] implement initial and typed later `RealizesSigma` reservations with exact submitted/search orientations, unmarked endpoints, threaded tags, and preservation of `ReservationInvariant`; - [x] implement the invariant-bound local Figure-7 pop/mark/mate-search/new pipeline over the operational waiting interpretation; - [x] define the generic canonical consumer/conclusion views and executable local `concl`/`nop`/`wait` transitions, including exact success witnesses and reservation-invariant preservation; - [x] define independent Boolean-free direct common-prefix, `concl`, `nop`, and `wait` relations, and prove executable soundness, completeness under `StructurallyWellFormed` plus `ReservationInvariant`, and output uniqueness; - [x] implement the bounded production-core `queuePar?`/`queueTensor?` component mutations and delayed-stack `prependReadyTop?`/`mergeTopReadyWaiting?`, with typed success witnesses, raw-unmarked conclusions, explicit local invariant preservation, and the deterministic list refinement `conclusion :: (payload ++ previousReady ++ activeReady)`; - [x] define the first non-circular state-based `SchedulerInvariant`: explicit structural well-formedness, exact live-component/`sigma` domain, extensional ready/frontier correspondence, global live-frontier and queued-occurrence uniqueness, queued raw-unmarkedness, observable causal produced-conclusion/premise marking, delayed pending-premise coverage, exact delayed-par waiting spans (including raw-unmarked conclusions), and production-tree connective-counter accounting; prove empty and successful initialization for structurally well-formed certificates, including search/submitted orientation reversal; - [x] prove the synchronized common `PreparedStep` preserves every current state-only `SchedulerInvariant` field, using an exact active-top `sigmaBoundary?` lemma, extensional ready/frontier removal, global queue `Nodup`, waiting-span transport, and the selected live-component witness for newly marked pending-premise coverage; derive exact/executable `concl`/`nop` preservation through `prepared.after`; - [x] add proof-only occurrence-faithful internal component/link provenance: exact submitted link indices, exact first-occurrence focuses, complete owned vertices, local `Nodup`, cross-live-slot disjointness, exact representative-slot ownership for every marked owned vertex, same-frontier coverage for every unmarked owned vertex, and reverse ownership of every concrete raw mark; prove formula-consistency soundness, exact axiom reservation, local par/tensor queue extension, and repeated-label alias rejection; - [ ] integrate `ComponentForestProvenance` into `SchedulerInvariant` and prove whole-forest initialization/preservation, including fresh submitted link/conclusion and branch-disjointness obligations; - [ ] connect those primitives into complete `forward`/`unify`: prove the tensor representatives are the scheduler boundaries `j/i`, orient `parent[i] := j`, and construct/activate every par component drained from `W(j)` (or justify producer-aware deferred construction), including `1 + |W(j)|` connective-counter accounting; - [ ] preserve the new semantic scheduler fields, including global queue uniqueness, through local `wait` and complete `forward`/`unify`, and integrate `concl`/`nop`/`wait` into the full history/dispatcher; - [x] characterize exact empty/init/operational-new histories and prove tag iff recorded touch, whole-history submitted-slot non-reuse, and reservation-count alignment; this does not characterize unimplemented rules, and the preservation record alone still admits reset tags; - [ ] formulate and preserve guards over raw assigned ages, not representatives; - [ ] full sequential scheduler correctness and completeness; - [ ] full implemented-operation complexity theorem; - [ ] adversarial, differential, downstream, API, and trust audits. `CyclicIntervalDescent` alone is deliberately not used as a convexity principle. A strict cyclic interval of a strict cyclic interval can wrap around the first cut's artificial boundary; for example, an outer interval `[b, c, d]` can be rotated and cut to `[d, b]`, which is not a cyclically contiguous subinterval of the original linear representation when outside elements separate `d` from `b`. Therefore a proof that a head-free terminal state lies in one scheduler step would be false for the generic descent type. The remaining proof must retain and use the specialized omitted-right chord, terminal-complement, and reverse-shell endpoint witnesses that generated each cut. Backward-search cuts satisfy this condition: their types bind the larger state's positioned obstruction to the exact scheduler tags, rotation, retained suffix, and strict interval. The terminal step now satisfies it as well: one indexed witness fixes its generator, arc, complement, derived cut, closed walk, source-fixed reverse-shell normalization, and nesting trace. The terminal path therefore no longer uses the generic `CyclicIntervalCut` lift to select a tagged complement. A data-indexed global result now packages the terminal base, exact ancestry, and closing outcome under the same `(base, complementBase, taggedComplement, taggedNormalized)` tuple; the endpoint split is indexed by that same `taggedNormalized`. The structural replay consumes each stored `SchedulerTaggedTerminalComplementStep` wrapper exactly once, threads the same hidden `SchedulerTaggedTerminalComplementStepAt` witness, and folds the exact reverse-shell, backward-search, nesting, and global ancestry frames into a proof-relevant cursor and occurrence-position endpoint zipper. The cursor still carries only a candidate gap. The zipper instead records an exact cut of the current cyclic list and defines its gap as the complete complementary arc between the fixed tagged endpoints. These two gaps are not equated. Every indexed flipped traversal is nonempty. With that hypothesis, an empty endpoint-zipper gap in the initial tagged scheduler family implies exactly the same-segment or segment-boundary coordinate adjacency already excluded by the closing endpoint witness. The complete initial gap is therefore nonempty. The earlier generic replay theorem still records the first local empty-to-nonempty transition and its terminal/ancestry phase split, but the stronger canonical construction now fixes the terminal phase. Starting at the normalized core, its reverse-shell frame inserts `closing ++ opening`; if that list is nonempty it is the first opening. Otherwise the generator's nonempty `taggedArc` opens the gap in the second frame. The construction keeps `closing.map erase = reverseTraversal (opening.map erase)`, the omitted-right anchor at `taggedArc.head?`, the forward retained-left occurrence at `taggedArc.getLast?`, and the exact base gap `closing ++ taggedArc ++ opening`. Its erased `taggedArc` is a closed `EdgeWalk` at the complement base and satisfies `CuspFreeTraversal` internally, while the exact cyclic closing pair from the outer last occurrence to the anchor is a cusp and the two directed occurrences are not reverses. Thus the cusp is the wraparound closure, not an internal turn rejected by the linear cusp-free predicate. The shell-nonempty/empty distinction is made inside the construction of the first-opening proof. The returned `CyclicEndpointFirstGapOpeningInReplayAt` proposition does not yet provide a separately consumable sum identifying which frame opened or tying that frame to the omitted-right anchor origin. The anchor-origin theorem and the first-opening theorem are retained alongside one another, not connected by such a payload. Every endpoint splice preserves its incoming complete gap as a sublist. Consequently the complete outer `taggedArc` survives the ancestry replay as an ordered sublist of the initial scheduler-family gap, with its same omitted-right head and retained-left last occurrence. A generic theorem now combines exact `head?`/`getLast?` lookups with that `List.Sublist` evidence to decompose the initial gap exactly as `g0 ++ anchor :: g1 ++ outerLast :: g2`. Together with the endpoint zipper rotation, this yields `CyclicFourPointDisplayAt firstTag lastTag anchor outerLast`. `CyclicFourPointDisplayAt` is deliberately weak as a generic relation: all four intervening lists may be empty and the four displayed values may repeat unless separate hypotheses rule that out. Thus the result preserves the named occurrence order but proves neither contiguity, a fixed linear scheduler rank, crossing, nor a strict cyclic-betweenness relation. No model-specific scheduler-order/proper-nesting theorem yet turns the terminal geometry into the closing-par contradiction or correct-state progress. For the actual complete initial family, the separate hypothesis is now available: `tagSchedulerFamily_nodup` proves uniqueness of exact `SchedulerOccurrence` coordinates even when their erased `DirectedEdge` values repeat. Applying it to the four-point display gives `[firstTag, lastTag, anchor, outerLast].Nodup`. This is not an injectivity theorem for erasure and does not make the four erased edges, edge endpoints, or vertices distinct. The terminal endpoint replay also retains the exact outer positioned par choice which generated `anchor` and `outerLast`, rather than reconstructing a new choice from erased values. Exact membership through the ancestry replay lifts that same outer witness, and separately lifts the normalized inner closing witness, to the complete initial `tagSchedulerFamily`. The specialized closing theorem returns both positioned witnesses together with the four-point display and its four-tag `Nodup` fact. Those results expose the cyclic occurrence order `firstTag → lastTag → anchor → outerLast`. Pairing the inner `(firstTag, lastTag)` and outer `(anchor, outerLast)` endpoints makes the two pairs separated, not alternating; therefore this is not a crossing witness. `Nodup` does not make any of the four intervening intervals nonempty. Ordinary laminarity permits the separated pairs as siblings, and the stable three-axiom regression refutes contiguous token-age/LIFO behavior for the flat eager scheduler. Consequently no generic scheduler-order/proper-nesting contradiction remains as a valid flat-scheduler route. Exact-state and structural-only confluence are also refuted. A residual-witness theorem or confluence modulo the marked-domain/occurrence-thread quotient is still open for flat completeness; the uncommitted exploratory local 80-certificate audit is neither a reproducible release gate nor that theorem. The bounded/tagged `NEXTAXIOM` and dynamic-start checkpoint is kernel checked, including per-call trace/tag invariants, exact oriented routes, local rank-scoped totality, and touched-set disjointness for successive calls that strictly thread `first.tags`; reset tags are outside that theorem. The operational inactive-boundary `W` domain, initial/later reservation bridge, local pop/mark/new pipeline, and exact init/new execution history are now kernel checked. Exact local `concl`/`nop`/`wait` are also kernel checked. Later-state selection totality, ready/waiting payload ownership, `forward`/`unify`, full-history integration, and full-rule reachability remain open for the separate linearity layer. Closing-par exclusion, progress, and pure-worklist completeness remain open. Planarity is not assumed. The endpoint replay realizes the required zipper/gap invariant rather than an adjacency claim. If a rotated parent view has the exact decomposition ```text V = rotationSuffix ++ rotationPrefix = leftContext ++ inner ++ rightContext, ``` then the closing seam of `inner` expands in `V` through the exact outside gap ```text last(inner) :: rightContext ++ leftContext ++ [head(inner)]. ``` It is a parent-view closing seam plus a left generator leg when only `leftContext` is nonempty, a right leg plus that seam when only `rightContext` is nonempty, and two legs around one parent-seam obligation when both are nonempty. Empty context on both sides is the identity case and cannot represent a strict cut. Re-basing from the rotated view also matters: when both rotation pieces are nonempty, the view closing seam is the parent's ordinary split adjacency; only an empty rotation piece carries the parent's closing-seam obligation outward. The terminal complement is the one-sided case, whereas every proper reverse shell is two-sided because its closing arm is the reverse traversal of its nonempty opening arm. These decompositions are stored in the exact replay and its first-opening witness. The canonical replay now proves terminal-phase opening by the internal shell case split, retains the exact reverse equation and closed cusp geometry, and transports the whole outer terminal arc in original linear order through ancestry. Its returned first-opening proposition does not expose the internal frame branch together with the anchor origin. The resulting exact `g0 ++ anchor :: g1 ++ outerLast :: g2` decomposition and generic `CyclicFourPointDisplayAt firstTag lastTag anchor outerLast` still do not establish contiguity, fixed linear rank, crossing, strict cyclic betweenness, a scheduler-order/proper-nesting contradiction, or exclusion of the closing-par base. In the complete initial family the four exact tags are now proved `Nodup`, and both the inner and outer positioned witnesses are retained there; the displayed order is nevertheless separated rather than crossing, and no intervening interval is known nonempty. Ordinary laminarity therefore does not exclude it, while the executable small regression rules out importing a flat token-age/LIFO invariant. The remaining flat-completeness route is residual-witness preservation or a theorem at the candidate quotient; the Figure-7 stack route extends the existing bounded/tagged `NEXTAXIOM` checkpoint with later-state selection, `σ`/`R`/`W`, and token-age sequencing. Per-call trace/tag invariants, oriented route correctness, initial/local rank-scoped totality, and strictly threaded touched-set disjointness are already proved.