IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolSpecificationAudit
Audit module for the Regge continuum TT Bloch symbol: it records that edge-class coefficients scale linearly with the TT polarization (entrywise scalar multiplication). Gravity analysts working the ReggeTTContinuumSymbol Stage-1 campaign cite it when checking frozen-model symbol identities. Content is a cluster of short algebraic scaling lemmas built on the preflight action and symbol objects.
claimFor the Regge TT Bloch symbol setup, if $P$ is a transverse-traceless polarization and $c\in\mathbb{R}$, the edge-class coefficient satisfies $\mathrm{polEdgeCoeff}(c\cdot P)=c\,\mathrm{polEdgeCoeff}(P)$ (entrywise). Parallel homogeneity holds for the plane-wave edge field, action profile, second-difference operator, and the predicate $\mathrm{TTBlochSymbolIs}$. The Frobenius square of a TT polarization is pinned under the same scaling.
background
This module sits in the quantum-gravity full-theory campaign around the Regge continuum TT symbol (ReggeTTContinuumSymbol, Stage 1). The imported preflight module supplies the true nonlinear Regge action, its flat background point, the frozen-model identification, and the TT Bloch symbol object against which continuum limits are checked.
Notation used throughout: a TT polarization is a discrete transverse-traceless mode on the lattice edges; the edge-class coefficient extracts the linear response of the action along an edge class; plane-wave edge fields and action profiles are the Fourier-mode test data; the second-difference operator is the discrete Hessian piece entering the Bloch symbol. The Frobenius square is the natural squared norm used to pin polarization scale.
The audit layer does not redefine those objects. It only certifies how they transform under real scalar multiplication of the polarization, which is the minimal homogeneity needed before continuum-symbol uniqueness or positivity arguments.
proof idea
Not a single theorem: a specification-audit bundle of short lemmas. Typical proofs are one-line or short tactic scripts that push a scalar through polEdgeCoeff, plane-wave constructors, the action profile, and ttSecondDifference via the corresponding smul or mul_left identities, then reassemble TTBlochSymbolIs under scaling. Limit lemmas such as tendsto_const_mul_punctured handle constant factors outside punctured-neighborhood limits. Frobenius-square lemmas close the scale-pinning side conditions for admissible TT polarizations.
why it matters in Recognition Science
Stage-1 of the Regge TT continuum-symbol program needs a clean homogeneity record before any claim that the Bloch symbol is well-defined, unique, or sign-controlled. This audit module is that record: it freezes the entrywise-linear response of edge-class coefficients and related profiles so later continuum or positivity arguments can rescale polarizations without re-proving algebra.
It has no downstream Lean dependents yet in the graph; its consumer is the broader ReggeTTContinuumSymbol campaign unlocked after the C10 probe sign-off. In the Recognition gravity stack it is infrastructure rather than a forcing-chain landmark (T0–T8), but it is required scaffolding for any discrete-to-continuum TT graviton symbol derived from the nonlinear Regge action.
scope and limits
- Does not construct the nonlinear Regge action or the flat background point.
- Does not prove continuum existence or uniqueness of the TT Bloch symbol.
- Does not establish positivity, signature, or dispersion of the symbol.
- Does not treat non-TT modes or curved-background linearization.
- Does not fix physical units or match continuum GR normalization constants.
depends on (1)
declarations in this module (14)
-
theorem
polEdgeCoeff_mul_left -
theorem
smul_polarization_apply -
theorem
polEdgeCoeff_smul -
theorem
planeWaveEdgeField_smul -
theorem
planeWaveActionProfile_smul -
theorem
ttSecondDifference_smul -
theorem
tendsto_const_mul_punctured -
theorem
TTBlochSymbolIs_smul_of -
theorem
TTBlochSymbolIs_smul -
def
frobeniusSq -
theorem
isTTPolarization_frobenius_pinned -
theorem
frobeniusSq_smul -
theorem
isTTPolarization_smul_iff -
theorem
reggeTT_target_scaling_wellPosed