Lax Lean Archive

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

Improved algorithms with thin hints

Lax350013.HintedAlgorithms · concepts/Lax350013/HintedAlgorithms.lean · lax-350013

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

    Theorem

    Corollary 40 supplies explicit and general phase-time savings for the three hinted Boolean matrix-vector problems. Theorem 4 contradicts their conjectured trade-offs in the stated thin-hint regimes, conditional on the displayed numerical lower bounds for rectangular multiplication exponents. Those lower bounds are hypotheses, not independently verified facts about matrix-multiplication exponents.

    Concept map
    7 concepts
    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 explicitTimes proven

    2 generalTimes proven

    3 theorem4 proven

    Lean source view on GitHub

    1/-
    2Copyright (c) 2026 Anthropic, PBC. All rights reserved.
    3Released under Apache 2.0 license as described in the file LICENSE.
    4SPDX-License-Identifier: Apache-2.0
    5-/
    6/-
    7Modified for the independent Lax packaging by Édouard Bonnet, 2026.
    8Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
    9Changes: Lax module/namespace layout, separated concepts and proofs, archive
    10annotations, and compatibility with the archive Lean/mathlib environment.
    11See NOTICE and README.md in the submission root for provenance and scope.
    12-/
    13
    14import Mathlib.Algebra.MvPolynomial.Basic
    15import Mathlib.Analysis.SpecialFunctions.Log.Base
    16import Mathlib.Analysis.SpecialFunctions.Log.Basic
    17import Mathlib.Analysis.SpecialFunctions.Pow.Real
    18import Mathlib.Combinatorics.SimpleGraph.Basic
    19import Mathlib.Data.Finset.Sort
    20import Mathlib.LinearAlgebra.Matrix.Notation
    21import Mathlib.MeasureTheory.Integral.Bochner.Basic
    22import Mathlib.NumberTheory.PrimeCounting
    23import Mathlib.Probability.Independence.Basic
    24import Mathlib.Tactic.DeriveFintype
    25import Lax350013.HintedMatrixVector
    26import Lax350013.MatrixParameters
    27
    28/-!
    29---
    30title: Improved algorithms with thin hints
    31type: theorem
    32---
    33Corollary 40 supplies explicit and general phase-time savings for the three hinted Boolean matrix-vector problems. Theorem 4 contradicts their conjectured trade-offs in the stated thin-hint regimes, conditional on the displayed numerical lower bounds for rectangular multiplication exponents. Those lower bounds are hypotheses, not independently verified facts about matrix-multiplication exponents.
    34-/
    35
    36namespace Lax350013.HintedAlgorithms
    37
    38open Finset
    39open Lax350013.WordRAM
    40open Lax350013.RAMResources
    41open Lax350013.ThinMatrices
    42open Lax350013.HintedMatrixVector
    43open Lax350013.MatrixParameters
    44
    45/-- **Corollary 40**, the running times of its first paragraph (also in **Theorem 4**): for
    46Conjectures 5.2 and 5.7 and "every 0 < τ < 1/18: Phase 2 takes O(n^{2−0.063τ}) time and Phase 3
    47takes O(n^{1+0.437τ}) time"; for Conjecture 5.12 and "every 0 < τ₁ < τ₂/18: Phase 3 takes
    48O(n^{1+τ₂−0.063τ₁}) time and Phase 4 takes O(n^{τ₂+0.437τ₁}) time, with polynomial Phase 1 and a
    49Phase 2 that only stores I". (Theorem 4 prints the first two bounds only.)
    50
    51NOTE. `τ₂ < 1` is assumed: it is the standing assumption of Section 5.4 ("for constants τ, τ_i ∈
    52(0,1)"). The words "only stores I" are read as `O(n^{τ₁})` time. -/
    53def Corollary_40_times : Prop :=
    54 (∀ τ : ℝ, 0 < τ → τ < 1 / 18 →
    55 AchievesVHinted τ (2 - 0.063 * τ) (1 + 0.437 * τ) ∧
    56 AchievesMvHinted τ (2 - 0.063 * τ) (1 + 0.437 * τ)) ∧
    57 ∀ τ₁ τ₂ : ℝ, 0 < τ₁ → τ₁ < τ₂ / 18 → τ₂ < 1 →
    58 AchievesUMvHinted τ₁ τ₂ τ₁ (1 + τ₂ - 0.063 * τ₁) (τ₂ + 0.437 * τ₁)
    59
    60/-- **The proof of Corollary 40**, paragraph "General τ": the running times. (For this range the
    61corollary itself says only that the conjectures fail: `Corollary_40_fail`.) For every `0 < τ < ε*`
    62there is a `γ > 0` with "Phase 2 in O(n²/D^γ) = O(n^{2−γτ}) time and Phase 3 in O(n D^{1/2}) =
    63O(n^{1+τ/2}) time"; and for every `0 < τ₁ < ε* τ₂` (and `τ₂ < 1`) there is a `γ > 0` with Phase 2 in
    64`O(n^{τ₁})`, Phase 3 in `O(n^{1+τ₂−γτ₁})` and Phase 4 in `O(n^{τ₂+τ₁/2})` time.
    65
    66NOTE. For Conjecture 5.12 ("we use the same blocks") the three bounds are those that the argument
    67gives, with `D^γ` and `D^{1/2}` in place of `D^{0.063}` and `D^{0.437}`. On `τ₂ < 1` see the NOTE
    68at `Corollary_40_times`. -/
    69def Corollary_40_general_times : Prop :=
    70 (∀ τ : ℝ, 0 < τ → τ < epsStar → ∃ γ : ℝ, 0 < γ ∧
    71 AchievesVHinted τ (2 - γ * τ) (1 + τ / 2) ∧ AchievesMvHinted τ (2 - γ * τ) (1 + τ / 2)) ∧
    72 ∀ τ₁ τ₂ : ℝ, 0 < τ₁ → τ₁ < epsStar * τ₂ → τ₂ < 1 → ∃ γ : ℝ, 0 < γ ∧
    73 AchievesUMvHinted τ₁ τ₂ τ₁ (1 + τ₂ - γ * τ₁) (τ₂ + τ₁ / 2)
    74
    75/-- **Corollary 40** (also **Theorem 4**), "fail": Conjectures 5.2 and 5.7 of
    76[vdBNS19], read as statements about programs of this machine, fail for every `0 < τ < τ₀`, and
    77Conjecture 5.12 fails for every `0 < τ₁ < τ₀ τ₂` (with `τ₂ < 1`), "whatever the value of ω".
    78
    79The exponents of rectangular matrix multiplication are not defined here. `ω`, `ω₂`, `ω₃` stand for
    80`ω(1,1,τ) = ω(1,τ,1)`, `ω(1,τ₁,1)`, `ω(τ₂,τ₁,1)`, and the statement is made for all real numbers
    81that satisfy the lower bounds of Corollary 40, "ω(1,1,τ) = ω(1,τ,1) ≥ 2 and ω(τ₂,τ₁,1) ≥ 1 + τ₂
    82because of the input and output sizes"; the bound `2 ≤ ω₂` is the first of these at `τ = τ₁`. That
    83the true exponents satisfy these bounds is not proved here. The paper has `τ₀ = 1/18` in the first
    84paragraph, `ε*` in the second, and `0.1204` in Theorem 4.
    85
    86NOTE. `τ₂ < 1` is assumed; see the NOTE at `Corollary_40_times`. -/
    87def Corollary_40_fail (τ₀ : ℝ) : Prop :=
    88 (∀ τ ω : ℝ, 0 < τ → τ < τ₀ → 2 ≤ ω →
    89 ¬ HintedMv.Conjecture52 (AchievesVHinted τ) ω τ ∧
    90 ¬ HintedMv.Conjecture57 (AchievesMvHinted τ) ω τ) ∧
    91 ∀ τ₁ τ₂ ω₂ ω₃ : ℝ, 0 < τ₁ → τ₁ < τ₀ * τ₂ → τ₂ < 1 → 2 ≤ ω₂ → 1 + τ₂ ≤ ω₃ →
    92 ¬ HintedMv.Conjecture512 (AchievesUMvHinted τ₁ τ₂) ω₂ ω₃ τ₁ τ₂
    93
    94/-- **Theorem 4**: "The v-hinted Mv, Mv-hinted Mv, and uMv-hinted uMv conjectures of
    95[vdBNS19] [...] are refuted in the regime of thin hints. For hint dimension t = n^τ with 0 < τ <
    961/18, the phase after the hint takes O(n^{2−0.063τ}) time and the phase after the vector
    97O(n^{1+0.437τ}) time [...]. Correspondingly, the uMv version [...] fails for τ₁ < τ₂/18. All three
    98fail, with smaller savings, for every τ < 0.1204 (for the uMv version, τ₁ < 0.1204 τ₂)." The three
    99parts follow the sentences of the theorem. (The first contains also the running times of the uMv
    100version, which are printed in Corollary 40 only; the second follows from the third.)
    101
    102NOTE. For the uMv version `τ₂ < 1` is assumed; see the NOTE at `Corollary_40_times`. -/
    103def Theorem_4 : Prop :=
    104 Corollary_40_times ∧ Corollary_40_fail (1 / 18) ∧ Corollary_40_fail 0.1204
    105
    106/-- Improved algorithms with thin hints: Corollary 40 times. -/
    107axiom explicitTimes : Corollary_40_times
    108
    109
    110/-- Improved algorithms with thin hints: Corollary 40 general times. -/
    111axiom generalTimes : Corollary_40_general_times
    112
    113
    114/-- Improved algorithms with thin hints: Theorem 4. -/
    115axiom theorem4 : Theorem_4
    116
    117end Lax350013.HintedAlgorithms
    118
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…