ep_relative_error
plain-language theorem explainer
The definition computes the relative error between the quadratic approximation to the J-cost and the exact J-cost for a real deviation parameter ε. A researcher deriving the equivalence principle from a single cost function would cite it to bound the approximation quality in the small-deviation regime. The definition is a direct algebraic ratio of the two J-cost expressions.
Claim. The relative error is defined by $r(ε) = (J_2(ε) - J(ε))/J(ε)$ where $J(x) = (x + x^{-1})/2 - 1$ is the unique cost function, $J_2$ is its quadratic truncation near $x=1$, and $ε$ is the real deviation from equilibrium.
background
The module derives the equivalence principle from the uniqueness of the cost function $J(x) = ½(x + x^{-1}) - 1$. Inertial mass is the second derivative $J''(1) = 1$ extracted from the quadratic term for small ledger deviations $x = 1 + ε$. Gravitational mass is the integrated J-cost defect that sources curvature. Both quantities are therefore functionals of the identical $J$, so they coincide for any body. Upstream structures calibrate $J$ via ledger factorization and phi-forcing, confirming the single-source property.
proof idea
One-line definition that subtracts the quadratic J-cost from the exact J-cost and normalizes by the exact value.
why it matters
The definition quantifies the O(ε⁴) truncation error that appears when the quadratic approximation is used for inertial mass. It supports the claim that the equivalence principle is a tautology once both masses are extracted from the same unique J (T5). No downstream theorems are recorded, but the quantity is referenced in sibling statements that establish ratio unity under single-source mass theories.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.