PPNDerivationHolds
plain-language theorem explainer
This definition supplies the model-level certificate that the toy extraction formulas for the post-Newtonian parameters γ and β coincide with the linearised ILG expressions once parameter ordering is identified. Researchers verifying consistency between the ILG layer and standard PPN expansions in modified gravity would cite it to close an earlier trivial stub. The body is the universal quantification over real α and C_lag together with the conjunction of the two equalities.
Claim. The proposition that for all real numbers α and C_lag, the toy extraction formula γ_extraction(α, C_lag) equals the linearised γ_lin(C_lag, α) and the toy extraction formula β_extraction(α, C_lag) equals the linearised β_lin(C_lag, α), where γ_extraction(α, C_lag) := 1 + (1/10)α C_lag, β_extraction(α, C_lag) := 1 + (1/20)α C_lag, γ_lin(C_lag, α) := 1 + (1/10)C_lag α and β_lin(C_lag, α) := 1 + (1/20)C_lag α.
background
In the ILG layer the lag coupling is fixed by C_lag := φ^{-5} from the eight-tick resonance construction. The linearised PPN functions are gamma_lin(C_lag, α) := 1 + (1/10)C_lag α and beta_lin(C_lag, α) := 1 + (1/20)C_lag α. The toy extraction formulas are defined identically except for multiplication order: gamma_extraction_formula(α, C_lag) := 1 + (1/10)α C_lag and beta_extraction_formula(α, C_lag) := 1 + (1/20)α C_lag. The module documentation states that these local definitions replace an earlier Prop := True stub while avoiding heavy dependence on the full Post-Newtonian stack.
proof idea
As a definition the body is simply the required universal statement. The downstream theorem ppn_derivation_holds discharges it by introducing α and C_lag, splitting the conjunction, and applying simp to each conjunct with mul_comm, mul_left_comm and mul_assoc to equate the swapped products.
why it matters
The definition supplies the explicit certificate that feeds the theorem ppn_derivation_holds and thereby eliminates the previous trivial stub in the ILG layer. It keeps the relativity module lightweight by remaining local to the linearised small-coupling regime without invoking the full eight-tick octave or spatial-dimension derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.