Gravity Analysis Regge Ttsymbol Specification Audit Plane Wave Action Profile Sm

The scaling rule

In the study of gravitational waves, a plane wave can be described by an amplitude and a polarization matrix, a 3 by 3 table of numbers that fixes the wave's directional character. The theorem planeWaveActionProfile_smul states a simple scaling rule: if you multiply every entry of the polarization matrix by a constant c, the resulting wave's action profile is exactly the original profile evaluated at the amplitude multiplied by c. In symbols, the action profile of (c·E) at amplitude t equals the action profile of E at amplitude c·t. This is a formal, machine-checked statement in the framework's library of theorems.

The statement matters because it exposes a gauge freedom. Rescaling the polarization by c and rescaling the amplitude by 1/c produce the same physical plane wave. The theorem proves that the action profile, a quantity built from the wave, respects this equivalence exactly. It is a consistency check on the mathematical description, not a statement about the physical value of any gravitational wave observable.

This scaling rule is a stepping stone in a larger audit. The framework's target for a continuum Regge TT symbol proposes a fixed value of -1/4. A fixed value is only meaningful if the statement cannot be rescaled into a contradiction. The theorem planeWaveActionProfile_smul is one link in the proof that a normalization condition on the polarization matrix makes the fixed-value claim well-posed. The audit shows that without such a normalization, the same physical family would report both a value and c² times that value, which would be contradictory.

The theorem does not claim that the value -1/4 is correct. It does not prove that any gravitational wave has that symbol value. The numerical target remains open. What the theorem establishes is a structural fact: the action profile transforms covariantly under rescaling, which is a necessary condition for any fixed-value statement to be coherent.

/-- (b) corollary: the action profile of the rescaled polarization is the
original profile at the rescaled amplitude. -/
theorem planeWaveActionProfile_smul (c : ℝ) (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) (t : ℝ) :
    planeWaveActionProfile N (c • E) k t =
      planeWaveActionProfile N E k (c * t) := by
  unfold planeWaveActionProfile
  rw [planeWaveEdgeField_smul]

/-- **GATE A0 VERDICT (THEOREM): the `-1/4` target statement is
well-posed under the `polEdgeCoeff` scaling convention.**

The three clauses, all kernel-checked, assemble the well-posedness
argument:

1. (pin) every `E` in the target's hypothesis class `IsTTPolarization`
   has Frobenius square-sum exactly `1`;
2. (quadratic scaling) the Bloch symbol value transforms as `H ↦ c²·H`
   under `E ↦ c·E`, so WITHOUT a normalization the fixed-value claim
   would be contradictory (the same family would report `H` and `c²·H`);
3. (pin bites) the only rescalings that stay inside the hypothesis class
   are `c² = 1`, and for those `c²·H = H` — the reported value is
   invariant on the quantified class.

Hence `ReggeTTContinuumIsotropyTarget`, which quantifies over
`IsTTPolarization` (pin included), assigns a scaling-coherent meaning to
the fixed constant `reggeTTContinuumCoefficient = -(1/4)`.  Nothing here
proves (or evidences) that the value IS `-1/4`; that target remains OPEN
with status flag `false`. -/
theorem reggeTT_target_scaling_wellPosed {c : ℝ} (hc : c ≠ 0)
    (m : Fin 3 → ℤ) (E : Fin 3 → Fin 3 → ℝ) (H : ℝ)
    (hE : IsTTPolarization m E) :
    frobeniusSq E = 1 ∧
      (TTBlochSymbolIs N E m H ↔ TTBlochSymbolIs N (c • E) m (c ^ 2 * H)) ∧
      (IsTTPolarization m (c • E) ↔ c ^ 2 = 1) :=
  ⟨isTTPolarization_frobenius_pinned m E hE,
    TTBlochSymbolIs_smul N hc E m H,
    isTTPolarization_smul_iff m E c hE⟩

What this page does not claim

The theorem does not prove that the Regge TT symbol value is -1/4. The theorem does not describe any measurable property of gravitational waves. The theorem does not claim that the action profile is a physical observable.

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: