FreudenthalExplicitFiberBilinearEndpointTemplateTarget
plain-language theorem explainer
Packages, for each of the seven positive cube displacements, the obligation that the explicit closed-form fiber sum on a periodic Freudenthal torus factors through a bilinear endpoint template F(ξ₀,ξ₁). Gravity workers cite it when reducing hinge-deficit or endpoint-dependence targets to a two-argument polynomial identity. The body is a pure existential Prop: existence of F obeying the length-chain template and matching the fiber sum on every edge of that displacement class.
Claim. For lattice sizes $N_x,N_y,N_z>2$ and displacement class $d\in\{0,\ldots,6\}$, the following holds: there exists $F:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ such that (i) $F$ satisfies the local length-chain endpoint template at $d$, and (ii) for every conformal vertex potential $\xi$ on the canonical encoded periodic Freudenthal torus and every positive-displacement periodic edge $e$ with $\mathrm{disp}(e)=d$, the explicit closed-form fiber sum along $e$ equals $F(\xi(v_0),\xi(v_1))$, where $v_0,v_1$ are the endpoints of $e$.
background
The module packages 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.
A periodic edge is a base vertex plus one of seven positive cube displacements. Vertex potentials are real assignments on the finite vertex set of a 3D triangulation; here the triangulation is the canonical encoded periodic Freudenthal torus of sizes $N_x,N_y,N_z>2$. The fiber sum is the explicit closed-form contribution along such an edge for a fixed displacement class.
The companion local template forces any admissible $F$ to vanish on the diagonal: $F(1,1)=0$. That identity is already proved for the length-chain endpoint template and is the source of the documented obstruction when the fiber sum on endpoint-unit potentials is nonzero.
proof idea
Definitional packaging only: the Prop is the existential statement that some $F:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ simultaneously satisfies the local displacement length-chain endpoint template at $d$ and reproduces the explicit closed-form fiber sum on every periodic edge of displacement $d$, evaluated at the two endpoint potentials via the canonical vertex finite equivalence. No tactics or lemmas are invoked in the body.
why it matters
This is the bilinear-endpoint gate for the physical six-tet cubic Dirichlet instance. Downstream, assuming it yields endpoint dependence of the explicit fiber sum and the per-displacement mixed hinge-deficit closed-form target. Equally important, the module already proves the target is false at displacement class $0$ (unconditionally on the witness lattice, and from a certified endpoint-unit fiber sum of $-4$), matching the doc-comment blockage: the template forces $F(1,1)=0$ while audits report a nonzero diagonal fiber sum for classes $0$ and $3$.
In the broader gravity chain this sits between the encoded periodic Freudenthal scaffold and Regge/Dirichlet correspondence on the cubic lattice. Discharge paths named in the comment are interior-vertex cancellation or abandoning the identification fiberSum $= F(\xi_0,\xi_1)$. It does not itself touch T0–T8 or the RCL; it is a discrete geometric obligation inside the Dirichlet model assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.