Track1DTTGramSelfAdjointEndpoint
plain-language theorem explainer
Defines the Track 1.D handoff proposition: the fixed finite transverse-traceless Gram operator on the N=5 combined conformal-plus-longitudinal coefficient space is self-adjoint for the standard coefficient inner product. Gravity auditors and Track 7 integration cite it as the explicit Gram symmetry endpoint. It is a pure Prop alias, not a proof; discharge is by the sector self-adjointness theorem.
Claim. The Track 1.D endpoint asserts: for all real coefficient functions $a,b$ on the fixed combined normal-equation index set (conformal vertex-delta generators plus longitudinal vertex-vector generators on the $N=5$ periodic torus), $\langle G a,\, b\rangle = \langle a,\, G b\rangle$, where $G$ is the TT Gram operator acting on coefficient vectors and $\langle\cdot,\cdot\rangle$ is the coefficient-space Euclidean inner product $\sum_{\mathrm{idx}} a_{\mathrm{idx}} b_{\mathrm{idx}}$.
background
Module context is Gravity Track 7 fork-handoff integration: a receipt lane that records what parallel forks prove without upgrading the discovery claim. Fork A covers Track 1.B Schläfli stationarity reduction at $N=5$; remaining Track 1 displacement-class leaves stay open dependencies.
The finite TT sector works on a fixed combined index: conformal vertex-delta generators summed with longitudinal gauge indices on the $N=5$ periodic torus. Coefficient space carries the plain Euclidean product $\sum a_i b_i$. The Gram operator is realized as a coefficient-vector map: apply the discrete TT Gram stencil to a coefficient function and read the result back as another coefficient function.
Self-adjointness of that Gram map for the coefficient product is the natural symmetry needed before range and residual arguments in the normal equations. Upstream definitions supply exactly those three pieces (index type, inner product, Gram-as-vector).
proof idea
No proof body: this is a definitional Prop alias. It packages the universal quantification over coefficient pairs and the equality of the two inner products with Gram applied on the left versus the right. The companion theorem track1D_tt_gram_self_adjoint_endpoint_holds discharges it in one line by applying TensorShearSector.periodicTTNormalEquationGram_selfAdjoint5.
why it matters
Track 1.D is the explicit Gram self-adjointness endpoint consumed by Track 7. Downstream, the holding theorem feeds the fork-handoff integration certificate structure, which bundles Track 1 reduction/interface facts with Track 2 many-body and Track 6 sensitivity packages. The module doc stresses that the structural master theorem still uses structural witnesses where required and that Track 1 here is a reduction/interface package, not closure of open Schläfli leaves.
In the gravity lane this pins a concrete finite-dimensional symmetry of the TT normal-equation Gram at $N=5$, so later residual and range criteria can treat $G$ as a genuine self-adjoint operator on coefficient space. It does not finish the full master gravity theorem; it records one handoff fact the integration cert expects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.