Track1DConformalGeneratorSpanEndpoint
plain-language theorem explainer
Every N=5 periodic edge perturbation in the vertex-conformal log-strain subspace is a finite real linear combination of the encoded-vertex conformal generators. Gravity auditors cite this Prop when packaging the Track 7 fork handoff for the master theorem. It is a pure proposition alias; the companion theorem discharges it by the TensorShearSector subspace-span lemma.
Claim. For every edge perturbation $c$ on the canonical $5\times 5\times 5$ periodic Freudenthal torus, if $c$ lies in the periodic conformal log-strain subspace (i.e., $c$ is the conformal edge log-strain of some vertex potential), then there exist real coefficients indexed by the encoded vertices such that, pointwise on every edge, $c$ equals the corresponding linear combination of the unit-vertex conformal generators.
background
Track 7 is the integration-lane receipt for parallel fork handoffs in the gravity master theorem. It records what each fork endpoint proves without upgrading the discovery claim, and leaves remaining Track 1 displacement-class leaves open.
The N=5 setting is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. Edge perturbations are real functions on its typed periodic edges. The periodic conformal log-strain subspace consists of those perturbations that arise as the conformal edge log-strain of some vertex potential on the torus.
The spanning family is indexed by encoded vertices: each generator is the conformal edge log-strain of a unit delta potential at one encoded vertex (zero elsewhere). The dimensionless bridge ratio $K=\varphi^{1/2}$ appears only as the torus vertex-count parameter in the coefficient domain.
proof idea
No proof body: this is a Prop definition (def_or_abbrev). It packages the universal quantification over periodic edge perturbations, the membership hypothesis in the conformal log-strain subspace, and the existence of real coefficients on the finite encoded-vertex index set such that the perturbation equals the pointwise linear combination of the unit-vertex conformal generators. The actual span fact is proved downstream by applying periodicConformalLogSubspace5_spanned_by_encodedVertexGenerators from TensorShearSector.
why it matters
This is the Track 1.D endpoint: the N=5 conformal slice already has an explicit finite spanning family indexed by encoded vertices. The companion theorem track1D_conformal_generator_span_endpoint_holds consumes it and feeds the Fork Handoff Integration certificate, which bundles Forks A–F for the structural master theorem.
Downstream packaging treats Track 1 as a reduction/interface package, not a closure of the open Schläfli leaves. After the conformal span is fixed by vertex generators, it is enough to supply gauge-generator projector data. The declaration therefore pins the finite-dimensional conformal slice that later Track 1 displacement reductions sit on, without claiming full stationarity or residual closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.