canonicalPeriodicMixedHingeDeficitExpandedLengthChainTypedEndpointTarget_of_explicitFiber
plain-language theorem explainer
On a canonical encoded periodic Freudenthal torus with periods larger than 2, the mixed hinge-deficit expanded length-chain identity in explicit fiber-table form implies the typed endpoint form. Lattice gravity workers use this to pass from precomputed displacement fibers to incidence-based edge-in-tet sums. The proof equates the two expanded sums via a fiber-table lemma, then reapplies the hypothesis.
Claim. Let $N_x,N_y,N_z\in\mathbb{N}$ with each period strictly larger than $2$. If the mixed hinge-deficit expanded length-chain identity holds on the canonical encoded periodic Freudenthal torus when the right-hand side is summed over the precomputed local pair-displacement fiber of each periodic edge, then the same identity holds when that right-hand side is rewritten as a sum over tetrahedra via the typed edge-in-tet incidence map.
background
This module packages the exact obligations needed to instantiate PhysicalSixTetCubicDirichletModel on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free. The ambient complex is the canonical encoded periodic Freudenthal torus $P$ built from periods $N_x,N_y,N_z>2$, with edge and tet equivalences relating typed periodic edges to the underlying triangulation $K$.
Two sibling targets encode the same mixed hinge-deficit expanded length-chain identity. The explicit-fiber form sums over the precomputed table freudenthalLocalPairDispFiber of local tet/edge-slot pairs for the edge's displacement, matching base cells via periodicMatchingBaseCell and cubeEdgeBase. The typed-endpoint form instead sums over all tets $\tau$, using the incidence map edgeInTet (none contributes zero; some $f$ contributes the Schläfli dihedral derivative times the local edge-length directional derivative).
Upstream geometry supplies Freudenthal cube incidence (localEdgeOf, edgeInTet) and the periodic torus encoding. The hinge measure directional derivative multiplies a negated expanded length-chain sum on both sides of the identity.
proof idea
Fix $P$ as the canonical encoded periodic Freudenthal torus and introduce a vertex potential $\xi$ and periodic edge. Let $e$ be the underlying edge via $P$'s edge equivalence.
The main step proves an inner equality: the double sum over the local pair-displacement fiber (with matched base cell and Schläfli dihedral derivatives) equals the typed sum over tets via edgeInTet. First, Finset.sum_congr plus definitional unfolding shows the fiber sum matches the named explicit-fiber expanded summand table. Then freudenthalExplicitFiberDispTableExpandedSum_eq_typedEdgeInTetExpandedIncidentSum rewrites that table sum into the typed incidence form.
Finally simpa unfolds both target predicates and the inner equality, and discharges the goal from the explicit-fiber hypothesis at $(\xi,\mathrm{edge})$.
why it matters
The declaration is a bridge inside the physical six-tet cubic Dirichlet instance: it lets later arguments work with the cleaner typed endpoint formulation while proofs may establish the more computational explicit-fiber form. The module's stated role is to connect the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model by packaging exact theorem obligations rather than asserting the continuum Dirichlet equality outright.
No downstream consumers are recorded yet (used_by is empty), so this is presently a leaf in the dependency graph. It sits in the discrete gravity stack that prepares Regge-style hinge deficits and length-chain expansions on Freudenthal triangulations, the lattice side of the Recognition gravity program. Closing the full physical Dirichlet instantiation still requires the remaining sibling targets (edge-stencil Dirichlet action, Hessian/Dirichlet certificates, and the nonlinear Regge correspondence imports).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.