pith. machine review for the scientific record. sign in
def definition def or abbrev high

cert

show as:
view Lean formalization →

The cert definition packages four lemmas into a single CoalitionSizeCert structure asserting that in three-dimensional configuration space there are exactly seven coalition types with a minimum winning coalition of size four. Game theorists applying Riker's size principle to dimensional models would reference this certificate when verifying the 2^D-1 count law at D=3. It is assembled by direct substitution of the four sibling theorems totalCoalitionTypes_eq, mwcSize_eq, mwcSize_le_half and mwcSize_pos.

claimLet $C$ be the structure with fields total_eq : totalCoalitionTypes = 7, mwc_eq : mwcSize = 4, mwc_le_half : $2$ mwcSize $leq$ totalCoalitionTypes + 1, mwc_pos : $0 <$ mwcSize. Then cert is the instance of $C$ with total_eq witnessed by totalCoalitionTypes_eq, mwc_eq by mwcSize_eq, mwc_le_half by mwcSize_le_half, and mwc_pos by mwcSize_pos.

background

In the GameTheory module, configDim is fixed at three, so totalCoalitionTypes unfolds to $2^3 - 1 = 7$ distinct coalition types while mwcSize is defined as ceil($2^{D-1}$) = 4. CoalitionSizeCert is the record type requiring exactly these four field proofs: equality of the total, equality of the minimum winning size, the half-bound inequality, and positivity of the size. The upstream lemmas totalCoalitionTypes_eq, mwcSize_eq, mwcSize_le_half and mwcSize_pos each reduce the claim to norm_num after unfolding the dimension-dependent definitions.

proof idea

This is a one-line wrapper that constructs the CoalitionSizeCert record by assigning its four fields directly to the sibling theorems totalCoalitionTypes_eq, mwcSize_eq, mwcSize_le_half and mwcSize_pos.

why it matters in Recognition Science

This definition completes the structural theorem for coalition sizes predicted by the Recognition Science forcing chain at T8 (D = 3) and the 2^D - 1 count law. It packages the D = 3 case of Riker's size principle inside the eight-tick octave, supplying a concrete certificate that can be cited when deriving minimum winning coalitions from the phi-ladder geometry. No downstream uses appear yet, leaving open its insertion into larger game-theoretic derivations.

scope and limits

formal statement (Lean)

  73noncomputable def cert : CoalitionSizeCert where
  74  total_eq := totalCoalitionTypes_eq

proof body

Definition body.

  75  mwc_eq := mwcSize_eq
  76  mwc_le_half := mwcSize_le_half
  77  mwc_pos := mwcSize_pos
  78

depends on (5)

Lean names referenced from this declaration's body.