gamma_bound
plain-language theorem explainer
gamma_bound establishes that the PPN parameter γ in the ILG model satisfies the solar-system observational bound |γ − 1| ≤ 10^{-5}. Researchers testing general relativity via solar-system dynamics or PPN expansions would reference this result for model consistency. The proof proceeds by simplifying the expression for γ using its definition to zero and verifying the trivial inequality with norm_num.
Claim. $|γ(C_{lag}, α) - 1| ≤ 1/100000$, where γ is the post-Newtonian parameter in the ILG potential-based formalism with lag coupling $C_{lag}$ and model parameter α.
background
The module supplies potential-based definitions for the parametrized post-Newtonian (PPN) formalism in the ILG setting, constructing gravitational potentials Φ and Ψ from the field ψ and input parameters. The local γ denotes the standard PPN γ coefficient, which equals 1 exactly in general relativity. Upstream results supply the lag coupling $C_{lag} = φ^{-5} ≈ 0.09$ from eight-tick resonance and the Euler-Mascheroni constant as a separate numerical constant.
proof idea
Term-mode proof that applies the definition of gamma to reduce the left-hand side to zero, then invokes norm_num to confirm the inequality 0 ≤ 1/100000 holds.
why it matters
The result confirms that the ILG construction meets the tight solar-system bound on the PPN γ parameter, aligning with Recognition Science landmarks such as the eight-tick octave and D = 3 spatial dimensions. It serves as a consistency check within the PPN module but has no listed downstream dependents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.