Track1MixedLengthAuditObstructionEndpoint
plain-language theorem explainer
Records the scalar obstruction that the old mixed length-chain edge-stencil right-hand side fails to match the exact finite N=5 single-vertex audit: twelve is not equal to six plus six root-two plus two root-three. Gravity Track 1.B and Track 7 handoff authors cite it as the Session 202 audit endpoint. The declaration is a bare Prop alias; the companion theorem discharges it by a named scalar-mismatch lemma.
Claim. The real number $12$ is not equal to $6 + 6\sqrt{2} + 2\sqrt{3}$. In context this asserts that the old mixed length-chain edge-stencil RHS is scalar-inconsistent with the exact finite $N=5$ single-vertex audit, so that target is retired in favor of the corrected axis-stencil mixed hinge-deficit target at $N=5$.
background
The ambient module is the Gravity Track 7 fork-handoff integration lane. It does not upgrade the discovery claim; it receipts parallel fork endpoints (Track 1.B stationarity reduction at $N=5$, physical residual/Bianchi, many-body amplitude-linear lift, Page-capacity transfer, dark-energy $w(z)$ band, and Track 6 falsifier packaging) and leaves open Track 1 displacement-class leaves as the next dependency.
Track 1.B works with discrete hinge-deficit and edge-stencil identities on a finite vertex audit (here $N=5$). A mixed length-chain stencil previously supplied a closed-form RHS built from integer and radical terms. Session 202 compares that RHS, after scalar reduction, against the exact single-vertex audit value $12$ and finds a mismatch.
The replacement target named in the doc-comment is the canonical periodic mixed hinge-deficit axis-stencil target at $N=5$, which later Session 204 material derives from a global explicit-fiber axis-stencil identity.
proof idea
This declaration is a definitional Prop alias, not a proved theorem: it is literally the inequality $12 \neq 6 + 6\sqrt{2} + 2\sqrt{3}$. No tactics run here.
The companion theorem track1_mixed_length_audit_obstruction_endpoint_holds is a one-line wrapper that applies the upstream scalar-mismatch fact canonicalPeriodicMixedLengthSingleVertexAudit_scalar_mismatch to inhabit this Prop. Downstream certificates only need the Prop name as a typed endpoint token.
why it matters
Inside Recognition Science gravity, Track 1.B is the stationarity-reduction fork feeding the structural master theorem. Documenting that the old mixed length-chain RHS is scalar-inconsistent prevents silent reuse of a wrong stencil constant in the $N=5$ audit and forces the corrected axis-stencil target.
The Prop is consumed by track1_mixed_length_audit_obstruction_endpoint_holds and sits in the same handoff family as the Schläfli and displacement-class reduction endpoints that ForkHandoffIntegrationCert packages. That certificate explicitly treats Track 1 as a reduction/interface package, not a closure of the open Schläfli leaves.
No T0–T8 forcing step is discharged here; the landmark contact is local discrete gravity bookkeeping (finite vertex audit, hinge deficit, axis stencil) on the path toward the master gravity theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.