beta_lin
The definition supplies the linearized post-Newtonian β parameter as 1 plus one-twentieth of the product of the lag coupling and scalar strength α. Workers deriving bounds on deviations from general relativity in scalar-tensor theories cite this expression when linearizing the PPN coefficients for small couplings. It is introduced as a direct algebraic formula in the potential-based PPN scaffold of the ILG module.
claimThe linearized PPN parameter β is given by $1 + (1/20) C_lag α$, where $C_lag = φ^{-5}$ is the lag coupling constant and α is the scalar coupling strength.
background
The module supplies potential-based definitions for the parametrized post-Newtonian parameters γ and β, expressed using the potentials Φ and Ψ derived from the scalar field ψ together with model parameters. The upstream result C_lag fixes the lag coupling as φ^{-5} ≈ 0.09, the RS-derived lag coupling from the eight-tick resonance structure. This supplies the small-coupling linearization for β in the ILG framework.
proof idea
The definition is a direct one-line algebraic expression setting the value to 1 plus (1/20) times the product C_lag α. No lemmas or tactics are applied beyond the arithmetic operations themselves.
why it matters in Recognition Science
This definition enters the proof of beta_bound_small, which bounds the deviation |β-1| by (1/20)κ under the hypothesis |C_lag α|≤κ, and supports the verification that the ILG PPN functions match the extraction formulas in PPNDerivationHolds. It implements the linearized β coefficient required for the PPN derivation in the Recognition Science chain, linking to the T7 eight-tick octave and the derived constants with ħ = φ^{-5}.
scope and limits
- Does not provide the full nonlinear expression for β.
- Does not fix the numerical value of α or derive C_lag from the forcing chain.
- Does not address higher post-Newtonian orders or solar-system observables.
formal statement (Lean)
43noncomputable def beta_lin (C_lag α : ℝ) : ℝ := 1 + (1/20 : ℝ) * (C_lag * α)
proof body
Definition body.
44
45/-- Bound: if |C_lag·α| ≤ κ then |γ−1| ≤ (1/10) κ. -/