canonicalPeriodicMixedHingeDeficitExpandedLengthChainExplicitFiberTarget_of_angleChain
plain-language theorem explainer
If the mixed hinge-deficit length-chain identity holds in angle-chain form on the canonical periodic Freudenthal torus, then it holds in the explicit table-fiber form. Gravity and Regge-calculus workers cite this when discharging the physical six-tet Dirichlet obligations. The proof rewrites each fiber summand by the local angle-chain equality and feeds the hypothesis through definitional unfolding.
Claim. Fix lattice sizes $N_x,N_y,N_z\ge 3$. Let $P$ be the canonical encoded periodic Freudenthal torus on that grid. If for every vertex potential $\xi$ and every periodic edge $e$ the mixed hinge-measure directional derivative identity holds with the right-hand side written via local angle-length chain derivatives on the explicit fiber pairs, then the same identity holds with the right-hand side written via the precomputed explicit-fiber expanded summands.
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.
The ambient geometry is the canonical encoded periodic Freudenthal torus $P$ on an $N_x\times N_y\times N_z$ grid with each side at least 3. Vertex potentials $\xi$ live on $P$'s triangulation. For each typed periodic edge one has a precomputed local pair-displacement fiber table; the mixed target equates a hinge-measure directional derivative times a signed sum over that fiber to a length-chain expansion.
Two Prop packages state the same mixed target. The angle-chain form writes each fiber contribution via localAngleLengthChainDeriv (the Schläfli-based angle derivative from the local edge-length chain rule). The explicit-fiber form writes the same contributions via the expanded summand table. The dimensionless bridge ratio $K=\varphi^{1/2}$ appears only as part of the triangulation data carried by $P$.
proof idea
Fix $P$ as the canonical encoded periodic Freudenthal torus. For arbitrary vertex potential $\xi$ and periodic edge, build a Finset sum congruence: each explicit-fiber expanded summand equals the corresponding local angle-length chain derivative on the selected tet and face, by the sibling lemma freudenthalExplicitFiberPairExpandedSummand_eq_angleChain.
Unfold both target Props and the expanded-summand abbreviation, substitute the sum equality, and apply the angle-chain hypothesis at $(\xi,\mathrm{edge})$. The remaining definitional noise is discharged by simpa.
why it matters
The bridge sits inside the gravity stack that connects the encoded periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet model. Downstream, canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitExplicitFiberAngleChainTargets consumes the explicit-fiber target (together with stationary weighted-deficit data) to obtain local edge-stencil correspondence on the canonical torus.
In the broader Recognition framework this is scaffolding for the continuum Dirichlet/Regge limit on the cubic lattice, not a forcing-chain step (T5–T8). It keeps the mixed hinge-deficit identity available in whichever bookkeeping form later stencil or Hessian arguments prefer, so the physical model can be instantiated without re-proving the length-chain expansion at each call site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.