Realization Determinism

M-E · todo/lean/070 · leg-4 program, keystone · kernel-checked, promoted 2026-07-17 · firewalled-Opus cold-review confirmed, standard axioms

Its companion essay, the Grand Tour (M-C), proves that a circle arrangement leaves a trail: delete one circle $c$, and the way it used to thread through everything that survives is a closed gate walk over the smaller arrangement. That is the extraction half of a completeness route — L4-conn, this project’s one road to counting the census with no external table to check against. But M-C stops at a trail. It never turns around and asks the harder question: given the trail, can you rebuild the arrangement it came from — and is the thing you rebuild the same arrangement? M-E answers yes. The walk data determines the child. Reassemble the extracted trail over the recovered parent and you get back the original, on the nose, up to relabelling.

Keep M-C’s vocabulary. $M$ is the arrangement with $c$ still in it — the child; $M'$ is $M$ with $c$ deleted, the parent (M.deleteCircle c h). Both are DartMaps: each arc carries two darts, one per end, and a single rotation permutation $\mathrm{rot}$ cycles the four darts around every degree-4 crossing ($\mathrm{rot}^4 = \mathrm{id}$). M-E is the reconstruction, and it is exactly one half of a counting argument: the faithfulness half. It shows the map from arrangements to walk data loses nothing. It does not show that map is onto — that every legal walk is hit by some arrangement, or that a search enumerates the walks. Those are separate, later obligations, and the essay names them at the end rather than smuggling them in.

The one datum M-C dropped

A gate walk, as M-C packages it, is spare on purpose: a parent map, a length $L$, and a sided sequence $w$ of parent half-edges — which arc the deleted circle crosses at step $k$, and on which side it approaches. What that sequence deliberately omits is an interleaving. When $c$ crosses a single parent arc more than once, the sequence records that the arc is used twice, but not the order in which the two new crossing-vertices sit along the arc. And that order is not cosmetic: the two orders are two genuinely different arrangements on the sphere. M-C called the missing field fwd and left a hole where it belongs.

This is not a corner case; it is the generic case. A parent arc is rarely a pristine circle-arc. Deletion fuses: erase $c$ and every arc it used to interrupt splices with its neighbours into one long parent arc — a run. A run can be crossed by the reinstated $c$ many times, and each crossing-count $\mathrm{cnt}(a)$ on parent arc $a$ means the arc must be cut back into $\mathrm{cnt}(a)+1$ pieces at reconstruction, with the $\mathrm{cnt}(a)$ interior cut-points placed in a definite order. The sided walk knows how many; it does not know where.

The position vector, read off the child

M-E supplies the missing datum as a position vector $\mathrm{pos}$ (in the Lean, posW): crossing $k$ sits at position $\mathrm{pos}(k)$ along its parent arc, counted one-based from the arc’s far (“false”) end, so that positions run $1$ through $\mathrm{cnt}(a)$ strictly between the two surviving endpoints at $0$ and $\mathrm{cnt}(a)+1$. Concretely $\mathrm{pos}(k)$ is the chain-index, along the fused run, of the true-ward strand at the tour’s $k$-th vertex — of the two strands crossing there, the one that resolves toward the arc’s true end — plus one.

The four words that carry the whole meaning of this round are read off the child. $\mathrm{pos}$ is not guessed, not enumerated, not searched for. M-E has a real child $M$ in hand and simply reads where each crossing already sits — a Nat.find down the actual fused run. That is what makes the reconstruction a theorem about the child rather than a hopeful construction: you are handed the arrangement, you extract its interleaving, and the claim is that the extracted interleaving rebuilds precisely what you were handed. The dual claim — that a walk-enumerator can produce a legal $\mathrm{pos}$ without a child to read it from — is a different problem (the Python seam G-W2), and M-E does not touch it.

Reading it off is only half of “coherent.” The vector has to be the sort of thing the assembly can consume: positions in range, and no two crossings of one arc colliding at the same spot. That is the structure AsmOK,

$$1 \le \mathrm{pos}(k) \le \mathrm{cnt}\big((w\,k)_1\big), \qquad (w\,k)_1 = (w\,k')_1 \;\wedge\; \mathrm{pos}(k) = \mathrm{pos}(k') \;\Rightarrow\; k = k'$$

and M-E proves the extracted $\mathrm{pos}$ satisfies it (asmOK_extracted). The injectivity rides on the tour meeting each vertex once; the range bound rides on the exact accounting $\mathrm{cnt}(a) = \mathrm{runLen}(a)$ — the number of tour steps crossing arc $a$ equals the run’s length, the count of deleted vertices strung along it (cntW_tourGate_eq_runLen). That equality is a small bijection in its own right, between tour steps and run vertices, and it is what lets the positions fill their slots without gap or overlap.

The assembly

Now forget the child for a moment. Given any parent map $M'$, a length $L$, a sided sequence $w$, and a coherent position vector $\mathrm{pos}$, there is a purely mechanical construction — asmDartMap — that builds a new DartMap on a fresh arc type. This is a real object, defined before any child is named. Its arcs are

