Lax Lean Archive

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

Quantitative collision and squared restriction exponents

Lax342547.CollisionCosts · concepts/Lax342547/CollisionCosts.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

    Explicit scale conditions put pruning below half the accepted overlap. The surviving key collision and scalar agreement yield a proved exponential lower bound, and squared restriction recovery preserves the original-law cost.

    Concept map
    9 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 collision_exponential_lower proven

    2 pruning_half_overlap proven

    3 restriction_exponential_lower proven

    Lean source view on GitHub

    1import Lax342547.CollisionExponents
    2import Lax342547.PairRecovery
    3
    4/-!
    5---
    6title: Quantitative collision and squared restriction exponents
    7type: lemma
    8---
    9Explicit scale conditions put pruning below half the accepted overlap. The surviving key collision and scalar agreement yield a proved exponential lower bound, and squared restriction recovery preserves the original-law cost.
    10-/
    11
    12namespace Lax342547.CollisionCosts
    13
    14
    15
    16axiom pruning_half_overlap (η N overlap : ℝ)
    17 (hscale : 1 ≤ (1/200-η)*N) (hoverlap : (2:ℝ)^(-η*N) ≤ overlap) :
    18 (2:ℝ)^(-N/200) ≤ overlap/2
    19
    20axiom collision_exponential_lower (k η N keys overlap error agreement holes : ℝ)
    21 (hkeys : 0 < keys) (hkeybound : keys ≤ (2:ℝ)^(k*N))
    22 (hoverlap : (2:ℝ)^(-η*N) ≤ overlap)
    23 (herror : error ≤ (2:ℝ)^(-N/200)) (hscale : 1 ≤ (1/200-η)*N)
    24 (hagreement : (2:ℝ)^(-N/50) ≤ agreement)
    25 (hholes : agreement*(overlap-error)/keys ≤ holes) :
    26 (2:ℝ)^(-((k+1/50+η)*N)-1) ≤ holes
    27
    28axiom restriction_exponential_lower (k η N mass restricted original : ℝ)
    29 (hmass : (2:ℝ)^(-η*N) ≤ mass)
    30 (hrestricted : (2:ℝ)^(-((k+1/50+η)*N)-1) ≤ restricted)
    31 (hrecovery : mass^2*restricted ≤ original) :
    32 (2:ℝ)^(-((k+1/50+3*η)*N)-1) ≤ original
    33
    34end Lax342547.CollisionCosts
    35
    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…