ppn_derivation_holds
plain-language theorem explainer
The theorem certifies that the toy extraction formulas for the post-Newtonian parameters γ and β coincide exactly with the linearised ILG expressions gamma_lin and beta_lin once the order of α and C_lag is swapped. A researcher checking consistency between scalar-tensor weak-field expansions and standard PPN linearisation would cite this algebraic identity. The proof is a short term-mode construction that intros the two real parameters and applies simp to discharge both conjuncts via commutativity of multiplication.
Claim. For all real numbers $α$ and $C_{lag}$, the gamma extraction formula equals the linearised $γ$ and the beta extraction formula equals the linearised $β$.
background
The module supplies local toy extraction formulas for the PPN parameters, deliberately isolated from the full Post-Newtonian stack. C_lag is the RS-derived lag coupling defined as $φ^{-5} ≈ 0.09$. The linearised functions are gamma_lin(C_lag, α) = 1 + (1/10) C_lag α and beta_lin(C_lag, α) = 1 + (1/20) C_lag α, while the extraction formulas are written with arguments in the order α C_lag. PPNDerivationHolds is the model-level certificate asserting that these two pairs of expressions agree for every real α and C_lag.
proof idea
The term proof intros α and C_lag, applies constructor to split the conjunction, then uses simp on gamma_extraction_formula together with gamma_lin and the multiplication commutativity lemmas to verify the first equality; the same pattern with beta_extraction_formula and beta_lin dispatches the second equality.
why it matters
This declaration discharges the previous Prop := True stub for PPNDerivationHolds with an explicit algebraic certificate, confirming that the ILG linearised PPN parameters reproduce the standard weak-field forms. It supports the Recognition Science claim that the eight-tick resonance and lag coupling C_lag = φ^{-5} recover conventional post-Newtonian coefficients in the linear regime. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.