Hinted Boolean matrix-vector problems
Lax350013.HintedMatrixVector · concepts/Lax350013/HintedMatrixVector.lean · lax-350013
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The v-hinted Mv, Mv-hinted Mv and uMv-hinted uMv problems reveal their inputs in successive phases. This specification includes the Boolean products, phase layouts and the conjectured trade-offs. Rectangular matrix-multiplication exponents are numerical parameters here; their values and lower bounds are not asserted.
Concept map
Lean source view on GitHub
| 1 | /- |
| 2 | Copyright (c) 2026 Anthropic, PBC. All rights reserved. |
| 3 | Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | SPDX-License-Identifier: Apache-2.0 |
| 5 | -/ |
| 6 | /- |
| 7 | Modified for the independent Lax packaging by Édouard Bonnet, 2026. |
| 8 | Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011. |
| 9 | Changes: Lax module/namespace layout, separated concepts and proofs, archive |
| 10 | annotations, and compatibility with the archive Lean/mathlib environment. |
| 11 | See NOTICE and README.md in the submission root for provenance and scope. |
| 12 | -/ |
| 13 | |
| 14 | import Mathlib.Algebra.MvPolynomial.Basic |
| 15 | import Mathlib.Analysis.SpecialFunctions.Log.Base |
| 16 | import Mathlib.Analysis.SpecialFunctions.Log.Basic |
| 17 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 18 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 19 | import Mathlib.Data.Finset.Sort |
| 20 | import Mathlib.LinearAlgebra.Matrix.Notation |
| 21 | import Mathlib.MeasureTheory.Integral.Bochner.Basic |
| 22 | import Mathlib.NumberTheory.PrimeCounting |
| 23 | import Mathlib.Probability.Independence.Basic |
| 24 | import Mathlib.Tactic.DeriveFintype |
| 25 | import Lax350013.ThinMatrices |
| 26 | |
| 27 | /-! |
| 28 | --- |
| 29 | title: Hinted Boolean matrix-vector problems |
| 30 | type: definition |
| 31 | --- |
| 32 | The v-hinted Mv, Mv-hinted Mv and uMv-hinted uMv problems reveal their inputs in successive phases. This specification includes the Boolean products, phase layouts and the conjectured trade-offs. Rectangular matrix-multiplication exponents are numerical parameters here; their values and lower bounds are not asserted. |
| 33 | -/ |
| 34 | |
| 35 | namespace Lax350013.HintedMatrixVector |
| 36 | |
| 37 | open Finset |
| 38 | open Lax350013.WordRAM |
| 39 | open Lax350013.RAMResources |
| 40 | open Lax350013.ThinMatrices |
| 41 | |
| 42 | namespace HintedMv |
| 43 | |
| 44 | /-- Section 5.4: "All three are over the Boolean semiring". The product of two Boolean matrices. -/ |
| 45 | def boolMul {l m r : ℕ} (M : Matrix (Fin l) (Fin m) Bool) (V : Matrix (Fin m) (Fin r) Bool) : |
| 46 | Matrix (Fin l) (Fin r) Bool := |
| 47 | fun i j => decide (∃ k, M i k = true ∧ V k j = true) |
| 48 | |
| 49 | /-- Proof of Corollary 40: "We compute over ℤ with 0/1 matrices". The 0/1 integer matrix |
| 50 | of a Boolean matrix. -/ |
| 51 | def toInt {l m : ℕ} (M : Matrix (Fin l) (Fin m) Bool) : Matrix (Fin l) (Fin m) ℤ := |
| 52 | fun i j => if M i j = true then 1 else 0 |
| 53 | |
| 54 | /-- Section 5.4, v-hinted Mv (Definition 5.1 of [vdBNS19]): "Phase 1: an n × t matrix M. Phase 2: a |
| 55 | t × n matrix V. Phase 3: an index i, after which the algorithm outputs MV_{[n],i}, the product of M |
| 56 | and column i of V." -/ |
| 57 | def vHintedOutput {n t : ℕ} (M : Matrix (Fin n) (Fin t) Bool) (V : Matrix (Fin t) (Fin n) Bool) |
| 58 | (i : Fin n) : Fin n → Bool := |
| 59 | fun r => boolMul M V r i |
| 60 | |
| 61 | /-- Section 5.4, Mv-hinted Mv (Definition 5.6 of [vdBNS19]): "Phase 1: N ∈ {0,1}^{n×n} and V ∈ |
| 62 | {0,1}^{t×n}. Phase 2: a vector I ∈ [n]^t of column indices. Phase 3: an index j, after which the |
| 63 | algorithm outputs N_{[n],I} V_{[t],j}, where N_{[n],I} is the n × t matrix whose k-th column is |
| 64 | column I_k of N." -/ |
| 65 | def MvHintedOutput {n t : ℕ} (N : Matrix (Fin n) (Fin n) Bool) (V : Matrix (Fin t) (Fin n) Bool) |
| 66 | (I : Fin t → Fin n) (j : Fin n) : Fin n → Bool := |
| 67 | fun r => boolMul (N.submatrix id I) V r j |
| 68 | |
| 69 | /-- Section 5.4, uMv-hinted uMv (Definition 5.11 of [vdBNS19]): "Phase 1: U ∈ {0,1}^{n×t₁}, N ∈ |
| 70 | {0,1}^{n×n}, and V ∈ {0,1}^{t₂×n}. Phase 2: I ∈ [n]^{t₁}. Phase 3: J ∈ [n]^{t₂}. Phase 4: indices |
| 71 | i and j, after which the algorithm outputs (U N_{I,J} V)_{i,j}, where N_{I,J} is the t₁ × t₂ |
| 72 | submatrix of N with the rows I and the columns J." -/ |
| 73 | def uMvHintedOutput {n t₁ t₂ : ℕ} (U : Matrix (Fin n) (Fin t₁) Bool) |
| 74 | (N : Matrix (Fin n) (Fin n) Bool) (V : Matrix (Fin t₂) (Fin n) Bool) (I : Fin t₁ → Fin n) |
| 75 | (J : Fin t₂ → Fin n) (i j : Fin n) : Bool := |
| 76 | boolMul (boolMul U (N.submatrix I J)) V i j |
| 77 | |
| 78 | /-- Section 5.4: "Each conjecture asserts that no algorithm simultaneously beats all of its listed |
| 79 | bounds, for any ε > 0." v-hinted Mv (Conjecture 5.2 of [vdBNS19]): "Bounds conjectured to be |
| 80 | impossible to achieve simultaneously: n^{ω(1,1,τ)-ε} for Phase 2 and n^{1+τ-ε} for Phase 3." |
| 81 | |
| 82 | Running times are not defined here, so the conjecture is stated relative to a parameter: |
| 83 | `Achieves a₂ a₃` stands for "some algorithm solves the problem with t = n^τ, with polynomial time in |
| 84 | Phase 1, O(n^{a₂}) time in Phase 2 and O(n^{a₃}) time in Phase 3". `ω` stands for the number |
| 85 | ω(1,1,τ). For programs of the word RAM the parameter is `AchievesVHinted τ`. The exponents of |
| 86 | rectangular matrix multiplication are not defined in Lean: `ω` is an arbitrary real number here, and |
| 87 | the definition says something only together with a condition on it. The statement that the |
| 88 | conjecture fails (`Items.Corollary_40_fail`) is made for every `ω ≥ 2`. |
| 89 | |
| 90 | [vdBNS19] words the bounds as lower bounds Ω(n^{x-ε}) on the time of a phase. That wording implies |
| 91 | the one used here, "not O(n^{x-ε})" (apply it with ε/2), so a refutation of the conjecture in this |
| 92 | form refutes it as worded there. The same holds for `Conjecture57` and `Conjecture512`. -/ |
| 93 | def Conjecture52 (Achieves : ℝ → ℝ → Prop) (ω τ : ℝ) : Prop := |
| 94 | ∀ ε > 0, ¬ Achieves (ω - ε) (1 + τ - ε) |
| 95 | |
| 96 | /-- Section 5.4, Mv-hinted Mv (Conjecture 5.7 of [vdBNS19]): "n^{ω(1,τ,1)-ε} for Phase 2 and |
| 97 | n^{1+τ-ε} for Phase 3." `Achieves` is as in `Conjecture52`, for the Mv-hinted Mv problem |
| 98 | (`AchievesMvHinted τ`); `ω` stands for ω(1,τ,1). -/ |
| 99 | def Conjecture57 (Achieves : ℝ → ℝ → Prop) (ω τ : ℝ) : Prop := |
| 100 | ∀ ε > 0, ¬ Achieves (ω - ε) (1 + τ - ε) |
| 101 | |
| 102 | /-- Section 5.4, uMv-hinted uMv (Conjecture 5.12 of [vdBNS19]): "n^{ω(1,τ₁,1)-ε} for Phase 2, |
| 103 | n^{ω(τ₂,τ₁,1)-ε} for Phase 3, and n^{τ₁+τ₂-ε} for Phase 4." `Achieves a₂ a₃ a₄` stands for "some |
| 104 | algorithm solves the problem with t₁ = n^{τ₁} and t₂ = n^{τ₂}, with polynomial time in Phase 1 and |
| 105 | O(n^{a₂}), O(n^{a₃}), O(n^{a₄}) time in Phases 2, 3, 4"; `ω₂` stands for ω(1,τ₁,1) and `ω₃` for |
| 106 | ω(τ₂,τ₁,1). For programs of the word RAM the parameter is `AchievesUMvHinted τ₁ τ₂`. -/ |
| 107 | def Conjecture512 (Achieves : ℝ → ℝ → ℝ → Prop) (ω₂ ω₃ τ₁ τ₂ : ℝ) : Prop := |
| 108 | ∀ ε > 0, ¬ Achieves (ω₂ - ε) (ω₃ - ε) (τ₁ + τ₂ - ε) |
| 109 | |
| 110 | end HintedMv |
| 111 | |
| 112 | open HintedMv |
| 113 | |
| 114 | /-- Section 5.4: the hint dimension "t = n^τ". |
| 115 | |
| 116 | NOTE. The paper treats `n^τ` as an integer; here it is rounded down, which keeps what the proof of |
| 117 | Corollary 40 needs, for `n ≥ 1`: `t ≥ 1` if `τ ≥ 0`, and `t^18 ≤ n` if `0 ≤ τ ≤ 1/18`. The number |
| 118 | `t` is given to the programs in Phase 1, after `n`; they need not compute it. -/ |
| 119 | noncomputable def hintSize (τ : ℝ) (n : ℕ) : ℕ := ⌊(n : ℝ) ^ τ⌋₊ |
| 120 | |
| 121 | /-- **v-hinted Mv** (Section 5.4; Definition 5.1 of [vdBNS19]) with `t = n^τ` is solved with |
| 122 | polynomial time in Phase 1, `O(n^{a₂})` time in Phase 2 and `O(n^{a₃})` time in Phase 3. Phase 1 |
| 123 | receives `n`, `t` and the `n × t` matrix `M`; Phase 2 the `t × n` matrix `V`; Phase 3 the index `i`; |
| 124 | the output is the `n` entries of the Boolean product of `M` and column `i` of `V`. -/ |
| 125 | def AchievesVHinted (τ a₂ a₃ : ℝ) : Prop := |
| 126 | ∃ (P₁ P₂ P₃ : List Instr) (b : ℕ) (C a₁ : ℝ), ∀ n : ℕ, 1 ≤ n → |
| 127 | ∀ (M : Matrix (Fin n) (Fin (hintSize τ n)) Bool) (V : Matrix (Fin (hintSize τ n)) (Fin n) Bool) |
| 128 | (i : Fin n) (bits : ℕ), Admissible b [n] bits → |
| 129 | ∃ s₁ s₂ s₃ : ℕ, Within s₁ C n a₁ ∧ Within s₂ C n a₂ ∧ Within s₃ C n a₃ ∧ |
| 130 | RunsPhases (fun c off => ∀ r : Fin n, output c off r.val = bit (vHintedOutput M V i r)) |
| 131 | (loadWords bits []) 0 |
| 132 | [(P₁, [(n : ℤ), (hintSize τ n : ℤ)] ++ rowMajor (toInt M), s₁), |
| 133 | (P₂, rowMajor (toInt V), s₂), (P₃, [(i.val : ℤ)], s₃)] |
| 134 | |
| 135 | /-- **Mv-hinted Mv** (Section 5.4; Definition 5.6 of [vdBNS19]) with `t = n^τ`, in the same sense. |
| 136 | Phase 1 receives `n`, `t`, the `n × n` matrix `N` and the `t × n` matrix `V`; Phase 2 the `t` column |
| 137 | indices `I`; Phase 3 the index `j`; the output is the `n` entries of `N_{[n],I} V_{[t],j}`. -/ |
| 138 | def AchievesMvHinted (τ a₂ a₃ : ℝ) : Prop := |
| 139 | ∃ (P₁ P₂ P₃ : List Instr) (b : ℕ) (C a₁ : ℝ), ∀ n : ℕ, 1 ≤ n → |
| 140 | ∀ (N : Matrix (Fin n) (Fin n) Bool) (V : Matrix (Fin (hintSize τ n)) (Fin n) Bool) |
| 141 | (I : Fin (hintSize τ n) → Fin n) (j : Fin n) (bits : ℕ), Admissible b [n] bits → |
| 142 | ∃ s₁ s₂ s₃ : ℕ, Within s₁ C n a₁ ∧ Within s₂ C n a₂ ∧ Within s₃ C n a₃ ∧ |
| 143 | RunsPhases (fun c off => ∀ r : Fin n, output c off r.val = bit (MvHintedOutput N V I j r)) |
| 144 | (loadWords bits []) 0 |
| 145 | [(P₁, [(n : ℤ), (hintSize τ n : ℤ)] ++ rowMajor (toInt N) ++ rowMajor (toInt V), s₁), |
| 146 | (P₂, List.ofFn fun k => ((I k).val : ℤ), s₂), (P₃, [(j.val : ℤ)], s₃)] |
| 147 | |
| 148 | /-- **uMv-hinted uMv** (Section 5.4; Definition 5.11 of [vdBNS19]) with `t₁ = n^{τ₁}` and `t₂ = |
| 149 | n^{τ₂}` is solved with polynomial time in Phase 1 and `O(n^{a₂})`, `O(n^{a₃})`, `O(n^{a₄})` time in |
| 150 | Phases 2, 3, 4. Phase 1 receives `n`, `t₁`, `t₂` and the matrices `U` (`n × t₁`), `N` (`n × n`), |
| 151 | `V` (`t₂ × n`); Phase 2 the `t₁` row indices `I`; Phase 3 the `t₂` column indices `J`; Phase 4 the |
| 152 | indices `i` and `j`; the output is the one entry `(U N_{I,J} V)_{i,j}`. -/ |
| 153 | def AchievesUMvHinted (τ₁ τ₂ a₂ a₃ a₄ : ℝ) : Prop := |
| 154 | ∃ (P₁ P₂ P₃ P₄ : List Instr) (b : ℕ) (C a₁ : ℝ), ∀ n : ℕ, 1 ≤ n → |
| 155 | ∀ (U : Matrix (Fin n) (Fin (hintSize τ₁ n)) Bool) (N : Matrix (Fin n) (Fin n) Bool) |
| 156 | (V : Matrix (Fin (hintSize τ₂ n)) (Fin n) Bool) (I : Fin (hintSize τ₁ n) → Fin n) |
| 157 | (J : Fin (hintSize τ₂ n) → Fin n) |
| 158 | (i j : Fin n) (bits : ℕ), Admissible b [n] bits → |
| 159 | ∃ s₁ s₂ s₃ s₄ : ℕ, Within s₁ C n a₁ ∧ Within s₂ C n a₂ ∧ Within s₃ C n a₃ ∧ Within s₄ C n a₄ ∧ |
| 160 | RunsPhases (fun c off => output c off 0 = bit (uMvHintedOutput U N V I J i j)) |
| 161 | (loadWords bits []) 0 |
| 162 | [(P₁, [(n : ℤ), (hintSize τ₁ n : ℤ), (hintSize τ₂ n : ℤ)] ++ rowMajor (toInt U) ++ |
| 163 | rowMajor (toInt N) ++ rowMajor (toInt V), s₁), |
| 164 | (P₂, List.ofFn fun k => ((I k).val : ℤ), s₂), |
| 165 | (P₃, List.ofFn fun k => ((J k).val : ℤ), s₃), |
| 166 | (P₄, [(i.val : ℤ), (j.val : ℤ)], s₄)] |
| 167 | |
| 168 | end Lax350013.HintedMatrixVector |
| 169 |
Builds on
Used by
From Mathlib
Mathlib.Algebra.MvPolynomial.BasicMathlib.Analysis.SpecialFunctions.Log.BaseMathlib.Analysis.SpecialFunctions.Log.BasicMathlib.Analysis.SpecialFunctions.Pow.RealMathlib.Combinatorics.SimpleGraph.BasicMathlib.Data.Finset.SortMathlib.LinearAlgebra.Matrix.NotationMathlib.MeasureTheory.Integral.Bochner.BasicMathlib.NumberTheory.PrimeCountingMathlib.Probability.Independence.BasicMathlib.Tactic.DeriveFintype
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments