Encyclopedia Gravity Gravity Analysis Regge Ttsymbol Specification Audit Regge Tt Target Scaling Well

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttsymbol Specification Audit Regge Tt Target Scaling Well

A machine-checked proof shows that a proposed constant for gravitational wave polarization is meaningful only because a normalization rule forces the result.

Verify this page

The scaling audit

In the search for a quantum theory of gravity, one candidate approach describes spacetime as a discrete structure of building blocks. A key question is whether a certain mathematical object, the continuum Bloch symbol, has a fixed value on every transverse-traceless polarization. A fixed value is only meaningful if the statement cannot be rescaled into a contradiction. The declaration reggeTT_target_scaling_wellPosed establishes exactly that: it proves that the statement is well-posed, meaning it is coherent and cannot be made to contradict itself by scaling.

The proof works by examining what happens when you multiply a polarization matrix by a constant. The plane-wave family is linear in the polarization, so rescaling the polarization reparametrizes the same family. The second-difference quadratic form, which is used to define the Bloch symbol, then scales quadratically. This means that without a normalization, the same physical family would report both a value and its square multiple, a contradiction. The theorem shows that the Frobenius normalization, which sets the sum of squares of the matrix entries to one, is the only clause that fixes this. Under this pin, the only rescalings that stay within the allowed class are those where the square of the constant equals one, making the reported value invariant.

This result is a theorem in the framework's machine-checked library of formal theorems. It does not, however, prove that the value of the Bloch symbol is actually -1/4. That target remains open. The theorem only establishes that the statement is well-posed, not that it is true. The audit also confirms that two conventions for summing over index pairs are consistent, a necessary check for the numerical evidence that supports the target.

THEOREM reggeTT_target_scaling_wellPosed · IndisputableMonolith/Gravity/Analysis/ReggeTTSymbolSpecificationAudit.lean
reggeTT_target_scaling_wellPosed · IndisputableMonolith/Gravity/Analysis/ReggeTTSymbolSpecificationAudit.lean:236 
/-- **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⟩
THEOREM ttSecondDifference_smul · IndisputableMonolith/Gravity/Analysis/ReggeTTSymbolSpecificationAudit.lean
ttSecondDifference_smul · IndisputableMonolith/Gravity/Analysis/ReggeTTSymbolSpecificationAudit.lean:115 
/-- (c) THEOREM: under `E ↦ c·E` the second-difference quadratic form
scales QUADRATICALLY, `D_{cE}(t) = c² · D_E(c·t)`.  This is the kernel
fact that makes any unnormalized "fixed `-1/4`" claim contradictory: the
same physical family would have to report both `H` and `c²·H`. -/
theorem ttSecondDifference_smul {c t : ℝ} (hc : c ≠ 0) (ht : t ≠ 0)
    (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) :
    ttSecondDifference N (c • E) k t =
      c ^ 2 * ttSecondDifference N E k (c * t) := by
  have hN : ((N : ℝ)) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
  unfold ttSecondDifference
  simp only [planeWaveActionProfile_smul, mul_zero, mul_neg]
  field_simp
THEOREM isTTPolarization_smul_iff · IndisputableMonolith/Gravity/Analysis/ReggeTTSymbolSpecificationAudit.lean
isTTPolarization_smul_iff · IndisputableMonolith/Gravity/Analysis/ReggeTTSymbolSpecificationAudit.lean:200 
/-- (e) THEOREM, the pin is real: starting from a TT polarization `E`, the
rescaled matrix `c • E` remains a TT polarization exactly when `c² = 1`.
Symmetry, tracelessness, and transversality survive every rescaling; the
Frobenius pin is the ONLY normalization-fixing clause, and it works. -/
theorem isTTPolarization_smul_iff (m : Fin 3 → ℤ)
    (E : Fin 3 → Fin 3 → ℝ) (c : ℝ) (h : IsTTPolarization m E) :
    IsTTPolarization m (c • E) ↔ c ^ 2 = 1 := by
  obtain ⟨hsym, htr, htrans, hfrob⟩ := h
  constructor
  · intro hcE
    have hpin := hcE.2.2.2
    have hfrob' : frobeniusSq (c • E) = 1 := hpin
    rw [frobeniusSq_smul] at hfrob'
    have hfrobE : frobeniusSq E = 1 := hfrob
    rw [hfrobE, mul_one] at hfrob'
    exact hfrob'
  · intro hc2
    refine ⟨?_, ?_, ?_, ?_⟩
    · intro i j
      show c * E i j = c * E j i
      rw [hsym i j]
    · show (∑ i : Fin 3, c * E i i) = 0
      rw [← Finset.mul_sum, htr, mul_zero]
    · intro j
      show (∑ i : Fin 3, (m i : ℝ) * (c * E i j)) = 0
      calc (∑ i : Fin 3, (m i : ℝ) * (c * E i j))
          = c * ∑ i : Fin 3, (m i : ℝ) * E i j := by
            rw [Finset.mul_sum]
            exact Finset.sum_congr rfl fun i _ => by ring
        _ = 0 := by rw [htrans j, mul_zero]
    · have h1 : frobeniusSq (c • E) = c ^ 2 * frobeniusSq E :=
        frobeniusSq_smul c E
      have h2 : frobeniusSq E = 1 := hfrob
      show frobeniusSq (c • E) = 1
      rw [h1, h2, hc2, mul_one]

What this page does not claim

The theorem does not prove that the value of the continuum Bloch symbol is -1/4. The theorem does not provide numerical evidence for the value of the Bloch symbol. The theorem does not prove that the continuum Bloch symbol is well-defined for all polarizations.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND