conformalRange_finrank_le_nV
plain-language theorem explainer
On any finite 3D Regge triangulation, the image of the vertex-conformal strain map inside edge-perturbation space has real dimension at most the number of vertices. Gravity and discrete-geometry workers cite it to bound the conformal slice before counting shear modes. The proof is a two-step rank comparison: Mathlib’s range-rank inequality composed with the exact rank of the vertex-potential space.
Claim. For every finite 3D triangulation $K$, if $C_K$ denotes the $\mathbb{R}$-linear map sending a scalar potential on vertices to the induced conformal log-strain on edges, then $\mathrm{finrank}_{\mathbb{R}}(\mathrm{range}(C_K)) \le n_V(K)$, where $n_V(K)$ is the number of vertices of $K$.
background
Lane 3 of the Seven-Gaps gravity stack studies the edge (tensor) sector beyond the pure conformal ansatz. On a triangulation $K$, a vertex potential is one real scalar per vertex. The conformal ansatz pushes that potential to edges by the symmetric log-strain $(\xi_u+\xi_v)/2$ on each undirected edge ${u,v}$, packaged here as the linear map conformalStrainLinearMap from vertex potentials into the full edge-perturbation space.
The ambient edge space has dimension equal to the number of edges; the conformal image is a linear subspace of that space. The module header records that membership in the range is exactly the predicate “is a conformal edge perturbation,” so dimension bounds on the range are dimension bounds on the conformal slice.
Upstream, the exact identity $\mathrm{finrank}(\mathrm{VertexPotential},K)=n_V(K)$ is already available, as is Mathlib’s general fact that the rank of a linear map’s range never exceeds the rank of its domain. This lemma simply chains those two facts for an arbitrary finite 3D triangulation.
proof idea
Term-mode, two lines. Apply Mathlib’s LinearMap.finrank_range_le to the conformal strain map: the finrank of its range is at most the finrank of the domain (vertex potentials). Then transitively compose with the already-proved equality finrank_vertexPotential K, whose .le form supplies $\mathrm{finrank}(\mathrm{VertexPotential},K)\le n_V(K)$. No case split on $K$ and no explicit basis construction.
why it matters
This is the abstract rank bound that feeds the concrete $N=5$ torus count. Downstream, periodicTorus5_conformalRange_finrank_le instantiates it at PeriodicTorus5.K and composes with $n_V=125$ to get conformal rank $\le 125$. That inequality is the left half of the dimension gap $125<875$ used to prove the conformal range is a proper subspace of the 875-dimensional edge space, hence that non-conformal (shear) edge perturbations exist on the Freudenthal 3-torus.
In the Recognition gravity program this closes the “conformal image is thin” half of Lane 3: once the conformal slice is known to be at most vertex-dimensional, the explicit rectangle-shear and uniform-strain witnesses can sit outside it. The result is fully proved (zero sorry) and holds for every finite 3D triangulation, not only the torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.