Jcost_additive_leading
plain-language theorem explainer
The theorem states that J-cost applied to the combined strain 1 + ε₁ + ε₂ equals the exact quadratic expression (ε₁ + ε₂)² / (2(1 + ε₁ + ε₂)) whenever each strain and their sum exceed -1. Researchers decomposing total J-cost into per-strain contributions in weak-field gravity models would cite this when isolating the leading quadratic term before cross corrections. The proof reduces directly to the single-strain exact identity by substituting the summed argument.
Claim. For real numbers $ε_1, ε_2$ with $ε_1 > -1$, $ε_2 > -1$ and $ε_1 + ε_2 > -1$, $J(1 + ε_1 + ε_2) = (ε_1 + ε_2)^2 / (2(1 + ε_1 + ε_2))$.
background
J-cost is the function satisfying the exact identity J(1 + ε) = ε² / (2(1 + ε)) for ε > -1; this identity bridges J-cost to the Hamiltonian, where kinetic energy approximates ε²/2. The declaration lives in the weak-field superposition module of the gravity section, where strains ε represent small metric perturbations and additive decomposition of total J-cost is required before cross terms are isolated. It depends on the upstream theorem Jcost_one_plus_exact, which proves the single-strain formula by unfolding the definition and applying field_simp under the positivity hypothesis.
proof idea
The proof is a one-line wrapper that applies the exact identity Jcost_one_plus_exact to the summed strain ε₁ + ε₂, discharging the positivity hypothesis h12 directly.
why it matters
This result confirms that the leading quadratic term in J-cost remains exact under addition of strains, supporting the additive decomposition step in the weak-field regime before the O(ε₁ ε₂) cross term is extracted in sibling declarations. It aligns with the Recognition Science treatment of J-cost as the cost functional whose quadratic leading term matches kinetic energy in gravity models. No open questions or scaffolding are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.