CanonicalPeriodicMixedHingeDeficitExpandedLengthChainLocalPairFiberTarget
plain-language theorem explainer
Defines the mixed hinge-deficit / length-chain target on the canonical periodic Freudenthal torus, rewritten as a sum over the explicit displacement fiber of local (tet, edge-slot) pairs. Gravity and Regge-lattice workers cite it when discharging the physical six-tet cubic Dirichlet model. The body is a pure Prop packaging: no proof, only the filtered local-pair equality that later theorems discharge.
Claim. For lattice sizes $N_x,N_y,N_z\ge 3$, the following holds: for every vertex potential $\xi$ and every periodic edge $e$ on the canonical encoded periodic Freudenthal torus, the product of the hinge-measure directional derivative along $e$ with the negative sum, over local Freudenthal pairs whose displacement matches $e$'s displacement, of the Schläfli dihedral derivatives times local edge-length directional derivatives, equals $\sqrt{|\mathrm{disp}(e)|^2}\,(\xi(v_1)-\xi(v_2))^2$.
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.
The ambient geometry is the canonical encoded periodic Freudenthal torus $P$ of sizes $N_x,N_y,N_z\ge 3$. Edges are typed periodic edges; each carries a base cell and a displacement. A Freudenthal local pair is a finite table entry $(\mathrm{tet},\mathrm{edge\text{-}slot})\in\mathrm{Fin},6\times\mathrm{Fin},6$ left after the periodic-cell base-offset equation is isolated. The sibling target (local-pair form without the fiber rewrite) collapses the periodic cell sum to the unique cell solving that base-offset equation for each local pair.
The left-hand side multiplies the hinge-measure directional derivative of $\xi$ along the edge by a filtered sum of Schläfli dihedral derivatives times local edge-length directional derivatives. The right-hand side is the squared potential jump across the edge endpoints, scaled by the Euclidean length of the edge displacement. The dimensionless bridge ratio $K=\varphi^{1/2}$ appears as the curvature scale on $P$.
proof idea
Definition only: the body is a let-bound Prop, not a proved theorem. It fixes $P$ as the canonical encoded periodic Freudenthal torus, then asserts a universal equality over vertex potentials and periodic edges. For each edge it pulls back via the edge equivalence, filters FreudenthalLocalPair by matching displacement, rebuilds the matching base cell from cubeEdgeBase and localEdgeOf, and sums the six tetrahedral Schläfli dihedral derivatives against local edge-length directional derivatives. No tactics or lemmas are applied at this declaration.
why it matters
This is the explicit displacement-fiber packaging of the mixed hinge-deficit / expanded length-chain target used to connect the encoded periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet model. Downstream, canonicalPeriodicMixedHingeDeficitExpandedLengthChainLocalPairTarget_of_fiber lifts a proof of this fiber form to the non-fiber local-pair target; canonicalPeriodicMixedHingeDeficitExpandedLengthChainLocalPairFiberTarget_of_explicitFiber discharges it from the fully explicit fiber table; and canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitLocalPairFiberTargets uses it as the mixed-target hypothesis in the canonical local-correspondence endpoint. In the broader RS gravity stack it sits on the path from discrete Regge/Freudenthal geometry toward the continuum Dirichlet (finite-difference) action, without yet claiming the physical equality itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.