canonicalPeriodicFirstVariationInput
plain-language theorem explainer
Packages the standard Regge first-variation input for the canonical periodic Freudenthal torus on an $N_x\times N_y\times N_z$ lattice with each side strictly larger than 2. Gravity workers cite it when discharging the first-variation side of edge-stencil local correspondence on that torus. Construction is a one-line application of the edge-slot-partition builder to the encoded periodic partition.
Claim. For $N_x,N_y,N_z\in\mathbb{N}$ with each $N_i>2$, the canonical flat length configuration on the encoded periodic Freudenthal torus of those periods carries a standard Regge first-variation input package, obtained from the torus edge-slot partition.
background
This module wires the encoded periodic Freudenthal torus scaffold into the physical six-tet cubic Dirichlet model. It does not give the physical Dirichlet equality for free; it packages the exact obligations needed to instantiate that model on a periodic Freudenthal lattice.
The first-variation input is the data bundle that Regge calculus needs before one can talk about stationary deficit angles or Hessian/Dirichlet comparison: a fixed combinatorial complex $K$ with a nondegeneracy witness, together with a length configuration (here the canonical periodic flat one). The edge-slot partition is the combinatorial splitting of edges that lets the first-variation package be assembled from local edge data rather than from a global abstract hypothesis.
Upstream, the encoded periodic Freudenthal torus supplies both $K$ and the partition; the flat configuration is the zero-curvature reference lengths on that torus. The dimensionless bridge ratio $K=\varphi^{1/2}$ appears elsewhere in the gravity stack but is not the content of this package.
proof idea
Definitional one-liner. Bind $P$ to the canonical encoded periodic Freudenthal torus for the given periods, then apply reggeActionFirstVariationInput_of_edgeSlotPartition to $P$'s complex, its nondegeneracy witness, the canonical periodic flat configuration, and the edge-slot partition extracted from $P$ by edgeSlotPartition_of_encodedPeriodicFreudenthalTorus. No tactic proof; the partition discharges the input constructor.
why it matters
Fills the first-variation slot that the three canonical periodic edge-stencil local-correspondence endpoints all consume. Downstream, canonicalPeriodicEdgeStencilLocalCorrespondence_of_eventuallyZero_and_edgeStencilTargets states that canonical flatness, first variation, edge-stencil Dirichlet equality, and the Taylor/remainder bridges are already supplied by preceding results, leaving only two Hessian-side geometric inputs. The stationary variants (cell-tet targets; length-chain targets) reuse the same package under weaker Schläfli stationarity.
In the Recognition gravity track this is scaffolding glue, not a new physical law: it lets the periodic six-tet cubic instance sit on the Freudenthal torus so later theorems can compare the Regge Hessian to the discrete Dirichlet form. It does not itself touch T5–T8 or the RCL; it is infrastructure for the continuum/lattice gravity comparison on the eight-tick-compatible cubic complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.