Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

PARITY, the parity of a marked subset

Lax945089.Parity · concepts/Lax945089/Parity.lean · lax-945089

definition

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

    Definition

    An instance is a finite set with a marked subset: a structure over the vocabulary with one unary relation. It is a yes-instance of PARITY when the number of marked elements is even; PARITY is the decision problem of the structures isomorphic to such an instance. This is the problem of the classical lower bounds for bounded-depth circuits, as opposed to EVEN, which asks for the parity of the whole universe.

    Concept map
    3 concepts; 12 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Semantics
    2import Mathlib.Data.Set.Card
    3import Mathlib.Algebra.Group.Even
    4import Lax904597.Problems
    5import Lax485149.Problems
    6
    7/-!
    8---
    9title: PARITY, the parity of a marked subset
    10type: definition
    11---
    12An instance is a finite set with a marked subset: a structure over the
    13vocabulary with one unary relation. It is a yes-instance of PARITY when the
    14number of marked elements is even; PARITY is the decision problem of the
    15structures isomorphic to such an instance. This is the problem of the
    16classical lower bounds for bounded-depth circuits, as opposed to EVEN, which
    17asks for the parity of the whole universe.
    18-/
    19
    20namespace Lax945089.Parity
    21
    22open Lax904597.Problems Lax485149.Problems
    23
    24open FirstOrder
    25
    26open FirstOrder.Language
    27
    28/-- The relation symbols of the language. -/
    29inductive markedSetRel : ℕ → Type where
    30/-- `mark x`: the element `x` belongs to the marked subset. -/
    31 | mark : markedSetRel 1
    32 deriving DecidableEq
    33
    34/-- The relational vocabulary of a *marked subset*: a finite set with a
    35distinguished subset of it. -/
    36def markedSet : FirstOrder.Language :=
    37 ⟨fun _ => Empty, markedSetRel⟩
    38
    39instance instIsRelationalMarkedSet : FirstOrder.Language.IsRelational markedSet := fun _ =>
    40 (inferInstance : IsEmpty Empty)
    41
    42/-- `mark x`: the element `x` belongs to the marked subset. -/
    43abbrev markedSetMark : markedSet.Relations 1 :=
    44 .mark
    45
    46open FirstOrder
    47
    48open Language Structure
    49
    50section Problem
    51
    52variable (A : Type) [markedSet.Structure A]
    53
    54/-- The marked subset of a structure. -/
    55def Marked : Set A :=
    56 {x : A | RelMap markedSetMark ![x]}
    57
    58end Problem
    59
    60/-- PARITY: is the marked subset of even size? -/
    61def PARITY : DecisionProblem markedSet :=
    62 DecisionProblem.ofPred fun A _ => Even (Marked A).ncard
    63
    64end Lax945089.Parity
    65
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…