finrank_vertexPotential
plain-language theorem explainer
On any finite 3D Regge triangulation the real vector space of vertex conformal potentials has dimension exactly equal to the vertex count. Gravity and discrete-geometry workers cite this when bounding the conformal edge-strain image inside the full edge-perturbation space. The proof is a one-line unfolding to function space on Fin nV followed by Mathlib's finite-type function-space rank formula.
Claim. For every finite 3D Regge triangulation $K$, the finite dimension of the real vector space of vertex conformal potentials on $K$ equals the number of vertices $n_V(K)$: $\mathrm{finrank}_{\mathbb{R}}(\mathrm{VertexPotential}(K)) = n_V(K)$.
background
In the Regge geometry layer a finite 3D triangulation $K$ carries abstract incidence data together with a nondegenerate squared-edge length on every tetrahedron; its vertex count is the natural number $n_V$. The vertex conformal potential space is defined simply as real-valued functions on the finite vertex set, i.e. $\mathrm{Fin}, n_V\to\mathbb{R}$.
The ambient module is the Seven-Gaps edge (tensor) sector. The vertex-conformal ansatz assigns one scalar per vertex and induces the symmetric log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. That ansatz is packaged as an $\mathbb{R}$-linear map from vertex potentials into the edge-perturbation space; the present rank identity is the domain-side half of the dimension comparison that shows the conformal image is a proper subspace on concrete triangulations.
Upstream, $\mathrm{VertexPotential}$ is an abbreviation, not a nontrivial construction, so the rank statement is pure linear algebra once the finite type is exposed.
proof idea
Rewrite the goal by unfolding the abbreviation $\mathrm{VertexPotential},K$ to $\mathrm{Fin},K.nV\to\mathbb{R}$. Apply Mathlib's $\mathrm{Module.finrank_fintype_fun_eq_card}$, which states that the finite dimension of the space of real functions on a finite type equals the cardinality of that type. The cardinality of $\mathrm{Fin},n_V$ is $n_V$, so the equality is immediate. No triangulation incidence data is used.
why it matters
This identity feeds the rank bound $\mathrm{conformalRange_finrank_le_nV}$: the conformal image inside edge-perturbation space has dimension at most $n_V$, obtained by composing Mathlib's $\mathrm{LinearMap.finrank_range_le}$ with the present equality. That bound is the abstract half of Lane 3 of the Seven-Gaps gravity program, which measures how small the conformal slice is inside the full edge space.
On the concrete $5\times5\times5$ periodic Freudenthal 3-torus one then obtains $n_V=125$ and $n_E=875$, hence a strict dimension gap (conformal rank $\le 125<875$). The gap underwrites existence of non-conformal edge perturbations and the explicit rectangle-shear witness. Within Recognition Science this is discrete-geometry scaffolding for the gravity sector rather than a T0–T8 forcing step, but it is fully proved (zero sorry) and closes the domain-rank half of the conformal-versus-shear comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.