Jcost_one_plus_eps
The algebraic identity equates the J-cost at a unit-scale perturbation to a rational quadratic in the perturbation size. Vortex-stretching analysts cite it when deriving dissipation bounds inside discrete Navier-Stokes operators. The proof is a direct algebraic reduction: unfold the Jcost definition, clear the nonzero denominator, and normalize via field simplification and ring.
claimFor every real number $eps$ with $eps geq 0$, $J(1 + eps) = frac{eps^2}{2(1 + eps)}$, where $J$ is the J-cost function satisfying the Recognition Composition Law.
background
The J-cost function is defined by $J(x) = (x + x^{-1})/2 - 1$ and obeys the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. In the Vortex-Stretching module this supplies the exact cost of a scale perturbation near unity, which is required for viscous-dissipation estimates. The module replaces three former sorry markers with complete proofs drawn from Thapa & Washburn (2026), Washburn & Zlatanovic (2026), and Pardo-Guerra et al. (2026). Upstream results on collision-free programs and simplicial edge lengths ensure the algebraic steps remain inside the self-referential forcing chain.
proof idea
Unfold the definition of Jcost. Apply linarith to obtain the nonzero hypothesis $1 + eps neq 0$. Invoke field_simp to clear the denominator, then finish with ring to reach the target rational expression.
why it matters in Recognition Science
The identity is the exact base case for the sibling inequality Jcost_one_plus_eps_le_sq, which in turn feeds the master absorption theorem and the exponential vorticity decay result. It closes one of the three analytic gaps listed in the module documentation and supplies the quadratic control on perturbation cost needed for the viscous-rate bounds inside the eight-tick octave structure. The step aligns with the canonical reciprocal cost uniqueness established in Washburn & Zlatanovic (2026).
scope and limits
- Does not prove the inequality Jcost(1+eps) le eps^2/2.
- Does not apply when eps is negative.
- Does not incorporate viscousRate or pair_budget_factored_bound.
- Does not address higher-order terms on the phi-ladder.
Lean usage
rw [Jcost_one_plus_eps heps]formal statement (Lean)
72theorem Jcost_one_plus_eps {eps : ℝ} (heps : 0 ≤ eps) :
73 Jcost (1 + eps) = eps ^ 2 / (2 * (1 + eps)) := by
proof body
Tactic-mode proof.
74 unfold Jcost
75 have hne : (1 : ℝ) + eps ≠ 0 := by linarith
76 field_simp [hne]; ring
77
78/-- J(1+eps) <= eps^2/2 for eps >= 0.
79
80Proof: eps^2/(2*(1+eps)) <= eps^2/2 because 1+eps >= 1 and the numerator
81is nonneg. -/