CanonicalPeriodicTrack1BClosureTarget
plain-language theorem explainer
Packages the two remaining Track 1.B obligations on a periodic Freudenthal torus of size (Nx,Ny,Nz): the second Schläfli identity along lines, and the mixed hinge-deficit length-chain identity. Gravity workers cite it as the single Prop that must hold before the local edge-stencil Regge/J-cost correspondence. It is a pure conjunction definition, not a proved statement.
Claim. For lattice sizes $N_x,N_y,N_z\ge 3$, the Track 1.B closure target is the conjunction of (i) the second Schläfli identity along lines on the canonical encoded periodic Freudenthal torus, and (ii) the mixed hinge-deficit identity written as an explicit finite length-chain sum over incident tetrahedron slots.
background
This module wires the encoded periodic Freudenthal torus scaffold into the physical six-tet cubic Dirichlet model. It does not grant the Dirichlet equality for free; it only packages the exact theorem obligations needed to instantiate that model on a periodic torus.
The first conjunct is the second Schläfli-along-line target specialized to the canonical encoded periodic Freudenthal complex and its hinge data. The second is the length-chain finite-sum form of the mixed hinge-deficit target: it unfolds the local dihedral derivative package into an explicit localAngleLengthChainDeriv sum over incident tetrahedron slots.
Both sit upstream of the concrete local nonlinear Regge/J-cost correspondence, whose quadratic term is the real edge-stencil Dirichlet operator on the same torus.
proof idea
Definitional packaging only: the body is the conjunction of the second Schläfli-along-line target and the mixed hinge-deficit length-chain target at the same $(N_x,N_y,N_z)$ and size hypotheses. No tactics, no lemmas applied.
why it matters
Track 1.B is the remaining analytic bridge from discrete Regge calculus on the six-tet cubic complex to the physical Dirichlet quadratic form. This Prop is the single named gate before the local edge-stencil correspondence that writes the quadratic term as the periodic edge-stencil Dirichlet action.
Downstream, it specializes to the canonical certificate scale $(5,5,5)$, and an iff theorem identifies it with nonemptiness of the typed open-input bundle used in finite stationarity calculations. Closing both conjuncts is what lets the gravity stack claim the physical six-tet cubic Dirichlet instance on the periodic Freudenthal torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.