finrank_encodedEdgePerturbation5
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal 3-torus the real vector space of encoded edge perturbations is exactly 875-dimensional. Gravity and discrete-geometry workers cite this as the concrete edge-space count that makes the conformal-versus-shear gap numerical. The proof is a two-step transport: general edge-space rank equals edge count, then the torus edge count is 875.
Claim. Let $E_5$ be the real vector space of encoded edge perturbations on the $5\times 5\times 5$ periodic Freudenthal 3-torus. Then $\dim_{\mathbb{R}} E_5 = 875$.
background
Lane 3 of the Seven-Gaps gravity program studies the edge (tensor) sector of a 3D Regge triangulation beyond the vertex-conformal ansatz. That ansatz assigns one scalar potential per vertex and induces the log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. The full edge-perturbation space is much larger: one independent real strain per edge.
For any finite triangulation $K$, the edge-perturbation module is definitionally $\mathbb{R}^{K.nE}$, so its finite rank equals the edge count $K.nE$ (finrank_edgePerturbation). On the concrete $N=5$ periodic torus, the triangulation PeriodicTorus5.K has $nV=125$ vertices and, by the canonical edge equivalence, $nE=125\cdot 7=875$ positive-displacement edges (periodicTorus5_nE_eq). EncodedEdgePerturbation5 is that edge space in the encoded coordinates used by the shear-sector API.
proof idea
Term-mode two-line chain. First apply finrank_edgePerturbation at PeriodicTorus5.K to obtain
$\mathrm{finrank}_{\mathbb{R}}(\mathrm{EncodedEdgePerturbation5})=\mathrm{PeriodicTorus5.K.nE}$.
Then transport across the already-proved numerical identity periodicTorus5_nE_eq : PeriodicTorus5.K.nE = 875 by Eq.trans. No new combinatorial counting happens here; the 875 is inherited from the torus edge census.
why it matters
This identity is the numerical right-hand side of the Lane 3 dimension gap. Downstream, periodicTorus5_conformalRange_finrank_lt_finrank_edgeSpace compares conformal rank $\le 125$ against this 875-dimensional edge space, proving the conformal slice is a proper subspace. The Lane 3 capstone periodicTorus5_edge_tensor_sector_beyond_conformal packages the same equality with the rank bound and the explicit non-conformal rectangle-shear witness.
In the Recognition gravity stack this is the discrete count that shows tensor/shear degrees of freedom exist beyond pure conformal (vertex-potential) strain on a concrete 3-torus, consistent with the $D=3$ forcing (T8) and the eight-tick/octave discreteness theme. It closes no open scaffold; it is a fully discharged census lemma that parent gap and witness theorems quote by name.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.