canonicalPeriodicMixedHingeDeficitExpandedLengthChainExplicitFiberTarget_of_flatUnfolded
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the flat-unfolded explicit-fiber mixed hinge-deficit target implies the expanded length-chain explicit-fiber target. Anyone discharging the six-tet cubic Dirichlet obligations via the flat form can cite this one-way implication. The proof equates the two fiber sums pointwise by the flat-to-expanded summand identity, then rewrites the target propositions.
Claim. Let $N_x,N_y,N_z\ge 3$. If the flat-unfolded explicit-fiber mixed hinge-deficit target holds on the canonical encoded periodic Freudenthal torus of those periods (fiber sums built from the flat-expanded pair summands), then the expanded length-chain explicit-fiber mixed target holds (same hinge-measure identity, fiber sums built from the ordinary expanded Schläfli/length-chain pair summands).
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 ambient geometry is the canonical encoded periodic Freudenthal torus $P$ of periods $N_x,N_y,N_z$ (each at least 3), with vertex potentials $\xi$ and typed periodic edges.
Two Prop-valued targets compare the same hinge-measure directional derivative against a length factor times a fiber sum over the precomputed local pair-displacement table for the edge. The expanded length-chain target uses the ordinary expanded Schläfli/length-chain summand on each fiber pair. The flat-unfolded target uses the flat-unfolded expanded summand entry by entry. An upstream lemma states that those two summands agree on every local pair.
proof idea
Fix the canonical encoded periodic Freudenthal torus $P$. For arbitrary potential $\xi$ and periodic edge, form the two fiber sums over freudenthalLocalPairDispFiber of the edge displacement. Pointwise equality of the flat-expanded and ordinary expanded summands (the lemma freudenthalExplicitFiberPairFlatExpandedSummand_eq_expanded) plus Finset.sum_congr gives equality of the sums. Unfold both target Props and rewrite the hypothesis through that sum identity.
why it matters
The declaration is one direction of the local equivalence between the expanded length-chain and flat-unfolded explicit-fiber mixed targets; the sibling iff theorem packages both directions. Downstream, the edge-stencil local correspondence theorem consumes the flat-unfolded side of the story when assembling weighted-deficit stationarity into a periodic edge-stencil correspondence on the same torus.
In the broader gravity stack this is bookkeeping inside the six-tet cubic Dirichlet instance: it lets proofs work in the flatter summand presentation and transport the obligation back to the expanded length-chain form required by the physical model packaging. It does not itself close the Dirichlet equality; it only identifies two presentations of the mixed hinge-deficit fiber target on the periodic scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.