canonicalPeriodicMixedHingeDeficitExpandedLengthChainLocalPairFiberTarget_of_explicitFiber
plain-language theorem explainer
On a periodic cubic lattice with periods larger than 2, the mixed hinge-deficit expanded length-chain target written over the filtered Freudenthal local-pair fiber is equivalent to the same target written against the precomputed displacement fiber table. Anyone assembling the physical six-tet Dirichlet instance from explicit fiber data cites this bridge. The proof is a one-line rewrite by the fiber-equals-filter identity, then direct application of the explicit hypothesis.
Claim. Fix periods $N_x,N_y,N_z\ge 3$. If the mixed hinge-deficit expanded length-chain identity holds for every vertex potential $\xi$ and every periodic edge when the local-pair sum runs over the precomputed Freudenthal displacement fiber of that edge, then the same identity holds when the sum is instead taken over the filtered set of all Freudenthal local pairs whose displacement equals the edge displacement.
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 assert the physical Dirichlet equality for free; it only arranges the geometric and combinatorial hypotheses that the model demands.
The ambient geometry is the canonical encoded periodic Freudenthal torus on periods $N_x,N_y,N_z$ (each at least 3). Edges are typed periodic edges; each carries a displacement. Freudenthal local pairs are the combinatorial pairs that appear in the one-cube Freudenthal triangulation; their displacements can be collected either by filtering the universe of pairs or by looking up a precomputed fiber table freudenthalLocalPairDispFiber.
The two target propositions compared here both assert a mixed identity: the hinge-measure directional derivative of a vertex potential along an edge, times a signed sum of expanded length-chain contributions over local pairs at that edge's displacement, matches the required deficit form. They differ only in how that local-pair sum is indexed (filter versus explicit fiber table).
proof idea
Bind the canonical encoded periodic Freudenthal torus for the given periods. Introduce an arbitrary vertex potential and periodic edge. Rewrite the filtered local-pair sum by the identity that the precomputed displacement fiber equals the filter of all Freudenthal local pairs at that displacement. The goal is then literally the explicit-fiber hypothesis, which is applied directly.
No analytic estimate or lattice-limit argument appears; the step is pure reindexing of a finite sum.
why it matters
The physical six-tet cubic Dirichlet instance needs a local-correspondence endpoint stated over the mixed hinge-deficit expanded length-chain target. Downstream, canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitExplicitFiberTargets consumes the explicit-fiber form of that target and produces the canonical edge-stencil local correspondence. This lemma converts an explicit-fiber certificate into the filtered local-pair fiber form that intermediate packaging uses, so the two presentations of the same combinatorial content stay interchangeable.
In the broader gravity stack this sits inside the Regge cubic-lattice limit path: Freudenthal triangulation of the periodic torus, hinge-aware deficit measures, and finite-difference Dirichlet action. It does not itself force $D=3$ or the eight-tick octave; those enter earlier in the forcing chain. It only keeps the discrete geometric bookkeeping coherent so the physical Dirichlet model can be instantiated without double-counting or missing local pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.