ep_relative_error
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the error scales as O(ε⁴).
- Does not define the explicit forms of the quadratic or exact J-cost.
- Does not extend to large deviations from equilibrium.
- Does not compare inertial and gravitational masses directly.
formal statement (Lean)
163def ep_relative_error (eps : ℝ) : ℝ :=
proof body
Definition body.
164 (Jcost_quadratic eps - Jcost_exact eps) / Jcost_exact eps
165
166/-- For the EP, what matters is NOT the size of corrections, but whether
167 they affect inertial and gravitational mass DIFFERENTLY.
168 In SingleSourceMassTheory, they cannot differ: both use J_full. -/