FreudenthalAxisDisp0ExplicitFiberClosedFormAllBilinearTarget_false
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal witness with endpoint-unit data, the universal claim that every displacement class obeys the explicit-fiber closed-form bilinear identity is false. Lattice-gravity and Regge-calculus workers cite this as a concrete counterexample blocking a naive all-class bilinear reduction of the mixed hinge deficit. The proof is a one-line specialization of the already-proved failure at axis class 0.
Claim. For lattice sizes $N_x=N_y=N_z=5$ (with $2<N_i$), it is not true that every displacement class $d\in\{0,\ldots,6\}$ satisfies the explicit-fiber closed-form bilinear identity for the canonical periodic mixed hinge deficit.
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; it records which closed-form identities hold or fail on concrete witnesses.
The all-class target asserts that, for every displacement index $d\in\mathrm{Fin},7$, the mixed hinge deficit on the canonical periodic scaffold obeys an explicit-fiber bilinear closed form. The witness lattice is the $5\times5\times5$ torus with the standard size bounds $2<N_i$, and the potential/edge data are the endpoint-unit configuration used throughout the axis-class counterexamples.
Upstream, the per-class statement already fails at axis class $0$: the global fiber sum equals $-4$, which forces the left-hand side of the identity to be $4$ while the right-hand side is $0$. The all-class target is simply the universal quantification of those per-class statements.
proof idea
One-line wrapper by specialization. Assume the all-class bilinear target. Instantiate the universal quantifier at displacement class $0$ to obtain the per-class identity at axis class $0$. That per-class claim is already refuted by FreudenthalAxisDisp0ExplicitFiberClosedFormPerDispTarget_zero_false on the same endpoint-unit witness, yielding the contradiction.
why it matters
Inside the gravity stack this is a negative certificate: the explicit-fiber bilinear closed form does not hold uniformly across all seven displacement classes on the standard $5\times5\times5$ endpoint-unit witness. The module's job is to connect the periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model; this theorem records that one attractive closed-form route (all-class bilinearity of the mixed hinge deficit) is blocked on the axis-class-0 fiber.
No downstream consumer is wired yet (used_by is empty). The result still matters for anyone assembling the Dirichlet instance: it forces either a restricted class set, a different potential/edge witness, or a non-bilinear closed form. It sits beside the positive fiber-sum facts that produce the numerical mismatch (LHS $4$ vs RHS $0$) and keeps the scaffolding honest about which identities survive on the Freudenthal lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.