conformalStrainLinearMap
plain-language theorem explainer
Packages the vertex-conformal log-strain ansatz as an ℝ-linear map from vertex potentials to edge perturbations on a finite 3D Regge triangulation. Anyone bounding the conformal slice inside the full edge-strain space cites this map. Linearity is checked pointwise by ring arithmetic after unfolding the average-of-endpoint formula.
Claim. For any finite 3D Regge triangulation $K$, the assignment sending a vertex potential $\xi$ to the edge log-strain $\varepsilon_e = (\xi_u + \xi_v)/2$ on each edge $e=\{u,v\}$ is an $\mathbb{R}$-linear map from the space of vertex potentials to the space of edge perturbations.
background
Lane 3 of the Seven-Gaps gravity program studies the edge (tensor) sector beyond the pure conformal ansatz. On a finite 3D Regge triangulation $K$ (vertex, edge, and tetrahedron counts with incidence data), a vertex potential is simply a real scalar per vertex. An edge perturbation is a real scalar per edge, linearized about a flat background length assignment.
The conformal ansatz of TensorShearSector induces, from any vertex potential $\xi$, the log-strain $(\xi_u + \xi_v)/2$ on the edge joining $u$ and $v$. That pointwise formula is already defined; this declaration only packages it as a Mathlib linear map so that range, finrank, and subspace membership become available.
The ambient setting is the $5\times 5\times 5$ periodic Freudenthal 3-torus, where one later compares the dimension of the conformal image to the full edge space (125 vertices vs 875 edges).
proof idea
Definitional packaging: the underlying function is exactly the existing conformal edge log-strain. Additivity and homogeneity are proved by funext on edges, unfolding the average-of-endpoints formula and the pointwise Pi add/smul structure, then closing with ring. No external lemmas beyond simp lemmas for those structures are required.
why it matters
This linear map is the handle for every subsequent rank and proper-subspace statement in the edge-tensor sector. Downstream, conformalStrainLinearMap_apply records pointwise agreement with the ansatz, and isConformalEdgePerturbation_iff_mem_range identifies the conformal predicate with membership in the range. The general bound conformalRange_finrank_le_nV (image dimension $\le$ number of vertices) is Mathlib's range-finrank inequality applied to this map, and specializes on the $N=5$ torus to the strict gap $\le 125 < 875$, hence a proper subspace and the existence of non-conformal (shear) edge modes. That gap is the quantitative content of "tensor sector beyond conformal" in the Seven-Gaps lane: pure vertex-conformal strain cannot exhaust the edge degrees of freedom on a realistic 3D lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.