TwoPlayerProfile
plain-language theorem explainer
TwoPlayerProfile defines the space of two-player strategy profiles as pairs of positive real ratios for Alice and Bob. Researchers formalizing game-theoretic equilibria from J-cost minima would reference this structure when building joint cost functions and Nash predicates. The declaration is a bare structure definition with positivity fields and no computational content.
Claim. A two-player strategy profile consists of positive real numbers $r_A > 0$ and $r_B > 0$ denoting the ratios selected by each player.
background
Recognition Science models player costs via the J-cost function, defined as the derived cost from multiplicative recognizers on positive ratios. The module sets up Nash equilibria as profiles minimizing the sum of individual J-costs on the strategy manifold. Upstream results include MultiplicativeRecognizerL4.cost, which supplies the cost as derivedCost on comparators, and ObserverForcing.cost, which equates recognition-event cost to Jcost of the state.
proof idea
The declaration is a structure definition with four fields: alice_ratio and bob_ratio as real numbers together with alice_pos and bob_pos as strict positivity proofs. No lemmas or tactics are applied.
why it matters
It supplies the domain for NashEquilibriumCert, whose fields certify joint-cost non-negativity, zero-cost equivalence to the canonical (1,1) profile, and that the canonical profile is Nash. This fills the algebraic content for the game-theory row deriving equilibria from J-cost minima, consistent with the Recognition Composition Law and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.