Gravity Analysis Regge Ttsymbol Specification Audit Plane Wave Edge Field Smul

Scaling the plane wave

A plane wave in this setting is a simple model of a disturbance on a discrete lattice. The framework writes each such wave as a base value plus an amplitude times a cosine that oscillates across the lattice. The amplitude itself is built from a polarization matrix, a small table of numbers that describes the wave's direction of vibration, and a coefficient that depends on that matrix. The declaration planeWaveEdgeField_smul concerns what happens when one multiplies every entry of the polarization matrix by a constant c.

The lemma establishes a clean statement: the wave with the rescaled polarization matrix and the original amplitude is exactly the same as the original wave with the amplitude multiplied by c. In symbols, planeWaveEdgeField(c·E, k, t) equals planeWaveEdgeField(E, k, c·t). This is a statement about the family of waves being reparametrized, not about any particular wave. It shows that the amplitude and the polarization scale together, so that changing one can be absorbed into the other. The proof is a direct computation from the definitions, and it is checked by the machine.

Why does this matter? The framework's larger target, the continuum TT Bloch symbol, aims to assign a fixed numerical value, -1/4, to every allowed polarization. A fixed value is only meaningful if the statement is stable under rescaling. Without a normalization, one could rescale the polarization and get a different value for the same physical situation, a contradiction. The scaling lemma is the first step in showing that the target is well-posed: it pins down how the relevant quantities change under rescaling, and it sets up the normalization that makes the fixed value a coherent statement.

It is important to be precise about what this lemma does not do. It does not establish that the -1/4 value is correct. It does not even provide evidence for that value. The target remains open, and its status flag is false. The lemma only establishes the scaling behavior, which is a necessary condition for the target to be meaningful. It is a piece of the infrastructure, not a result about the value itself.

/-- (b) THEOREM: rescaling the polarization by `c` reparametrizes the SAME
plane-wave edge-field family by `t ↦ c·t`.  This is the exact sense in
which the polarization normalization and the amplitude normalization are
one and the same gauge. -/
theorem planeWaveEdgeField_smul (c : ℝ) (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) (t : ℝ) :
    planeWaveEdgeField N (c • E) k t = planeWaveEdgeField N E k (c * t) := by
  funext e
  simp only [planeWaveEdgeField, polEdgeCoeff_smul]
  ring

/-- (b) THEOREM: rescaling the polarization by `c` reparametrizes the SAME
plane-wave edge-field family by `t ↦ c·t`.  This is the exact sense in
which the polarization normalization and the amplitude normalization are
one and the same gauge. -/
theorem planeWaveEdgeField_smul (c : ℝ) (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) (t : ℝ) :
    planeWaveEdgeField N (c • E) k t = planeWaveEdgeField N E k (c * t) := by
  funext e
  simp only [planeWaveEdgeField, polEdgeCoeff_smul]
  ring

What this page does not claim

The declaration does not establish that the -1/4 target value is correct. The declaration does not provide numerical evidence for any particular value of the Bloch symbol. The declaration does not address the physical interpretation of the plane wave model.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/ReggeTTSymbolSpecificationAudit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: