canonical_is_nash
The canonical strategy profile with both players at ratio 1 is a Nash equilibrium under joint J-cost: its cost is minimal against any unilateral deviation. Game theorists working from Recognition Science first principles cite this to anchor equilibrium at the J-minimum on the strategy simplex. The proof is a direct term reduction that unfolds the profile and joint cost then invokes non-negativity of the sum of individual J-costs.
claimLet $p$ be the two-player profile with both strategy ratios equal to 1. Then for every alternative profile $q$, the joint J-cost of $p$ is at most the joint J-cost of $q$, where the joint J-cost of a profile is the sum of the individual $J$-costs and $J(x) = (x-1)^2/(2x)$.
background
In this module the cost of a strategy is the J-functional $J(x) = (x-1)^2/(2x)$, which vanishes exactly at the unit ratio. The joint J-cost of a profile is the sum of the two players' individual J-costs. The Nash predicate states that a profile $p$ is an equilibrium precisely when its joint J-cost is minimal over all alternative profiles $q$ on the strategy simplex. The canonical profile is the concrete point where both ratios equal 1. The module sits inside the Recognition Science derivation of game theory from the J-functional, where equilibria are identified with joint minima of this non-negative cost.
proof idea
The term proof introduces an arbitrary profile $q$, unfolds the definitions of canonicalProfile and jointJCost, simplifies the resulting expression with the lemma that Jcost at 1 is zero, and finishes by applying the theorem that joint J-cost is always non-negative.
why it matters in Recognition Science
This theorem supplies the canonical_nash field inside the master NashEquilibriumCert certificate. It completes the algebraic verification that the joint J-minimum is attained at the canonical profile, thereby closing the structural existence argument for Nash equilibria in the Recognition Science game-theory development. The result rests on the non-negativity of J-cost that follows from the Recognition Composition Law and feeds directly into the master certificate that packages non-negativity, zero-iff-canonical, and Nash stability together.
scope and limits
- Does not prove Nash equilibria exist for games with more than two players.
- Does not show that the canonical profile is the unique equilibrium.
- Does not treat continuous or infinite strategy spaces beyond the ratio simplex.
- Does not derive the J-functional or the Recognition Composition Law.
formal statement (Lean)
89theorem canonical_is_nash : isNashEquilibrium canonicalProfile := by
proof body
Term-mode proof.
90 intro q
91 unfold canonicalProfile jointJCost
92 simp [Jcost_unit0]
93 exact jointJCost_nonneg q
94
95/-! ## Master certificate -/
96
97/-- **NASH EQUILIBRIUM MASTER CERTIFICATE.** -/