FreudenthalAxisDisp0ExpandedLengthChainTypedEndpointTarget_false
plain-language theorem explainer
On the canonical 5×5×5 periodic Freudenthal torus with the axis-displacement-0 unit witness, the typed-endpoint expanded mixed hinge-deficit length-chain identity fails. Lattice-gravity and Regge-calculus workers cite this as the finite-N typed-endpoint obstruction for Track 1.B. The proof is a one-step reduction: typed endpoint implies the explicit-fiber target, already known false at this witness.
Claim. For the canonical encoded periodic Freudenthal torus with periods $N_x = N_y = N_z = 5$ (and the standard witnesses $2 < N_i$), the typed-endpoint form of the expanded mixed hinge-deficit length-chain target does not hold: it is not true that for every vertex potential $\xi$ and every periodic edge the hinge directional derivative times the signed tet sum equals the expanded length-chain expression built from typed edge displacements and endpoints.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus; it does not grant the physical Dirichlet equality for free.
The proposition under negation is the typed-endpoint expanded mixed target: its right-hand side is written directly from typed periodic edge displacements and endpoints on the canonical encoded torus $P$. The witness used here is the axis-displacement-0 unit configuration at $N=5$ in each direction, with the trivial inequalities $2 < 5$ discharged by decide.
Upstream, the same witness already falsifies the explicit-fiber form of the expanded length-chain target. A conversion lemma states that any proof of the typed-endpoint target yields a proof of that explicit-fiber target, so the typed form is strictly stronger and inherits the obstruction.
proof idea
Term-mode reductio. Assume the typed-endpoint target at the $N=5$ axis-disp-0 witness. Apply the conversion lemma that turns a typed-endpoint proof into an explicit-fiber proof at the same $(N_x,N_y,N_z)$ and hinge witnesses. The resulting explicit-fiber assertion contradicts the already-proved falsehood of the explicit-fiber expanded length-chain target at this witness. Discharge.
why it matters
This is the typed-endpoint half of the finite-$N=5$ obstruction package. Downstream it is quoted verbatim to discharge the Track 1.B finite-lane typed-endpoint obstruction certificate, whose doc-comment stresses that the certificate "does not close Track 1.B" but records that flat finite Freudenthal reindexing and the $N=5$ typed-endpoint target fail. It also feeds the local edge-stencil correspondence negation at the same witness: if the typed target held, local correspondence would follow, so the obstruction blocks that route.
In the broader gravity stack this sits inside the periodic Freudenthal / Regge cubic-lattice limit path toward a physical Dirichlet instance. It is a concrete negative certificate at a fixed finite lattice, not a continuum or forcing-chain (T0–T8) statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.