isConformalEdgePerturbation_iff_mem_range
plain-language theorem explainer
On any finite 3D Regge triangulation, an edge perturbation is vertex-conformal exactly when it lies in the range of the conformal strain linear map from vertex potentials. Gravity and discrete-geometry workers cite this to move freely between the predicate language and linear-algebra rank arguments. The proof is a two-line constructor that unpacks the existential definition of range membership against the structure of the conformal predicate.
Claim. Let $K$ be a finite 3D Regge triangulation and $\varepsilon$ an edge-length perturbation on $K$. Then $\varepsilon$ is a vertex-conformal edge perturbation if and only if $\varepsilon$ lies in the range of the $\mathbb{R}$-linear map sending a vertex potential $\xi$ to the edge log-strain $(\xi_u+\xi_v)/2$ on each edge $\{u,v\}$.
background
The module works in the edge (tensor) sector of discrete gravity on finite 3D Regge triangulations. A Triangulation3D carries vertex, edge, and tetrahedron counts together with incidence data. An edge perturbation is a real assignment to each edge (a linearized change of edge lengths about a flat background).
The vertex-conformal ansatz assigns one scalar potential $\xi$ per vertex and induces the symmetric log-strain $(\xi_u+\xi_v)/2$ on the edge ${u,v}$. That assignment is packaged here as the $\mathbb{R}$-linear map conformalStrainLinearMap from vertex potentials into the edge-perturbation space; pointwise it agrees with the conformal edge log-strain of TensorShearSector.
The predicate IsConformalEdgePerturbation asserts existence of some vertex potential realizing $\varepsilon$. Linear-algebra arguments (rank bounds, proper-subspace witnesses) need the equivalent formulation as membership in the image of that linear map. This lemma records the equivalence on an arbitrary finite triangulation before specializing to the $5\times5\times5$ periodic Freudenthal 3-torus.
proof idea
Term-mode proof by constructor on the biconditional. Forward: from a witness $\xi$ with $\varepsilon=\mathrm{conformalEdgeLogStrain}(K,\xi)$, apply LinearMap.mem_range.mpr to obtain range membership (symmetry of equality). Backward: unpack range membership via LinearMap.mem_range.mp to a preimage $\xi$, then repackage as the conformal-predicate witness. No triangulation geometry is used; only the definitions of the predicate and of linear-map range.
why it matters
Lane 3 of the Seven-Gaps gravity program measures how small the conformal slice sits inside the full edge-perturbation space, and exhibits concrete shear. The module status header lists this equivalence among the fully proved linearity facts that underwrite all later rank comparisons.
Downstream, periodicTorus5_exists_nonconformal converts a non-membership-in-range witness on the $N=5$ torus into the predicate language: if $\varepsilon$ were conformal then the equivalence would force range membership, contradicting the proper-subspace fact (conformal rank $\le 125 < 875$). Without the bridge, rank bounds and explicit shear faces (rectangle shear, uniform $x$-strain) could not be stated as non-conformal edge perturbations.
In the broader Recognition gravity stack this separates pure conformal (scalar) modes from genuine tensor shear on the discrete geometry, a prerequisite for arguing that the edge sector is not exhausted by the vertex ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.