canonicalPeriodicMixedHingeDeficitExpandedLengthChainExplicitFiberAngleChainTarget_of_explicit
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the explicit-fiber mixed hinge-deficit target written with precomputed expanded summands implies the same target written with local angle–length chain derivatives. Anyone wiring the physical six-tet cubic Dirichlet model from the expanded fiber table would cite this bridge. The proof rewrites the fiber sum termwise by the expanded-summand/angle-chain identity and discharges via the hypothesis.
Claim. Let $N_x,N_y,N_z\in\mathbb{N}$ with each period strictly larger than $2$. If the mixed hinge-deficit expanded length-chain target holds in explicit-fiber form (for every vertex potential $\xi$ and periodic edge, the hinge-measure directional derivative times the negated sum of precomputed expanded fiber summands over the Freudenthal local pair-displacement table), then it holds in angle-chain form, where each fiber contribution is the local angle–length chain derivative on the selected tetrahedron face of the canonical encoded periodic Freudenthal torus.
background
This module packages the exact 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 the model target.
The ambient geometry is the canonical encoded periodic Freudenthal torus on periods $N_x,N_y,N_z>2$. The mixed target equates a hinge-measure directional derivative along a periodic edge to a negated fiber sum over the precomputed Freudenthal local pair-displacement table for that edge's displacement. Two presentations of the fiber summands appear: an expanded explicit-fiber form, and an angle-chain form built from localAngleLengthChainDeriv.
That local angle–length chain derivative is the first-variation object predicted by the local edge-length chain rule and closed Schläfli derivative data: a sum over the six edge slots of dihedral derivatives times local edge-length directional derivatives. The dimensionless bridge ratio $K=\varphi^{1/2}$ enters the triangulation data of the torus.
proof idea
Fix the canonical encoded periodic Freudenthal torus $P$ on the given periods. For arbitrary vertex potential $\xi$ and periodic edge, form the fiber sum of local angle–length chain derivatives over the Freudenthal local pair-displacement table. By Finset.sum_congr and the pointwise identity that each expanded fiber summand equals the corresponding angle-chain derivative (applied in the reverse direction), that sum equals the expanded-summand fiber sum. Unfolding both target predicates and simplifying then reduces the angle-chain target at $(\xi,\mathrm{edge})$ to the explicit-fiber hypothesis at the same point.
why it matters
In the gravity domain this is a presentation bridge inside the physical six-tet cubic Dirichlet instance: it lets the mixed hinge-deficit expanded length-chain obligation be stated with Schläfli/angle-chain first-variation data once the expanded explicit-fiber form is known. The module's role is to package theorem obligations for the physical model on the periodic Freudenthal torus rather than to close the free Dirichlet equality.
No downstream consumers are recorded yet, so the lemma is presently a leaf in the dependency graph. It sits with the sibling packaging results that certify Hessian/Dirichlet structure, periodic edge stencils, and related finite-difference Dirichlet targets on the same torus. Within Recognition Science gravity, such bridges keep the Regge-style first variation (hinge deficits, length chains) aligned with the encoded periodic geometry used for continuum limits on the cubic lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.