equivalence_principle_automatic
plain-language theorem explainer
The declaration establishes symmetry of the J-cost function under inversion, showing that inertial mass from the second derivative at unity and gravitational mass from the cost itself arise from the identical unique function. Researchers deriving gravity from ledger defects or recognition-based unification would cite it to ground the equivalence principle in cost uniqueness alone. The proof is a one-line wrapper applying the double-inverse identity to reduce the goal to reflexivity.
Claim. For all real numbers $x > 0$, $J(x) = J(x^{-1})$, where $J(y) = (y + y^{-1})/2 - 1$ is the unique solution to the Recognition Composition Law.
background
The ZeroParameterGravity module derives gravity as large-scale curvature of the ledger lattice induced by J-cost defects, with G-003 asserting that the equivalence principle follows automatically. The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ that solves the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ and possesses a unique minimum at $x=1$ with $J''(1)=1$. Upstream results supply the RS-native gravitational constant $G = lambda_rec^2 c^3 / (pi hbar)$ and the continuum bridge equating the simplicial Laplacian on defect distributions to curvature.
proof idea
The proof proceeds in term mode by introducing the positive real $x$, invoking the lemma inv_inv x to obtain the identity $(x^{-1})^{-1} = x$, and rewriting the right-hand side to reach reflexivity.
why it matters
This result discharges G-003 by showing the equivalence principle is forced by uniqueness of the J-cost under the Recognition Composition Law (T5). It confirms that both notions of mass are computed from the same function, supporting the claim that gravity emerges from defect distributions without extra parameters. The theorem aligns with the eight-tick octave and D=3 forcing while leaving open the explicit continuum limit to the Einstein equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.