FreudenthalAxisDisp0ExplicitFiberClosedFormPerDispTarget_zero_false
plain-language theorem explainer
The per-displacement closed-form explicit-fiber mixed identity fails at axis class d=0 on the N=5 periodic Freudenthal witness. Gravity and Regge-lattice workers cite this to block endpoint-only fiber packaging for axis edges. The proof evaluates the unit-potential axis edge, uses the global fiber-sum audit value −4, and reduces to 4√1=0.
Claim. On the periodic Freudenthal torus with $N_x=N_y=N_z=5$ (and the standard $2<N_i$ witnesses), the per-displacement closed-form explicit-fiber mixed target fails at displacement class $d=0$: there is no identity equating the scaled endpoint-mean times minus the explicit fiber sum to a pure function of the two endpoint potentials alone, for every potential and every edge of class $0$.
background
This module packages the exact obligations needed to instantiate PhysicalSixTetCubicDirichletModel on an encoded periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
The target in question is the per positive-displacement-class closed-form explicit-fiber mixed identity: for fixed $d\in\mathrm{Fin},7$, every vertex potential $\xi$ and every periodic edge of class $d$ should satisfy
$$\sqrt{\ell_d^2}\cdot\frac{\xi(v_0)+\xi(v_1)}{2}\cdot\bigl(-S_{\mathrm{fiber}}(\xi,e,d)\bigr)=F(\xi(v_0),\xi(v_1))$$
for some fixed $F:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$. Here $\ell_d^2=$ periodicDispSqEdge $d$ (so class $0$ has squared length $1$), and $S_{\mathrm{fiber}}$ is the explicit freudenthal fiber sum.
The sibling doc notes that endpoint-only packaging is already blocked for $d\in{0,3}$ by vertex expansion plus the finite audit script: interior coefficients do not vanish, and at $(\xi_0,\xi_1)=(1,1)$ the fiber sum is $-4$ while any pure endpoint template forces $F(1,1)=0$. The axis witness edge is base $(1,0,0)$, disp $0$, endpoints $(1,0,0)$ and $(2,0,0)$.
proof idea
Assume the per-disp target at $d=0$. Instantiate it on the axis-witness unit potential and the axis witness edge (endpoints match by axisWitness_edge_endpoints). Rewrite with the global endpoint-unit fiber-sum fact FreudenthalAxisDisp0GlobalEndpointUnitFiberSumTarget_holds and the unit-potential evaluation lemmas, so both endpoint values are $1$ and the fiber sum is $-4$.
The assumed identity then rearranges to
$$\sqrt{\texttt{periodicDispSqEdge},0}\cdot 4 = \sqrt{\cdots}\cdot(1-1)^2=0.$$
periodicDispSqEdge_sqrt_ne_zero rules out the square-root factor vanishing; mul_eq_zero plus norm_num kills the remaining $4=0$ branch.
why it matters
This is the concrete $d=0$ counterexample that kills endpoint-only closed-form fiber packaging on the physical six-tet cubic Dirichlet instance. Downstream, FreudenthalAxisDisp0ExplicitFiberClosedFormAllBilinearTarget_false lifts the failure to the all-bilinear packaging, and canonicalPeriodicEdgeStencilLocalCorrespondence_not_of_closedFormPerDisp_at_axisWitness uses it to show that local edge-stencil correspondence cannot rest on a per-disp closed-form fiber identity at the axis witness.
In the broader RS gravity stack this sits under the Regge cubic lattice limit and Freudenthal length-chain endpoint certificates: the module connects the periodic Freudenthal torus scaffold to the physical Dirichlet model without pretending the mixed hinge deficit factors through endpoints alone. The failure is forced by the audited fiber sum $-4$ at unit data, matching the Python finite audit cited in the target doc. It does not touch the T0–T8 forcing chain directly; it is a lattice-geometry obstruction inside the gravity instantiation path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.