FreudenthalLocalThreeLengthChainEndpointTemplateTarget
plain-language theorem explainer
Packages the three distinct local Freudenthal length-chain endpoint identities (slots 0, 3, and 6) that underlie the seven positive displacement classes on the cubic lattice. Gravity and discrete-geometry workers cite it when wiring angle-template data into the physical six-tet Dirichlet model. It is a pure conjunction of three endpoint-template predicates on a seven-slot family of real bivariate maps.
Claim. For a family $F:\{0,\ldots,6\}\to(\mathbb{R}\times\mathbb{R}\to\mathbb{R})$, the three-length-chain endpoint template target holds when the local displacement length-chain endpoint template identity is satisfied at slots $0$, $3$, and $6$ for the maps $F(0)$, $F(3)$, and $F(6)$ respectively.
background
This module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not assert the physical Dirichlet equality for free; it packages the exact theorem obligations needed to instantiate that model on a periodic Freudenthal torus.
In Regge calculus the hinge deficit is $2\pi-\sum\theta$ (dihedral-angle and Schläfli forms). Local displacement classes on the cubic lattice organize edge-length and angle data into seven positive classes; only three of those classes are geometrically distinct as length-chain endpoint identities. The family $F$ assigns to each of the seven slots a bivariate real map used as a local angle or length template.
Upstream scaffolding includes the hinge-aware zero-mode analysis for periodic Regge geometry and the cubic Taylor bound on the Regge action. Those supply the geometric language in which the three endpoint identities are stated.
proof idea
Definitional abbreviation only: the predicate is the conjunction of three applications of the local displacement length-chain endpoint template target, at indices $0$, $3$, and $6$, each fed the corresponding component of $F$. No tactics, no lemmas applied.
why it matters
Inside the gravity domain this definition isolates the three independent local length-chain endpoint identities that the seven positive displacement classes reduce to. The module’s job is to turn the periodic Freudenthal torus into a concrete instance of the physical six-tet cubic Dirichlet model; this Prop is one of the packaged obligations on the angle-template side.
It sits downstream of deficit geometry (hinge deficit $2\pi-\sum\theta$) and the Regge cubic Taylor bound, and alongside sibling Dirichlet and periodic edge-stencil targets. No downstream consumers are recorded yet, so it is presently a named interface rather than a proved link in the forcing chain. Framework-wise it supports the discrete $D=3$ cubic lattice setting in which the eight-tick and spatial-dimension landmarks are realized geometrically, without itself claiming continuum Einstein equations or a closed Dirichlet equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.