A ledger balances the moment you write — the true count of disconnected sphere-types set equal to the count of distinct keys the census emits. It is trustworthy only once both columns behind that equality, nothing counted twice and nothing missed, have been checked independently. D-H is the round that finally writes this equality down as one theorem, kernel-checked. What the theorem discloses, in its own hypothesis list rather than in a footnote, is that only one of its two columns is actually checked; the other is entered on credit.
Recall the vocabulary the last two rounds built. Most of this project’s arrangements are one connected tangle of crossing circles. A composite is what is left over: several such tangles — clusters, each connected, some possibly a single circle with no crossings at all (a bare cluster) — sitting together on one sphere, some nested inside a face of another. The nesting forest is the containment structure: which cluster sits inside which face of which other cluster, recorded as a parent pointer per cluster, with the clusters nested inside nothing called roots. A composite sphere key is the canonical fingerprint of the whole scene, built by walking that forest and serializing it recursively — the Matryoshka’s subject. is nesting-respecting composite isomorphism, and the diagonal mirror flips the entire scene — every cluster’s orientation and the nesting itself — all at once, never one cluster at a time: the Boomerang’s subject, and D-F’s before it.
Write for the true, finite set of disconnected sphere-types at whatever circle count is in play, and K for the finite set of distinct keys the composition enumerator actually emits after deduping. The campaign’s obligation Kd asks two independent things of that dedupe: no-overcount — two keys that survive deduping really are two different types, so K never inflates ’s true count by secretly counting one type twice under two different keys — and no-undercount — every true type in actually has a representative among the emitted keys, so K never falls short by missing one. D-H is the round that puts both halves into a single theorem, and is honest about which half it actually proves.
parent(1) = 0, parent(2) = 0. All eight pairwise circle relations (two lens crossings, plus the containment-and-exclusion margins placing C, D, and E in their stated faces) were checked numerically before this was drawn — the smallest margin is 7.9 units against a radius of 55.Three clusters, one root, two children in two different faces of that root — already enough to show what a nesting forest actually is: not a flat catalogue of five circles, but a containment relation with real structure, the kind has to respect and the kind a mirror has to carry along wholesale, never cluster-by-cluster. D-G, the Boomerang, proved that a sphere key can always be decoded back to a genuine -witness at a shape’s default rooting, given an honesty qualifier it had to discover the hard way. D-H’s job is to assemble that fact, and everything built before it, into the one theorem that would let a Finset of keys stand in for itself.
Strip the Lean down to English. composite_census_complete takes a Finset K of keys and a decoder dec that turns each key back into a PackedComposite — a composite bundled with the extra rooting and gauge data (fm, rf, ce, ceM) its own sphere key needs in order to be computed at all. Given six named facts about that setup, the conclusion is a genuine bijection: , and no two distinct keys in K decode to -or-mirror composites.
Read left to right. hcanon is canonicity — every emitted key, decoded and re-keyed at its own default gauge, gives back the identical bytes (Gd3’s per-key fixed point, checked over all 16,597 disconnected census keys). hkeyInj is no-overcount, stated directly as a hypothesis rather than proved (the section below is about exactly this). hdr supplies each decoded composite’s DecodeReady package — the well-formedness, laminarity, and forest-faithfulness the Boomerang’s separation core demands (Gd1/Gd2). hattA is the attainment qualifier the Boomerang discovered was necessary — each decoded composite’s sphere key really is attained at its own default rooting, not merely equal to it by coincidence (Gd3 again). hmem is soundness — every decoded key actually names a genuine member of , never a phantom (Sd2). And hgen, the heaviest of the six, bundles L2 (composition exhausts the disconnected types), generation-exhaustiveness (the enumerator’s sweep over the connected-≤5 pool is complete), and connected-≤5 completeness itself — the seam that stands in for the number A288568 supplied, ready-made, in the connected campaign (Gd4).
The connected census’s completeness theorem, census_count_match, worked by squeeze: A288568 supplies an independently published count of connected types at each circle number, so once the emitted keys are shown pairwise distinct, the two counts pin each other down and completeness falls out of arithmetic. The disconnected stratum has no such number. Nobody has published a count of disconnected pseudocircle sphere-types at six circles; the figure this campaign works against, 16,597, is not corroborated from outside — it is the count of distinct keys the composition enumerator happens to emit. There is nothing external left to squeeze against.
What replaces the missing number is L2, the claim that disconnected types are exactly composites of connected types at smaller circle counts, folded into hgen above. And because there is no external count, both directions of Kd carry real weight in the final theorem — where the connected campaign found its separation direction, K2, came “nearly free,” useful for soundness but never on the count-match’s critical path. Here, K2d’s attainment-qualified separation core is exactly what lets hgen’s existential (some generated composite realizes each true type) turn into an actual membership fact about K. Remove either direction and the bijection does not go through.
D-F and D-G, laying the keyer’s two directions, each pushed one piece of unfinished business downstream by name into this round. D-H is graded on whether it paid those debts rather than smuggled them past the kernel.
The oriented groupoid. D-G built its separation core directly and left CompositeIso.symm/trans undefined, because nothing in that round ever composed two isomorphisms through a decoded middle object. This round writes both: symm inverts every field of a witness back through Equiv.apply_symm_apply; trans composes them, chaining the forest fields through the promoted per-node DartIso.trans. Worth noticing what this infrastructure is not yet doing: the capstone theorem below never once calls .symm or .trans. It is paid down ahead of the obligation that will actually spend it — the still-open closure-collapse replay, discussed below, which will need to chain witnesses through intermediate composites, exactly what a genuine groupoid structure is for. This round retires a piece of infrastructure debt before the theorem that owes it exists.
The forest under the mirror. The diagonal mirror flips a whole composite’s orientation and remaps its nesting faces through a per-host face map fm. This round proves that whenever every host’s fm is injective — a property the real census face map actually has, being a bijection of each host’s own face ids — the entire nesting forest survives untouched: same containment, same depths, same parent table, same laminarity, same forest-faithfulness. Geometrically the reason is simple: sentinels are fixed by the mirror and face ids are only permuted, never merged, so “this cell is not the outer face” is exactly as true after the mirror as before. But it had to be proved field by field, because nothing about mirrorC’s bare definition makes that survival automatic.
DecodeReady.mirror, the round’s named obligation. The Boomerang’s mirror branch worked by taking the mirror side’s whole DecodeReady package — well-formedness, laminarity, forest-faithfulness, per-cluster circle-faithfulness — as a hypothesis supplied from outside, rather than built from the plain side’s package. This round builds that transport. Given DecodeReady B ceB and an injective per-host face map, DecodeReady.mirror hands back DecodeReady (B.mirrorC fm) ceM: laminarity and forest-faithfulness ride the forest-under-mirror lemmas just proved; well-formedness rides the promoted per-cluster mirror machinery; circle-faithfulness rides the promoted CircleFaithful.mirror. What it does not derive, and says so in its own docstring, is the mirror ce table’s shape and canonicity — the same Gd2 seam the forward direction already sits behind, passed through as an honest input, never smuggled in as a free conclusion.
Put the six hypotheses together and the theorem below has exactly two moving, load-bearing parts, matching the two things Kd asks of dedupe. One is checked in the kernel. The other is written down and trusted.
No-undercount is derived, not assumed. For a true type in , hgen hands over a generated composite g whose key is actually in K. Canonicity says decoding that key and re-keying it returns the identical bytes. The attainment-qualified K2d — the Boomerang’s separation core, never the naive form the Boomerang kernel-refuted (lensBare_lensInBare_no_iso: two re-rootings of one sphere, equal keys, no default-gauge isomorphism) — then forces the decoded composite to be -or-mirror to g. When the mirror disjunct fires, it is DecodeReady.mirror, built in this round, that supplies the mirror-side package the separation core demands, with no floating hypothesis left over.
have hsurj : ∀ t ∈ Td, ∃ p ∈ K.attach, Φ p = t := by
intro t ht
-- obtain the generated composite g and its bundled hgen facts
-- the mirror-side package, BUILT from `g`'s by the named mirror-transport
have hBM : DecodeReady (g.C.mirrorC g.fm) (g.ceM none) bord :=
hgB.mirror g.fm hgfm (g.ceM none) hgshaped hgcanon
-- the decoded emitted key `g.key` re-keys to `g.key` (canonicity)
have hkey : (dec (g.key sord) hgk).key sord = g.key sord := hcanon (g.key sord) hgk
-- K2d, attainment-qualified: `dec (g.key)` is ≅ₙ-or-mirror to `g`
have hK2 := compositeIso_or_mirror_of_sphereKeyToks_eq
(hA := hdr (g.key sord) hgk) (hB := hgB) (hBM := hBM)
(hattA := hattA (g.key sord) hgk) (hattB := hgatt) (h := hkey)
-- Or.inl/Or.inr into IsoOrMirrorC, then stypeOf_eq_of_isoOrMirror closes the goalDecoded: this is where the round’s whole point lives. hgB.mirror is DecodeReady.mirror firing — a built transport, not a hypothesis. compositeIso_or_mirror_of_sphereKeyToks_eq is the Boomerang’s attainment-qualified separation core, consuming exactly the two DecodeReady packages it demands, never the kernel-false naive form.
No-overcount is assumed, not derived. This is where D-H is weaker than its connected sibling. census_count_match, the connected campaign’s capstone, derives its injectivity conjunct outright, because IsoOrMirror at the single-cluster level was proved to be a genuine Equivalence directly — reflexivity from DartIso.refl, symmetry and transitivity from the promoted transport suite — so its quotient’s classes are exactly the isomorphic-or-mirror classes, no closure required, and the single-step invariance lemma K1 is all injectivity needs. Here, the analogous fact is a hypothesis instead:
(hkeyInj : ∀ k₁ k₂ (hk₁ : k₁ ∈ K) (hk₂ : k₂ ∈ K),
(dec k₁ hk₁).typeOf = (dec k₂ hk₂).typeOf → k₁ = k₂)Why can’t the promoted descent lemma, sphereKeyToks_k1d (D-F’s invariance direction: or implies equal sphere key), discharge this the same way? Because CompositeIso’s base relation, IsoOrMirrorC, has no proof of its own transitivity — composing a mirror-branch witness with another mirror-branch witness needs its own argument about how the diagonal mirror interacts with composition, and that argument does not exist yet. So CompositeSphereType falls back to the EqvGen equivalence closure, which is a genuine Setoid for free but says nothing about whether its classes coincide with IsoOrMirrorC’s own. Type equality in that closure can be witnessed by a chain: A related to some intermediate composite, that composite to another, down to B, each link one IsoOrMirrorC step or its reverse. sphereKeyToks_k1d only ever proves invariance for one such link, and only for composites carrying actual sphere-key sweep data — an fm, a rooting list, a ce table. An arbitrary intermediate composite in the chain carries none of that; there is nothing to apply the promoted lemma to. Closing hkeyInj honestly means proving those chains never actually arise on real census geometry — the closure collapses back to one direct step — and that replay remains open.
One more honesty check worth making explicit. The theorem’s pairwise conclusion — that distinct keys in K decode to composites that are never -or-mirror — reads like a second, independent distinctness fact. It is not. It falls straight out of hkeyInj’s contrapositive plus stypeOf_eq_of_isoOrMirror: if two decoded composites WERE -or-mirror, their types would be equal, and hkeyInj would then force their keys equal, contradicting k₁ ≠ k₂. It is the same assumed hypothesis wearing its logical converse, not a second thing paid for.
Td must correspond to some emitted key in K, and the correspondence has to run both ways before the counts can be set equal. No-undercount, solid and accent-colored, is derived: hgen’s generated witness, the attainment-qualified K2d, and DecodeReady.mirror together guarantee every type is hit. No-overcount, dashed and muted, is assumed: hkeyInj states distinct types get distinct keys directly, as a hypothesis, because the EqvGen-closure quotient blocks the connected campaign’s route to deriving it.This is the Lean, unmodified. First the oriented groupoid D-G left undefined, now discharged (A250001/CompositeCensusComplete.lean):
def symm (E : CompositeIso A B) : CompositeIso B A where
clusterEquiv := E.clusterEquiv.symm
nodeIso i := by
have h := (E.nodeIso (E.clusterEquiv.symm i)).symm
rwa [Equiv.apply_symm_apply] at h
-- locFace_bare, inside_iff elided (~14 lines) -- the same shape: chase σ.symm
-- through `Equiv.apply_symm_apply`, twice each.
parent_comm X := by
have h := E.parent_comm (E.clusterEquiv.symm X)
rw [Equiv.apply_symm_apply] at h
rw [h]
cases hp : A.parent (E.clusterEquiv.symm X) with
| none => rfl
| some a => simpDecoded: every field of symm inverts the corresponding field of E through Equiv.apply_symm_apply — clusterEquiv by Equiv.symm, each per-node witness by the promoted DartIso.symm, parent_comm by chasing the same equation backward. trans (not shown; the same shape, composing rather than inverting) completes the groupoid.
The forest surviving the mirror, one representative lemma of several (parent itself):
theorem mirrorC_parent (hfm : ∀ Y, Function.Injective (fm Y)) (X : Fin C.numClusters) :
(C.mirrorC fm).parent X = C.parent X := by
show (List.finRange (C.mirrorC fm).numClusters).foldl ((C.mirrorC fm).parentStep X) none = _
rw [CompositeMap.parent]
congr 1
· funext best Y
exact mirrorC_parentStep hfm X best YDecoded: the mirrored composite’s own parent scan, unfolded, is provably the identical function to the plain composite’s — not merely equal in value on census inputs, but the same computation, once every containment test underneath (built on injectivity of the per-host face map) has been shown unchanged.
The round’s named obligation, the mirror-transport of the decode package:
theorem DecodeReady.mirror {B : CompositeMap} {ceB : Fin B.numClusters → ClusterEnc}
{bord : LinearOrder (List ℕ)} (hB : DecodeReady B ceB bord)
(fm : Fin B.numClusters → ℕ → ℕ) (hfm : ∀ Y, Function.Injective (fm Y))
(ceM : Fin (B.mirrorC fm).numClusters → ClusterEnc)
(hshaped : EncShaped (B.mirrorC fm) ceM)
(hcanonM : ∀ (X : Fin (B.mirrorC fm).numClusters) (P : PackedMap) (of : ℕ),
(B.mirrorC fm).node X = .cluster P of →
∃ mark, (ceM X).enc = (P.bodyRecord bord ++ [mark]).map .sym) :
DecodeReady (B.mirrorC fm) ceM bord where
wf := CompositeMap.mirrorC_wellFormed fm hB.wf
lam := CompositeMap.mirrorC_laminar hfm hB.lam
ff := CompositeMap.mirrorC_forestFaithful hfm hB.ff
shaped := hshaped
canonical := hcanonM
faithful := by
-- proof elided here (∼15 lines) -- a mirrored crossing node is `cluster P.mirrorP _`,
-- whose map is `mirror P.map`; CircleFaithful.mirror + mirror_circ_surjective close it.Decoded: four of five fields are genuinely BUILT — carried through by the forest-under-mirror lemmas and the promoted per-cluster mirror machinery. shaped and canonical are passed straight through as supplied inputs — the same Gd2 fence the plain direction’s own DecodeReady already sits behind, not weakened further, not smuggled past.
And the statement of record itself:
theorem composite_census_complete (bord : LinearOrder (List ℕ)) (sord : LinearOrder (List SerTok))
{K : Finset (List SerTok)} (dec : ∀ k ∈ K, PackedComposite)
-- Gd3: each emitted key re-keys to itself (attainment at the default gauge)
(hcanon : ∀ k (hk : k ∈ K), (dec k hk).key sord = k)
-- K1d on the family: the keyer is injective on decoded types (no overcount)
(hkeyInj : ∀ k₁ k₂ (hk₁ : k₁ ∈ K) (hk₂ : k₂ ∈ K),
(dec k₁ hk₁).typeOf = (dec k₂ hk₂).typeOf → k₁ = k₂)
-- the decoder-side K2d inputs (A-side of the separation core)
(hdr : ∀ k (hk : k ∈ K), DecodeReady (dec k hk).C ((dec k hk).ce none) bord)
(hattA : ∀ k (hk : k ∈ K), (dec k hk).key sord =
(dec k hk).C.orientedKeyToks ((dec k hk).ce none) sord (dec k hk).nCircles)
{Td : Finset CompositeSphereType}
-- Sd2 soundness: every emitted key names a genuine type
(hmem : ∀ k (hk : k ∈ K), (dec k hk).typeOf ∈ Td)
-- L2 + generation-exhaustiveness + connected-≤5 (+ g-side K2d inputs), the Gd4 seam
(hgen : ∀ t ∈ Td, ∃ (g : PackedComposite),
g.typeOf = t ∧ g.key sord ∈ K ∧
(∀ Y, Function.Injective (g.fm Y)) ∧
DecodeReady g.C (g.ce none) bord ∧
EncShaped (g.C.mirrorC g.fm) (g.ceM none) ∧
(∀ (X : Fin (g.C.mirrorC g.fm).numClusters) (P : PackedMap) (of : ℕ),
(g.C.mirrorC g.fm).node X = ClusterNode.cluster P of →
∃ mark, ((g.ceM none) X).enc = (P.bodyRecord bord ++ [mark]).map SerTok.sym) ∧
(g.key sord = g.C.orientedKeyToks (g.ce none) sord g.nCircles ∨
g.key sord = (g.C.mirrorC g.fm).orientedKeyToks (g.ceM none) sord g.nCircles)) :
(∀ k₁ k₂ (hk₁ : k₁ ∈ K) (hk₂ : k₂ ∈ K), k₁ ≠ k₂ →
¬ (dec k₁ hk₁).C.IsoOrMirrorC (dec k₂ hk₂).C) ∧
Td.card = K.card := by
-- proof elided here (∼45 lines) -- kernel-checked, standard axioms only.
-- builds the class map Φ, gets injectivity straight from hkeyInj, gets surjectivity from
-- the hsurj argument shown above, closes with Finset.card_image_of_injOn + Finset.card_attach.Decoded: six hypotheses in, a bijection out. No smuggled seventh fact — every step is one of the six named hypotheses, one of the built lemmas above, or a standard Finset cardinality fact.
The Boomerang closed K2d’s honest form; the Matryoshka closed K1d. Between them, Kd’s two directions existed as separate theorems, each already careful about its own honesty fence. D-H is where they have to occupy the same statement, and the composite census’s ledger becomes exactly one theorem: a Finset of keys can genuinely stand in for Td, provided six named facts hold. That “provided” is the entire content of the round. It is also, plainly, weaker than it would be if hkeyInj were proved — and the file’s own docstring says so, rather than letting a reader find out from the hypothesis list alone.
It matters beyond this one file, too. The disconnected stratum’s completeness argument was never going to be a cardinality squeeze; the scoping document said as much before a line of this round’s Lean existed. What D-H demonstrates is that the injective-complete-invariant argument proposed instead actually assembles — that six named, independently inspectable facts really do compose into a bijection, in the kernel, with no hidden seventh fact doing invisible work. The firewalled cold review’s whole job was checking for that seventh fact. It did not find one.
Proved, kernel-checked on standard axioms only (7 #print axioms gates in Tests.lean plus the whole-environment sweep; independently rebuilt by a firewalled adversarial cold review, 8504 jobs green, verdict STANDS-WITH-CAVEATS — not STANDS-WITH-ERRATA, the verdict every round before it earned. The difference is not cosmetic: an erratum is a wording fix; a caveat is a fact about what the theorem does and does not establish, left standing on purpose rather than patched away): the oriented groupoid (CompositeIso.symm/trans); the forest-under-mirror lemmas; DecodeReady.mirror, the round’s named mirror-transport; the EqvGen-closure quotient CompositeSphereType; and the assembly composite_census_complete as a valid implication — six named hypotheses in, a genuine bijection out, no circularity, hgen confirmed not to beg its own conclusion, the naive unqualified K2d confirmed never invoked anywhere in the chain.
Not proved — two caveats, named rather than absorbed into fine print. First, no-overcount is assumed: hkeyInj is a typed hypothesis, not a theorem, and that is a real trust regression against the connected campaign’s census_count_match, which derives the equivalent fact outright. Closing it is the re-rooted-gauge and closure-collapse replay — showing every EqvGen chain between census composites collapses to one direct step — and it remains open. Second, with no closure-collapse lemma proved, CompositeSphereType is known only to be at least as coarse as -or-mirror: stypeOf_eq_of_isoOrMirror guarantees that composites related by one step get equal types, but nothing here rules out the closure identifying more than that. Where the real granularity settles is fenced to L2 and Sd2 — exactly where the topological content of this whole campaign has always lived.
None of this is a defect in the Ledger. A ledger that only ever reported balanced totals, with no visible column, would be the actual failure — not this one, which shows its work and names its own open debt. is real, kernel-checked, and conditional: six seams, five of them closed by proof, one of them still a promise. The promise has a name, a location, and a stated reason it hasn’t been kept yet. That is what makes it a ledger, and not merely a number.