A Notes on the formalization

This chapter records the wrong turns the formalization of Katoh–Tanigawa’s Theorem 5.5  [ KT11 ] took on the way to the argument the earlier chapters present: statements whose formal strength diverged from the source’s, decompositions that did not survive contact with the assembly they were meant to feed, and obligations left with no artifact tracking them. Three patterns recur across most of the sections below and are named in the next paragraph. Section A.1 is a scaffolding narrative the three-way classification does not apply to at all, and section A.4 groups two episodes by a shared symptom instead of by one pattern, each episode there self-classifying separately. Within a section, an episode narrates what a check did and did not read at the time a divergence was introduced, and the check that eventually caught it. Because the subject here is the formalization itself, Lean declarations, their types, and short code excerpts appear directly in the prose below, rather than only as parenthetical citations, as they do in the rest of this document.

A genuine mis-factoring is an internal decomposition — an abstraction layer, a splice of two arguments, a case split — that did not match the structure the final assembly needed, so the decomposition was replaced without changing the underlying mathematics. A source-faithfulness correction is a Lean statement whose formal strength diverged from Katoh–Tanigawa’s — weaker, stronger, or differently quantified — found and corrected without invalidating any proof already built on it. A process failure is a decision that was sound when made but left with no artifact tracking it, or an error that no check running at the time could have read.

Commits are cited by an eight-character abbreviated SHA linking to the corresponding commit on GitHub; every cited commit postdates the project’s 2026-05-13 move to a standalone repository.

A.1 The \(d = 3\)-first scaffolding arc

The episode below sits outside the three-way classification above: it is not a mis-factoring, a source-faithfulness correction, or a process failure, but a scaffolding choice, refined twice at contact with a build, that left nothing already proved to redo.

Katoh–Tanigawa present Case III (KT §6.4, Theorem 5.5’s hardest case) twice: concretely at \(d = 3\) (§6.4.1, Lemma 6.10, a fixed dispatch on four vertices \(v, a, b, c\)), then at general dimension (§6.4.2, Lemma 6.13, a length-\(d\) chain \(v_0 v_1 \dots v_d\)), with the remark that “the proof strategy is exactly the same as \(d = 3\)” (p. 692). The formalization took the same order, and made the choice explicit rather than assumed, at Phase 22c’s second design-recon pass (commit 6511a01a, 2026-06-05): \(d = 3\) first, following “KT’s own §6.4.1-then-§6.4.2 cut,” with the general-\(d\) lift assigned to its own later phase before any of the concrete case was built.

The same pass staged the \(d = 3\) choice again, one level down, rather than attempting Lemma 6.10 — KT’s longest proof, roughly twelve printed pages — as a single build: it split the lemma into three difficulty strata (the eq.-(6.12) degenerate placement, giving a rank one short of full; the redundant-row argument of Claim 6.11, named the genuinely new research crux; and Claim 6.12’s candidate-completion finish), and committed only the first stratum to the sub-phase then opening (Phase 22c itself). The three strata were then built in turn across Phases 22c–22h, entirely inside the concrete carrier — every panel normal a literal Fin 4 vector, every screw a literal element of the six-dimensional \(\bigwedge ^2{\mathbb {R}}^4\), arithmetic such as screwDim 2 \(= 6\) closing by decide — closing with the \(d = 3\) Case-III node itself reaching green, modulo a small number of explicitly carried hypotheses later discharged in subsequent sub-phases (commit b9a45ea9, 2026-06-11, closing Phase 22h).

Once the \(d = 3\) construction reached this state, a design pass drew a reuse map against it before any general-\(d\) Lean was written (commit 036804b2, 2026-06-07): Claim 6.11’s redundant-row mechanism (exists_redundant_panelRow_ab_of_finrank_eq) and Lemma 2.1’s extensor-span finish were read as reusable verbatim once re-stated at general grade; the exterior-algebra meet API (complementIso, topEquiv, pairingDualEquiv) needed only dimension-parametric re-statement; and the fixed three-candidate dispatch, together with the bespoke \(\bigwedge ^2{\mathbb {R}}^4\) duality, were marked for wholesale replacement by a \(d\)-candidate chain dispatch and a \(\bigwedge ^{d-1}({\mathbb {R}}^{d+1})\) duality — the same one-dimensional top-exterior-power fact at a different grade, not the general Hodge-star construction Katoh–Tanigawa never invoke. The same map recorded one further claim: that the realization spine underlying all three cases — the genericity device, theorem_55’s skeleton, and Cases I and II — was already general and green, the graph-side combinatorics being dimension-free throughout.

