FreudenthalAxisDisp0ExplicitFiberExpandedLengthChainExplicitFiberTarget_false
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus with the axis-displacement-0 unit endpoint witness, the expanded-length-chain explicit-fiber form of the mixed hinge-deficit target fails. Gravity and discrete-Regge auditors cite it when ruling out that fiber presentation for the axis-0 case. The proof is a one-line reduction: expanded fiber implies flat-unfolded fiber, and the latter is already false.
Claim. For lattice sizes $N_x = N_y = N_z = 5$ (with the standard bounds $2 < N_i$), the proposition $\mathrm{CanonicalPeriodicMixedHingeDeficitExpandedLengthChainExplicitFiberTarget}$ does not hold: it is not true that for every vertex potential $\xi$ and every periodic edge, the hinge directional derivative times the signed sum over the precomputed Freudenthal local pair-displacement fiber equals the expanded length-chain explicit-fiber right-hand side.
background
The module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
The target in question is the explicit table-fiber form of the mixed hinge-deficit identity. It uses the precomputed freudenthalLocalPairDispFiber table for each typed edge's displacement, and asks that hinge measure times a signed fiber sum match an expanded length-chain expression for every potential and edge on the canonical encoded periodic torus.
Witness sizes are fixed at $N_x=N_y=N_z=5$ with decidable proofs $2<5$. An upstream implication shows that any instance of the expanded-length-chain explicit-fiber target yields the corresponding flat-unfolded explicit-fiber target. A sibling theorem already shows that flat-unfolded target is false for this same axis-disp-0 unit endpoint witness.
proof idea
Term-mode contradiction. Assume the expanded-length-chain explicit-fiber target at the axis-disp-0 unit witness. Apply canonicalPeriodicMixedHingeDeficitExplicitFiberFlatUnfoldedTarget_of_expandedLengthChainExplicitFiber to obtain the flat-unfolded explicit-fiber target at the same witness. Feed that into FreudenthalAxisDisp0ExplicitFiberFlatUnfoldedTarget_false, which already negates the flat-unfolded form. Done.
why it matters
This is a negative certificate in the gravity/Regge lattice stack: it closes the expanded-length-chain explicit-fiber presentation for the axis-displacement-0 endpoint unit witness on the 5-cube. Downstream, FreudenthalAxisDisp0ExpandedLengthChainTypedEndpointTarget_false uses it when ruling out the typed-endpoint expanded-length-chain target at the same witness.
In the broader Recognition gravity program the module sits between the encoded periodic Freudenthal torus scaffold and the physical six-tet cubic Dirichlet model. Negative fiber certificates prune which discrete presentations can carry the Dirichlet/Regge correspondence; they do not themselves force $D=3$ or the eight-tick octave, but they keep the lattice side of that correspondence honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.