conformalEdgeLengthPerturbation
plain-language theorem explainer
First-order edge-length variation induced by a vertex conformal potential on a finite 3D Regge triangulation. Cite it when comparing the conformal weak-field slice to full edge shear or TT modes. The definition is a one-line packaging of the directional derivative of the conformal hinge measure as an edge-level map.
Claim. Given a finite 3D Regge triangulation $K$ with consistent incidence data and a real vertex potential $\xi$, the conformal edge-length perturbation is the edge map $e \mapsto$ the directional derivative of the conformal hinge length of $e$ at the flat background. Explicitly, if $u,v$ are the endpoints of $e$, this value is $\sqrt{\ell_e^2}\,(\xi_u+\xi_v)/2$.
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity. The older Track 1.B conformal ansatz puts one scalar at each vertex and induces edge strains by averaging the two endpoint values. That scalar slice cannot carry pure shear, so it cannot alone represent transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations as the ambient space and embeds the conformal ansatz inside it.
A vertex potential is a real assignment to each vertex of $K$. An edge perturbation is a real assignment to each global edge; that is the natural finite surface for anisotropic shear. The upstream hinge directional derivative evaluates, at the flat background, the first variation of conformal hinge length along a given edge: $\sqrt{\ell_e^2}$ times the average of the two endpoint potentials. Incidence consistency supplies the global squared edge lengths used in that formula.
proof idea
Pure definitional packaging. The body is the function that sends each edge $e$ to the already-defined hinge-measure directional derivative of the conformal ansatz at that edge. No extra algebra is performed here; equality with the square-root times log-strain form is proved by a separate one-line rfl theorem.
why it matters
This map is the concrete embedding of the vertex-conformal ansatz into the full edge-perturbation space used by the tensor/shear track. Downstream, the sibling identity conformalEdgeLengthPerturbation_eq_sqrt_mul_logStrain records that the packaged map equals background edge length times the conformal log-strain, so later rectangle-obstruction and non-conformality arguments can work indifferently with either presentation. The module goal is to prove that nontrivial rectangle shear is not vertex-conformal, which is the elementary obstruction showing the conformal slice is proper. In the broader Recognition gravity program this is scaffolding toward a discrete TT sector, not yet a continuum GR claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.