$$\#\{\text{sub-arcs of }a\} = \mathrm{cnt}(a)+1, \qquad \#\{\text{new-circle arcs}\} = L$$

each parent arc $a$ chopped into $\mathrm{cnt}(a)+1$ sub-arcs (sub-arc $\langle a,\, j\rangle$ spanning positions $j$ to $j$+1), plus $L$ brand-new arcs for the reinstated circle, labelled with a fresh circle $c$ that the parent did not have.

The rotation is where the geometry lives. At each surviving vertex — positions $0$ and $\mathrm{cnt}(a)$, the two ends that were already there — the parent’s own rotation is carried across unchanged. At each reinstated crossing vertex $k$ the local rotation is the four-cycle

$$\mathrm{cin}_k \;\longrightarrow\; \mathrm{strB}_k \;\longrightarrow\; \mathrm{cout}_k \;\longrightarrow\; \mathrm{strA}_k \;\longrightarrow\; \mathrm{cin}_k$$

— the incoming new-circle dart, then the departure-side strand, then the outgoing new-circle dart, then the approach-side strand, and around. Which parent-arc side each strand resolves to is dictated by the one side bit the sided sequence carries at step $k$: it is the σ-correct case of the dictionary M-B built for reading a crossing’s rotation. This assembled rotation is not assumed to be a permutation; it is proved one. A per-dart case bash shows an explicit inverse rotation undoes it at every dart (rotAsm_leftInverse — surviving vertices via the parent’s inverse, crossing vertices via the position-lookup identities), and finiteness upgrades a left inverse to a two-sided one. So rotAsmPerm is a genuine Equiv.Perm, and asmDartMap a genuine DartMap — a standalone gadget that takes walk data to a sphere-arrangement candidate, whether or not the data came from anywhere real.

The dictionary, and the one equation that matters

The theorem is that when the walk data is extracted from a real child, this mechanical assembly is isomorphic to that child:

