finrank_edgePerturbation
plain-language theorem explainer
On any finite 3D Regge triangulation the real vector space of edge-length perturbations has finite dimension equal to the number of edges. Regge and Recognition gravity work cites this when comparing the conformal (vertex) slice to the full edge space. The proof reduces the type to Fin nE → ℝ and applies Mathlib's finrank-of-function-space identity.
Claim. For every finite 3D Regge triangulation $K$, $\dim_{\mathbb{R}}(\mathrm{EdgePerturbation}(K)) = n_E(K)$, where $n_E(K)$ is the number of edges of $K$ and the edge-perturbation space is the real vector space of assignments of a scalar strain to each edge.
background
A Triangulation3D is a finite abstract 3D Regge complex: vertex, edge, and tetrahedron counts together with incidence maps and a nondegenerate squared-edge tuple on every tet. An edge perturbation is a real scalar on each edge (linearized length strain about a flat background); as a type it is definitionally equivalent to functions Fin nE → ℝ.
This module is Seven-Gaps Lane 3: the edge (tensor) sector beyond the vertex-conformal ansatz. The conformal ansatz sends one scalar per vertex to the log-strain $(\xi_u+\xi_v)/2$ on edge ${u,v}$. To show that ansatz is a proper subspace of the full edge space one needs exact dimensions of both domain and codomain.
Upstream, EdgePerturbation is the structure carrying the edgewise strain eta, and Mathlib supplies Module.finrank_fintype_fun_eq_card for finite-dimensional function spaces over a field.
proof idea
One-line type reduction plus Mathlib. Rewrite the goal as Module.finrank ℝ (Fin K.nE → ℝ) = K.nE (definitional unfolding of the edge-perturbation type), then simp with Module.finrank_fintype_fun_eq_card, which states that the finite rank of ι → ℝ for finite ι equals the cardinality of ι. No case split on the triangulation geometry is required.
why it matters
This is the codomain half of the rank comparison that powers Lane 3. Together with finrank_vertexPotential and Mathlib's LinearMap.finrank_range_le it yields conformalRange_finrank_le_nV: the conformal image has rank at most the number of vertices.
Downstream, finrank_encodedEdgePerturbation5 specializes to the $5\times5\times5$ periodic Freudenthal 3-torus and obtains dimension $875$ via periodicTorus5_nE_eq. That count feeds periodicTorus5_conformalRange_finrank_lt_finrank_edgeSpace (conformal rank $\le 125 < 875$), the proper-subspace facts, and the existence of explicit non-conformal shear witnesses such as rectangleShearFace5. In the Recognition gravity program this is the linear-algebraic certificate that the edge-tensor sector is strictly larger than the conformal ansatz on the working torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.