FreudenthalAxisDisp0ExplicitFiberFlatUnfoldedTarget_false
plain-language theorem explainer
On the N=5 periodic Freudenthal torus, the flat-unfolded explicit-fiber mixed hinge-deficit target fails for the axis displacement class. Gravity auditors cite this to rule out that candidate correspondence before trying closed-form or length-chain variants. The proof specializes the universal quantifier to the unit-endpoint axis edge, reduces the fiber sum to −4, and obtains √1 · 4 = 0, a contradiction.
Claim. For the canonical encoded periodic Freudenthal torus with $N_x = N_y = N_z = 5$ (and the corresponding size hypotheses $2 < N_i$), the flat-unfolded explicit-fiber mixed target fails: it is not true that for every vertex potential $\xi$ and every periodic edge $e$, the product of the hinge-measure directional derivative along $e$ with the negated sum of flat-expanded explicit-fiber pair summands equals $\sqrt{\mathrm{dispSq}(e)}\cdot(\xi(v_1)-\xi(v_0))^2$.
background
This module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
The disputed target asserts a local edgewise identity: hinge-measure directional derivative times a negated fiber sum of flat-expanded pair summands equals $\sqrt{\mathrm{periodicDispSqEdge}(d)},(\Delta\xi)^2$. Squared edge lengths depend only on the positive displacement class; class $0$ has $\mathrm{periodicDispSqEdge}(0)=1$.
The witness data fix $N=5$ and an axis edge of displacement class $0$ with base $(1,0,0)$ and endpoints $(1,0,0)$, $(2,0,0)$. The unit-endpoint potential evaluates to the coordinate $\xi$ values used in the audit scripts. An upstream global sum identity already evaluates the flat fiber sum on this axis witness to $-4$.
proof idea
Assume the target. Specialize to the axis unit-endpoint potential and the axis edge of class $0$. The global endpoint-unit fiber-sum theorem plus the closed-form identification of the flat fiber sum yields fiber sum $=-4$.
Unfold the target definition and rewrite the hinge directional derivative via the canonical encoded-periodic edge formula, the axis endpoint pair, and the unit-potential evaluations. The assumed identity collapses to $\sqrt{\mathrm{periodicDispSqEdge}(0)}\cdot 4=0$ after algebraic rearrangement of the $(1-1)^2$ factor.
Apply zero-divisor elimination: either the square root vanishes or $4=0$. The former contradicts $\mathrm{periodicDispSqEdge}(0)=1$ (sqrt nonzero); the latter is false by norm_num.
why it matters
Negative certificate: the flat-unfolded explicit-fiber candidate is not the correct local correspondence on the physical $N=5$ witness. Downstream results reuse it directly: the closed-form fiber target is likewise false (by reduction through this fact), the expanded length-chain explicit-fiber target is false, and the local stencil correspondence theorem is stated as a non-implication from the flat-unfolded hypothesis at $N=5$.
In the gravity stack this prunes one natural Regge/Freudenthal fiber presentation before the module commits to a working Dirichlet or stencil target. It sits inside the periodic Freudenthal torus scaffold that feeds the physical six-tet cubic Dirichlet model, not in the T0–T8 forcing chain itself, but it is part of making the discrete gravity side match continuum Dirichlet structure on the cubic lattice limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.