beta_lin
plain-language theorem explainer
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.
Claim. The 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
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}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.