IsConformalEdgePerturbation
plain-language theorem explainer
An edge-length perturbation is called conformal when it equals the first-order log-length strain of some scalar vertex potential. Gravity and discrete-geometry workers cite this predicate to mark the Track 1.B conformal slice inside the full edge space. The body is a one-line existential definition, not a proof.
Claim. For a 3D triangulation $K$ and an edge-length perturbation $\varepsilon$ (one real per global edge), $\varepsilon$ is conformal when there exists a scalar vertex potential $\xi$ such that $\varepsilon$ equals the first-order log-length strain induced by averaging the endpoint values of $\xi$.
background
Track 1.B of the gravity scaffold assigns one real scalar to each vertex and pushes it to edges by averaging the two endpoint potentials. That map produces a first-order log-length strain on every edge; the resulting edge vectors form the conformal slice of the weak-field sector.
Edge perturbations themselves are unrestricted maps from the global edge set into $\mathbb{R}$. They are the natural finite Regge surface for anisotropic shear and transverse-traceless modes, which a pure vertex scalar cannot generate. The module therefore separates the full edge space from the conformal image and records the elementary rectangle obstruction: opposite sides of a quadrilateral forced to equal log-strains cannot carry a nontrivial shear.
The local setting is the Track 1.D tensor/shear scaffold on 3D triangulations (including the $N=5$ periodic Freudenthal torus used downstream).
proof idea
Definitional, not a derived proof. The predicate is the existential statement that $\varepsilon$ lies in the image of the conformal log-strain map sending vertex potentials to edge vectors. No tactics or lemmas are invoked; the equality is definitional identity with that map.
why it matters
This predicate is the typed name of the conformal subspace that Track 1.B lives inside. Downstream, EdgeTensorSector rewrites it as membership in the range of the linear conformal-strain map, then proves the $N=5$ periodic torus has conformal rank at most 125 inside an 875-dimensional edge space, with explicit non-conformal witnesses (localized rectangle face shear, uniform $x$-strain).
Those results close the Lane 3 claim that the conformal ansatz cannot cover the full weak-field metric sector, so pure shear and TT gravitational-wave modes require independent edge degrees of freedom. The definition is the hinge between the scalar Track 1.B slice and the tensor/shear track opened in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.