gamma_bound_small
plain-language theorem explainer
A bound on the deviation of the linearized post-Newtonian parameter gamma from unity is established whenever the absolute value of the lag coupling times the scalar amplitude stays at most kappa. Researchers deriving small-coupling corrections in Recognition Science gravity would cite this to keep post-Newtonian deviations under explicit control. The proof reduces the claim to the triangle inequality after expanding the linear definition and applying absolute-value properties.
Claim. If $|C_{lag} α| ≤ κ$, then $|γ_{lin}(C_{lag}, α) - 1| ≤ (1/10) κ$, where $γ_{lin}(C_{lag}, α) := 1 + (1/10) C_{lag} α$ and $C_{lag} = φ^{-5}$.
background
The module supplies potential-based PPN definitions that express the gravitational potentials Φ and Ψ in terms of a scalar field ψ together with coupling parameters. The lag coupling is taken from the eight-tick resonance construction and equals φ^{-5} ≈ 0.09, the RS-derived lag coupling. The linearised gamma is defined by the expression 1 + (1/10) C_lag α, which approximates the PPN parameter γ for small scalar amplitudes α.
proof idea
The tactic proof unfolds the definition of gamma_lin, cancels the additive 1, rewrites the absolute value of the product, and finishes with a short calculation that multiplies the hypothesis by the positive constant 1/10.
why it matters
The bound supplies quantitative control on the PPN gamma parameter inside the linearised small-coupling regime of the ILG module. It rests directly on the lag-coupling definition imported from eight-tick resonance and on the linearised gamma expression already present in the same file. No downstream theorems are listed, yet the result closes one of the concrete numerical estimates required for consistency checks against observed post-Newtonian parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.