track1D_tensorShearScaffoldEndpoint_holds
plain-language theorem explainer
Packages the Track 1.D tensor/shear scaffold as three facts: a vertex-potential-to-edge-strain map, an N=5 encoded/periodic edge-perturbation equivalence, and the rectangle obstruction that pure shear is not vertex-conformal. Gravity integrators and Track 7 handoff proofs cite it as the Session 215 endpoint. The proof is a three-way constructor assembling existing maps and the rectangle non-existence lemma.
Claim. The Track 1.D tensor/shear scaffold endpoint holds: (i) there exists a map sending each 3D triangulation $K$ and vertex potential $\xi$ to an edge perturbation; (ii) the encoded and typed periodic edge-perturbation surfaces for the $N=5$ torus are equivalent; (iii) for all real $h \neq v$, no four vertex potentials $\xi_a,\xi_b,\xi_c,\xi_d$ realize opposite-edge averages $(h,h,v,v)$.
background
Track 1.B assigns one scalar potential per vertex and induces edge-length variations by averaging the two endpoints. That conformal slice cannot represent pure shear, so it misses transverse-traceless weak-field modes. Track 1.D separates independent edge perturbations from vertex-conformal ones and records the elementary obstruction.
The conformal edge log-strain on a triangulation $K$ sends a vertex potential $\xi$ to the edge map $e \mapsto (\xi(u)+\xi(v))/2$ for endpoints $u,v$ of $e$. A rectangle strain with horizontal average $h$ and vertical average $v$ is vertex-conformal only if four scalars realize those four midpoint conditions; when $h \neq v$ no such scalars exist.
On the $N=5$ periodic torus, edge perturbations admit two presentations (encoded Fin nE data versus typed periodic edges). The scaffold endpoint asserts that those presentations are equivalent, that the conformal strain map exists, and that the rectangle obstruction holds for every nontrivial shear pair.
proof idea
Term-mode proof by nested constructor on the three conjuncts of the endpoint proposition.
First conjunct: supply the nonempty witness fun K => conformalEdgeLogStrain K, the standard vertex-to-edge averaging map.
Second conjunct: supply periodicEdgePerturbationEquiv5 as the equivalence between encoded and periodic $N=5$ edge-perturbation types.
Third conjunct: for any $h \neq v$, discharge the non-existence claim by nontrivial_rectangle_shear_not_vertexConformal. No further algebra is done at this layer; the endpoint only assembles prior results.
why it matters
Closes the Session 215 Track 1.D scaffold: conformal scalar gravity is properly separated from a genuine tensor/shear sector. Downstream, track1D_tensor_shear_scaffold_integration_endpoint_holds in the Master Theorem handoff consumes this theorem verbatim as the Track 7 integration endpoint, so TT modes can be treated as finite orthogonality to the periodic conformal slice plus a caller gauge slice.
In the broader Recognition gravity program this is the first formal cut between the Track 1.B conformal ansatz and independent edge shear. Without the rectangle obstruction, one could not claim that pure shear (hence linearized TT waves on the discrete complex) lies outside vertex potentials. The $N=5$ equivalence ties the abstract edge data to the periodic Freudenthal torus geometry used elsewhere in the gravity stack.
It does not yet construct dynamical TT propagation or match continuum GR polarization counts; it only locks the scaffold facts the handoff needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.