canonicalPeriodicMixedHingeDeficitExpandedLengthChainExplicitFiberTarget_iff_flatUnfolded
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the mixed hinge-deficit target written with the expanded length-chain fiber table is equivalent to the same target with each fiber summand fully flat-unfolded. Anyone equating the two bookkeeping forms of the six-tet cubic Dirichlet instance will cite this. The proof is the pair of already-proved one-direction implications packaged as an Iff.
Claim. For natural periods $N_x,N_y,N_z$ each at least $3$, the following are equivalent: (i) the mixed hinge-deficit identity on the canonical encoded periodic Freudenthal torus, with the fiber sum taken from the precomputed local pair-displacement table and expanded length-chain summands; (ii) the same identity with every fiber entry replaced by its flat-unfolded explicit summand.
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.
The left-hand target is the explicit table-fiber form of the mixed hinge-deficit identity: for every vertex potential $\xi$ and every periodic edge, the hinge-measure directional derivative times a signed sum over the precomputed freudenthalLocalPairDispFiber table equals a geometric factor built from the edge displacement. The right-hand target is the flat-unfolded variant of the same identity, in which each fiber entry is the fully expanded summand freudenthalExplicitFiberPairFlatExpandedSummand rather than a length-chain intermediate.
Both statements live on the canonical encoded periodic Freudenthal torus for periods $N_x,N_y,N_z>2$. The two one-way implications between them are already available in-module; this declaration only records their logical equivalence.
proof idea
Term-mode Iff constructor. The forward direction is the existing theorem that the expanded length-chain explicit-fiber target follows from the flat-unfolded target; the reverse direction is the existing theorem that the flat-unfolded target follows from the expanded length-chain explicit-fiber target. Both are applied at the same periods and size hypotheses, with no further rewriting.
why it matters
In the gravity stack this sits inside the physical six-tet cubic Dirichlet instance, which bridges the encoded periodic Freudenthal torus scaffold to the physical model target. Equating the expanded length-chain fiber bookkeeping with the fully flat-unfolded fiber bookkeeping lets later arguments switch presentation without re-proving the mixed hinge-deficit identity.
No downstream consumers are recorded yet; the declaration is a local closure step among the mixed-target variants rather than a leaf of the forcing chain. It does not itself touch T5–T8, the Recognition Composition Law, or the continuum Dirichlet limit; those enter only once the packaged obligations are discharged into the physical model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.