That last claim did not survive Phase 23’s own opening design pass (commit 6ea8a691, 2026-06-17). Re-reading every spine declaration against its landed Lean grade found theorem_55_d3, case_III_realization, and case_III_candidate_dispatch all carrying ScrewSpace 2 and Fin 4 literally: dimension-parametricity held for the graph-side bookkeeping the earlier map had checked, not for the panel-geometric spine the induction is actually stated over. The correction split the remaining work along a fault line the earlier map had not drawn — a mechanical lift of the pinned spine to symbolic screwDim k, kept apart from the genuinely new chain dispatch and duality — and scheduled the lift first, as sub-phase 23a: not because it was mathematically hard, but because the chain dispatch and the duality both had to be stated at general grade, which presupposes a general-grade spine to state their conclusions over, and because the symbolic-\(k\) arithmetic underlying screwDim k — concrete and decidable at \(k = 2\), symbolic thereafter — was the one named risk of a build-time blocker, best surfaced before new mathematics was built on top of it.

The same correction repeated at a finer grain the same day. Lifting the spine’s own closing declaration found that four further producers — the base, cut-edge, Case-I, and forgetful-map realizations — were themselves Fin 4-pinned through the same \(\bigwedge ^2{\mathbb {R}}^4\) duality lemma, and so were not liftable by the numeral pass that generalized the rest of the spine (commit ee1674df, 2026-06-17, closing sub-phase 23a). They were carried forward as four explicit hypotheses, the project’s standing green-modulo idiom, to be discharged once the general chain-dispatch duality became available.

None of these three revisions — the \(d = 3\)-first cut itself, the reuse map, and its correction at Phase 23’s own opening — reopened anything already proved: the \(d = 3\) construction stayed green throughout, and Phase 23 closed (commit 623846d0, 2026-07-02) with Conjecture 1.2 stated as a theorem, along exactly the division the corrected map had drawn. Building the hardest case concretely first did not remove the need to re-scope its generalization; it moved the re-scoping to a point where a whole worked case, not a paper reading alone, was there to check the scope against.

A.2 Statement-faithfulness episodes

The episodes below are source-faithfulness corrections in the sense of the introduction: a Lean statement’s formal strength diverged from Katoh–Tanigawa’s, and the divergence was found and repaired without invalidating proofs already built against it.

A realization predicate weaker than its prose

KT Theorem 5.5 asserts that a minimal \(k\)-dof graph admits a panel-hinge realization whose rigidity matrix attains the maximal rank. In KT’s definition (KT §5.1) each hinge is a line: a nonzero \(2\)-extensor contained in both endpoint panels. The formalization introduced the realization predicate in June 2026 (commit 1cd26cce) as

with no condition on the hinge extensors. The omission makes the predicate satisfiable for every connected graph. The framework assigning every hinge the degenerate endpoint pair \((a_0, a_0)\) has all support extensors zero; the constraint at an edge \(uv\), that the screw difference \(S_u - S_v\) lie in the span of the edge’s extensor, then reads \(S_u = S_v\), so on a connected graph every infinitesimal motion is constant and the rank is the full \(D(|V|-1)\). The realization conjunct of the formalized Theorem 5.5 was satisfied by this witness independently of the theorem’s content.

The predicate had been introduced as rank bookkeeping for the induction of KT §5 and was not compared against KT’s definition of realization, either at its introduction or at the one later redesign that reworked it (the two-motive split of e4693d61’s design pass re-read KT on the simple-versus-non-simple axis and did not pose the question). The blueprint did not expose the divergence: the definition’s dependency-graph node was marked formalized beside prose at the paper’s strength, and none of the per-commit checks compared a definition’s Lean body with its prose — the name-resolution check verifies that pinned declarations exist, and the hypothesis audit reads a theorem’s hypotheses, of which a definition has none.

The divergence was found by a pre-build audit of the theorem’s hypothesis feeds (commit e4693d61, 2026-06-11), before any construction was built against the degenerate witness. It was a weakness of statement selection rather than of proof: the general-position motive introduced at the two-motive split is at KT’s strength, and the rank arguments beneath the bare conjunct required no rework. The repair was scheduled at the motive redesign that the same audit had already forced, so the definition surface was reshaped once rather than twice, and landed as (652ea99f)

