FreudenthalLocalDispLengthChainEndpointTemplateTarget
plain-language theorem explainer
Endpoint-template identity for each of the seven positive Freudenthal displacement classes: once the closed-form fiber sum is reduced to a bivariate map F of the two endpoint potentials, it must obey √s_d·(ξ₀+ξ₁)/2·(-F(ξ₀,ξ₁))=√s_d·(ξ₀-ξ₁)². Gravity workers instantiating the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus cite this Prop as the local algebraic obligation. It is a pure definition of that predicate, not a proved equality.
Claim. For each displacement class $d\in\{0,\ldots,6\}$ and map $F:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, the endpoint template asserts that for all endpoint potentials $\xi_0,\xi_1\in\mathbb{R}$, $$\sqrt{s_d}\cdot\frac{\xi_0+\xi_1}{2}\cdot(-F(\xi_0,\xi_1))=\sqrt{s_d}\cdot(\xi_0-\xi_1)^2,$$ where $s_d$ is the squared edge length of class $d$ on the periodic Freudenthal torus.
background
The module packages exact theorem obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It connects the encoded periodic Freudenthal torus scaffold to that target without freely asserting the Dirichlet equality.
Seven positive displacement classes carry squared edge lengths $s_d$ (axis edges $s=1$, face diagonals $s=2$, and so on), supplied by the periodic squared-displacement map. After the encoded closed-form fiber sum of the mixed hinge deficit is identified with a function $F$ of the two endpoint potentials alone, the local length-chain identity must hold class by class: the weighted midpoint times $-F$ equals the squared potential difference, both scaled by $\sqrt{s_d}$.
Upstream length and positivity primitives from the recognition calculus are ambient infrastructure. The template is the algebraic skeleton that later forces concrete point values such as $F(1,1)=0$ and $F(1,0)=-2$.
proof idea
Pure definition of a Prop. The body is the universal quantification over endpoint potentials $\xi_0,\xi_1$ of the displayed identity equating $\sqrt{s_d}\cdot(\xi_0+\xi_1)/2\cdot(-F(\xi_0,\xi_1))$ to $\sqrt{s_d}\cdot(\xi_0-\xi_1)^2$. No tactics, no lemmas: the predicate is the obligation itself.
why it matters
Local algebraic core of the explicit-fiber mixed target on the periodic Freudenthal torus. Downstream, the packaged bilinear endpoint target asserts existence of an $F$ satisfying both this identity and the fiber-sum identification on the canonical encoded torus. The three-class packaging conjoins the template on classes $0,3,6$ (the distinct length representatives among the seven). Evaluation lemmas extract $F(1,1)=0$ and $F(1,0)=-2$ directly from any $F$ meeting the template, and the closed-form-per-disp lifting theorem turns an endpoint-template hypothesis into the full mixed-hinge deficit obligation.
The packaging is currently blocked: the template forces $F(1,1)=0$, while finite audits report a nonzero diagonal fiber sum for classes $0$ and $3$. That tension is the open scaffold question this definition surfaces on the path to the physical Dirichlet model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.