Lax Lean Archive

Accepting local views of a proof

Lax323828.LocalTests · concepts/Lax323828/LocalTests.lean · lax-323828

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

    Fix a proof with mm Boolean positions and a set of rr random choices. A local view is a partial assignment to proof positions. For each random choice, a finite list of accepting local views specifies a test: a proof passes when it extends at least one of those views.

    This is the finite combinatorial data extracted from a verifier on a fixed input. A local view records every queried position and its answer, including positions chosen adaptively. No running-time assertion is built into this data. Uniform computation of the lists is a separate obligation.

    Concept map
    1 concept; 9 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Data.Fintype.Pi
    2import Mathlib.Data.Fintype.Option
    3import Mathlib.Data.Finset.Lattice.Fold
    4
    5/-!
    6---
    7title: Accepting local views of a proof
    8type: definition
    9---
    10Fix a proof with mm Boolean positions and a set of rr random choices.
    11A local view is a partial assignment to proof positions. For each random
    12choice, a finite list of accepting local views specifies a test: a proof
    13passes when it extends at least one of those views.
    14
    15This is the finite combinatorial data extracted from a verifier on a fixed
    16input. A local view records every queried position and its answer, including
    17positions chosen adaptively. No running-time assertion is built into this
    18data. Uniform computation of the lists is a separate obligation.
    19-/
    20
    21namespace Lax323828.LocalTests
    22
    23open scoped Classical
    24
    25/-- A complete Boolean proof with `m` positions. -/
    26abbrev Oracle (m : ℕ) := Fin m → Bool
    27/-- A partial proof; `none` means that the position is not queried. -/
    28abbrev View (m : ℕ) := Fin m → Option Bool
    29
    30/-- The complete proof agrees with every specified answer in the local view. -/
    31def Extends {m : ℕ} (π : Oracle m) (a : View m) : Prop :=
    32 ∀ i b, a i = some b → π i = b
    33
    34/-- The two partial views agree at all positions where both specify an answer. -/
    35def Compatible {m : ℕ} (a b : View m) : Prop :=
    36 ∀ i x y, a i = some x → b i = some y → x = y
    37
    38/-- For each random choice, the collection of local views that make the verifier accept. -/
    39structure System (r m : ℕ) where
    40 /-- The acceptable partial answer patterns for this random choice. -/
    41 accepting : Fin r → Finset (View m)
    42
    43/-- The random choices on which the supplied proof extends an accepting view. -/
    44noncomputable def System.acceptedSeeds {r m : ℕ} (C : System r m)
    45 (π : Oracle m) : Finset (Fin r) :=
    46 Finset.univ.filter fun seed ↦ ∃ a ∈ C.accepting seed, Extends π a
    47
    48/-- The largest number of accepting random choices attained by any single proof. -/
    49noncomputable def System.optimum {r m : ℕ} (C : System r m) : ℕ :=
    50 Finset.univ.sup fun π : Oracle m ↦ (C.acceptedSeeds π).card
    51
    52end Lax323828.LocalTests
    53
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…