conformalStrainLinearMap_apply
plain-language theorem explainer
On any finite 3D Regge triangulation, the packaged real-linear map from vertex conformal potentials to edge perturbations evaluates exactly to the classical conformal edge log-strain. Discrete-gravity and Regge analysts cite this when rewriting range or rank statements in linear-map language. The proof is pure definitional reflexivity from the map's underlying function field, exposed as a simp lemma.
Claim. For every finite 3D Regge triangulation $K$ and every vertex potential $\xi\colon\{0,\ldots,n_V(K)-1\}\to\mathbb{R}$, the conformal strain linear map applied to $\xi$ equals the conformal edge log-strain of $\xi$ (the edgewise assignment $(\xi(u)+\xi(v))/2$ on endpoints of each edge).
background
A finite 3D Regge triangulation $K$ carries abstract incidence data: $n_V$ vertices, $n_E$ edges, tetrahedra, and a nondegenerate squared-edge length tuple on each tet. A vertex conformal potential is simply a real scalar per vertex, i.e. a map $\mathrm{Fin},n_V\to\mathbb{R}$.
The vertex-conformal ansatz induces, on an edge with endpoints $u,v$, the log-strain $(\xi u+\xi v)/2$. That assignment is the classical conformal edge log-strain from the tensor-shear sector. The present module packages it as an honest $\mathbb{R}$-linear map from vertex potentials into the full edge-perturbation space, so that range, rank, and membership arguments can use Mathlib linear-algebra lemmas.
Local setting is Seven-Gaps Lane 3: measure how small that conformal image is inside the full edge space on the $5\times5\times5$ periodic Freudenthal 3-torus, and exhibit an explicit shear complement (rectangle face strain, uniform $x$-strain) outside the conformal slice.
proof idea
One-line term proof by rfl. The linear map is defined with underlying function toFun ξ := conformalEdgeLogStrain K ξ (and separate map_add' / map_smul' obligations already discharged in the definition). Application is therefore definitionally equal to the classical log-strain, so reflexivity closes the goal. The @[simp] attribute makes the rewrite fire automatically in downstream simp or rw steps.
why it matters
This is the first item in the module's honest-status theorem list: the conformal ansatz is packaged as a genuine $\mathbb{R}$-linear map that agrees pointwise with the classical log-strain. That packaging is what lets later results identify the conformal subspace predicate with membership in the linear image, bound the image finrank by $n_V$ via Mathlib's range-rank inequality, and obtain the concrete dimension gap on the $N=5$ torus ($\le 125 < 875$). In the Recognition gravity program this cleanly separates pure conformal (trace/vertex) deformations from the shear/tensor edge sector that carries the non-conformal degrees of freedom beyond the vertex ansatz. No external used-by edges are recorded yet; the consumers are the sibling range, finrank, and non-conformal-witness theorems in the same Lane 3 file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.