c_T_squared_derived
The declaration establishes that the squared tensor gravitational-wave speed equals unity at vanishing couplings and admits a linear correction in the product of the parameters α and C_lag. Gravitational-wave analysts working in modified-gravity extensions would cite the identity when bounding deviations from general relativity. The argument is a direct term-mode construction that invokes the GR-limit case and supplies the explicit numerical prefactor 0.01.
claim$c_T^2(0,0)=1$ and for all real numbers α and C_lag there exists a real number coeff such that $c_T^2(α,C_lag)=1+coeff·(α·C_lag)$.
background
The module defines the squared tensor-wave speed as the linear function 1 + 0.01·(α·C_lag). C_lag is the lag coupling φ^{-5} taken from the eight-tick resonance construction. The auxiliary coefficient function from the pipelines module supplies the series expansion used elsewhere for gap corrections, though the present statement only requires existence of some real multiplier. The local setting is the propagation-speed analysis within the gravitational-wave sector of the Recognition Science framework.
proof idea
The proof applies the constructor tactic to split the conjunction. The first conjunct is discharged by direct appeal to the GR-limit theorem c_T_squared_GR_limit. The second conjunct is handled by introducing the universal quantifiers, refining the existential witness to the constant 0.01, and simplifying the definition of c_T_squared.
why it matters in Recognition Science
This result anchors the parameterization of tensor-mode propagation speed in the RS-derived gravitational-wave sector. It supplies the exact GR limit together with the leading correction term that feeds into observational bounds such as those from GW170817. Within the framework it connects the eight-tick resonance lag C_lag to the propagation-speed deviation, consistent with the overall forcing chain that fixes D=3 and the value of α^{-1} near 137.
scope and limits
- Does not compute the numerical value of the coefficient from the gap series.
- Does not incorporate higher-order terms in α or C_lag.
- Does not address vector or scalar mode propagation speeds.
- Does not derive the specific form of c_T_squared from the action expansion.
formal statement (Lean)
48theorem c_T_squared_derived :
49 c_T_squared 0 0 = 1 ∧
50 (∀ α C_lag, ∃ coeff, c_T_squared α C_lag = 1 + coeff * (α * C_lag)) := by
proof body
Term-mode proof.
51 constructor
52 · exact c_T_squared_GR_limit
53 · intro α C_lag
54 refine ⟨0.01, ?_⟩
55 simp [c_T_squared]
56
57end GW
58end Relativity
59end IndisputableMonolith