FreudenthalExplicitFiberBilinearEndpointTemplateTarget_false_of_endpointUnitSum_neg_four
plain-language theorem explainer
On a periodic Freudenthal torus with grid sizes >2, the bilinear endpoint template at displacement class 0 cannot hold if the closed-form fiber sum on the two-endpoint unit potential equals -4. Anyone auditing the six-tet cubic Dirichlet instance or the blocked bilinear packaging will cite this. The proof builds that unit potential, applies the template identity F(1,1)=0, and obtains 0=-4.
Claim. Let $N_x,N_y,N_z>2$. Fix a periodic edge $e$ with displacement class $0$ and endpoints $(v_0,v_1)$. Let $\xi$ be the vertex potential that is $1$ at the finite indices of $v_0$ and $v_1$ and $0$ elsewhere. If the explicit closed-form fiber sum of $\xi$ on $e$ at class $0$ equals $-4$, and if the bilinear endpoint template target holds at class $0$ (existence of $F$ matching the local length-chain template and equaling the fiber sum on endpoint values), then contradiction.
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 freely assert the physical Dirichlet equality; it records theorem-shaped targets that must be discharged or refuted.
Vertices are points of the periodic cubic grid $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. A periodic edge is a base vertex plus one of seven positive cube displacements. The canonical encoded torus supplies a finite index equivalence vertexFinEquiv so potentials are functions on a Fin type. The explicit closed-form fiber sum evaluates the fiber contribution of a potential along an edge at a fixed displacement class.
The bilinear endpoint template target asserts existence of a bivariate $F$ that satisfies the local displacement length-chain endpoint template and equals the fiber sum whenever the edge has that displacement, with $F$ depending only on the two endpoint potential values. The sibling packaging note records that this target is blocked for the explicit fiber sum: the template forces $F(1,1)=0$, while finite audits give a nonzero diagonal fiber sum on classes $0$ and $3$.
proof idea
Destructure the bilinear target into a witness $F$, the local template hypothesis, and the fiber-matching hypothesis. From the local template, apply FreudenthalLocalDispLengthChainEndpointTemplateTarget_F_eq_zero_at_one_one to obtain $F(1,1)=0$.
Build the endpoint-unit potential $\xi$ that is $1$ exactly at the finite indices of the two given endpoints. Specialize the fiber-matching clause at this $\xi$ and the given edge (displacement $0$). Endpoint projections from the hypothesis rewrite the right-hand side to $F(\xi_{v_0},\xi_{v_1})$. The two pointwise evaluations $\xi_{v_0}=\xi_{v_1}=1$ plus $F(1,1)=0$ yield fiber sum $=0$. The certified sum hypothesis says the same sum is $-4$. linarith closes.
why it matters
This is a concrete inconsistency lemma for displacement class $0$: the bilinear endpoint packaging cannot coexist with a certified endpoint-unit fiber sum of $-4$. Downstream, FreudenthalExplicitFiberBilinearEndpointTemplateTarget_false_at_disp0_of_globalWitness lifts the argument to a global witness grid, turning a global endpoint-unit fiber-sum certificate into a refutation of the bilinear target at class $0$.
In the module's program, that refutation is part of clarifying which template shapes can still serve the physical six-tet cubic Dirichlet instance on the periodic Freudenthal scaffold. The sibling doc already flags the obstruction: template forces $F(1,1)=0$ while the audit diagonal is nonzero on classes $0$ and $3$. This theorem is the local algebraic form of that obstruction under an explicit $-4$ sum hypothesis. It does not by itself settle the full Dirichlet equality; it prunes one blocked packaging route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.