beta_extraction_formula
The beta_extraction_formula supplies the explicit linear expression for the PPN beta parameter in the ILG toy model. Researchers checking consistency between the linearized ILG functions and standard PPN forms would cite it when closing the previous Prop := True stub. It is realized as a direct algebraic definition that inserts the coefficient 1/20 in front of the product alpha times C_lag.
claim$beta(alpha, C_lag) := 1 + (1/20) alpha C_lag$, where $alpha$ is the model parameter and $C_lag = phi^{-5}$ is the lag coupling constant from the eight-tick resonance.
background
The module supplies local toy extraction formulas for PPN parameters to avoid heavy dependency edges from the full Post-Newtonian stack. The upstream Model structure from LawOfExistence carries the constants C together with defectMass, orthoMass, energyGap and tests maps. C_lag is imported from EightTickResonance and defined as phi to the power of negative five, approximately 0.09.
proof idea
The declaration is a direct noncomputable definition that returns the expression 1 + (1/20) * (alpha * C_lag). No lemmas or tactics are invoked; the body is the literal algebraic assignment that matches the coefficient required by the downstream matching statement.
why it matters in Recognition Science
This definition completes one conjunct of the PPNDerivationHolds certificate used by the theorem ppn_derivation_holds. It replaces an earlier stub proposition in the ILG layer and thereby certifies that the linearized PPN functions agree with the toy formulas after parameter identification. The construction sits inside the Recognition Science post-Newtonian limit that inherits the eight-tick octave and phi-ladder structure.
scope and limits
- Does not derive the full nonlinear PPN parameters.
- Does not compute numerical values or observational comparisons.
- Does not import or depend on the complete Post-Newtonian stack.
- Does not establish the origin of alpha or C_lag from deeper axioms.
formal statement (Lean)
18noncomputable def beta_extraction_formula (α C_lag : ℝ) : ℝ :=
proof body
Definition body.
19 1 + (1/20 : ℝ) * (α * C_lag)
20
21/-- Model-level “certificate”: the ILG linearised PPN functions match the toy extraction
22formulas after identifying parameter order. -/