JEquilibriumUniversalityCert
plain-language theorem explainer
The universality certificate packages three propositions each stating that the J-cost vanishes at unity into one structure that also records their identity and a shared positivity condition away from the fixed point. A researcher unifying equilibrium concepts across game theory, economics, and biology would cite it when demonstrating that Nash, market-clearing, and homeostatic equilibria are the same algebraic object. The structure is assembled directly from three sibling definitions and two lemmas that establish the equality of the three cases
Claim. A J-equilibrium universality certificate consists of three propositions $N$, $M$, $H$ each asserting $J(1)=0$, the conjunction $N=M=M=H$, and the predicate that $J(r)>0$ for every real $r>0$ with $r≠1$, where $J$ denotes the J-cost functional.
background
In the Recognition Science setting the J-cost functional satisfies $J(1)=0$ at its unique fixed point. Module C7 shows that this single algebraic fact serves as the equilibrium condition in three a priori distinct domains. NashEquilibrium is the proposition $J(1)=0$ labelled for game-theoretic payoffs; MarketEquilibrium and HealthEquilibrium are the identical proposition labelled for efficient markets and for biological homeostasis. The upstream definitions each specialise the core Jcost-unit lemma to a domain label while the lemmas all_three_equal and shared_sensitivity supply the equality and the perturbation positivity.
proof idea
The declaration is a structure definition with no proof body. It directly assembles the three equilibrium propositions from the sibling definitions NashEquilibrium, MarketEquilibrium, and HealthEquilibrium together with the two lemmas that witness their identity and the shared sensitivity condition.
why it matters
The structure supplies the single universality witness required by the downstream definition jEquilibriumUniversalityCert. It thereby closes the C7 claim that the same theorem Jcost 1 = 0 is the equilibrium condition across Nash, market, and health models. In the broader framework this realises the Recognition Composition Law at the level of equilibria, confirming that the eight-tick octave produces a domain-independent sensitivity at the fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.