minimum_at_one
The theorem establishes that the J-cost function on positive reals attains its global minimum of zero at argument one. Cross-domain modelers in hydrodynamics, medicine, and game theory cite it to guarantee that any deviation from equilibrium incurs positive cost. The term proof proceeds by rewriting the unit value, splitting into equality and inequality cases, and invoking the strict positivity lemma for the latter.
claimFor every real number $r > 0$, $J(1) = 0$ and $J(1) ≤ J(r)$, where $J$ is the J-cost function satisfying $J(r) > 0$ for all $r ≠ 1$.
background
The J-cost function is defined in the Cost module as $J(r) = (r-1)^2/(2r)$ for $r > 0$, with the property that it vanishes at unity and is positive elsewhere. This theorem sits in the CrossDomain module under the C16 universality claim, which extends the equilibrium result C7 by showing the same positivity source applies uniformly across specialized domains. Upstream lemmas establish the explicit squared form and the strict inequality for unequal arguments.
proof idea
The proof opens by fixing a positive real r and rewriting the target inequality using the fact that Jcost at one equals zero. It then performs case analysis on whether r equals one; the equality case is immediate by substitution, while the strict inequality case applies the positivity lemma Jcost_pos_of_ne_one to obtain the desired comparison.
why it matters in Recognition Science
This result supplies the core inequality for the jPositivityUniversalityCert definition, which packages the positivity statement for turbulent cost, disease cost, off-target cost, and related cross-domain instances. It completes the structural claim C16 that a single lemma generates non-equilibrium cost in every RS domain. The parent chain step is the extension of C7 to off-equilibrium settings, with no open scaffolding remaining.
scope and limits
- Does not derive the closed-form expression for the J-cost function.
- Does not extend the domain to non-positive reals.
- Does not quantify the rate of growth away from unity.
- Does not connect directly to the Recognition Composition Law.
formal statement (Lean)
70theorem minimum_at_one : ∀ r : ℝ, 0 < r → Jcost 1 ≤ Jcost r := by
proof body
Term-mode proof.
71 intro r hr
72 rw [Jcost_unit0]
73 rcases eq_or_ne r 1 with heq | hne
74 · rw [heq, Jcost_unit0]
75 · exact le_of_lt (Jcost_pos_of_ne_one r hr hne)
76