conformalEdgeLengthPerturbation_eq_sqrt_mul_logStrain
plain-language theorem explainer
On an incidence-consistent 3D triangulation, the conformal edge-length perturbation induced by a vertex potential equals the geometric edge length times that potential's log-strain on the edge. Gravity and discrete-geometry workers separating Track 1.B conformal modes from pure shear cite this identity. The proof is pure definitional reflexivity.
Claim. Let $K$ be a 3D triangulation with incidence-consistency witness $h_K$, let $\xi$ be a real potential on the vertices of $K$, and let $e$ be an edge index. Then the conformal edge-length perturbation of $e$ equals $\sqrt{\ell_e^2}\,\cdot\,(\delta\log\xi)_e$, where $\ell_e^2$ is the global squared length of $e$ and $(\delta\log\xi)_e$ is the conformal log-strain of $\xi$ on $e$.
background
Track 1.D opens the tensor/shear sector of the discrete weak-field metric. Track 1.B already assigns one scalar potential to each vertex and induces edge-length variations by averaging the endpoint values. That conformal slice cannot represent pure shear, so it cannot cover transverse-traceless gravitational-wave modes by itself.
This module therefore separates arbitrary edge perturbations from the subspace of vertex-conformal ones. Two sibling quantities appear: the conformal log-strain of a vertex potential on an edge (endpoint average of $\xi$), and the conformal edge-length perturbation (that strain scaled by the geometric edge length). Incidence consistency supplies a global squared edge length for each edge via the Freudenthal-style triangulation data.
The local setting is elementary linear algebra on edge space: identify which first variations of edge lengths come from vertex scalars, then prove rectangle-type obstructions showing that nontrivial shear lies outside that subspace.
proof idea
One-line definitional proof: rfl. The length perturbation is defined to be exactly the product of the positive square root of the global squared edge length with the conformal log-strain, so the stated equality holds by unfolding.
why it matters
This identity is the bookkeeping link between the scalar conformal ansatz (Track 1.B) and the edge-perturbation language used to isolate shear. Downstream siblings such as the vertex-conformal rectangle log-strain forcing a square, and the nontrivial-rectangle shear obstruction, rely on treating length perturbations and log-strains interchangeably up to the geometric factor $\sqrt{\ell_e^2}$.
In the broader Recognition gravity program the point is structural, not numerical: pure shear (tensor) modes must be admitted as independent edge data before discrete TT gravitational waves can sit inside the framework. The module doc states the goal explicitly: separate independent edge perturbations from vertex-conformal ones and prove the elementary rectangle obstruction for the conformal ansatz. No parent theorem yet lists this lemma in used_by (count zero); it is infrastructure for that shear-sector scaffold rather than a forcing-chain landmark (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.