beta_bound
plain-language theorem explainer
beta_bound supplies an illustrative solar-system bound |β − 1| ≤ 10^{-5} on the post-Newtonian parameter β inside the linearized ILG model. Researchers auditing consistency between the Recognition-derived lag coupling and weak-field gravity tests would cite it. The proof is a one-line term wrapper that substitutes the constant definition of beta and reduces the claim to the trivial numerical inequality 0 ≤ 1/100000.
Claim. $ |β(C_{lag}, α) − 1| ≤ 10^{-5} $, where β is the post-Newtonian parameter set identically to 1 in the small-coupling linearized model.
background
The module supplies potential-based PPN definitions as a scaffold that expresses γ and β in terms of the potentials Φ and Ψ derived from the scalar field ψ together with the coupling parameters. Upstream, C_lag is fixed at φ^{-5} ≈ 0.09 by the eight-tick resonance construction. The local beta definition is the constant function returning 1 for any real inputs C_lag and α. This stands in contrast to the thermodynamic inverse-temperature beta = 1/(k_B T) appearing in the partition-function module.
proof idea
The proof is a one-line term-mode wrapper. It invokes simpa with the beta definition to replace the left-hand side by |1 − 1|, then applies norm_num to confirm the resulting inequality 0 ≤ 1/100000 holds.
why it matters
The declaration closes the illustrative bound for the PPN β parameter within the linearized ILG section. It confirms that the constant definition remains compatible with solar-system constraints once the lag coupling C_lag = φ^{-5} is inserted. The result sits inside the broader Recognition Science forcing chain that fixes D = 3 and the eight-tick octave, yet carries no downstream dependencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.