gamma_lin
The linearised expression for the PPN gamma parameter supplies 1 plus one tenth times the product of the lag coupling and scalar coupling alpha. Researchers deriving post-Newtonian limits from Recognition Science models cite this definition when matching to solar system constraints. It is a direct algebraic definition that serves as the base for bound theorems and derivation certificates.
claimThe linearised PPN parameter satisfies $gamma_lin(C_lag, alpha) = 1 + (1/10) C_lag alpha$, where $C_lag = phi^{-5}$ is the RS-derived lag coupling.
background
The module establishes potential-based PPN definitions that express the parameters in terms of the gravitational potentials Phi and Psi obtained from the scalar field psi and the coupling parameters. The lag coupling is supplied by the upstream definition C_lag equals phi to the power of negative five, approximately 0.09, which encodes the RS-derived lag from the eight-tick resonance. This definition operates inside the scaffold for linearised expansions that connect the ILG action to standard PPN forms.
proof idea
This declaration is a one-line definition that directly encodes the linear approximation for small scalar coupling alpha. It applies the constant lag coupling from the EightTickResonance module with no further reduction or lemma application.
why it matters in Recognition Science
This definition is used by the bound theorem that controls |gamma minus 1| for small couplings and by the derivation certificate that verifies the ILG linearised functions match the extraction formulas. It fills the PPN scaffold in the Relativity.ILG module and connects to the Recognition Science constants with C_lag equal to phi to the negative five. It supports matching to the alpha band and the phi-ladder structure.
scope and limits
- Does not derive the full nonlinear PPN coefficients beyond the linear term.
- Does not fix the value of the scalar coupling alpha outside the small-coupling regime.
- Does not incorporate the complete ILG action or higher-order potentials.
formal statement (Lean)
40noncomputable def gamma_lin (C_lag α : ℝ) : ℝ := 1 + (1/10 : ℝ) * (C_lag * α)
proof body
Definition body.
41
42/-- Linearised β with small scalar coupling. -/