periodicGaugeGeneratorMap5
plain-language theorem explainer
Linear map that turns a coefficient vector on a finite family of edge-perturbation generators into the corresponding linear combination of those generators, evaluated edgewise. Anyone working the Track 1.D gauge or conformal projectors on the N=5 periodic Freudenthal torus cites it as the common generator-to-perturbation interface. The body is the pointwise finite sum of coefficient times generator.
Claim. Fix a finite index type $I$ and a family $(g_i)_{i\in I}$ of real edge perturbations on the typed periodic Freudenthal edges. The gauge generator map sends a coefficient vector $c:I\to\mathbb{R}$ to the edge perturbation $e\mapsto\sum_{i\in I} c_i\, g_i(e)$.
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity on the periodic Freudenthal torus. Track 1.B's conformal ansatz puts one scalar potential per vertex and averages endpoint values onto edges; that scalar slice cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations as the ambient space and carves out conformal and gauge subspaces inside it.
An edge perturbation here is simply a real function on the typed periodic edges (PeriodicEdge5 → ℝ). Longitudinal gauge generators are finite families of such functions. Coefficient vectors on those generators play the role of discrete gauge potentials: the map defined here converts potentials into edge-length variations by linear combination.
The same pattern is reused for the conformal generators (vertex-delta basis), so one linear-combination interface serves both the gauge span and the conformal projector.
proof idea
Pure definition, not a theorem. The body is the pointwise finite sum
fun coeff e => ∑ i, coeff i * gaugeGen i e
over the finite index type. No lemmas are invoked; finiteness of the index type supplies the sum.
why it matters
This is the shared generator interface for the whole Track 1.D gauge story. Specializing the generators to the encoded vertex-delta conformal family yields the conformal generator map and its two-point support and subspace-membership lemmas. The image-span theorem records that anything in the gauge subspace of a generator-defined map is, by construction, a linear combination of those generators.
Downstream, generator-map projector data closes the finite orthogonal decomposition target for the N=5 Freudenthal TT problem, and the master-theorem handoff endpoint states that when the gauge map is defined directly from finite generators, the separate gauge-span proof is automatic. In short, the definition turns "finite generator family" into a first-class linear map that the TT projector and handoff stack can quote without re-proving span each time.
Framework role: scaffolding for the shear/TT sector that the conformal (scalar) ansatz cannot reach; not itself a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.