freudenthalExplicitFiberExpandedDispFiberSum_eq_closedFormFiberSum
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the fiber sum of expanded pair summands over the local displacement fiber equals the closed-form fiber sum for that positive edge class. Gravity and discrete-Regge workers cite it when collapsing explicit pair expansions to the closed fiber formula. The proof is a two-step equality transit through the flat expanded summands.
Claim. Let $N_x,N_y,N_z>2$ and let $\xi$ be a vertex conformal potential on the canonical encoded periodic Freudenthal torus of those periods. For any positive-displacement periodic edge $e$ with displacement class $d$, the sum of the expanded pair summands of $\xi$ over the local displacement fiber of $d$ equals the closed-form fiber sum of $\xi$ for $e$ at $d$.
background
This module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not freely assert the physical Dirichlet equality; it supplies the algebraic identities needed to hit that target.
A periodic edge is a base vertex together with one of seven positive cube displacements. Vertex potentials are real assignments on the triangulation vertices of the canonical encoded torus. The closed-form fiber sum is the packaged scalar for one positive displacement class; the expanded pair summands are the termwise contributions before that packaging.
Upstream, the flat-dispersion fiber sum is already known to match the closed form, and each expanded pair summand matches its flat counterpart. The dimensionless bridge ratio $K=\varphi^{1/2}$ appears only as lattice bookkeeping on the encoded torus, not as a dynamical input here.
proof idea
Term-mode Eq.trans of two equalities. First, Finset.sum_congr rewrites every summand by the pointwise identity that the expanded pair summand equals the flat expanded summand (applied in the reverse direction). Second, the already-proved flat-dispersion fiber-sum identity replaces the summed flat summands by the closed-form fiber sum. No new arithmetic is performed; the expanded sum is routed through the flat intermediate.
why it matters
The identity is a bookkeeping step inside the physical six-tet cubic Dirichlet instance: it lets the expanded pair presentation of the Freudenthal fiber agree with the closed fiber formula used by the Dirichlet target. That target is the bridge from the encoded periodic Freudenthal torus scaffold to the physical model, feeding the broader Regge cubic-lattice and length-chain endpoint certification path in the gravity stack.
No downstream consumers are recorded yet, so the lemma presently closes an internal obligation rather than a named parent theorem. In the Recognition framework it sits on the discrete-geometry side of the gravity derivation (periodic Freudenthal scaffold, six-tet cubic Dirichlet action), not on the T5–T8 forcing chain or the mass ladder. It removes one expansion mismatch that would otherwise block equating stencil actions to closed fiber sums.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.