whose nonzero-normal and nonzero-extensor conjuncts are the nondegeneracy conditions of KT’s definition. The check this produced is the cheapest-witness audit (blueprint/CLAUDE.md, the definition-faithfulness gate): when a definition modeling a paper notion is marked formalized, its blueprint prose is read against the cheapest satisfying witness of the Lean body, not against the paper.

Katoh–Tanigawa Lemma 4.1’s over-quantified statement

Katoh–Tanigawa’s own argument for the degree-of-freedom bookkeeping a splitting-off or a vertex removal induces, on the way to Theorem 4.9, is a forest surgery, [ KT11 , Lemma 4.1 ] (p. 660; the 2009 arXiv predecessor, Lemma 5.1, p. 11, is essentially verbatim): “for any independent set \(I\) of \(M(\tilde G)\) …there exists \(I'\) …with \(|I'| = |I| - D\).” Formalizing this quantifier literally, rather than paraphrasing it into the base-restricted form the induction actually needs, exposed at once that it cannot hold as written: for an independent \(I\) with \(|I| {\lt} D\) — \(I = \emptyset \) suffices — the promised \(|I'|\) would have to be negative. The disproof was recorded as a Lean witness rather than quietly paraphrased away, in the same commit that added the remark distinguishing the finding’s three layers (remark 21.15) and re-pointed Theorem 4.9’s degree-of-freedom tracking off the forest surgery entirely (commit f0934296, 2026-06-03). It was introduced as an anonymous example; a later cleanup pass promoted it to a named lemma so the corresponding blueprint node could pin it directly, replacing a comment noting it was an anonymous, unpinnable example (commit bc579c3f):

(bodyBarDim n is \(D\); bodyHingeMult n the per-edge multiplicity of \(\tilde G\)’s edge fibers.)

A second, subtler layer came with the same finding. Katoh–Tanigawa’s proof of the intended, base-quantified reading converts each of the \(D\) forests of a chosen packing by removing one edge, silently assuming the packing is balanced at the degree-2 vertex \(v\) under surgery — every forest already meets one of \(v\)’s two incident edges. Neither the 2011 paper nor its 2009 predecessor justifies this, and the finding first recorded it as an open question. It resolved positively later the same day: a counting bound (a base of \(M(\tilde G)\) meets at least \(D\) of \(v\)’s \(2(D-1)\) incident fibers) together with a redistribution move (a forest avoiding \(v\) has \(v\) isolated, so it absorbs a free fiber as a pendant without creating a cycle) and a finite descent construct a balanced packing for every base and every \(D \ge 2\) (commit 398ce7ac). By the time this second layer closed, though, Theorem 4.9’s tracking no longer needed it: the same finding commit had already re-pointed the induction onto a direct partition-count argument through the def \(=\) corank bridge (theorem 20.12, rank_add_deficiency_eq, Phase 19), discharged within the same session, bypassing the forest surgery. The repaired surgery survives as a sound, off-critical-path formalization of KT 4.1’s splitting-off direction; the removal direction, KT 4.2, stays deferred, needed by neither route.

This is a divergence in the source’s own statement, not in how the Lean represented it: what the induction actually consumes — the base-quantified deficiency inequality — is exactly Katoh–Tanigawa’s intended content, and stating that content precisely, rather than transcribing the paper’s literal quantifier, was the formalization’s task. Full three-layer statement and repair: remark 21.15.

A fixed-candidate disjunction for Claim 6.12’s free line choice

Katoh–Tanigawa’s Claim 6.12 [ KT11 , § 6.4.1 ] (eqs. (6.30)–(6.45)) underlies the \(d = 3\) Case-III realization: three candidate placements \(p_1, p_2, p_3\) are built by splitting off along a freely chosen \((d-2)\)-affine line — “we may choose any \(L \subset \Pi (a)\), \(L' \subset \Pi (b)\), \(L'' \subset \Pi (c)\)” — and the claim is that for some choice at least one of the corresponding blocks \(M_1, M_2, M_3\) has full rank. The capstone formalizing this, case_III_claim612, first modeled the claim not at a free line but at the three specific lines the realization producer happens to build (the split edges \(va\), \(vb\), \(ac\)), with conclusion \(r(C_1) \ne 0 \lor r(C_2) \ne 0 \lor r(C_3) \ne 0\) for the three corresponding fixed extensors, discharged contrapositively through an explicit duality hypothesis (commit 56aef7c4, 2026-06-07):

Tracing what discharges hduality two days later found the fixed antecedent mathematically unusable, not merely incomplete: \(C_1, C_2, C_3\) are three vectors in the six dimensions of \(\bigwedge ^2 {\mathbb {R}}^4\), so “\(r \perp C_1, C_2, C_3\)” can never force \(r = 0\), while Katoh–Tanigawa’s own text confirms the three lines are freely chosen, not graph-fixed — so Claim 6.12 is a genuine existential over that continuum, not a disjunction at three fixed points (commit 82b3b50a). The repair restated the capstone as the existential it actually is, over the six pairwise joins of four affinely-independent points, which do span \(\bigwedge ^2 {\mathbb {R}}^4\) (lemma 18.9, KT Lemma 2.1) even though three fixed lines cannot (commit d5ff3648, 2026-06-09): The realization producer consumes the existential by building its candidate placement so its hinge line is the witness join’s line. A later generalization to arbitrary \(d\) subsumed this \(d = 3\)-specific form into case_III_claim612_gen, the declaration the blueprint node lemma 23.191 pins today.

Unlike Lemma 4.1’s divergence, which sits in Katoh–Tanigawa’s own text, this one originated in the Lean’s internal decomposition of the claim: modeling a free line choice as a disjunction over three graph-fixed candidates was a shape choice, not a mistranscription of KT’s statement, and the fix corrects that shape — which happened also to be mathematically undischargeable, not merely a looser reading of the source.

A.3 Abstraction-layer mis-factorings

The episodes below are genuine mis-factorings in the sense of the introduction: an internal decomposition — an abstraction layer, a splice of two arguments — that did not match the structure the final assembly needed, so the decomposition was replaced without changing the underlying mathematics.

The Claim 6.12 candidate-row producers

Katoh–Tanigawa’s Claim 6.12 [ KT11 , § 6.4.1 ] , introduced above (section A.2), supplies the row that completes Case III’s rank count: the redundant-row argument of Claim 6.11 falls one row short of the target, and Claim 6.12 supplies the last row from one of three candidate splittings \(p_1, p_2, p_3\). Phase 22e (2026-06-06) formalized the second and third candidates as abstract row-family linear-independence theorems, quantified over an arbitrary BodyHingeFramework, not over any concrete construction:

(commit 9b8a6c67, 2026-06-06; the symmetric third candidate, split at the other degree-2 body along \(ac\), landed the same day as linearIndependent_sum_p3_candidateRow, commit 87ea1295). Both are graph-free: F is an arbitrary abstract framework, and each theorem concludes independence of the row family the candidate completion assembles, packaged for whichever concrete carrier eventually supplies the surrounding old and new row blocks rn/ro.

A design pass the following day planned to consume these producers directly: compose the abstract row-family independence with a fixed-framework device-feed brick, so that discharging the witness condition hr would close the realization (commit a893639a, 2026-06-07). Four days later, reading Katoh–Tanigawa’s own eq. (6.29) sketch against that plan found it was not literally transferable: the composed family has to be consumed at the one-parameter shear family Case III’s construction actually builds, and the certified family the row-family producers supply is not of that shape (the candidate row, and part of the transported bottom family, are not rows of the sheared candidate at \(t \neq 0\)). The corrected route instead certifies the target rank at the fixed, unsheared framework \(F_0\), converts the count to a rank lower bound, re-extracts a literal panelRow family from that bound, and transfers that family along the shear (commit 5aff1320, 2026-06-11 — “certify-then-rebase”). The rank certification this needs, case_III_rank_certification, landed the same day (commit f6856538), and the three arm closers that consume it — case_III_arm_realization (\(M_1\)), case_III_arm_realization_M2 (\(M_2\), commit 2981429e), and case_III_arm_realization_M3 (\(M_3\)) — each read their target rank bound off the certification, not off linearIndependent_sum_p2_candidateRow or _p3_candidateRow: their own doc-comments record this explicitly, factoring the arm closer as the part that depends only on the certified rank bound and the split/seed data, “not on how that rank was certified”.

Neither producer, nor their selector packagings, ever gained a caller outside the file that defines them once the certify-then-rebase route landed: a later audit during the Phase-26 cleanup round found both producers and their selectors dead against the live Lean call chain into the theorem, alongside the \(d = 3\) candidate dispatch they were built to feed (commit fe2f2a73, 2026-07-07). They were kept for a time — they grounded the worked \(d = 3\) case exposition the blueprint’s Case III chapter presents, even though the theorem no longer built through them — and a cleanup round deleted them in October 2026, still without a caller; the abstraction itself, correct and graph-free as built, never reached the assembly it was factored to feed. This is a genuine mis-factoring: the row-family layer was mathematically sound at every stage, and what replaced it is a different decomposition of the same rank count, not a correction to its content.

A motion-space splice for Katoh–Tanigawa’s block-triangular rank-addition

Katoh–Tanigawa’s Case I inductive step [ KT11 , eq. (6.3) ] adds the ranks of two separately-placed rigidity matrices: a rigid subgraph \(H\) realized at its own generic placement contributes \(D(|V(H)|-1)\) rows, and the contraction \(G/E(H)\) realized at its own generic placement contributes the rest, the two ranks adding because each block occupies disjoint columns once the other is projected away. No step of KT’s argument asks for one placement simultaneously realizing both legs.

Phase 21b’s first Case-I composer nonetheless took two same-placement rigidity outputs as hypotheses — the rigid subgraph and the contraction both rigid on the same witness placement, with no Lean lemma constructing such a placement — flagged the same day by a blueprint-honesty audit as premature (commit 615638e4, 2026-06-04). The repair that followed built an honest, satisfiable glue lemma in place of assuming the common placement outright:

(lem:case-I-splice-seed, commit 5b6f5a6a, 2026-06-04). This is a locally sound modelling choice — KT eq. (6.3) read as two overlapping rigid pieces glued along their shared body — and it is genericity-free, exactly as KT’s own splice is. But hblock and hcontract are both stated of the same framework F: the glue demands one placement simultaneously rigid on both legs, where KT’s block-triangular structure places each leg independently and adds the resulting ranks.

Phase 22a’s realization producer, built on this glue, then had to supply that common-seed rigidity, and tried to do so across two re-plans on the same day before the divergence was named, each producing a hypothesis that type-checked but was not dischargeable. The first composer bundled a placement-independent complement-isolation equality — for every placement \(q\), the pinned-motion dimension at the contraction’s surviving body set \(s_c\) equals \(D \cdot |s_c^{\complement }|\) — found generically false the same day: off the full vertex set, the contraction leg’s interior bodies still carry surviving boundary-edge constraints, so the equality fails (commit c95d7bc0, 2026-06-05). An asymmetric-coupling repair deleted that equality and fed the contraction leg’s rigidity directly from a universally-quantified general-position hypothesis — for every general-position placement \(q\), the leg is rigid at \(q\) — and a second verification pass the same day found this equally undischargeable: general position is pairwise normal independence, strictly weaker than the maximal rank the hypothesis demands (commit 85f5b054, 2026-06-05). Both passes had taken the glue’s shape as fixed and tried to satisfy its obligation; neither questioned the glue itself.

The divergence, once named, was structural rather than a missing hypothesis: the project’s rigidity model is a motion-space predicate — every infinitesimal motion constant on a body set — and the glue had translated KT’s rank-addition into a motion-space statement that needs a common witness KT’s own argument never constructs. The repair replaced the glue’s obligation with a row count read off a single framework’s rigidity-row span directly — independent rows in each block, rather than rigidity of each leg — eliminating the common-seed demand by construction (commit f504955c, 2026-06-05, the block-triangular reframe; lemma 23.89 and lemma 23.100 record the corrected form). The reframe’s own first cut restated the surviving block’s obligation with the same universal quantifier over general position again — the same over-quantification recurring one level down — corrected the same day to a rank-polynomial non-root condition, KT’s genuine Zariski-open genericity locus (commit c9750bdf, 2026-06-05).

This is a genuine mis-factoring: the motion-space model that carried Phases 4–16 without incident re-expressed KT’s block-triangular rank-addition as a different argument with a different, harder obligation, and the tell across both re-plans was the same — the arithmetic closed, but each pass needed a fresh hypothesis to bridge a gap Katoh–Tanigawa’s own proof does not have.

A.4 Walls from mis-modelling

The two episodes below share a symptom rather than one cause: each is a point at which the formalization’s chosen approach turned out to be unable, in principle, to produce the fact the next step needed — a wall, in the sense that no further building along the same route would have closed it — and each was diagnosed only once the target quantity was traced directly through the source construction, rather than by a check of the surrounding declarations’ types. The two do not share one classification from the introduction’s three-way taxonomy; each states its own below.

The member-mapping wall

Katoh–Tanigawa’s proof of Case III at general dimension (KT §6.4.2, Lemma 6.13, the length-\(d\) chain \(v_0 v_1 \dots v_d\)) certifies the rank added at each induction step \(i\) by a \(D \times D\) corner block \(M_i\), whose rank adds to a base block’s to reach the full \(D + D(|V|-2) = D(|V|-1)\) (eqs. (6.64)–(6.65)). The corner’s second row is one fixed vector \(r \in {\mathbb {R}}^D\) at every step \(i\) — held fixed by a degree-two cancellation, not transported across the induction (eq. (6.66)) — and the construction shows some choice of the corner’s first row makes \(M_i\) invertible against \(r\), over a free line each step is built from (eq. (6.67)).

The formalization’s first approach to the general-\(d\) step (Phase 23b, opened 2026-06-17) modeled this certification as a transported span membership instead: hold one witness row’s membership in the span of already-certified rows fixed, and carry it forward across the induction. Several distinct routes were tried in turn — a per-step fold along the chain, a fresh re-derivation of the redundancy at each candidate, a re-shaping of the base realization consuming Katoh–Tanigawa’s column operation directly — and each, checked against what that operation actually does, reached the same obstruction: Katoh–Tanigawa’s own column operation (eq. (6.62)) relabels which of the base graph’s rows plays the corner’s redundant-row role as \(i\) advances, rather than fixing one witness row whose membership a single argument keeps certifying; a route asking for one witness row’s membership to survive past the first step therefore has, in the text, nothing to derive it from (commit 591cf306, 2026-06-21, the last of these routes to be refuted this way).

Reshaping the certification itself to Katoh–Tanigawa’s own block form — rather than transporting a membership at all — was sketched in outline that same afternoon (commit 50fb3229, 2026-06-21): certify the rank as a block matrix whose corner is \(M_i\) and whose bottom is the base rows with the one redundant row removed, holding \(r\) fixed only as an equation between two vectors in \({\mathbb {R}}^D\), never as a transported membership. Confirming that this was the only escape took three more days: Phase 23c, opened that same afternoon, spent them checking whether the existing certification could instead be fed the needed fact some other way — a different base block, a different re-derivation of the redundancy — and found every such feed reduced to the identical obstruction. It closed at what the design notes call the member-mapping-wall STOP (commit 4efcabf5, 2026-06-24): the wall was confirmed intrinsic to Katoh–Tanigawa’s own row bookkeeping, not an artifact of one Lean encoding, and the block-form reshape was confirmed the only route around it.

Turning that reshape into a literal Lean certificate took two more false starts once building resumed. A bottom block built from the split-off graph with the reduced vertex removed failed, because that graph’s rows are not literally contained in the candidate’s own rigidity-row span (the candidate graph lacks the corresponding edge); and a construction following the project’s column operation directly failed for the same underlying reason approached from the other side, zeroing the wrong block and stranding the fill row the bottom needs in the block the certificate discards. Both were, on inspection, one obstruction restated: a certificate whose corner and bottom occupy disjoint row blocks of the candidate graph’s own edges cannot express Katoh–Tanigawa’s argument, which shares one row’s data between the corner’s \(\pm r\) entry and the bottom’s redundant-row fill. The shape that dodges it — zero in the other corner, so a single row operation on the corner side, not the bottom, produces the needed block-triangular form — was found and landed axiom-clean, closing Phase 23e (commits a02b8c58 and f4c7ae57, both 2026-06-26):

This is a genuine mis-factoring: the transported-membership certificate was a locally sound internal decomposition of the same rank count Katoh–Tanigawa’s own certificate proves, and it was replaced — without changing the target rank or reopening any already-certified step — by a decomposition matching the source’s own block structure. The formal proof later made these counts with spans of rows rather than with matrices, and a cleanup round deleted the matrix certificate in October 2026, when nothing used it any longer.

The eq.-(6.12) \(+(D-1)\) vs \(+D\) shortfall

Katoh–Tanigawa’s Lemma 6.8 (KT §6.3, eq. (6.12)) realizes a \(k\)-reducible degree-two vertex \(v\) by a degenerate placement: with \((G_v^{ab}, q)\) the inductive realization, \(v\)’s hinge to \(b\) is placed at the very hinge \(q(ab)\) the split-off edge already occupies. Column operations then exhibit \(R(G_v^{ab}, q)\) as a submatrix of \(R(G, p_1)\), with the \(vb\)-row reproducing \(R(G_v^{ab}, q)\)’s \(ab\)-row, so the rank adds: \((D-1)\) new rows plus whatever rank \(R(G_v^{ab}, q)\) already has.

The project’s degree-two split producer (Phase 21b, planned under the name “Case II”) took this construction as its route to the full rank \(D(|V|-1)\) the theorem’s \(k=0\) split needs. Several re-plans circled the one row the construction seemed to be missing without first checking whether eq. (6.12) reaches the target at all; two, both on 2026-06-04, are representative. The first was a row-side attempt to extract that row directly from \(G_v^{ab}\)’s own old block, avoiding the split edge (commit 524e741c), found geometrically impossible (\(G - v\) is not itself rigid, so no such row exists to extract). The second was a motion-side reframing, pinning the missing freedom directly rather than adding a row (commit 7d205752), which assumed a motion of \(G\) constant off \(v\) — not something a rigid \(G\) actually forces, since \(G - v\) need not itself be rigid.

A math-first pass against Katoh–Tanigawa’s own text, rather than against either re-plan’s declarations, found the target unreachable by eq. (6.12) alone at \(k=0\) regardless of which row is added: by KT Lemma 4.8(i), \(G_v^{ab}\) is minimal \(0\)-dof at this split, so \(R(G_v^{ab}, q)\) is already full rank, \(D(|V \setminus \{ v\} |-1)\), and eq. (6.12) gives rank at least \((D-1) + D(|V \setminus \{ v\} |-1)\), i.e. \(D(|V|-1) - 1\) — exactly one row short of the \(D(|V|-1)\) target. Katoh–Tanigawa’s own text states the same shortfall directly, illustrated at \(d=3\) (\(D=6\)) in the sketch introducing Lemma 6.10 (KT p. 680): “we only have rank \(R(G,p_1) \ge 6(|V|-1)-1 \dots \) which does not complete the proof.” Lemma 6.8’s \(+(D-1)\) bound suffices only for the \(k {\gt} 0\) split it is stated for; the project’s split is the \(k=0\) case, whose missing row is supplied not by Lemma 6.8 but by the redundant-edge argument of Lemma 6.10/6.13 (§6.4, section A.1) — Case III, not Case II (commit db1bfca5, 2026-06-04, closing Phase 21b and re-scoping the producer to Phases 22–23).

The shortfall was visible in the arithmetic above from the day the producer was scoped, but sat under these re-plans because each reasoned about which named construction could supply the missing row rather than tracing the target count through Katoh–Tanigawa’s own construction by hand; the checks the project runs on a new declaration — name resolution, the audit of a theorem’s hypotheses — read types and hypotheses, not the numeral a rank inequality closes at, so neither re-plan’s declarations tripped anything before the math-first pass traced the count directly.

This is a process failure: the arithmetic gap was real from the day the producer was scoped, and no check running at the time — type-correctness, hypothesis-honesty — was positioned to read it; only tracing the target quantity through the source construction by hand could.

A.5 Process/tracking failures

The two episodes below are process failures in the introduction’s sense: each is a call that was reasonable given what was read at the time, but left no artifact for a later check to find, or read a signal that looked decisive and was not.

The Case-I dispatch’s untracked Lemma-6.5 arm

Katoh–Tanigawa’s Case I (KT §6.2, pp. 673, 676–677) trifurcates on the simplicity of the contraction \(G/E(H)\) of a proper rigid subgraph \(H\): Lemma 6.2 handles a non-simple \(G\) directly; Lemma 6.3 handles a simple \(G\) with some simple contraction, adding the rigid block’s rank to the contraction’s own inductive rank by KT’s block-triangular structure (eq. (6.3), section A.3); and Lemma 6.5 handles what remains — every contraction non-simple — via Claim 6.6, which extracts a degree-two vertex \(v\) from a maximal proper rigid subgraph and re-attaches it after inducting on the smaller graph \(G - v\).

A design recon opening the Case-I sub-phase read this trifurcation correctly against Katoh–Tanigawa’s text and named the right tracking idiom for its harder leg: carry the Lemma-6.3-versus-6.5 dispatch as an explicit hypothesis rather than build it outright (commit ac958152, 2026-06-04). The composer that landed the next day discharged only the Lemma-6.3 leg, taking the case hypothesis hcSimple — that \(G/E(H)\) is simple — as a fixed input, and recorded the alternative directly in its own doc-comment rather than tracking it: “the hcontract non-simple branch …and full-theorem_55 dispatch are the coordinator’s wiring” (commit c1ef55a0, 2026-06-05). The blueprint flip that landed the same day minted a red node for the one hypothesis the composer’s own signature carried as content — KT Claim 6.4, the surviving block’s generic rank (lemma 23.98) — and none for the Lemma-6.3-versus-6.5 dispatch or the Lemma-6.5 arm (commit 8fa5b02a); the sub-phase’s own close then recorded Claim 6.4 as “the single deferred obligation” (commit 0e10b5ed). Neither the dispatch nor the Lemma-6.5 arm appeared on any forward list from this point.

Both resurfaced five sub-phases later, in the same audit of the realization layer’s hypothesis feeds against the landed Lean that also found the vacuous bare realization predicate (section A.2): tracing what discharges hcontractGP found no Lemma-6.3-versus-6.5 dispatch anywhere in the tree, and the Lemma-6.5 arm genuinely missing rather than merely deferred (commit e4693d61, 2026-06-11). The dispatch itself was formalized that same day as a classical case split on whether some proper rigid subgraph has a simple contraction, with the Lemma-6.5 branch carried forward as a new named hypothesis h65 rather than built (commit 06763ffb). Building Claim 6.6 itself — the vertex-extraction argument the branch needed — took five more days, landing as case_I_realization_h65 (lemma 23.106; its form for every \(d \ge 2\), case_I_realization_h65_gen, later replaced it) and completing the dispatch (lemma 23.107), which now cases on all three of KT’s Lemmas 6.2, 6.3, and 6.5 (commit 0f40c44d, 2026-06-16).

This is a process failure: the recon that opened the sub-phase read Katoh–Tanigawa’s case split correctly and named the idiom for tracking its harder leg, but the commit that built the easier leg described the rest as coordination rather than mathematics instead of using that idiom, and the blueprint flip that followed took the composer’s own carried hypotheses as the complete list of what remained open. A hypothesis with no corresponding node is invisible to any check that reads only \uses edges or a lemma’s hypothesis list against its own dependencies; it surfaced only once a scheduled audit read the Lean’s actual case coverage against Katoh–Tanigawa’s own case split.

The \(d = 3\) Claim-6.12 “dead island” misread

Katoh–Tanigawa’s Claim 6.12 at general dimension (KT §6.4.2, Lemma 6.13) subsumes the \(d = 3\)-specific development described in section A.1: once the general chain dispatch landed, the \(d = 3\)-only entry point case_III_candidate_dispatch kept no caller in the live proof. A cleanup-round audit flagged this the same week the general lift closed: case_III_candidate_dispatch has zero callers, so the chain running through it to case_III_claim612 “may be describing dead code as if live,” and the flag was carried forward, unresolved, as the next round’s first task (commit 582ed642, 2026-07-05).

The cleanup round that inherited the flag opened by reading it as settled fact rather than as the hedge it had been recorded as: its task list stated outright that “the live all-k path routes through chainData_dispatch for every grade incl. \(d=3\), so the island is bypassed,” proposing to retire the whole section. A lean_references reachability pass the same morning found this partly right and partly wrong: exactly three declarations were genuinely dead — the (k:=2) wrapper case_III_claim612 itself, a self-obsolete predecessor, and the abstract row-family cluster of section A.3’s first episode — while the rest of the concrete chain remained reachable from within itself (commit fc5deb3f, 2026-07-07). The two clearly-dead declarations were cut and case_III_claim612’s node was re-pinned to the general case_III_claim612_gen the same morning, still under a plan to demote the whole section as secondary (commit 78404289).

Tracing the actual Lean call chain behind the discriminator node (lemma 23.200) reversed that plan the same afternoon: chainData_fire_discriminator calls exists_shared_redundancy_and_matched_candidate, then exists_chainData_discriminator_pick, then exists_complementIso_ne_zero_of_homogeneousIncidence_gen, which invokes case_III_claim612_gen directly — so the re-pinned node was not dead at all, but the general Claim 6.12 the general chain itself calls. Its zero incoming \uses edges, the signal that had made it look orphaned from the start, was a blueprint wiring gap, not a fact about the Lean (commit fe2f2a73, 2026-07-07); the missing edges, from the discriminator’s proof to lemma 23.191 and lemma 22.16, were added the same day (commit a528e227). Only the concrete \(d = 3\) dispatch itself is genuinely bypassed by the general chain, and it was kept, not cut, as the worked \(d = 3\) case section A.1 grounds.

This is a process failure, in the same audit as the candidate-row episode of section A.3, but with the opposite tell: two signals that each look decisive on their own — a dep-graph node with no incoming \uses edge, a declaration with no grep-visible caller — agreed on a section that was in fact load-bearing, because the caller of a general-purpose declaration is a fact about the Lean call chain, not about either static signal, and a hedge recorded at one audit read as settled fact by the time a later one inherited it.