Lax Lean Archive

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

Accepting local views of a proof

Lax253009.LocalTests · concepts/Lax253009/LocalTests.lean · lax-253009

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 Lax253009.LocalTests
    22
    23abbrev Oracle (m : ℕ) := Fin m → Bool
    24abbrev View (m : ℕ) := Fin m → Option Bool
    25
    26def Extends {m : ℕ} (π : Oracle m) (a : View m) : Prop :=
    27 ∀ i b, a i = some b → π i = b
    28
    29def Compatible {m : ℕ} (a b : View m) : Prop :=
    30 ∀ i x y, a i = some x → b i = some y → x = y
    31
    32structure System (r m : ℕ) where
    33 accepting : Fin r → Finset (View m)
    34
    35noncomputable def System.acceptedSeeds {r m : ℕ} (C : System r m)
    36 (π : Oracle m) : Finset (Fin r) := by
    37 classical
    38 exact Finset.univ.filter fun seed ↦ ∃ a ∈ C.accepting seed, Extends π a
    39
    40noncomputable def System.optimum {r m : ℕ} (C : System r m) : ℕ :=
    41 Finset.univ.sup fun π : Oracle m ↦ (C.acceptedSeeds π).card
    42
    43end Lax253009.LocalTests
    44
    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…