RawEdgePerturbationSplitting
plain-language theorem explainer
Defines a raw additive splitting of any edge-valued real field into three maps: conformal, gauge, and transverse-traceless (TT), required only to sum pointwise back to the original field. Gravity Track 1.D cites it as the algebraic carrier before membership predicates are imposed. There is no proof body: it is a structure packing three operators plus the reconstruction identity.
Claim. A raw edge-perturbation splitting on an edge type $E$ is a triple of operators $C,G,T:(E\to\mathbb{R})\to(E\to\mathbb{R})$ such that for every edge field $\varepsilon$ and every edge $e$, $C(\varepsilon)(e)+G(\varepsilon)(e)+T(\varepsilon)(e)=\varepsilon(e)$. No subspace membership is required yet.
background
Track 1.D opens the tensor/shear sector of weak-field gravity on the Recognition lattice. Track 1.B already assigns one scalar potential per vertex and induces edge-length changes by averaging endpoint values; that conformal slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes.
An edge perturbation is simply a real-valued function on edges. The module separates those free edge fields from vertex-conformal ones and records elementary rectangle obstructions showing that nontrivial shear is not vertex-conformal.
This structure is the minimal algebraic package for a three-way split of such fields. Spatial dimension $D=3$ (forced by T8) and the periodic Freudenthal torus at $N=5$ supply the concrete edge types used downstream; the structure itself is parametric in any edge type $E$.
proof idea
No proof: the declaration is a structure (definition). It packages three function fields conformalPart, gaugePart, ttPart and a single propositional field reconstruct asserting pointwise additive recovery of every edge perturbation. Instantiation later means exhibiting three maps and proving the sum identity.
why it matters
This is the algebraic spine of Track 1.D. Downstream targets quantify over an inhabitant of this structure and then impose conformal/trace, gauge/longitudinal, and TT membership: PeriodicFreudenthalTTDecompositionTargetAtN5 asks for a split whose three parts land in supplied predicates; the orthogonal variant replaces TT by finite orthogonality to the conformal and gauge subspaces; PeriodicTTProjectorData5 packages the three projectors that would construct such a split.
periodicRawSplittingOfEncoded5 transports any splitting on encoded finite edges across the canonical periodic-edge equivalence, so the raw identity is the common interface between encoded and geometric presentations.
In the broader RS gravity program this is the first step past the conformal ansatz toward genuine shear and TT modes on the eight-tick, $D=3$ lattice. The open load is constructing the actual Freudenthal projectors and proving membership plus reconstruction at $N=5$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.