canonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormTarget_of_flatUnfolded
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the mixed hinge-deficit identity with closed-form explicit-fiber summands follows from the same identity written with flat-unfolded summands. Anyone packaging the physical six-tet cubic Dirichlet model on the encoded torus cites this bridge. The proof is a Finset sum congruence plus the entrywise equality of the two expanded summands, then a simp rewrite of the target propositions.
Claim. Let $N_x,N_y,N_z\ge 1$ with $N_x,N_y,N_z>2$. If for every vertex potential $\xi$ and every periodic edge the mixed hinge identity holds when the explicit-fiber sum uses the flat-unfolded expanded summands, then the same identity holds when that sum uses the closed-form expanded summands instead.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus; it does not freely assert the physical Dirichlet equality.
The ambient geometry is the canonical encoded periodic Freudenthal torus $P$ built from periods $N_x,N_y,N_z>2$. Two Prop-targets compare the same mixed hinge identity: the directional hinge measure times a negated sum over the local displacement fiber equals a square-root edge-length factor. They differ only in which expanded summand fills the fiber: the flat-unfolded form versus the closed-form form.
Upstream, each local pair has a closed-form expanded summand and a flat-unfolded expanded summand, already proved equal entrywise by freudenthalExplicitFiberPairClosedFormExpandedSummand_eq_flat. The local fiber is the finite set of Freudenthal local pairs attached to the edge displacement.
proof idea
Fix the canonical encoded torus $P$. Introduce a potential $\xi$ and a periodic edge. Build a Finset sum congruence: the sum of flat-unfolded expanded summands over the local pair fiber equals the sum of closed-form expanded summands, by applying the entrywise equality lemma (in the reverse direction) at each pair. Then simpa rewrites both target Props and the sum equality into the flat-unfolded hypothesis applied at $\xi$ and the edge.
why it matters
The closed-form explicit-fiber mixed target is the form one wants when the fiber contribution is written in closed algebraic terms rather than a flat expansion. This lemma discharges that target from the flat-unfolded sibling, so later packaging of the physical six-tet cubic Dirichlet instance can choose whichever summand presentation is convenient and still land on the closed-form obligation.
In the broader gravity stack this sits inside the Regge/Freudenthal cubic-lattice limit path: hinge deficits on the periodic torus must match Dirichlet-type finite-difference actions. No downstream consumers are recorded yet (used_by is empty), so the lemma is presently a local bridge inside the instance module rather than a cited parent theorem. It does not itself close the physical Dirichlet equality; it only transfers one fiber presentation to another under the already-proved summand identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.