jPositivityUniversalityCert
plain-language theorem explainer
The declaration assembles seven domain-specific instances of J-cost positivity into one certificate record. Cross-domain researchers in hydrodynamics, medicine, game theory, finance, and cognition cite it to confirm that every off-equilibrium cost reduces to the same inequality on the J function. The construction is a direct record literal that wires each field to its specialized theorem.
Claim. Let $J$ be the J-cost function. The certificate asserts that $J(r)>0$ for all $r>0$ with $r≠1$, that this statement is identical across the seven domains (turbulent flow, disease deviation from homeostasis, off-target CRISPR effects, off-equilibrium games, market arbitrage, biased reasoning, and recognition deficit), that $J$ attains its global minimum of zero at $r=1$, and that symmetry holds at equilibrium.
background
JPositivityUniversalityCert is the structure that collects the seven domain propositions, each defined as the universal statement $∀ r:ℝ, 0<r → r≠1 → 0<Jcost r$. The module doc states that this is the off-equilibrium analogue of C7 and that all seven propositions are definitionally the same. The upstream theorem all_seven_are_one proves the equality chain among the seven propositions. Each individual cost theorem (disease_cost, market_arbitrage_gap, etc.) is obtained by applying the core lemma Jcost_pos_of_ne_one.
proof idea
The definition is a one-line record construction. It populates the seven domain fields by direct reference to the corresponding theorems (turbulent_cost, disease_cost, …), the equality field by all_seven_are_one, the minimum field by minimum_at_one, and the symmetry field by symmetry_at_equilibrium. No further tactics are required.
why it matters
This definition completes the C16 claim that J-cost positivity is universal across domains. It extends the equilibrium result C7 (Jcost(1)=0) by showing that the same lemma Jcost_pos_of_ne_one supplies the cost in every listed application. In the Recognition framework it illustrates how the J-uniqueness property forces non-zero cost away from the fixed point r=1 in hydrodynamics, biology, economics, and cognition alike.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.