Gravity Analysis Regge Ttsymbol Specification Audit Ttbloch Symbol Is Smul Of

The scaling rule for the Bloch symbol

The declaration TTBlochSymbolIs_smul_of is a formal theorem inside the Recognition Science framework's machine-checked library of formal theorems. It concerns the Bloch symbol, a quantity that describes how a plane wave of gravitational radiation behaves on a discrete lattice of points. The theorem states a precise scaling rule: if you multiply the polarization matrix, which encodes the wave's orientation and shape, by a nonzero constant c, then the Bloch symbol value is multiplied by c squared. In plainer terms, if you stretch the wave's polarization pattern by a factor, the resulting symbol value stretches by the square of that factor.

This rule is not an isolated curiosity. It is the kernel fact that makes a proposed fixed value for the Bloch symbol meaningful. The framework's open target, ReggeTTContinuumIsotropyTarget, claims the symbol takes the specific value -1/4 for every transverse-traceless polarization. Without a scaling rule, that claim would be self-contradictory: the same physical wave, described with a differently scaled polarization, would report a different symbol value. The theorem TTBlochSymbolIs_smul_of, together with its companion result TTBlochSymbolIs_smul, proves that the symbol transforms exactly quadratically under rescaling. This is the essential consistency check that any fixed-value statement must pass.

The theorem's proof is a short chain of algebra. It first shows that the edge-class coefficient, a sum over index pairs that appears in the plane-wave definition, is linear in the polarization matrix. That linearity feeds into the second-difference form, which measures the wave's curvature, and the form scales quadratically. The theorem then composes these facts with a continuity argument to reach the final statement. The entire proof is checked by the Lean kernel with no axioms beyond the standard three, and no use of native code or trusted compiler shortcuts.

What the theorem does not do is just as important. It does not prove that the Bloch symbol value is -1/4. The value itself remains an open target, with its status flag set to false. The theorem only establishes the scaling behavior, which is a necessary condition for the fixed-value claim to be well-posed. It also does not say anything about the physical meaning of the Bloch symbol or its connection to gravitational waves in continuous spacetime. Those questions belong to other parts of the framework, and they are not settled here.

/-- One direction of (d): if the symbol value at `E` is `H`, the symbol
value at `c • E` is `c² · H`. -/
theorem TTBlochSymbolIs_smul_of {c : ℝ} (hc : c ≠ 0)
    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) (H : ℝ)
    (h : TTBlochSymbolIs N E m H) :
    TTBlochSymbolIs N (c • E) m (c ^ 2 * H) := by
  unfold TTBlochSymbolIs at h ⊢
  have hcomp := h.comp (tendsto_const_mul_punctured hc)
  have hmul := hcomp.const_mul (c ^ 2)
  refine hmul.congr' ?_
  filter_upwards [self_mem_nhdsWithin] with t ht
  have ht' : t ≠ 0 := ht
  exact (ttSecondDifference_smul N hc ht' E (commensurateMomentum N m)).symm

/-- (d) THEOREM: the Bloch symbol value predicate transforms exactly
quadratically under polarization rescaling, as an equivalence.  Any
well-posed fixed-value target must therefore fix the polarization
normalization; `IsTTPolarization` does (§5). -/
theorem TTBlochSymbolIs_smul {c : ℝ} (hc : c ≠ 0)
    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) (H : ℝ) :
    TTBlochSymbolIs N E m H ↔ TTBlochSymbolIs N (c • E) m (c ^ 2 * H) := by
  constructor
  · exact TTBlochSymbolIs_smul_of N hc E m H
  · intro h
    have hc' : c⁻¹ ≠ 0 := inv_ne_zero hc
    have h' := TTBlochSymbolIs_smul_of N hc' (c • E) m (c ^ 2 * H) h
    have hE : c⁻¹ • c • E = E := by
      rw [smul_smul, inv_mul_cancel₀ hc, one_smul]
    have hH : (c⁻¹) ^ 2 * (c ^ 2 * H) = H := by
      field_simp
    rwa [hE, hH] at h'

/-- **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 Bloch symbol value is -1/4; that target remains open. The theorem does not establish any physical meaning for the Bloch symbol or its connection to continuous gravitational waves. The theorem does not address the behavior of the symbol under transformations other than uniform rescaling of the polarization matrix.

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: