beta_bound_small
plain-language theorem explainer
The bound controls the deviation of the linearized PPN beta from 1 whenever the absolute value of the product of the lag coupling and the scalar parameter stays at most kappa. Workers deriving post-Newtonian observables from the Recognition Science action would reference it to keep the scalar perturbation small enough for consistency with general relativity. Substitution of the explicit linear form, followed by factoring the absolute value and applying monotonicity of multiplication by a positive constant, completes the argument.
Claim. If $|C_{rm lag} alpha| leq kappa$, then $|beta - 1| leq (1/20) kappa$, where $beta$ denotes the linearized post-Newtonian parameter given explicitly by $1 + (1/20) C_{rm lag} alpha$.
background
The ILG module supplies potential-based definitions for the post-Newtonian parameters that enter the parametrized post-Newtonian formalism. These are constructed from the scalar field psi together with the coupling parameters appearing in the underlying action. The lag coupling equals phi to the power minus five and originates in the eight-tick resonance construction; it supplies the numerical strength of the time-lag term. The auxiliary linear expression supplies the first-order correction to the beta parameter in the small-coupling regime.
proof idea
The proof unfolds the linear expression to obtain 1 plus one-twentieth times the product, cancels the leading 1, and rewrites the absolute value via the product rule. It then applies the hypothesis together with the lemma mul_le_mul_of_nonneg_left to bound the result by one-twentieth times kappa, using norm_num for the coefficient arithmetic.
why it matters
This result supplies the small-coupling control on the beta parameter required for the PPN expansion in the ILG framework to remain close to general relativity. It closes one step in the chain that extracts observable parameters from the Recognition Composition Law and the forced value of the lag coupling. No immediate downstream theorems are recorded, yet the bound supports overall consistency of the phi-ladder with weak-field tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.