Lax Lean Archive

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

Uniform collision scales and bounded numerical options

Lax342547.CollisionScales · concepts/Lax342547/CollisionScales.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 fixed ambient multiplier pays linear record and scalar bit costs. An explicit overlap threshold controls pruning, and a finite option sum has a witnessed option with its precise exponent cost.

    Concept map
    10 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 bounded_option_exponent proven

    2 bounded_options proven

    3 eventual_pruning_gap proven

    4 record_scale proven

    5 scalar_scale proven

    Lean source view on GitHub

    1import Lax342547.CollisionCosts
    2
    3/-!
    4---
    5title: Uniform collision scales and bounded numerical options
    6type: lemma
    7---
    8A fixed ambient multiplier pays linear record and scalar bit costs. An explicit overlap threshold controls pruning, and a finite option sum has a witnessed option with its precise exponent cost.
    9-/
    10
    11namespace Lax342547.CollisionScales
    12
    13
    14
    15axiom record_scale (C M₀ n : ℝ) (hn : 1 ≤ n) (hM : 200*(C+1) ≤ M₀) :
    16 1+C*n ≤ M₀*n/200
    17
    18axiom scalar_scale (c M₀ n : ℝ) (hn : 0 ≤ n) (hM : 100*c ≤ M₀)
    19 (s : ℕ) (hs : (s:ℝ) ≤ c*n) : (s:ℝ) ≤ M₀*n/100
    20
    21axiom eventual_pruning_gap (η : ℝ) (hη : η < 1/200) :
    22 ∃ N₀ : ℝ, ∀ N : ℝ, N₀ ≤ N → 100 ≤ N ∧ 1 ≤ (1/200-η)*N
    23
    24axiom bounded_options {O : Type} [Fintype O] [Nonempty O]
    25 (f : O → ℝ) (overlap : ℝ) (h : overlap ≤ ∑ o, f o) :
    26 ∃ o, overlap / Fintype.card O ≤ f o
    27
    28axiom bounded_option_exponent (cost δ N options probability : ℝ)
    29 (hoptions : 0 < options) (hcount : options ≤ (2:ℝ)^(δ*N))
    30 (hprobability : (2:ℝ)^(-cost*N)/options ≤ probability) :
    31 (2:ℝ)^(-(cost+δ)*N) ≤ probability
    32
    33end Lax342547.CollisionScales
    34
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…