Lax Lean Archive

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

Witness atoms and their numerical tester records

Lax342547.WitnessAtoms · concepts/Lax342547/WitnessAtoms.lean · lax-342547

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

    Lemma

    A witness atom includes an actual allowed base vector and selector label. Its numerical record keeps only the tag and tester summary. These records determine the tester part of every atom-pair gradient entry.

    Concept map
    11 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 allowed_index proven

    2 atom_testers proven

    3 tester_properties proven

    Lean source view on GitHub

    1import Lax342547.Atoms
    2import Lax342547.BinaryPrescriptions
    3
    4/-!
    5---
    6title: Witness atoms and their numerical tester records
    7type: lemma
    8---
    9A witness atom includes an actual allowed base vector and selector label.
    10Its numerical record keeps only the tag and tester summary. These records
    11determine the tester part of every atom-pair gradient entry.
    12-/
    13
    14namespace Lax342547.WitnessAtoms
    15
    16open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    17open Lax342547.ConcreteCut Lax342547.Atoms
    18
    19structure PointAtom (k n b degree : ℕ) where
    20 tag : Tag k
    21 label : Fin b → Binary
    22 base : Base k n → Binary
    23 supported : ∀ i, i ∉ allowedBase k n tag → base i = 0
    24
    25def PointAtom.vector {k n b degree : ℕ} (x : PointAtom k n b degree) : Vector k n b degree :=
    26 point selectorEval x.label x.base
    27
    28noncomputable def PointAtom.profile {k n b degree : ℕ} (x : PointAtom k n b degree) :
    29 Profile k n b degree := atom x.tag x.label x.base x.supported
    30
    31structure Numerical (k : ℕ) where
    32 tag : Tag k
    33 summary : Option (Tag k × Tag k) → Binary
    34
    35def PointAtom.numerical {k n b degree r : ℕ} (hr : 2 * r ≤ n) (x : PointAtom k n b degree) :
    36 Numerical k := ⟨x.tag, testerSummary (degree := degree) hr x.label x.base⟩
    37
    38def Numerical.aTag {k : ℕ} (x : Numerical k) (t : Tag k) : Binary :=
    39 ∑ d, x.summary (some (d, t))
    40
    41def Numerical.bTag {k : ℕ} (x : Numerical k) (t : Tag k) : Binary :=
    42 if x.tag = t then 0 else x.summary none
    43
    44def Numerical.role {k : ℕ} (x : Numerical k) : Binary := ∑ t, x.aTag t
    45
    46def testerEntry {k : ℕ} (x y : Numerical k) : Binary :=
    47 x.role * y.role + ∑ t, (x.aTag t * y.bTag t + x.bTag t * y.aTag t)
    48
    49abbrev ProductIndex (k J : ℕ) := Fin J × Lax342547.CutProfiles.Component (Tag k) ×
    50 Lax342547.CutProfiles.Component (Tag k)
    51
    52def allowedIndex {k J : ℕ} (x y : Numerical k) (t : ProductIndex k J) : Prop :=
    53 x.tag ∈ t.2.1.val ∧ y.tag ∈ t.2.2.val
    54
    55axiom tester_properties {k : ℕ} :
    56 (∀ x y : Numerical k, testerEntry x y = testerEntry y x) ∧
    57 ∀ x : Numerical k, testerEntry x x = x.role
    58
    59axiom atom_testers {k n b degree r : ℕ} {hr : 2 * r ≤ n}
    60 (D : Testers (k := k) (b := b) (degree := degree) hr) (x : PointAtom k n b degree) :
    61 D.role x.profile = (x.numerical hr).role ∧
    62 (∀ t, D.aTag t x.profile = (x.numerical hr).aTag t) ∧
    63 ∀ t, D.bTag t x.profile = (x.numerical hr).bTag t
    64
    65axiom allowed_index {k J : ℕ} (hk : 0 < k) (hJ : 0 < J) (x y : Numerical k) :
    66 ∃ t : ProductIndex k J, allowedIndex x y t
    67
    68end Lax342547.WitnessAtoms
    69
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…