$$\mathrm{asm}\big(M',\; L,\; \mathrm{tourGate},\; \mathrm{posW}\big) \;\cong\; M$$

as DartMaps — a DartIso, meaning a bijection of darts and a bijection of circle labels that commute with twin, rotation, and the circle partition. The dart bijection $\mathrm{cont}$ — asmToChild — is the obvious dictionary once you believe the picture. A sub-arc $\langle a,\, j\rangle$ of the assembly is the $j$+1-st arc of parent arc $a$’s fused run, so it maps to that run’s $j$-th chain dart; the reinstated circle’s $k$-th arc maps to the tour’s $k$-th dart $d_k$. That it is a bijection is a two-sided bookkeeping argument: on the reinstated circle it is the tour’s own injectivity and coverage (each vertex met once, every vertex met), and on the parent side it is a run partition — the fact, load-bearing and separately proved, that every dart off $c$ lies on exactly one run at exactly one index, because the splice map is injective and so two chains can never merge.

The heart of the proof is not the bijection but the intertwining: that the dictionary carries the assembled rotation to the child’s,

$$\Phi\big(\mathrm{rot}_{\mathrm{asm}}\, x\big) \;=\; \mathrm{rot}_M\big(\Phi\, x\big)$$

proved dart by dart (asmToChild_rot). Surviving vertices ride the deletion’s decode dictionary from the previous rounds. Reinstated vertices ride two facts in tandem: that the position reads back (the chain dart at $\mathrm{pos}(k)$−1 is exactly the true-ward strand), and the side-bit case analysis relating $\mathrm{rot}$ and $\mathrm{rot}^3$ of that strand to the tour darts. This is the round’s long pole — a dozen coordinated rotation-power identities at a degree-4 vertex — and it is the exact point where “the assembly looks right” becomes “the assembly is the child.”

The statement of record

This is the Lean, unmodified, from A250001/RealizationDeterminism.lean. Its hypotheses are the verbatim standing packages of the earlier rounds — a legal deletion (DeleteOK) and a well-formed tour (TourOK) — and its conclusion is the census’s own notion of sameness, a nonempty DartIso:

theorem realization_determinism (h : M.DeleteOK c) {d₀ : Arc × Bool} {L : ℕ}
    (ht : M.TourOK c d₀ L) :
    Nonempty (DartIso
      (asmDartMap (M.deleteCircle c h) L (M.tourGate c h ht.onC) (M.posW c h ht.onC)
        (M.asmOK_extracted c h ht.onC L ht)) M) :=
  ⟨ { dartEquiv   := M.asmToChildEquiv c h ht.onC L ht
      circleEquiv := circleOptionEquiv c
      twin_comm   := M.asmToChild_dartTwin c h ht.onC L
      rot_comm    := M.asmToChild_rot c h ht.onC L ht
      circ_comm   := M.asmToChild_circ c h ht.onC L } ⟩

Decoded: extract $(L,\, w,\, \mathrm{pos})$ — M-C’s length and sided gate sequence, plus this file’s position vector posW — from a real child, assemble it over the recovered parent, and the result is DartIso to the child. The five fields are the five commutations; the load-bearing one is rot_comm. A concrete threeChain control proves both hypotheses by raw kernel computation, so the theorem is not vacuous over an empty class.

One subtlety the phrasing hides is worth saying plainly. The parent is part of the walk data — the assembly runs over M.deleteCircle c h, the parent recovered from the very child in question. So the honest content is not “a gate sequence determines a child” but a parent together with a sided gate sequence and a position vector determines the child, up to isomorphism. That is exactly the shape a completeness induction needs: the DartIso conclusion is the census’s own equivalence, so every predicate the later induction (M-H) cares about transports across it for free.

A second subtlety: the main theorem spends no sphericity and no gate property. None. The geometry it needs is entirely encapsulated in TourOK’s combinatorial fields — the tour closes, meets each vertex once, is two-sided, and covers $c$ — and the reconstruction is indifferent to why those hold. That is a genuine strengthening: it means M-E composes with whatever discharges TourOK, and round P-1 (“Sphericity’s Dividends”) discharges those fields from sphericity plus faithfulness, so on a census map TourOK costs nothing beyond the decoder’s own guards. But it also fixes M-E’s exact strength: it is only as strong as the DeleteOK+TourOK base. It is not an independent geometric guarantee; it inherits the trust of P-1, sphericity, and the decoder axioms it stands on.

The mirror, stated honestly

There is a companion result for chirality, and its shape is easy to get wrong, so the module states it carefully. Negate every side bit of the extracted sequence — the global σ-flip flipW — and assemble over the mirrored parent. The result is DartIso to the mirror child:

$$\mathrm{asm}\big(\overline{M'},\; L,\; \mathrm{flipW}(\mathrm{tourGate}),\; \mathrm{posW}\big) \;\cong\; \overline{M}$$

The reason it must be the mirrored parent, and not the original, is the honest part. Flipping the side bits reverses the four-cycle at every reinstated crossing — the two strands trade places — which is what mirroring does at a crossing. But it does nothing at the surviving vertices, and mirroring an arrangement must invert the rotation there too. So the flip alone, over the unmirrored parent, is provably not the mirror child: the survivors would keep the parent’s original chirality. Mirroring the child mirrors its parent as well, and the flip is exactly the residue left over at the reinstated crossings once the parent has been mirrored. If a later seam ever needs a same-parent form of this, that residue is a parent-level statement, and it is not closable inside M-E.

What’s proved, and what isn’t

Proved, kernel-checked, standard axioms only (propext, Classical.choice, Quot.sound; no sorry, no new axioms, no fenced hypotheses; independently rebuilt and re-run under firewalled cold review): from a legal deletion and a well-formed tour of a real child, the walk data extracted from that child — length, sided gate sequence, and the position vector read off its interleaving — reassembles over the recovered parent into a map DartIso to the child, and the σ-flipped data reassembles over the mirrored parent into the mirror child. The trust label is PROVED-about-model: reconstruction is faithful, and no more.

Open, and named rather than glossed:

• The reconstruction half only. M-E shows walk data, once extracted, loses nothing. It does not show that every child arises from a walk — nothing here says a legal walk over a parent is realized by any arrangement, still less that a search finds them all. That converse is the business of M-D’s rooting quotient, the DFS seam G-W2, and the M-H induction, and none of it is attempted here.
• $\mathrm{pos}$ is read off the child. The position vector is extracted from an arrangement already in hand. That an enumerator can generate a coherent $\mathrm{pos}$ with no child to read — the interleaving choices a walk must offer — is precisely the deferred G-W2, and it is where the completeness of the count, not just its faithfulness, will be earned.
• The parent is part of the data. The content is “$(L,\, w,\, \mathrm{pos})$ over the recovered parent determines the child,” not “a bare gate sequence does.” This is the right shape for the induction — the parent is a smaller census object — but it is not a claim about gate sequences in isolation.
• As strong as its base, no stronger. The theorem consumes no sphericity directly, which is a real strengthening — but the geometry it leans on sits in TourOK’s fields, discharged from sphericity by P-1. M-E is only as trustworthy as that base of DeleteOK, TourOK, P-1, and the decoder axioms; it is not an independent geometric certificate.
• The mirror carries the mirrored parent. A same-parent σ-flip is provably false. The chirality result is honest about needing the mirrored parent, and leaves the same-parent residue as a parent-level open statement.

None of this is a shortfall in M-E. It is the exact shape of the keystone in a multi-round build: M-C proved the trail is a walk; M-E proves the walk rebuilds its arrangement, faithfully and up to the sphere’s own notion of sameness — and it is what unblocks the assembling induction, M-H, that the earlier rounds were waiting on. The forward map loses nothing. Showing it hits everything is the road still ahead.