FreudenthalLocalDispLengthChainEndpointTemplateTarget_F_eq_zero_at_one_one
plain-language theorem explainer
Any real bivariate F obeying the length-chain endpoint template for a fixed positive displacement class must vanish at (1,1). Gravity workers wiring the physical six-tet cubic Dirichlet model on the periodic Freudenthal torus cite this when reducing endpoint fiber identities. The proof specializes the template at unit potentials, cancels the nonzero squared-edge factor, and finishes by the real zero-product rule.
Claim. Fix a displacement class $d\in\{0,\ldots,6\}$ and let $s_d>0$ be its squared edge length. If $F:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ satisfies $\sqrt{s_d}\cdot(\xi_0+\xi_1)/2\cdot(-F(\xi_0,\xi_1))=\sqrt{s_d}\cdot(\xi_0-\xi_1)^2$ for all real endpoint potentials $\xi_0,\xi_1$, then $F(1,1)=0$.
background
This module packages the exact theorem 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; it connects the encoded periodic Freudenthal torus scaffold to that target.
For each of the seven positive displacement classes $d$, the squared edge length $s_d$ is a positive constant fixed by the class alone (values $1$, $1$, $1$, $2$, $2$, $\ldots$). The length-chain endpoint template is the per-class identity obtained after the encoded closed-form fiber sum is identified with a function $F$ of the two endpoint potentials only: $\sqrt{s_d}\cdot(\xi_0+\xi_1)/2\cdot(-F(\xi_0,\xi_1))=\sqrt{s_d}\cdot(\xi_0-\xi_1)^2$ for all real $\xi_0,\xi_1$. A sibling fact records $\sqrt{s_d}\neq 0$.
proof idea
Specialize the template at $\xi_0=\xi_1=1$. The right-hand side is zero because $(1-1)^2=0$. After simplification the identity collapses to $\sqrt{s_d}\cdot(-F(1,1))=0$. Split the product by the zero-product rule: either $\sqrt{s_d}=0$ or $-F(1,1)=0$. The first branch contradicts the sibling nonvanishing of $\sqrt{s_d}$; the second yields $F(1,1)=0$ after canceling the sign.
why it matters
Diagonal vanishing is the first algebraic consequence of the endpoint template and is reused inside the same module. It supports the inconsistency of a bilinear endpoint template against a certified endpoint-unit fiber sum equal to $-4$, and it sits in the chain that upgrades uniform affine endpoint coefficients to the explicit-fiber endpoint-dependence target (with $F(\xi_0,\xi_1)=c_0\xi_0+c_1\xi_1$). Those reductions tighten the obligations that close the physical six-tet cubic Dirichlet instance on the periodic Freudenthal torus, feeding the gravity master-theorem structural template (all hypothesis inputs witnessed). In the broader RS gravity program this is discrete Regge-type action matching on the cubic lattice, not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.