Lax Lean Archive

Passing and assigning either truth value

Lax783278.Passes · concepts/Lax783278/Passes.lean · lax-783278

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Lemma 5, in its finite form. Give the two players a shared supply of pp passes, and allow either player to assign either truth value to a selected unassigned variable. Passing consumes one unit of the supply. Play ends as soon as all variables are assigned, with the same satisfaction rule. For every finite supply, this game has the same winner as ordinary positive CNF, including at intermediate positions. A finite supply avoids infinite plays consisting of passes and covers all passes in the reduction graph.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax783278.PositiveCNF
    2
    3/-!
    4---
    5title: Passing and assigning either truth value
    6type: theorem
    7---
    8Lemma 5, in its finite form. Give the two players a shared supply of pp
    9passes, and allow either player to assign either truth value to a selected
    10unassigned variable. Passing consumes one unit of the supply. Play ends
    11as soon as all variables are assigned, with the same satisfaction rule.
    12For every finite supply, this game has the same winner as ordinary positive
    13CNF, including at intermediate positions. A finite supply avoids infinite
    14plays consisting of passes and covers all passes in the reduction graph.
    15-/
    16
    17namespace Lax783278.Passes
    18
    19open PositiveCNF
    20
    21/-- Evaluate the game with passes for a fixed number of remaining rounds.
    22At a True turn one successful move suffices; at a False turn every legal
    23move must preserve True's win. Assignments and passes each use one round. -/
    24def TrueWinsAfter (φ : Formula) : ℕ → Finset (Fin φ.nvars) →
    25 Finset (Fin φ.nvars) → Bool → ℕ → Prop
    26 | 0, _, T, _, _ => Satisfied φ T
    27 | rounds + 1, U, T, trueTurn, passes =>
    28 if U = ∅ then Satisfied φ T
    29 else if trueTurn then
    30 (∃ x ∈ U, ∃ b : Bool,
    31 TrueWinsAfter φ rounds (U.erase x) (if b then insert x T else T) false passes) ∨
    32 (0 < passes ∧ TrueWinsAfter φ rounds U T false (passes - 1))
    33 else
    34 (∀ x ∈ U, ∀ b : Bool,
    35 TrueWinsAfter φ rounds (U.erase x) (if b then insert x T else T) true passes) ∧
    36 (0 < passes → TrueWinsAfter φ rounds U T true (passes - 1))
    37
    38/-- True has a winning strategy with the given supply of passes.
    39There are at most `U.card + passes` moves before all variables are assigned. -/
    40def TrueWins (φ : Formula) (U T : Finset (Fin φ.nvars))
    41 (trueTurn : Bool) (passes : ℕ) : Prop :=
    42 TrueWinsAfter φ (U.card + passes) U T trueTurn passes
    43
    44axiom outcome_equivalent (φ : Formula) (U T : Finset (Fin φ.nvars))
    45 (hd : Disjoint U T) (turn : Bool) (passes : ℕ) :
    46 TrueWins φ U T turn passes ↔ PositiveCNF.TrueWins φ U T turn
    47
    48end Lax783278.Passes
    49
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…