all_seven_are_one
plain-language theorem explainer
The theorem establishes that seven domain-labeled non-equilibrium cost predicates are definitionally identical. Cross-domain researchers cite it to treat turbulence, disease deviation, arbitrage gaps, and cognitive biases as instances of one J-cost positivity statement. The proof is a term-mode 6-tuple of reflexivity steps on the shared definitional expansion.
Claim. The seven predicates are identical: TurbulentCost = DiseaseCost = OffTargetCost = OffEquilibriumGameCost = MarketArbitrageGap = BiasedReasoningCost = RecognitionDeficit, where each asserts that $J(r) > 0$ for every real $r > 0$ with $r ≠ 1$.
background
Module C16 records the off-equilibrium extension of the equilibrium result C7. Each predicate is defined identically as the proposition ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r. These labels specialize the same statement to turbulent flow, disease (homeostasis deviation), CRISPR off-target effects, non-equilibrium games, market arbitrage, biased reasoning, and recognition deficit. The upstream lemma Jcost_pos_of_ne_one supplies the positivity fact that all seven predicates invoke.
proof idea
The proof is a term proof that constructs a 6-tuple of reflexivity proofs. Because each of the seven definitions expands to the identical expression built from Jcost_pos_of_ne_one, Lean reduces every equality to rfl.
why it matters
The result completes the universality claim of C16 by showing that domain labels add no distinct mathematical content. It supplies the equality needed for the downstream certificate jPositivityUniversalityCert. In the Recognition framework it unifies the off-equilibrium case of J-uniqueness (T5) across applications while preserving the same phi-ladder and eight-tick structure that yields D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.