all_three_equal
plain-language theorem explainer
The theorem shows that the Nash equilibrium proposition, the market equilibrium proposition, and the health equilibrium proposition are identical because each expands to the same statement Jcost 1 = 0. Cross-domain modelers would cite it to justify transferring perturbation multipliers from game theory to economics or biology without re-derivation. The proof is a direct reflexivity application on the shared definition.
Claim. The proposition that the J-cost vanishes at unit scale, specialized to the Nash domain, equals the corresponding market-domain proposition and the health-domain proposition: $J_1=0$ (Nash) $= J_1=0$ (market) and $J_1=0$ (market) $= J_1=0$ (health).
background
The module introduces three propositions, each defined as the statement Jcost 1 = 0. NashEquilibrium, MarketEquilibrium, and HealthEquilibrium are therefore literally the same Prop in Lean. This construction sits inside the C7 universality claim that a single equilibrium condition Jcost_unit0 applies across game theory, efficient-market clearing, and homeostatic regulation.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity twice. Because the three named propositions are definitionally equal to Jcost 1 = 0, the conjunction of their pairwise identities holds by rfl.
why it matters
The result populates the three_are_one field of the JEquilibriumUniversalityCert structure, which certifies the module's claim that sensitivity at equilibrium is shared. It instantiates the T5 J-uniqueness result in a cross-domain setting and supports the downstream transfer of the Hessian multiplier across the three fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.