gamma_extraction_formula
plain-language theorem explainer
The gamma_extraction_formula supplies the explicit linear expression for the PPN gamma parameter in the ILG model as 1 plus one-tenth alpha times the lag coupling. Researchers working on post-Newtonian expansions inside Recognition Science cite it to obtain a lightweight match to the standard gamma_lin form without pulling in the full PostNewtonian library. The definition is a direct algebraic assignment of the supplied parameters.
Claim. The extraction formula for the PPN parameter gamma is defined by gamma(alpha, C_lag) := 1 + (1/10) alpha C_lag, where C_lag is the lag coupling constant.
background
This definition lives inside the ILG layer of the Relativity module and supplies toy extraction formulas for PPN parameters. The module deliberately keeps the formulas local to avoid heavy dependency edges from the main Relativity file and to replace an earlier Prop := True stub with a concrete certificate. The upstream C_lag result from EightTickResonance supplies the lag coupling as phi to the minus five, approximately 0.09, described as the RS-derived lag coupling.
proof idea
The definition is a one-line wrapper that directly assigns the expression 1 + (1/10) * (alpha * C_lag) using the two real parameters.
why it matters
This definition is the concrete content that lets PPNDerivationHolds assert equality between the ILG linearised PPN functions and the toy extraction formulas after parameter identification. It is invoked inside the ppn_derivation_holds theorem, which discharges the certificate by simplification and commutativity. In the Recognition framework the definition closes a small dependency gap while preserving the eight-tick resonance origin of C_lag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.