Lax Lean Archive

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

The class #P, by witness counting

Lax366625.WitnessCounting · concepts/Lax366625/WitnessCounting.lean · lax-366625

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

    Given a block of second-order relation variables and a first-order sentence φ\varphi over a vocabulary expanded by the block, the witness count of φ\varphi on a structure is the number of assignments of relations to the block under which φ\varphi holds. A counting problem CC over LL is #P-definable when there are a block and a sentence φ\varphi over L∪{≤}L \cup \{\le\} and the block such that, for every nonempty finite LL-structure AA and every linear order on AA, C(A)C(A) is the witness count of φ\varphi on AA with that order: the number of witnesses of an existential second-order sentence, after Saluja, Subrahmanyam, and Thakur. #P is the counting class of the #P-definable problems.

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

    Lean source view on GitHub

    1import Mathlib.SetTheory.Cardinal.Finite
    2import Mathlib.Tactic.FinCases
    3import Mathlib.Order.PiLex
    4import Mathlib.Data.Prod.Lex
    5import Mathlib.Data.Fintype.EquivFin
    6import Mathlib.ModelTheory.Order
    7import Mathlib.ModelTheory.Semantics
    8import Mathlib.ModelTheory.Complexity
    9import Mathlib.Logic.Equiv.Fin.Basic
    10import Mathlib.Data.Fintype.Lattice
    11import Mathlib.Data.Finite.Sigma
    12import Lax366625.CountingProblems
    13import Lax904597.SecondOrder
    14import Lax366625.CountingClasses
    15
    16/-!
    17---
    18title: The class #P, by witness counting
    19type: definition
    20---
    21Given a block of second-order relation variables and a first-order sentence
    22φ\varphi over a vocabulary expanded by the block, the witness count of
    23φ\varphi on a structure is the number of assignments of relations to the
    24block under which φ\varphi holds. A counting problem CC over LL is
    25#P-definable when there are a block and a sentence φ\varphi over
    26L∪{≤}L \cup \{\le\} and the block such that, for every nonempty finite
    27LL-structure AA and every linear order on AA, C(A)C(A) is the witness count
    28of φ\varphi on AA with that order: the number of witnesses of an
    29existential second-order sentence, after Saluja, Subrahmanyam, and Thakur.
    30#P is the counting class of the #P-definable problems.
    31-/
    32
    33namespace Lax366625.WitnessCounting
    34
    35open Lax366625.CountingProblems Lax904597.SecondOrder
    36
    37open FirstOrder
    38
    39open Language Structure
    40
    41section Witness
    42
    43variable {L : Language.{0, 0}}
    44
    45/-- The number of assignments of the block `B` on the structure `A` under which
    46the first-order kernel `φ` holds. -/
    47noncomputable def witnessCount (B : SOBlock) (φ : (L.sum B.lang).Sentence) (A : Type)
    48 [inst : L.Structure A] : ℕ :=
    49 Nat.card {ρ : B.Assignment A //
    50 @Sentence.Realize (L.sum B.lang) A (@sumStructure L B.lang A inst (B.structure ρ)) φ}
    51
    52end Witness
    53
    54section Definable
    55
    56variable {L : Language.{0, 0}} [L.IsRelational]
    57
    58/-- A counting problem is **`#P`-definable** if, on nonempty finite structures,
    59it counts the witnesses of an existential second-order sentence over the
    60ordered expansion: for some block `B` and first-order kernel `φ`, its value is
    61the number of assignments of `B` satisfying `φ`, whatever the linear order of
    62the instance. -/
    63def SharpPDefinable (C : CountingProblem L) : Prop :=
    64 ∃ (B : SOBlock) (φ : ((L.sum Language.order).sum B.lang).Sentence),
    65 ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
    66 C A = witnessCount B φ A
    67
    68end Definable
    69
    70open Lax366625.CountingClasses
    71
    72/-- **#P**: the class of the `#P`-definable counting problems. -/
    73def SharpP : CountingClass :=
    74 CountingClass.ofMem fun C => SharpPDefinable C
    75
    76end Lax366625.WitnessCounting
    77
    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…