EdgePerturbation
plain-language theorem explainer
A record type holds small real-valued changes to each edge length in a simplicial complex with a given number of edges. Physicists linearizing the Regge action around flat backgrounds cite this record when introducing first-order perturbations for deficit-angle expansions. The definition is a direct structure constructor with one field mapping edge indices to reals.
Claim. Let $n_E$ be a natural number. An edge perturbation is a map $η : Fin(n_E) → ℝ$, where each component records the infinitesimal change in the length of the corresponding edge of a flat simplicial complex.
background
The module packages the Piran-Williams linearization of the Regge deficit angle around a flat simplicial complex, labeled Phase C4. Around a flat complex with edge lengths $a$, a perturbation $η$ induces the first-order deficit $δ_h({a + η_e}) = Σ_e (∂δ_h / ∂L_e)|_{flat} · η_e + O(η²)$, with coefficients fixed by combinatorics and vertex angles. The record simply packages the vector $η_e$ for later use in the linear term of the Regge action $S_Regge = Σ_h A_h · δ_h$ after the linear piece vanishes by Schläfli's identity.
proof idea
The declaration is a structure definition that introduces the type with a single field eta : Fin nE → ℝ. No lemmas are applied and no tactics are used; it is a bare record constructor.
why it matters
This record supplies the perturbation data consumed by linearizedDeficit and by the certificate that the linear Regge action vanishes. It advances discharge of the Regge deficit linearization hypothesis in the Recognition Science program, connecting to the composition law and the phi-ladder forcing chain. It fills the Phase C4 slot needed before the quadratic action and the eight-tick octave can be recovered from flatness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.