periodicConformalLogSubspace5_zero
plain-language theorem explainer
The zero periodic edge perturbation lies in the vertex-conformal log-strain subspace on the five-edge periodic torus. Anyone checking that the conformal sector is a genuine linear subspace, or building shear-orthogonal complements, would cite this. The proof is a direct witness: the zero vertex potential maps to the zero edge strain under the averaging ansatz.
Claim. The zero map on periodic edges of the five-slot torus belongs to the conformal log-strain subspace: there exists a vertex potential $\xi$ such that the zero edge perturbation equals the encoded conformal log-strain of $\xi$. Explicitly, $\xi \equiv 0$ works.
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity from the pure conformal (scalar) slice. The conformal ansatz assigns a scalar potential to each vertex and induces first-order log-length strain on an edge by averaging the endpoint potentials: $(\xi_u + \xi_v)/2$. That construction cannot represent pure shear, so transverse-traceless modes need independent edge data.
On the periodic five-edge torus geometry, edge perturbations are typed periodic maps. Membership in the periodic conformal log-strain subspace means the edge perturbation is the pullback, via the edge-encoding equivalence, of some conformal log-strain coming from a vertex potential. This theorem records the elementary fact that the origin sits in that subspace.
The upstream conformal log-strain map is exactly that endpoint average; the encoding map reindexes finite encoded edges to typed periodic edges.
proof idea
Witness the existential with the zero vertex potential. After refine, it remains to check pointwise equality of edge maps. funext reduces to a single edge; simp unfolds the encoding pullback and the average-of-endpoints definition of conformal log-strain, both of which send zero to zero.
why it matters
The module scaffolds the tensor/shear track so pure shear can be separated from vertex-conformal modes; the rectangle obstruction already shows nontrivial shear is not conformal. Establishing that the conformal log subspace contains zero is the trivial subspace axiom needed before quotients, orthogonal complements, or dimension counts against the full edge-perturbation space. No downstream consumers are wired yet. The result is baseline for any later claim that the conformal sector is a linear subspace of periodic edge strains on the five-torus. It sits inside Track 1.D of the gravity program, not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.