Lax Lean Archive

Passing and assigning either truth value

Lax689614.Passes · concepts/Lax689614/Passes.lean · lax-689614

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 Lax689614.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 Lax689614.Passes
    18
    19open PositiveCNF
    20
    21def TrueWins (φ : Formula) (U T : Finset (Fin φ.nvars))
    22 (trueTurn : Bool) (passes : ℕ) : Prop :=
    23 if U = ∅ then Satisfied φ T
    24 else if trueTurn then
    25 (∃ x : U, ∃ b : Bool,
    26 TrueWins φ (U.erase x.val) (if b then insert x.val T else T) false passes) ∨
    27 (∃ _h : 0 < passes, TrueWins φ U T false (passes - 1))
    28 else
    29 (∀ x : U, ∀ b : Bool,
    30 TrueWins φ (U.erase x.val) (if b then insert x.val T else T) true passes) ∧
    31 (∀ _h : 0 < passes, TrueWins φ U T true (passes - 1))
    32termination_by U.card + passes
    33decreasing_by
    34 all_goals first
    35 | have := Finset.card_erase_lt_of_mem x.property; omega
    36 | omega
    37
    38axiom outcome_equivalent (φ : Formula) (U T : Finset (Fin φ.nvars))
    39 (hd : Disjoint U T) (turn : Bool) (passes : ℕ) :
    40 TrueWins φ U T turn passes ↔ PositiveCNF.TrueWins φ U T turn
    41
    42end Lax689614.Passes
    43
    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…