From 7085d68db489c129c39d3795fb25b3683fded7d7 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 22:56:13 +0000 Subject: [PATCH 1/8] feat(Foundations): correction factorization and reward transport for transition matrices Pure linear algebra for the correction-and-copy hierarchy (#1444 Phase 2, ideas 2 and 4 of #474), following the OpenAI preprint (2026-09-23), Section 4: the factorization 1 - (C - E + EC) = (1 + E)(1 - C), the corrected inverse, copy splitting intertwined with its projection, and the reward transport identity with the stage error bound. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../Matrix/CorrectionHierarchy.lean | 461 ++++++++++++++++++ ComplexityTests/CorrectionHierarchy.lean | 122 +++++ references.bib | 9 + 4 files changed, 593 insertions(+) create mode 100644 Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean create mode 100644 ComplexityTests/CorrectionHierarchy.lean diff --git a/Complexity.lean b/Complexity.lean index f59b96f22..c0e4b8629 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2620,6 +2620,7 @@ public import Complexity.Foundations.LinearAlgebra.ExchangeReplacement public import Complexity.Foundations.LinearAlgebra.ImageSparsification public import Complexity.Foundations.LinearAlgebra.Interpolation public import Complexity.Foundations.LinearAlgebra.KernelVector +public import Complexity.Foundations.LinearAlgebra.Matrix.CorrectionHierarchy public import Complexity.Foundations.LinearAlgebra.Matrix.CutRank public import Complexity.Foundations.LinearAlgebra.Matrix.Kronecker public import Complexity.Foundations.LinearAlgebra.Matrix.Lindsey diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean b/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean new file mode 100644 index 000000000..606c43617 --- /dev/null +++ b/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean @@ -0,0 +1,461 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.LinearAlgebra.Matrix.Block +public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Tactic.NoncommRing + +/-! +# Corrections, copies and reward transport for transition matrices + +Let `C` be the transition matrix of a finite Markov chain that may stop (its rows sum to at most +one), and let `e` be a reward collected when it stops. The expected reward `p` from each state +solves `(1 - C) p = e`; when `C` is nilpotent, `p = (1 - C)⁻¹ e`. For the time-layered +configuration graph of a randomized machine, `p` is the vector of acceptance probabilities. + +This file develops the exact algebra of a hierarchy that shrinks the entries of `C` while keeping +`p` recoverable, following the OpenAI preprint (2026-09-23), Section 4, idea 2 and the deterministic +part of idea 4 in issue #474 [OpenAI2026LogSpace]. The estimates that choose the corrections and +the copies (factorial truncation, detectors) are not part of this file. + +* **Correction.** For any matrix `E`, the *corrected* matrix `D = C - E + E C` satisfies + `1 - D = (1 + E) (1 - C)` (`one_add_mul_one_sub_eq_one_sub`, a ring identity). So the same `p` + solves `(1 - D) p = (1 + E) e` (`Matrix.one_sub_correction_mulVec`): the correction moves + transition weight into the reward `e + E e`. When `1 + E` is invertible, for example when `E` is + strictly upper triangular, `(1 - D)⁻¹ (e + E e) = (1 - C)⁻¹ e` + (`Matrix.inv_one_sub_correction_mulVec`). If `E ≥ 0` and the rows of `C` sum to at most one, + the rows of `D` sum to at most as much (`Matrix.correction_mulVec_one_le`). +* **Copies.** A vertex `x` is replaced by copies `(x, i)`, weighted by `r i x`, and an entry + `D x y` is split among the copies of `y` in proportions `s x y j` (`Matrix.copySplit`). + If the weighted proportions sum to one on the support of `D`, the projection + `Matrix.copyWeight r` intertwines the two matrices: `copySplit r s D * copyWeight r = + copyWeight r * D` (`Matrix.copySplit_mul_copyWeight`). +* **Reward transport.** Iterating, a sequence of stages with transition matrices `C l`, + corrections `E l` and projections `P l` satisfying `C (l + 1) * P l = P l * D l` carries the + cumulative projection `Matrix.copyProjection` and the transported reward + `Matrix.rewardTransport`, with `C l * Pc l = Pc l - B l * (1 - C 0)` + (`Matrix.mul_copyProjection`). Hence the stage-`l` reward `W l = B l e` equals + `Pc l p - C l Pc l p` (`Matrix.rewardTransport_mulVec`). At a vertex `z l` reached from `z 0` + by primary copies only, the transported reward underestimates `p (z 0)` by at most the row + sum of `C l` (`Matrix.sub_rewardTransport_mulVec_mem_Icc`), so by at most `|A l| * ε l` when + the entries of `C l` are at most `ε l` and its nonzero columns lie in `A l` + (`Matrix.sub_rewardTransport_mulVec_le_card_mul`). With the paper's per-stage rates (entries + shrink by `2 ^ (c + 1)`, active columns at most double) this is the stage bound + `0 ≤ p (z 0) - W l (z l) ≤ n / 2 ^ (c l)` (`Matrix.sub_rewardTransport_mulVec_le_pow`). + +## Main definitions + +* `Matrix.IsStrictUpperTriangular`: entries vanish unless the row index is below the column index. +* `Matrix.copySplit`, `Matrix.copyWeight`: a copy step and its weighted projection. +* `Matrix.copyProjection`, `Matrix.rewardTransport`: cumulative projections and rewards of a + sequence of stages. + +## Main results + +* `one_add_mul_one_sub_eq_one_sub`: `(1 + e) (1 - c) = 1 - (c - e + e c)` in any ring. +* `Matrix.one_sub_correction_mulVec`, `Matrix.inv_one_sub_correction_mulVec`: the expected reward + of `C` is the expected corrected reward of `C - E + E C`. +* `Matrix.IsStrictUpperTriangular.det_one_add`: `det (1 + E) = 1` for strictly upper triangular + `E`. +* `Matrix.correction_mulVec_one_le`: corrections keep matrices substochastic. +* `Matrix.copySplit_mul_copyWeight`: a copy step intertwines with its projection. +* `Matrix.mul_copyProjection`, `Matrix.rewardTransport_mulVec`: the reward transport identity. +* `Matrix.sub_rewardTransport_mulVec_mem_Icc`, `Matrix.sub_rewardTransport_mulVec_le_card_mul`, + `Matrix.sub_rewardTransport_mulVec_le_pow`: the transported reward is a lower bound with error + controlled by the last transition matrix. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 4 (preprint, not peer reviewed) +-/ + +public section + +open Finset + +/-- **The correction factorization.** In any ring, correcting `c` by `e` to `c - e + e * c` +factors `1 - (c - e + e * c)` as `(1 + e) * (1 - c)` [OpenAI2026LogSpace, Section 4]. -/ +theorem one_add_mul_one_sub_eq_one_sub {R : Type*} [Ring R] (c e : R) : + (1 + e) * (1 - c) = 1 - (c - e + e * c) := by + noncomm_ring + +namespace Matrix + +section Triangular + +variable {V R : Type*} + +/-- A square matrix is *strictly upper triangular* when its entry at `(i, j)` vanishes unless +`i < j`. For the time-layered transition matrices of a machine, ordered by time, this says that +every transition moves strictly forward. -/ +def IsStrictUpperTriangular [LT V] [Zero R] (M : Matrix V V R) : Prop := + ∀ ⦃i j⦄, ¬ i < j → M i j = 0 + +namespace IsStrictUpperTriangular + +variable [Preorder V] {M N : Matrix V V R} + +/-- A strictly upper triangular matrix is upper triangular. -/ +theorem isUpperTriangular [Zero R] (h : M.IsStrictUpperTriangular) : M.IsUpperTriangular := + fun _ _ hji => h (lt_asymm hji) + +theorem add [AddZeroClass R] (hM : M.IsStrictUpperTriangular) (hN : N.IsStrictUpperTriangular) : + (M + N).IsStrictUpperTriangular := fun i j hij => by + simp only [add_apply, hM hij, hN hij, add_zero] + +theorem neg [SubtractionMonoid R] (hM : M.IsStrictUpperTriangular) : + (-M).IsStrictUpperTriangular := fun i j hij => by + simp only [neg_apply, hM hij, neg_zero] + +theorem sub [SubtractionMonoid R] (hM : M.IsStrictUpperTriangular) + (hN : N.IsStrictUpperTriangular) : (M - N).IsStrictUpperTriangular := fun i j hij => by + simp only [sub_apply, hM hij, hN hij, sub_zero] + +theorem mul [Fintype V] [NonUnitalNonAssocSemiring R] (hM : M.IsStrictUpperTriangular) + (hN : N.IsStrictUpperTriangular) : (M * N).IsStrictUpperTriangular := fun i j hij => by + refine Finset.sum_eq_zero fun k _ => ?_ + change M i k * N k j = 0 + by_cases hik : i < k + · rw [hN fun hkj => hij (hik.trans hkj), mul_zero] + · rw [hM hik, zero_mul] + +/-- `1 + E` has determinant one when `E` is strictly upper triangular. -/ +theorem det_one_add {V : Type*} [Fintype V] [DecidableEq V] [LinearOrder V] [CommRing R] + {E : Matrix V V R} (h : E.IsStrictUpperTriangular) : (1 + E).det = 1 := by + have hT : (1 + E).IsUpperTriangular := fun i j (hji : j < i) => by + rw [add_apply, one_apply_ne (ne_of_lt hji).symm, h.isUpperTriangular hji, add_zero] + rw [det_of_isUpperTriangular hT] + exact Finset.prod_eq_one fun i _ => by rw [add_apply, one_apply_eq, h (lt_irrefl i), add_zero] + +end IsStrictUpperTriangular + +end Triangular + +section Correction + +variable {V R : Type*} [Fintype V] + +/-- **Corrections preserve the expected reward.** Correcting `C` to `C - E + E * C` turns the +equation `(1 - C) p = e` into `(1 - D) p = (1 + E) e` for the same `p`: the weight removed from +the transitions reappears in the reward [OpenAI2026LogSpace, Section 4]. -/ +theorem one_sub_correction_mulVec [DecidableEq V] [Ring R] (C E : Matrix V V R) (p : V → R) : + (1 - (C - E + E * C)) *ᵥ p = (1 + E) *ᵥ ((1 - C) *ᵥ p) := by + rw [mulVec_mulVec, one_add_mul_one_sub_eq_one_sub] + +/-- **The corrected inverse.** When `1 + E` is invertible, the expected reward +`(1 - C)⁻¹ e` of `C` equals the expected reward of the corrected matrix `C - E + E * C` with the +corrected reward `e + E e`. -/ +theorem inv_one_sub_correction_mulVec [DecidableEq V] [CommRing R] {C E : Matrix V V R} + (hE : IsUnit (1 + E).det) (e : V → R) : + (1 - (C - E + E * C))⁻¹ *ᵥ (e + E *ᵥ e) = (1 - C)⁻¹ *ᵥ e := by + have h : (1 - (C - E + E * C))⁻¹ * (1 + E) = (1 - C)⁻¹ := by + rw [← one_add_mul_one_sub_eq_one_sub, mul_inv_rev, + nonsing_inv_mul_cancel_right (1 + E) (1 - C)⁻¹ hE] + rw [← h, ← mulVec_mulVec, add_mulVec, one_mulVec] + +/-- The corrected inverse for a strictly upper triangular correction. -/ +theorem IsStrictUpperTriangular.inv_one_sub_correction_mulVec [DecidableEq V] [LinearOrder V] + [CommRing R] {C E : Matrix V V R} (hE : E.IsStrictUpperTriangular) (e : V → R) : + (1 - (C - E + E * C))⁻¹ *ᵥ (e + E *ᵥ e) = (1 - C)⁻¹ *ᵥ e := + Matrix.inv_one_sub_correction_mulVec (by rw [hE.det_one_add]; exact isUnit_one) e + +/-- The row sums of a corrected matrix: `(C - E + E C) 1 = C 1 - E (1 - C 1)`. -/ +theorem correction_mulVec_one [Ring R] (C E : Matrix V V R) : + (C - E + E * C) *ᵥ 1 = C *ᵥ 1 - E *ᵥ (1 - C *ᵥ 1) := by + rw [add_mulVec, sub_mulVec, ← mulVec_mulVec, mulVec_sub] + abel + +/-- An entrywise nonnegative matrix maps nonnegative vectors to nonnegative vectors. -/ +theorem mulVec_nonneg {m n : Type*} [Fintype n] [Semiring R] [PartialOrder R] [IsOrderedRing R] + {M : Matrix m n R} (hM : ∀ i j, 0 ≤ M i j) {v : n → R} (hv : 0 ≤ v) : 0 ≤ M *ᵥ v := + fun i => Finset.sum_nonneg fun j _ => mul_nonneg (hM i j) (hv j) + +/-- An entrywise nonnegative matrix whose rows sum to at most one maps vectors with entries at +most one to vectors with entries at most one. -/ +theorem mulVec_le_one {m n : Type*} [Fintype n] [Semiring R] [PartialOrder R] [IsOrderedRing R] + {M : Matrix m n R} (hM : ∀ i j, 0 ≤ M i j) (hM1 : M *ᵥ 1 ≤ 1) {v : n → R} + (hv : v ≤ 1) : + M *ᵥ v ≤ 1 := fun i => + le_trans (Finset.sum_le_sum fun j _ => mul_le_mul_of_nonneg_left (hv j) (hM i j)) (hM1 i) + +/-- **Corrections keep rows substochastic.** If `E ≥ 0` and the rows of `C` sum to at most one, +then each row of `C - E + E C` sums to at most the corresponding row of `C`. -/ +theorem correction_mulVec_one_le [Ring R] [PartialOrder R] [IsOrderedRing R] + {C E : Matrix V V R} (hE : ∀ i j, 0 ≤ E i j) (hC : C *ᵥ 1 ≤ 1) : + (C - E + E * C) *ᵥ 1 ≤ C *ᵥ 1 := by + rw [correction_mulVec_one] + exact sub_le_self _ (mulVec_nonneg hE (sub_nonneg.mpr hC)) + +end Correction + +section Copy + +variable {V ι R : Type*} + +/-- **A copy step.** Each vertex `x` gets copies `(x, i)` with row weights `r i x`, and the entry +`D x y` is split among the copies `(y, j)` of its target in proportions `s x y j`. In the +preprint the proportions depend only on the size of `D x y`, and the copies beyond a primary one +are activated only at targets where the correction was suppressed +[OpenAI2026LogSpace, Section 4.4]. -/ +@[expose] def copySplit [Mul R] (r : ι → V → R) (s : V → V → ι → R) (D : Matrix V V R) : + Matrix (V × ι) (V × ι) R := + of fun a b => r a.2 a.1 * D a.1 b.1 * s a.1 b.1 b.2 + +/-- The *copy projection* from copies to their parents, weighted by `r`: the copy `(x, i)` maps +to `x` with weight `r i x`. -/ +@[expose] def copyWeight [DecidableEq V] [Zero R] (r : ι → V → R) : Matrix (V × ι) V R := + of fun a z => if a.1 = z then r a.2 a.1 else 0 + +@[simp] +theorem copyWeight_mulVec [Fintype V] [DecidableEq V] [NonUnitalNonAssocSemiring R] + (r : ι → V → R) (v : V → R) (a : V × ι) : + (copyWeight r *ᵥ v) a = r a.2 a.1 * v a.1 := by + simp [copyWeight, mulVec, dotProduct, ite_mul] + +/-- A copy with weight one projects to its parent exactly. -/ +theorem copyWeight_apply_of_eq_one [DecidableEq V] [Semiring R] {r : ι → V → R} {x : V} + {i : ι} (h : r i x = 1) (w : V) : copyWeight r (x, i) w = if w = x then 1 else 0 := by + simp [copyWeight, h, eq_comm] + +/-- **Copies intertwine with their projection.** If, on every nonzero entry `D x y`, the +proportions `s x y j` weighted by `r j y` sum to one, then splitting `D` into copies and +projecting back agrees with projecting first: `copySplit r s D * copyWeight r = +copyWeight r * D` [OpenAI2026LogSpace, Proposition 4.5]. -/ +theorem copySplit_mul_copyWeight [Fintype V] [DecidableEq V] [Fintype ι] [Semiring R] + {r : ι → V → R} {s : V → V → ι → R} {D : Matrix V V R} + (hs : ∀ x y, D x y ≠ 0 → ∑ j, s x y j * r j y = 1) : + copySplit r s D * copyWeight r = copyWeight r * D := by + ext ⟨x, i⟩ z + have hL : (copySplit r s D * copyWeight r) (x, i) z = r i x * D x z * ∑ j, s x z j * r j z := by + rw [mul_apply, Fintype.sum_prod_type, Fintype.sum_eq_single z fun y hy => ?_, Finset.mul_sum] + · simp [copySplit, copyWeight, mul_assoc] + · simp [copyWeight, hy] + have hR : (copyWeight r * D) (x, i) z = r i x * D x z := by + rw [mul_apply, Fintype.sum_eq_single x fun y hy => ?_] + · simp [copyWeight] + · simp [copyWeight, Ne.symm hy] + rw [hL, hR] + by_cases hD : D x z = 0 + · simp [hD] + · rw [hs x z hD, mul_one] + +theorem copySplit_nonneg [Semiring R] [PartialOrder R] [IsOrderedRing R] {r : ι → V → R} + {s : V → V → ι → R} {D : Matrix V V R} (hr : ∀ i x, 0 ≤ r i x) + (hs : ∀ x y j, 0 ≤ s x y j) (hD : ∀ x y, 0 ≤ D x y) (a b : V × ι) : + 0 ≤ copySplit r s D a b := + mul_nonneg (mul_nonneg (hr _ _) (hD _ _)) (hs _ _ _) + +/-- **Copies keep rows substochastic** when the weights are at most one and the proportions of +each entry sum to at most one. -/ +theorem copySplit_mulVec_one_le [Fintype V] [Fintype ι] [Semiring R] [PartialOrder R] + [IsOrderedRing R] {r : ι → V → R} {s : V → V → ι → R} {D : Matrix V V R} + (hr0 : ∀ i x, 0 ≤ r i x) (hr1 : ∀ i x, r i x ≤ 1) (hs1 : ∀ x y, ∑ j, s x y j ≤ 1) + (hD0 : ∀ x y, 0 ≤ D x y) (hD1 : D *ᵥ 1 ≤ 1) : copySplit r s D *ᵥ 1 ≤ 1 := by + rintro ⟨x, i⟩ + have hrow : ∑ b : V × ι, copySplit r s D (x, i) b ≤ r i x * ∑ y, D x y := by + rw [Fintype.sum_prod_type, Finset.mul_sum] + refine Finset.sum_le_sum fun y _ => ?_ + simp only [copySplit, of_apply, ← Finset.mul_sum] + exact mul_le_of_le_one_right (mul_nonneg (hr0 i x) (hD0 x y)) (hs1 x y) + have hDx : ∑ y, D x y ≤ 1 := by simpa [mulVec, dotProduct] using hD1 x + simpa [mulVec, dotProduct] using + (hrow.trans (mul_le_of_le_one_right (hr0 i x) hDx)).trans (hr1 i x) + +end Copy + +section Hierarchy + +variable {V : ℕ → Type*} [∀ l, Fintype (V l)] [∀ l, DecidableEq (V l)] {R : Type*} + +/-- **The cumulative projection** of a sequence of stages with projections +`P l : Matrix (V (l + 1)) (V l) R`: the product `P (l - 1) * ⋯ * P 0`, from stage `l` to +stage `0`. -/ +@[expose] def copyProjection [Semiring R] (P : ∀ l, Matrix (V (l + 1)) (V l) R) : + ∀ l, Matrix (V l) (V 0) R + | 0 => 1 + | l + 1 => P l * copyProjection P l + +/-- **The transported reward matrix** of a sequence of stages with projections `P l` and +corrections `E l`: `B (l + 1) = P l * (1 + E l) * B l`, starting from `B 0 = 1`. Applied to the +initial reward `e`, it gives the stage-`l` reward `B l e`. -/ +@[expose] def rewardTransport [Semiring R] (P : ∀ l, Matrix (V (l + 1)) (V l) R) + (E : ∀ l, Matrix (V l) (V l) R) : ∀ l, Matrix (V l) (V 0) R + | 0 => 1 + | l + 1 => P l * (1 + E l) * rewardTransport P E l + +variable {C E : ∀ l, Matrix (V l) (V l) R} {P : ∀ l, Matrix (V (l + 1)) (V l) R} + +/-- **The reward transport identity.** If each stage's transition matrix intertwines with the +corrected matrix of the previous stage, `C (l + 1) * P l = P l * (C l - E l + E l * C l)`, then +`C l * Pc l = Pc l - B l * (1 - C 0)` for the cumulative projection `Pc` and the transported +reward matrix `B` [OpenAI2026LogSpace, Proposition 4.7]. -/ +theorem mul_copyProjection [Ring R] + (h : ∀ l, C (l + 1) * P l = P l * (C l - E l + E l * C l)) (l : ℕ) : + C l * copyProjection P l = copyProjection P l - rewardTransport P E l * (1 - C 0) := by + induction l with + | zero => simp [copyProjection, rewardTransport] + | succ l ih => + have hD : C l - E l + E l * C l = 1 - (1 + E l) * (1 - C l) := by + rw [one_add_mul_one_sub_eq_one_sub, sub_sub_cancel] + have hB : (1 - C l) * copyProjection P l = rewardTransport P E l * (1 - C 0) := by + rw [Matrix.sub_mul, Matrix.one_mul, ih, sub_sub_cancel] + calc C (l + 1) * copyProjection P (l + 1) + = P l * (C l - E l + E l * C l) * copyProjection P l := by + rw [copyProjection, ← Matrix.mul_assoc, h] + _ = P l * copyProjection P l - P l * (1 + E l) * ((1 - C l) * copyProjection P l) := by + rw [hD] + simp only [Matrix.mul_sub, Matrix.sub_mul, Matrix.mul_one, Matrix.one_mul, + Matrix.mul_assoc] + _ = copyProjection P (l + 1) - rewardTransport P E (l + 1) * (1 - C 0) := by + rw [hB] + simp only [copyProjection, rewardTransport, Matrix.mul_assoc] + +/-- **The transported reward.** If `p` solves `(1 - C 0) p = e`, the stage-`l` reward is +`B l e = Pc l p - C l (Pc l p)`: the projected solution minus what the remaining transitions +still carry [OpenAI2026LogSpace, Proposition 4.7]. -/ +theorem rewardTransport_mulVec [Ring R] + (h : ∀ l, C (l + 1) * P l = P l * (C l - E l + E l * C l)) {p e : V 0 → R} + (hp : (1 - C 0) *ᵥ p = e) (l : ℕ) : + rewardTransport P E l *ᵥ e = + copyProjection P l *ᵥ p - C l *ᵥ (copyProjection P l *ᵥ p) := by + rw [mulVec_mulVec, mul_copyProjection h, sub_mulVec, ← mulVec_mulVec, hp, sub_sub_cancel] + +/-- The stage rewards are updated by adding the correction's contribution and projecting: +`W (l + 1) = P l (W l + E l W l)`. -/ +theorem rewardTransport_succ_mulVec [Semiring R] (e : V 0 → R) (l : ℕ) : + rewardTransport P E (l + 1) *ᵥ e = + P l *ᵥ (rewardTransport P E l *ᵥ e + E l *ᵥ (rewardTransport P E l *ᵥ e)) := by + rw [rewardTransport, ← mulVec_mulVec, ← mulVec_mulVec, add_mulVec, one_mulVec] + +/-- Along *primary copies* `z l`, whose rows of `P l` are unit vectors, the cumulative projection +reads off the original coordinate. -/ +theorem copyProjection_mulVec_primary [Semiring R] {z : ∀ l, V l} + (hz : ∀ l w, P l (z (l + 1)) w = if w = z l then 1 else 0) (p : V 0 → R) (l : ℕ) : + (copyProjection P l *ᵥ p) (z l) = p (z 0) := by + induction l with + | zero => simp [copyProjection] + | succ l ih => + rw [copyProjection, ← mulVec_mulVec] + simp [mulVec, dotProduct, hz, ite_mul, ← ih] + +section Order + +variable [Ring R] [PartialOrder R] [IsOrderedRing R] + +private theorem one_apply_nonneg {n : Type*} [DecidableEq n] (i j : n) : + (0 : R) ≤ (1 : Matrix n n R) i j := by + rw [one_apply]; split_ifs <;> simp + +private theorem mul_nonneg_entries {m n o : Type*} [Fintype n] {A : Matrix m n R} + {B : Matrix n o R} (hA : ∀ i j, 0 ≤ A i j) (hB : ∀ i j, 0 ≤ B i j) (i : m) (k : o) : + 0 ≤ (A * B) i k := + Finset.sum_nonneg fun j _ => mul_nonneg (hA i j) (hB j k) + +theorem copyProjection_nonneg (hP : ∀ l i j, 0 ≤ P l i j) (l : ℕ) : + ∀ i j, 0 ≤ copyProjection P l i j := by + induction l with + | zero => exact one_apply_nonneg + | succ l ih => exact mul_nonneg_entries (hP l) ih + +/-- The cumulative projection of substochastic projections is substochastic. -/ +theorem copyProjection_mulVec_one_le (hP : ∀ l i j, 0 ≤ P l i j) (hP1 : ∀ l, P l *ᵥ 1 ≤ 1) + (l : ℕ) : copyProjection P l *ᵥ 1 ≤ 1 := by + induction l with + | zero => simp [copyProjection] + | succ l ih => + rw [copyProjection, ← mulVec_mulVec] + exact mulVec_le_one (hP l) (hP1 l) ih + +theorem rewardTransport_nonneg (hP : ∀ l i j, 0 ≤ P l i j) (hE : ∀ l i j, 0 ≤ E l i j) + (l : ℕ) : ∀ i j, 0 ≤ rewardTransport P E l i j := by + induction l with + | zero => exact one_apply_nonneg + | succ l ih => + exact mul_nonneg_entries (mul_nonneg_entries (hP l) + (fun i j => add_nonneg (one_apply_nonneg i j) (hE l i j))) ih + +variable (hP : ∀ l i j, 0 ≤ P l i j) (hP1 : ∀ l, P l *ᵥ 1 ≤ 1) + (hC : ∀ l i j, 0 ≤ C l i j) (hstep : ∀ l, C (l + 1) * P l = P l * (C l - E l + E l * C l)) + {p e : V 0 → R} + (hp : (1 - C 0) *ᵥ p = e) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) +include hP hP1 hC hstep hp hp0 hp1 + +/-- The stage rewards are bounded by the projected solution, hence by one. -/ +theorem rewardTransport_mulVec_le (l : ℕ) : + rewardTransport P E l *ᵥ e ≤ copyProjection P l *ᵥ p ∧ + copyProjection P l *ᵥ p ≤ 1 := by + have hPc0 : 0 ≤ copyProjection P l *ᵥ p := mulVec_nonneg (copyProjection_nonneg hP l) hp0 + refine ⟨?_, mulVec_le_one (copyProjection_nonneg hP l) + (copyProjection_mulVec_one_le hP hP1 l) hp1⟩ + rw [rewardTransport_mulVec hstep hp] + exact sub_le_self _ (mulVec_nonneg (hC l) hPc0) + +/-- **The stage error.** Along primary copies `z l`, the stage-`l` reward underestimates the +solution at `z 0` by at most the row sum of `C l` at `z l` +[OpenAI2026LogSpace, Proposition 4.7]. -/ +theorem sub_rewardTransport_mulVec_mem_Icc {z : ∀ l, V l} + (hz : ∀ l w, P l (z (l + 1)) w = if w = z l then 1 else 0) (l : ℕ) : + p (z 0) - (rewardTransport P E l *ᵥ e) (z l) ∈ Set.Icc 0 (∑ y, C l (z l) y) := by + have hPc0 : 0 ≤ copyProjection P l *ᵥ p := mulVec_nonneg (copyProjection_nonneg hP l) hp0 + have hPc1 : copyProjection P l *ᵥ p ≤ 1 := + (rewardTransport_mulVec_le hP hP1 hC hstep hp hp0 hp1 l).2 + rw [rewardTransport_mulVec hstep hp, Pi.sub_apply, copyProjection_mulVec_primary hz, + sub_sub_cancel] + exact ⟨mulVec_nonneg (hC l) hPc0 _, Finset.sum_le_sum fun y _ => + mul_le_of_le_one_right (hC l _ y) (hPc1 y)⟩ + +/-- **The stage error, by counting.** If the entries of `C l` are at most `ε` and its nonzero +columns lie in `A`, the stage-`l` reward along primary copies underestimates the solution by at +most `|A| ε`. -/ +theorem sub_rewardTransport_mulVec_le_card_mul {z : ∀ l, V l} + (hz : ∀ l w, P l (z (l + 1)) w = if w = z l then 1 else 0) (l : ℕ) {ε : R} + (hε : ∀ x y, C l x y ≤ ε) {A : Finset (V l)} (hA : ∀ x y, C l x y ≠ 0 → y ∈ A) : + p (z 0) - (rewardTransport P E l *ᵥ e) (z l) ≤ A.card • ε := by + refine (sub_rewardTransport_mulVec_mem_Icc hP hP1 hC hstep hp hp0 hp1 hz l).2.trans ?_ + rw [← Finset.sum_subset (Finset.subset_univ A) fun y _ hy => by_contra fun h => hy (hA _ y h)] + exact Finset.sum_le_card_nsmul _ _ _ fun y _ => hε _ y + +end Order + +/-- **The stage bound.** If the entries of `C l` are at most `(2 ^ (c + 1))⁻¹ ^ l` and its +nonzero columns lie in a set of at most `2 ^ l * n` vertices, then along primary copies +`0 ≤ p (z 0) - W l (z l) ≤ n * (2 ^ c)⁻¹ ^ l`. With `n` the number of vertices of stage `0`, +this is the preprint's bound `|V₀| 2 ^ (-(H - 1) l)` for `H = c + 1` +[OpenAI2026LogSpace, Proposition 4.7]. -/ +theorem sub_rewardTransport_mulVec_le_pow [Field R] [LinearOrder R] [IsStrictOrderedRing R] + (hP : ∀ l i j, 0 ≤ P l i j) (hP1 : ∀ l, P l *ᵥ 1 ≤ 1) (hC : ∀ l i j, 0 ≤ C l i j) + (hstep : ∀ l, C (l + 1) * P l = P l * (C l - E l + E l * C l)) {p e : V 0 → R} + (hp : (1 - C 0) *ᵥ p = e) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {z : ∀ l, V l} + (hz : ∀ l w, P l (z (l + 1)) w = if w = z l then 1 else 0) {c n : ℕ} + (hε : ∀ l x y, C l x y ≤ ((2 : R) ^ (c + 1))⁻¹ ^ l) (A : ∀ l, Finset (V l)) + (hA : ∀ l x y, C l x y ≠ 0 → y ∈ A l) (hAn : ∀ l, (A l).card ≤ 2 ^ l * n) + (l : ℕ) : + 0 ≤ p (z 0) - (rewardTransport P E l *ᵥ e) (z l) ∧ + p (z 0) - (rewardTransport P E l *ᵥ e) (z l) ≤ n * ((2 : R) ^ c)⁻¹ ^ l := by + refine ⟨(sub_rewardTransport_mulVec_mem_Icc hP hP1 hC hstep hp hp0 hp1 hz l).1, ?_⟩ + refine (sub_rewardTransport_mulVec_le_card_mul hP hP1 hC hstep hp hp0 hp1 hz l (hε l) + (hA l)).trans ?_ + rw [nsmul_eq_mul] + calc ((A l).card : R) * ((2 : R) ^ (c + 1))⁻¹ ^ l + ≤ (2 ^ l * n : ℕ) * ((2 : R) ^ (c + 1))⁻¹ ^ l := + mul_le_mul_of_nonneg_right (by exact_mod_cast hAn l) + (pow_nonneg (inv_nonneg.mpr (pow_nonneg zero_le_two _)) _) + _ = n * ((2 : R) ^ c)⁻¹ ^ l := by + have h2 : (2 : R) ^ l ≠ 0 := pow_ne_zero _ two_ne_zero + push_cast + rw [pow_succ, mul_inv, mul_pow, inv_pow (2 : R), mul_comm ((2 : R) ^ l), mul_assoc, + ← mul_assoc ((2 : R) ^ l), mul_comm ((2 : R) ^ l), mul_assoc _ ((2 : R) ^ l), + mul_inv_cancel₀ h2, mul_one] + +end Hierarchy + +end Matrix diff --git a/ComplexityTests/CorrectionHierarchy.lean b/ComplexityTests/CorrectionHierarchy.lean new file mode 100644 index 000000000..03ad463c2 --- /dev/null +++ b/ComplexityTests/CorrectionHierarchy.lean @@ -0,0 +1,122 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexity.Foundations.LinearAlgebra.Matrix.CorrectionHierarchy + +/-! +# Tests for corrections, copies and reward transport +-/ + +namespace ComplexityTests.CorrectionHierarchy + +open Matrix + +/-- A walk on three time layers: from `0` to `1` and from `1` to `2`, each with probability +`1 / 2`; it stops otherwise. -/ +private def C : Matrix (Fin 3) (Fin 3) ℚ := !![0, 1 / 2, 0; 0, 0, 1 / 2; 0, 0, 0] + +/-- The reward is collected at `2`. -/ +private def e : Fin 3 → ℚ := ![0, 0, 1] + +/-- The expected rewards: `1 / 4` from `0`, `1 / 2` from `1`. -/ +private def p : Fin 3 → ℚ := ![1 / 4, 1 / 2, 1] + +private theorem one_sub_C_mulVec_p : (1 - C) *ᵥ p = e := by + ext i; fin_cases i <;> norm_num [C, p, e, mulVec, dotProduct, Fin.sum_univ_three, one_apply] + +/-- The correction removes the second transition. -/ +private def E : Matrix (Fin 3) (Fin 3) ℚ := !![0, 0, 0; 0, 0, 1 / 2; 0, 0, 0] + +private theorem E_strict : E.IsStrictUpperTriangular := by + intro i j h + fin_cases i <;> fin_cases j <;> simp_all [E] + +-- The corrected matrix keeps only the first transition. +example : C - E + E * C = !![0, 1 / 2, 0; 0, 0, 0; 0, 0, 0] := by + ext i j; fin_cases i <;> fin_cases j <;> simp [C, E] + +-- The removed weight `1 / 2` reappears as a reward at `1`, and `p` still solves the corrected +-- equation. +example : (1 - (C - E + E * C)) *ᵥ p = ![0, 1 / 2, 1] := by + rw [one_sub_correction_mulVec, one_sub_C_mulVec_p] + ext i; fin_cases i <;> simp [E, e, mulVec, dotProduct, Fin.sum_univ_three, one_apply] + +private theorem inv_one_sub_C : (1 - C)⁻¹ = 1 + C + C * C := + inv_eq_left_inv <| by + ext i j; fin_cases i <;> fin_cases j <;> + simp [C, mul_apply, Fin.sum_univ_three, one_apply] + +-- The acceptance probabilities of the corrected walk with the corrected reward are those of +-- the original walk: `1 / 4` from `0`. +example : ((1 - (C - E + E * C))⁻¹ *ᵥ (e + E *ᵥ e)) 0 = 1 / 4 := by + rw [E_strict.inv_one_sub_correction_mulVec, inv_one_sub_C] + simp [C, e, mulVec, dotProduct, Fin.sum_univ_three, one_apply] + norm_num + +-- Corrections keep the rows substochastic. +example : (C - E + E * C) *ᵥ 1 ≤ C *ᵥ 1 := + correction_mulVec_one_le (fun i j => by fin_cases i <;> fin_cases j <;> simp [E]) fun i => by + fin_cases i <;> simp [C, mulVec, dotProduct, Fin.sum_univ_three] <;> norm_num + +/-! ### Copies -/ + +/-- Both copies of every vertex are active. -/ +private def r : Fin 2 → Fin 3 → ℚ := fun _ _ => 1 + +/-- Every entry is split evenly between the two copies of its target. -/ +private def s : Fin 3 → Fin 3 → Fin 2 → ℚ := fun _ _ _ => 1 / 2 + +-- Splitting halves the entries and intertwines with the copy projection. +example : copySplit r s C ((0 : Fin 3), (0 : Fin 2)) ((1 : Fin 3), (1 : Fin 2)) = 1 / 4 := by + norm_num [copySplit, r, s, C] + +example : copySplit r s C * copyWeight r = copyWeight r * C := + copySplit_mul_copyWeight fun _ _ _ => by simp [r, s] + +example : copySplit r s C *ᵥ 1 ≤ 1 := + copySplit_mulVec_one_le (fun _ _ => by simp [r]) (fun _ _ => le_rfl) + (fun _ _ => by simp [s]) + (fun i j => by fin_cases i <;> fin_cases j <;> simp [C]) + fun i => by fin_cases i <;> norm_num [C, mulVec, dotProduct, Fin.sum_univ_three] + +/-! ### Reward transport + +A one-step hierarchy: the correction `C + C ^ 2` removes every transition of `C`, since +`C ^ 3 = 0`, so the stage-`1` matrix is zero and the stage-`1` reward is exact. -/ + +private def Cs (l : ℕ) : Matrix (Fin 3) (Fin 3) ℚ := if l = 0 then C else 0 + +private def Es (l : ℕ) : Matrix (Fin 3) (Fin 3) ℚ := if l = 0 then C + C * C else 0 + +private def Ps (_ : ℕ) : Matrix (Fin 3) (Fin 3) ℚ := 1 + +private theorem C_cube : C * C * C = 0 := by + ext i j; fin_cases i <;> fin_cases j <;> simp [C, mul_apply, Fin.sum_univ_three] + +private theorem hstep (l : ℕ) : Cs (l + 1) * Ps l = Ps l * (Cs l - Es l + Es l * Cs l) := by + rcases l with _ | l + · simp only [Cs, Es, Ps, ↓reduceIte, Nat.add_one_ne_zero, Matrix.zero_mul, Matrix.one_mul] + rw [← C_cube]; noncomm_ring + · simp [Cs, Es, Ps] + +private theorem nonneg_C : ∀ i j, 0 ≤ C i j := by + intro i j; fin_cases i <;> fin_cases j <;> simp [C] + +-- From `0`, the stage-`1` reward equals the acceptance probability `1 / 4`: the error bound is +-- the row sum of the zero matrix. +example : (rewardTransport (V := fun _ => Fin 3) Ps Es 1 *ᵥ e) 0 = 1 / 4 := by + have h := sub_rewardTransport_mulVec_mem_Icc (V := fun _ => Fin 3) (C := Cs) (E := Es) + (P := Ps) (z := fun _ => 0) (fun _ i j => by simp [Ps, one_apply]; split_ifs <;> simp) + (fun _ => by simp [Ps]) (fun l i j => by unfold Cs; split_ifs <;> simp [nonneg_C]) + hstep (p := p) (e := e) (by simpa [Cs] using one_sub_C_mulVec_p) + (fun i => by fin_cases i <;> norm_num [p]) + (fun i => by fin_cases i <;> norm_num [p]) + (fun _ w => by simp [Ps, one_apply, eq_comm]) 1 + have hp0 : p 0 = 1 / 4 := rfl + simp only [Cs, Nat.add_one_ne_zero, ↓reduceIte, Matrix.zero_apply, Finset.sum_const_zero, + Set.mem_Icc] at h + linarith [h.1, h.2] + +end ComplexityTests.CorrectionHierarchy diff --git a/references.bib b/references.bib index ffd09ecfe..39e270d93 100644 --- a/references.bib +++ b/references.bib @@ -3451,6 +3451,15 @@ @misc{OpenAI2026ETH url = {https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf} } +@misc{OpenAI2026LogSpace, + author = {{OpenAI}}, + title = {Exact Derandomization of Logarithmic Space: {L} = {RL} = {BPL}}, + year = {2026}, + howpublished = {Preprint}, + note = {Dated 23 September 2026, not peer reviewed; source revision 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a}, + url = {https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026/paper.pdf} +} + @misc{OpenAI2026RationalHitting, author = {{OpenAI}}, title = {{Rational} matrix hitting lists for noncommutative rational formulas}, From 832f9390cd08ee432c7d3a14ae70d623b647fd80 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:05:28 +0000 Subject: [PATCH 2/8] fix(Foundations): expose IsStrictUpperTriangular so importers can apply it Co-Authored-By: Claude Opus 5.5 --- .../Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean b/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean index 606c43617..4ded7fdbb 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean @@ -97,7 +97,7 @@ variable {V R : Type*} /-- A square matrix is *strictly upper triangular* when its entry at `(i, j)` vanishes unless `i < j`. For the time-layered transition matrices of a machine, ordered by time, this says that every transition moves strictly forward. -/ -def IsStrictUpperTriangular [LT V] [Zero R] (M : Matrix V V R) : Prop := +@[expose] def IsStrictUpperTriangular [LT V] [Zero R] (M : Matrix V V R) : Prop := ∀ ⦃i j⦄, ¬ i < j → M i j = 0 namespace IsStrictUpperTriangular From 1fbc2671b8dbcee6119dbd9f79b4a36b2bf4b52a Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:15:03 +0000 Subject: [PATCH 3/8] fix(Foundations): separate row-sum control from nonnegativity; add reward lower bound Review of #1676: correction_mulVec_one_le only shows that row sums do not grow, so its docstring, the module summary and the test comment no longer call it substochasticity. Add rewardTransport_mulVec_nonneg, the lower half of (4.30), under nonnegative projections, corrections and reward. Co-Authored-By: Claude Opus 5.5 --- .../Matrix/CorrectionHierarchy.lean | 24 ++++++++++++++----- ComplexityTests/CorrectionHierarchy.lean | 12 +++++++++- 2 files changed, 29 insertions(+), 7 deletions(-) diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean b/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean index 4ded7fdbb..2420fb961 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean @@ -65,9 +65,11 @@ the copies (factorial truncation, detectors) are not part of this file. of `C` is the expected corrected reward of `C - E + E C`. * `Matrix.IsStrictUpperTriangular.det_one_add`: `det (1 + E) = 1` for strictly upper triangular `E`. -* `Matrix.correction_mulVec_one_le`: corrections keep matrices substochastic. +* `Matrix.correction_mulVec_one_le`: nonnegative corrections do not increase row sums. * `Matrix.copySplit_mul_copyWeight`: a copy step intertwines with its projection. * `Matrix.mul_copyProjection`, `Matrix.rewardTransport_mulVec`: the reward transport identity. +* `Matrix.rewardTransport_mulVec_nonneg`, `Matrix.rewardTransport_mulVec_le`: the stage rewards + lie between `0` and the projected solution. * `Matrix.sub_rewardTransport_mulVec_mem_Icc`, `Matrix.sub_rewardTransport_mulVec_le_card_mul`, `Matrix.sub_rewardTransport_mulVec_le_pow`: the transported reward is a lower bound with error controlled by the last transition matrix. @@ -187,8 +189,10 @@ theorem mulVec_le_one {m n : Type*} [Fintype n] [Semiring R] [PartialOrder R] [I M *ᵥ v ≤ 1 := fun i => le_trans (Finset.sum_le_sum fun j _ => mul_le_mul_of_nonneg_left (hv j) (hM i j)) (hM1 i) -/-- **Corrections keep rows substochastic.** If `E ≥ 0` and the rows of `C` sum to at most one, -then each row of `C - E + E C` sums to at most the corresponding row of `C`. -/ +/-- **Corrections do not increase row sums.** If `E ≥ 0` and the rows of `C` sum to at most one, +then each row of `C - E + E C` sums to at most the corresponding row of `C`. This says nothing +about the signs of the entries of `C - E + E C`; their nonnegativity depends on how `E` is +chosen [OpenAI2026LogSpace, Lemma 4.4]. -/ theorem correction_mulVec_one_le [Ring R] [PartialOrder R] [IsOrderedRing R] {C E : Matrix V V R} (hE : ∀ i j, 0 ≤ E i j) (hC : C *ᵥ 1 ≤ 1) : (C - E + E * C) *ᵥ 1 ≤ C *ᵥ 1 := by @@ -254,8 +258,9 @@ theorem copySplit_nonneg [Semiring R] [PartialOrder R] [IsOrderedRing R] {r : ι 0 ≤ copySplit r s D a b := mul_nonneg (mul_nonneg (hr _ _) (hD _ _)) (hs _ _ _) -/-- **Copies keep rows substochastic** when the weights are at most one and the proportions of -each entry sum to at most one. -/ +/-- **Copies keep row sums at most one** when the weights lie in `[0, 1]`, `D` is nonnegative +with row sums at most one, and the proportions of each entry sum to at most one. Together with +`Matrix.copySplit_nonneg` this makes the copy step substochastic. -/ theorem copySplit_mulVec_one_le [Fintype V] [Fintype ι] [Semiring R] [PartialOrder R] [IsOrderedRing R] {r : ι → V → R} {s : V → V → ι → R} {D : Matrix V V R} (hr0 : ∀ i x, 0 ≤ r i x) (hr1 : ∀ i x, r i x ≤ 1) (hs1 : ∀ x y, ∑ j, s x y j ≤ 1) @@ -383,13 +388,20 @@ theorem rewardTransport_nonneg (hP : ∀ l i j, 0 ≤ P l i j) (hE : ∀ l i j, exact mul_nonneg_entries (mul_nonneg_entries (hP l) (fun i j => add_nonneg (one_apply_nonneg i j) (hE l i j))) ih +/-- The stage rewards are nonnegative when the projections, the corrections and the initial reward +are [OpenAI2026LogSpace, Proposition 4.7]. -/ +theorem rewardTransport_mulVec_nonneg (hP : ∀ l i j, 0 ≤ P l i j) (hE : ∀ l i j, 0 ≤ E l i j) + {e : V 0 → R} (he : 0 ≤ e) (l : ℕ) : 0 ≤ rewardTransport P E l *ᵥ e := + mulVec_nonneg (rewardTransport_nonneg hP hE l) he + variable (hP : ∀ l i j, 0 ≤ P l i j) (hP1 : ∀ l, P l *ᵥ 1 ≤ 1) (hC : ∀ l i j, 0 ≤ C l i j) (hstep : ∀ l, C (l + 1) * P l = P l * (C l - E l + E l * C l)) {p e : V 0 → R} (hp : (1 - C 0) *ᵥ p = e) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) include hP hP1 hC hstep hp hp0 hp1 -/-- The stage rewards are bounded by the projected solution, hence by one. -/ +/-- The stage rewards are bounded by the projected solution, hence by one. For the lower bound +see `Matrix.rewardTransport_mulVec_nonneg`. -/ theorem rewardTransport_mulVec_le (l : ℕ) : rewardTransport P E l *ᵥ e ≤ copyProjection P l *ᵥ p ∧ copyProjection P l *ᵥ p ≤ 1 := by diff --git a/ComplexityTests/CorrectionHierarchy.lean b/ComplexityTests/CorrectionHierarchy.lean index 03ad463c2..c6bb668e6 100644 --- a/ComplexityTests/CorrectionHierarchy.lean +++ b/ComplexityTests/CorrectionHierarchy.lean @@ -55,7 +55,7 @@ example : ((1 - (C - E + E * C))⁻¹ *ᵥ (e + E *ᵥ e)) 0 = 1 / 4 := by simp [C, e, mulVec, dotProduct, Fin.sum_univ_three, one_apply] norm_num --- Corrections keep the rows substochastic. +-- A nonnegative correction does not increase the row sums. example : (C - E + E * C) *ᵥ 1 ≤ C *ᵥ 1 := correction_mulVec_one_le (fun i j => by fin_cases i <;> fin_cases j <;> simp [E]) fun i => by fin_cases i <;> simp [C, mulVec, dotProduct, Fin.sum_univ_three] <;> norm_num @@ -119,4 +119,14 @@ example : (rewardTransport (V := fun _ => Fin 3) Ps Es 1 *ᵥ e) 0 = 1 / 4 := by Set.mem_Icc] at h linarith [h.1, h.2] +-- The transported rewards are nonnegative. +example : 0 ≤ rewardTransport (V := fun _ => Fin 3) Ps Es 1 *ᵥ e := + rewardTransport_mulVec_nonneg (V := fun _ => Fin 3) + (fun _ i j => by simp only [Ps, one_apply]; split_ifs <;> simp) + (fun l i j => by + unfold Es; split_ifs + · fin_cases i <;> fin_cases j <;> norm_num [C, mul_apply, Fin.sum_univ_three] + · simp) + (fun i => by fin_cases i <;> simp [e]) 1 + end ComplexityTests.CorrectionHierarchy From b5cc0590faa36fabf897783af15a6384793707f6 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:05:40 +0000 Subject: [PATCH 4/8] feat(Foundations): factorial truncation of cutoff corrections Second slice of #1444 Phase 2 (idea 3 of #474), following the OpenAI preprint (2026-09-23), Lemma 4.1 and Lemma 4.4: the cutoff correction recursion E = phi((C + EC)) on a strictly upper triangular C has a unique fixed point, its iterates increase towards it, and after k iterations the error is at most f e^(1/theta) (L/theta)^k / k!, independently of the size of the matrix. The corrected matrix of a finite iterate is nonnegative and small in fully corrected columns. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../Matrix/FactorialTruncation.lean | 483 ++++++++++++++++++ ComplexityTests/FactorialTruncation.lean | 93 ++++ 3 files changed, 577 insertions(+) create mode 100644 Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean create mode 100644 ComplexityTests/FactorialTruncation.lean diff --git a/Complexity.lean b/Complexity.lean index c0e4b8629..b1c2b3181 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2622,6 +2622,7 @@ public import Complexity.Foundations.LinearAlgebra.Interpolation public import Complexity.Foundations.LinearAlgebra.KernelVector public import Complexity.Foundations.LinearAlgebra.Matrix.CorrectionHierarchy public import Complexity.Foundations.LinearAlgebra.Matrix.CutRank +public import Complexity.Foundations.LinearAlgebra.Matrix.FactorialTruncation public import Complexity.Foundations.LinearAlgebra.Matrix.Kronecker public import Complexity.Foundations.LinearAlgebra.Matrix.Lindsey public import Complexity.Foundations.LinearAlgebra.Matrix.ListProd diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean b/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean new file mode 100644 index 000000000..ad9fe5b9c --- /dev/null +++ b/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean @@ -0,0 +1,483 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.LinearAlgebra.Matrix.CorrectionHierarchy +public import Mathlib.Analysis.SpecialFunctions.Exp +import Mathlib.Algebra.Ring.GeomSum +import Mathlib.Data.Nat.Choose.Bounds +import Mathlib.Topology.Algebra.Order.Floor + +/-! +# Factorial truncation of cutoff corrections + +Let `C` be a strictly upper triangular transition matrix with nonnegative entries at most `f` +and rows summing to at most one. A *cutoff correction* chooses the correction `E` of +`Matrix.one_sub_correction_mulVec` entrywise from the corrected input, +`E x y = φ y ((C + E C) x y)`, where each cutoff `φ y` is monotone, `L`-Lipschitz and leaves at +least `θ f` behind: `0 ≤ φ y t ≤ max (t - θ f) 0`. In the OpenAI preprint (2026-09-23), idea 3 in +issue #474, `φ y t = f Q (t / f) g y` for a smooth ramp `Q` and a column multiplier `g` +[OpenAI2026LogSpace, Section 4.1]. + +The equation is a recursion along the order of the columns, so it has exactly one solution +`Matrix.cutoffCorrectionFix φ C`, reached by iterating `Matrix.cutoffCorrection φ C` from zero +`card V` times (`Matrix.cutoffCorrection_fix`, `Matrix.eq_cutoffCorrectionFix`). The point of +the estimate is that far fewer iterations suffice, independently of the size of `V`: after `k` +iterations every entry is within `f e^(1 / θ) (L / θ)^k / k!` of the fixed point +(`Matrix.cutoffCorrectionFix_sub_iter_le`). + +The proof counts chains. In a fixed row, every positive entry of the fixed point leaves a residual +at least `θ f`, and the residuals of a row sum to at most one, so the row has at most `1 / (θ f)` +positive entries. Unrolling the recursion `k` times along that row expresses the error as a sum +over increasing chains of `k` of these entries, each weighted by at most `(L f)^k`; there are at +most `binomial (1 / (θ f), k) ≤ (θ f)^(-k) / k!` of them. + +For the finite correction `E = E k`, the corrected matrix `C - E + E C` is nonnegative +(`Matrix.cutoffCorrection_residual_nonneg`), and in a column whose cutoff leaves at most `θ₂ f` +behind its entries are at most `θ₂ f` plus the truncation error +(`Matrix.cutoffCorrection_residual_le`). Since `x ^ k / k!` tends to zero, a number of iterations +depending only on `θ`, `L` and the target accuracy suffices (`Matrix.exists_factorial_bound_le`). + +## Main definitions + +* `Matrix.cutoffCorrection`: one step `F ↦ φ y ((C + F C) x y)` of the recursion. +* `Matrix.cutoffCorrectionIter`: its `k`-th iterate from zero. +* `Matrix.cutoffCorrectionFix`: its unique fixed point. + +## Main results + +* `Matrix.cutoffCorrection_fix`, `Matrix.eq_cutoffCorrectionFix`: existence and uniqueness of the + fixed point, for strictly upper triangular `C`. +* `Matrix.cutoffCorrectionIter_le_fix`: the iterates increase towards the fixed point. +* `Matrix.cutoffCorrectionFix_sub_iter_le`: **factorial truncation**, the bound + `E* - E k ≤ f e^(1 / θ) (L / θ)^k / k!`. +* `Matrix.cutoffCorrection_residual_nonneg`, `Matrix.cutoffCorrection_residual_le`: the corrected + matrix of a finite iterate is nonnegative, with small entries in fully corrected columns. +* `Matrix.exists_factorial_bound_le`: a uniform number of iterations reaches any accuracy. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Lemma 4.1 and Lemma 4.4 (preprint, not peer reviewed). The estimate is of Picard type: compare + the factorial bound for Picard iterates of Lipschitz ODEs. +-/ + +public section + +open Finset + +namespace Matrix + +variable {V R : Type*} [Fintype V] + +section Recursion + +variable [NonUnitalNonAssocSemiring R] + +/-- **One step of the cutoff correction recursion**: the matrix with entry +`φ y ((C + F C) x y)` at `(x, y)`. -/ +@[expose] def cutoffCorrection (φ : V → R → R) (C F : Matrix V V R) : Matrix V V R := + of fun x y => φ y ((C + F * C) x y) + +/-- The `k`-th iterate of `Matrix.cutoffCorrection φ C` from the zero matrix. -/ +@[expose] def cutoffCorrectionIter (φ : V → R → R) (C : Matrix V V R) (k : ℕ) : Matrix V V R := + (cutoffCorrection φ C)^[k] 0 + +/-- The *cutoff correction* of `C`: the iterate after `card V` steps, which is the unique fixed +point of `Matrix.cutoffCorrection φ C` when `C` is strictly upper triangular. -/ +@[expose] def cutoffCorrectionFix (φ : V → R → R) (C : Matrix V V R) : Matrix V V R := + cutoffCorrectionIter φ C (Fintype.card V) + +variable {φ : V → R → R} {C : Matrix V V R} + +theorem cutoffCorrectionIter_succ (k : ℕ) : + cutoffCorrectionIter φ C (k + 1) = cutoffCorrection φ C (cutoffCorrectionIter φ C k) := + Function.iterate_succ_apply' _ _ _ + +variable [LinearOrder V] + +/-- The entry `(x, y)` of a correction step depends only on the entries `(x, z)` with `z < y`. -/ +private theorem cutoffCorrection_congr (hC : C.IsStrictUpperTriangular) {F G : Matrix V V R} + {x y : V} (h : ∀ z < y, F x z = G x z) : + cutoffCorrection φ C F x y = cutoffCorrection φ C G x y := by + simp only [cutoffCorrection, of_apply, add_apply, mul_apply] + congr 2 + refine Finset.sum_congr rfl fun z _ => ?_ + by_cases hz : z < y + · rw [h z hz] + · rw [hC hz, mul_zero, mul_zero] + +private theorem card_filter_lt_lt {y z : V} (hzy : z < y) : + #{w | w < z} < #{w | w < y} := + Finset.card_lt_card <| Finset.ssubset_iff_of_subset + (fun w hw => by simp only [mem_filter, mem_univ, true_and] at hw ⊢; exact hw.trans hzy) + |>.mpr ⟨z, by simpa using hzy, by simp⟩ + +/-- The iterates are stationary at `(x, y)` from the `(#{z | z < y} + 1)`-th on. -/ +private theorem cutoffCorrectionIter_succ_apply (hC : C.IsStrictUpperTriangular) (k : ℕ) : + ∀ x y : V, #{z | z < y} < k → + cutoffCorrectionIter φ C (k + 1) x y = cutoffCorrectionIter φ C k x y := by + induction k with + | zero => intro x y h; exact absurd h (Nat.not_lt_zero _) + | succ k ih => + intro x y h + rw [cutoffCorrectionIter_succ (k := k + 1)] + conv_rhs => rw [cutoffCorrectionIter_succ] + exact cutoffCorrection_congr hC fun z hz => + ih x z ((card_filter_lt_lt hz).trans_le (Nat.lt_succ_iff.mp h)) + +/-- **Existence of the cutoff correction**: `Matrix.cutoffCorrectionFix φ C` is a fixed point of +the recursion when `C` is strictly upper triangular [OpenAI2026LogSpace, Lemma 4.1]. -/ +theorem cutoffCorrection_fix (hC : C.IsStrictUpperTriangular) : + cutoffCorrection φ C (cutoffCorrectionFix φ C) = cutoffCorrectionFix φ C := by + ext x y + rw [cutoffCorrectionFix, ← cutoffCorrectionIter_succ] + refine cutoffCorrectionIter_succ_apply hC _ x y (Finset.card_lt_card ?_) + exact Finset.ssubset_iff_of_subset (Finset.subset_univ _) |>.mpr ⟨y, mem_univ _, by simp⟩ + +/-- **Uniqueness of the cutoff correction**: every fixed point of the recursion is +`Matrix.cutoffCorrectionFix φ C` when `C` is strictly upper triangular +[OpenAI2026LogSpace, Lemma 4.1]. -/ +theorem eq_cutoffCorrectionFix (hC : C.IsStrictUpperTriangular) {F : Matrix V V R} + (hF : cutoffCorrection φ C F = F) : F = cutoffCorrectionFix φ C := by + ext x y + induction y using WellFoundedLT.induction with + | ind y ih => + rw [← hF, ← cutoffCorrection_fix hC] + exact cutoffCorrection_congr hC ih + +end Recursion + +section Bounds + +variable [LinearOrder V] {φ : V → ℝ → ℝ} {C : Matrix V V ℝ} {f θ L : ℝ} + +omit [Fintype V] in +/-- Counting increasing chains by rank: summing a nonnegative `g` of the rank within `S` over the +members of `S` below `y` is at most summing `g` over the ranks below the rank of `y`. -/ +private theorem sum_rank_le (S : Finset V) (y : V) {g : ℕ → ℝ} (hg : ∀ j, 0 ≤ g j) : + ∑ z ∈ S.filter (· < y), g #(S.filter (· < z)) ≤ + ∑ j ∈ range #(S.filter (· < y)), g j := by + have hlt : ∀ {a b : V}, a ∈ S → a < b → #(S.filter (· < a)) < #(S.filter (· < b)) := + fun {a b} ha hab => Finset.card_lt_card <| Finset.ssubset_iff_of_subset + (fun w hw => by simp only [mem_filter] at hw ⊢; exact ⟨hw.1, hw.2.trans hab⟩) + |>.mpr ⟨a, by simp [ha, hab], by simp⟩ + have hinj : Set.InjOn (fun z => #(S.filter (· < z))) (S.filter (· < y) : Set V) := by + intro a ha b hb hab + simp only [coe_filter, Set.mem_ofPred_eq] at ha hb + by_contra hne + rcases lt_or_gt_of_ne hne with h | h + · exact (hlt ha.1 h).ne hab + · exact (hlt hb.1 h).ne hab.symm + rw [← Finset.sum_image (f := g) hinj] + refine Finset.sum_le_sum_of_subset_of_nonneg (fun j hj => ?_) fun j _ _ => hg j + obtain ⟨z, hz, rfl⟩ := Finset.mem_image.mp hj + simp only [mem_filter] at hz + exact Finset.mem_range.mpr (hlt hz.1 hz.2) + +/-- The hockey-stick identity `∑ j < n, (j choose k) = n choose (k + 1)`. -/ +private theorem sum_range_choose_eq (n k : ℕ) : + ∑ j ∈ range n, (j.choose k : ℝ) = (n.choose (k + 1) : ℝ) := by + induction n with + | zero => simp + | succ n ih => rw [sum_range_succ, ih, Nat.choose_succ_succ', Nat.cast_add, add_comm] + +variable (hC : C.IsStrictUpperTriangular) (hC0 : ∀ x y, 0 ≤ C x y) (hCf : ∀ x y, C x y ≤ f) + (hC1 : C *ᵥ 1 ≤ 1) (hφ0 : ∀ y t, 0 ≤ φ y t) (hφθ : ∀ y t, φ y t ≤ max (t - θ * f) 0) + (hφm : ∀ y, Monotone (φ y)) (hφL : ∀ y s t, s ≤ t → φ y t - φ y s ≤ L * (t - s)) + +section Monotone + +omit [LinearOrder V] in +include hC0 hφm in +private theorem cutoffCorrection_mono {F G : Matrix V V ℝ} (hFG : ∀ x y, F x y ≤ G x y) + (x y : V) : cutoffCorrection φ C F x y ≤ cutoffCorrection φ C G x y := by + refine hφm y ?_ + simp only [add_apply, mul_apply] + exact add_le_add_right (Finset.sum_le_sum fun z _ => + mul_le_mul_of_nonneg_right (hFG x z) (hC0 z y)) _ + +omit [LinearOrder V] in +include hφ0 in +theorem cutoffCorrectionIter_nonneg (k : ℕ) (x y : V) : 0 ≤ cutoffCorrectionIter φ C k x y := by + cases k with + | zero => simp [cutoffCorrectionIter] + | succ k => rw [cutoffCorrectionIter_succ]; exact hφ0 _ _ + +omit [LinearOrder V] in +include hC0 hφ0 hφm in +/-- The iterates increase. -/ +theorem cutoffCorrectionIter_le_succ (k : ℕ) (x y : V) : + cutoffCorrectionIter φ C k x y ≤ cutoffCorrectionIter φ C (k + 1) x y := by + induction k generalizing x y with + | zero => exact cutoffCorrectionIter_nonneg hφ0 1 x y + | succ k ih => + rw [cutoffCorrectionIter_succ, cutoffCorrectionIter_succ (k := k + 1)] + exact cutoffCorrection_mono hC0 hφm ih x y + +include hC hC0 hφ0 hφm in +/-- **The iterates increase towards the fixed point** [OpenAI2026LogSpace, Lemma 4.1]. -/ +theorem cutoffCorrectionIter_le_fix (k : ℕ) (x y : V) : + cutoffCorrectionIter φ C k x y ≤ cutoffCorrectionFix φ C x y := by + induction k generalizing x y with + | zero => exact cutoffCorrectionIter_nonneg hφ0 _ x y + | succ k ih => + rw [cutoffCorrectionIter_succ, ← cutoffCorrection_fix hC] + exact cutoffCorrection_mono hC0 hφm ih x y + +end Monotone + +omit [LinearOrder V] in +/-- The input `(C + F C) x y` of a correction step is nonnegative. -/ +private theorem correctionInput_nonneg (hC0 : ∀ x y, 0 ≤ C x y) {F : Matrix V V ℝ} + (hF : ∀ x y, 0 ≤ F x y) (x y : V) : 0 ≤ (C + F * C) x y := + add_nonneg (hC0 x y) (Finset.sum_nonneg fun z _ => mul_nonneg (hF x z) (hC0 z y)) + +omit [Fintype V] [LinearOrder V] in +include hφθ in +/-- A cutoff never exceeds its nonnegative input. -/ +private theorem cutoff_le_self (hθf : 0 ≤ θ * f) (y : V) {t : ℝ} (ht : 0 ≤ t) : φ y t ≤ t := + (hφθ y t).trans (max_le (by linarith) ht) + +omit [Fintype V] [LinearOrder V] in +include hφθ in +/-- A positive cutoff leaves at least `θ f` behind. -/ +private theorem le_sub_cutoff_of_pos (y : V) {t : ℝ} (h : 0 < φ y t) : θ * f ≤ t - φ y t := by + have h1 := hφθ y t + have h2 : 0 < t - θ * f := by + by_contra hneg + rw [max_eq_right (by linarith)] at h1 + linarith + rw [max_eq_left h2.le] at h1 + linarith + +include hC in +private theorem fix_apply (x y : V) : + cutoffCorrectionFix φ C x y = φ y ((C + cutoffCorrectionFix φ C * C) x y) := by + conv_lhs => rw [← cutoffCorrection_fix hC] + rfl + +section Row + +variable (x : V) + +/-- The positive entries of row `x` of the fixed point. -/ +private noncomputable abbrev support : Finset V := {z | cutoffCorrectionFix φ C x z ≠ 0} + +include hC hC0 hC1 hφ0 hφθ in +/-- In each row, the fixed point has at most `1 / (θ f)` positive entries: each leaves a +residual at least `θ f`, and the residuals of a row sum to at most one. -/ +private theorem card_support_mul_le (hθf : 0 ≤ θ * f) : + (#(support (φ := φ) (C := C) x) : ℝ) * (θ * f) ≤ 1 := by + set E := cutoffCorrectionFix φ C + have hE0 : ∀ i j, 0 ≤ E i j := cutoffCorrectionIter_nonneg hφ0 _ + have hEfix : ∀ y, E x y = φ y ((C + E * C) x y) := fix_apply hC x + have hres : ∀ y, (C - E + E * C) x y = (C + E * C) x y - E x y := fun y => by + simp only [add_apply, sub_apply]; ring + have hres0 : ∀ y, 0 ≤ (C - E + E * C) x y := fun y => by + rw [hres, hEfix y, sub_nonneg] + exact cutoff_le_self hφθ hθf y (correctionInput_nonneg hC0 hE0 x y) + have hrow : ∑ y, (C - E + E * C) x y ≤ 1 := by + simpa [mulVec, dotProduct] using (correction_mulVec_one_le hE0 hC1 x).trans (hC1 x) + calc (#(support (φ := φ) (C := C) x) : ℝ) * (θ * f) + = ∑ y ∈ support (φ := φ) (C := C) x, θ * f := by rw [sum_const, nsmul_eq_mul] + _ ≤ ∑ y ∈ support (φ := φ) (C := C) x, (C - E + E * C) x y := by + refine Finset.sum_le_sum fun y hy => ?_ + have hpos : 0 < φ y ((C + E * C) x y) := by + rw [← hEfix y] + exact lt_of_le_of_ne (hE0 x y) (Ne.symm (by simpa using hy)) + rw [hres, hEfix y] + exact le_sub_cutoff_of_pos hφθ y hpos + _ ≤ ∑ y, (C - E + E * C) x y := + Finset.sum_le_sum_of_subset_of_nonneg (subset_univ _) fun y _ _ => hres0 y + _ ≤ 1 := hrow + +/-- A sum `∑ z, F x z * C z y` only sees the members of `support x` below `y`, when `F` vanishes +outside the support. -/ +private theorem sum_mul_eq_sum_support (hC : C.IsStrictUpperTriangular) {F : Matrix V V ℝ} + (hF : ∀ z, cutoffCorrectionFix φ C x z = 0 → F x z = 0) (y : V) : + ∑ z, F x z * C z y = ∑ z ∈ (support (φ := φ) (C := C) x).filter (· < y), F x z * C z y := by + refine (Finset.sum_subset (subset_univ _) fun z _ hz => ?_).symm + simp only [mem_filter, mem_univ, true_and, not_and_or, not_not] at hz + rcases hz with hz | hz + · rw [hF z hz, zero_mul] + · rw [hC hz, mul_zero] + +include hC hC0 hCf hφ0 hφθ in +/-- The entries of the fixed point grow at most geometrically along the support of a row. -/ +private theorem fix_le_pow (hf : 0 ≤ f) (hθf : 0 ≤ θ * f) (y : V) : + cutoffCorrectionFix φ C x y ≤ + f * (1 + f) ^ #((support (φ := φ) (C := C) x).filter (· < y)) := by + set E := cutoffCorrectionFix φ C + have hE0 : ∀ i j, 0 ≤ E i j := cutoffCorrectionIter_nonneg hφ0 _ + induction y using WellFoundedLT.induction with + | ind y ih => + set S := support (φ := φ) (C := C) x + have hEfix : E x y = φ y ((C + E * C) x y) := fix_apply hC x y + have hsum : ∑ z, E x z * C z y = ∑ z ∈ S.filter (· < y), E x z * C z y := + sum_mul_eq_sum_support x hC (fun _ h => h) y + calc E x y ≤ (C + E * C) x y := by + rw [hEfix]; exact cutoff_le_self hφθ hθf y (correctionInput_nonneg hC0 hE0 x y) + _ = C x y + ∑ z ∈ S.filter (· < y), E x z * C z y := by + rw [add_apply, mul_apply, hsum] + _ ≤ f + ∑ z ∈ S.filter (· < y), f * (1 + f) ^ #(S.filter (· < z)) * f := by + refine add_le_add (hCf x y) (Finset.sum_le_sum fun z hz => ?_) + exact mul_le_mul (ih z (mem_filter.mp hz).2) (hCf z y) (hC0 z y) (by positivity) + _ = f + f * f * ∑ z ∈ S.filter (· < y), (1 + f) ^ #(S.filter (· < z)) := by + rw [Finset.mul_sum]; congr 1; exact Finset.sum_congr rfl fun z _ => by ring + _ ≤ f + f * f * ∑ j ∈ range #(S.filter (· < y)), (1 + f) ^ j := by + gcongr + exact sum_rank_le S y fun j => by positivity + _ = f * (1 + f) ^ #(S.filter (· < y)) := by + have := geom_sum_mul_add f #(S.filter (· < y)) + rw [add_comm f 1] at this + linear_combination f * this + +include hC hC0 hCf hφ0 hφθ hφm hφL in +/-- The iteration error along a row is bounded by counting increasing chains in its support. -/ +private theorem fix_sub_iter_le_choose (hf : 0 ≤ f) (hθf : 0 ≤ θ * f) (hL : 0 ≤ L) (k : ℕ) + (y : V) : cutoffCorrectionFix φ C x y - cutoffCorrectionIter φ C k x y ≤ + f * (1 + f) ^ #(support (φ := φ) (C := C) x) * (L * f) ^ k * + (#((support (φ := φ) (C := C) x).filter (· < y))).choose k := by + set E := cutoffCorrectionFix φ C + set S := support (φ := φ) (C := C) x + have hE0 : ∀ i j, 0 ≤ E i j := cutoffCorrectionIter_nonneg hφ0 _ + have hM : ∀ y, E x y ≤ f * (1 + f) ^ #S := fun y => + (fix_le_pow hC hC0 hCf hφ0 hφθ x hf hθf y).trans <| mul_le_mul_of_nonneg_left + (pow_le_pow_right₀ (by linarith) (card_le_card (filter_subset _ _))) hf + induction k generalizing y with + | zero => + simpa using (sub_le_self _ (cutoffCorrectionIter_nonneg hφ0 0 x y)).trans (hM y) + | succ k ih => + set F := cutoffCorrectionIter φ C k + have hFE : ∀ z, F x z ≤ E x z := cutoffCorrectionIter_le_fix hC hC0 hφ0 hφm k x + have hEfix : E x y = φ y ((C + E * C) x y) := fix_apply hC x y + have hsum : ∑ z, (E - F) x z * C z y = ∑ z ∈ S.filter (· < y), (E - F) x z * C z y := + sum_mul_eq_sum_support x hC (fun z hz => by + change E x z = 0 at hz + rw [sub_apply, hz, sub_eq_zero] + exact le_antisymm (cutoffCorrectionIter_nonneg (C := C) hφ0 k x z) (hz ▸ hFE z)) y + have hdiff : (C + E * C) x y - (C + F * C) x y = ∑ z, (E - F) x z * C z y := by + simp only [add_apply, mul_apply, sub_apply, sub_mul, Finset.sum_sub_distrib]; ring + have hle : (C + F * C) x y ≤ (C + E * C) x y := by + rw [← sub_nonneg, hdiff] + exact Finset.sum_nonneg fun z _ => mul_nonneg (by rw [sub_apply, sub_nonneg]; exact hFE z) + (hC0 z y) + calc E x y - cutoffCorrectionIter φ C (k + 1) x y + = φ y ((C + E * C) x y) - φ y ((C + F * C) x y) := by + rw [hEfix, cutoffCorrectionIter_succ]; rfl + _ ≤ L * ∑ z ∈ S.filter (· < y), (E - F) x z * C z y := by + rw [← hsum, ← hdiff] + exact hφL y _ _ hle + _ ≤ L * ∑ z ∈ S.filter (· < y), + f * (1 + f) ^ #S * (L * f) ^ k * (#(S.filter (· < z))).choose k * f := by + refine mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun z _ => ?_) hL + rw [sub_apply] + exact mul_le_mul (ih z) (hCf z y) (hC0 z y) (by positivity) + _ = f * (1 + f) ^ #S * (L * f) ^ (k + 1) * + ∑ z ∈ S.filter (· < y), ((#(S.filter (· < z))).choose k : ℝ) := by + rw [Finset.mul_sum, Finset.mul_sum] + exact Finset.sum_congr rfl fun z _ => by ring + _ ≤ f * (1 + f) ^ #S * (L * f) ^ (k + 1) * + ∑ j ∈ range #(S.filter (· < y)), (j.choose k : ℝ) := by + gcongr + exact sum_rank_le S y (g := fun j => (j.choose k : ℝ)) fun j => by positivity + _ = f * (1 + f) ^ #S * (L * f) ^ (k + 1) * (#(S.filter (· < y))).choose (k + 1) := by + rw [sum_range_choose_eq] + +end Row + +include hC hC0 hCf hC1 hφ0 hφθ hφm hφL in +/-- **Factorial truncation.** After `k` iterations of the cutoff correction recursion, every entry +is within `f e^(1 / θ) (L / θ)^k / k!` of the fixed point, uniformly in the size of `V` +[OpenAI2026LogSpace, Lemma 4.1]. -/ +theorem cutoffCorrectionFix_sub_iter_le (hf : 0 < f) (hθ : 0 < θ) (hL : 0 ≤ L) (k : ℕ) + (x y : V) : cutoffCorrectionFix φ C x y - cutoffCorrectionIter φ C k x y ≤ + f * Real.exp (1 / θ) * (L / θ) ^ k / k.factorial := by + have hθf : 0 ≤ θ * f := by positivity + set S := support (φ := φ) (C := C) x + set m := #S + have hm : (m : ℝ) * f ≤ 1 / θ := by + rw [le_div_iff₀ hθ] + nlinarith [card_support_mul_le hC hC0 hC1 hφ0 hφθ x hθf] + have hr : #(S.filter (· < y)) ≤ m := card_le_card (filter_subset _ _) + refine (fix_sub_iter_le_choose hC hC0 hCf hφ0 hφθ hφm hφL x hf.le hθf hL k y).trans ?_ + have hexp : (1 + f) ^ m ≤ Real.exp (1 / θ) := by + calc (1 + f) ^ m ≤ Real.exp f ^ m := by + gcongr; linarith [Real.add_one_le_exp f] + _ = Real.exp (m * f) := by rw [← Real.exp_nat_mul] + _ ≤ Real.exp (1 / θ) := Real.exp_le_exp.mpr hm + have hchoose : ((#(S.filter (· < y))).choose k : ℝ) ≤ (m : ℝ) ^ k / k.factorial := + (Nat.choose_le_pow_div k _).trans (by gcongr) + have hLf : (L * f) ^ k * ((m : ℝ) ^ k / k.factorial) ≤ (L / θ) ^ k / k.factorial := by + rw [← mul_div_assoc, ← mul_pow] + gcongr + calc L * f * m = L * (m * f) := by ring + _ ≤ L * (1 / θ) := by gcongr + _ = L / θ := by ring + calc f * (1 + f) ^ m * (L * f) ^ k * ((#(S.filter (· < y))).choose k : ℝ) + ≤ f * Real.exp (1 / θ) * ((L * f) ^ k * ((m : ℝ) ^ k / k.factorial)) := by + rw [mul_assoc (f * (1 + f) ^ m)] + gcongr + _ ≤ f * Real.exp (1 / θ) * ((L / θ) ^ k / k.factorial) := by gcongr + _ = f * Real.exp (1 / θ) * (L / θ) ^ k / k.factorial := by ring + +omit [LinearOrder V] in +include hC0 hφ0 hφθ hφm in +/-- **The corrected matrix of a finite iterate is nonnegative.** -/ +theorem cutoffCorrection_residual_nonneg (hθf : 0 ≤ θ * f) (k : ℕ) (x y : V) : + 0 ≤ (C - cutoffCorrectionIter φ C k + cutoffCorrectionIter φ C k * C) x y := by + cases k with + | zero => simpa [cutoffCorrectionIter] using hC0 x y + | succ k => + have hF0 := cutoffCorrectionIter_nonneg (C := C) hφ0 k + have hstep : cutoffCorrectionIter φ C (k + 1) x y = + φ y ((C + cutoffCorrectionIter φ C k * C) x y) := by + rw [cutoffCorrectionIter_succ]; rfl + have hcut := cutoff_le_self hφθ hθf y (correctionInput_nonneg hC0 hF0 x y) + have hgrow : (cutoffCorrectionIter φ C k * C) x y ≤ + (cutoffCorrectionIter φ C (k + 1) * C) x y := + Finset.sum_le_sum fun z _ => mul_le_mul_of_nonneg_right + (cutoffCorrectionIter_le_succ hC0 hφ0 hφm k x z) (hC0 z y) + rw [← hstep, add_apply] at hcut + rw [add_apply, sub_apply] + linarith + +include hC hC0 hCf hC1 hφ0 hφθ hφm hφL in +/-- **Fully corrected columns have small residuals.** If the cutoff of column `y` leaves at most +`θ₂ f` behind, the corrected matrix of the `k`-th iterate has entries at most +`θ₂ f + f e^(1 / θ) (L / θ)^k / k!` in that column [OpenAI2026LogSpace, Lemma 4.4]. -/ +theorem cutoffCorrection_residual_le (hf : 0 < f) (hθ : 0 < θ) (hL : 0 ≤ L) {θ₂ : ℝ} {y : V} + (hgood : ∀ t, t - θ₂ * f ≤ φ y t) (k : ℕ) (x : V) : + (C - cutoffCorrectionIter φ C k + cutoffCorrectionIter φ C k * C) x y ≤ + θ₂ * f + f * Real.exp (1 / θ) * (L / θ) ^ k / k.factorial := by + set E := cutoffCorrectionFix φ C + set F := cutoffCorrectionIter φ C k + have hEfix : E x y = φ y ((C + E * C) x y) := fix_apply hC x y + have hΔ := cutoffCorrectionFix_sub_iter_le hC hC0 hCf hC1 hφ0 hφθ hφm hφL hf hθ hL k x y + have hΔC : (F * C) x y ≤ (E * C) x y := + Finset.sum_le_sum fun z _ => mul_le_mul_of_nonneg_right + (cutoffCorrectionIter_le_fix hC hC0 hφ0 hφm k x z) (hC0 z y) + have hT := hgood ((C + E * C) x y) + rw [← hEfix] at hT + simp only [add_apply, sub_apply] at hT hΔC ⊢ + linarith + +/-- **A constant number of iterations suffices**: for every accuracy `δ > 0` there is `k`, depending +only on `θ`, `L` and `δ`, with `e^(1 / θ) (L / θ)^k / k! ≤ δ` [OpenAI2026LogSpace, Lemma 4.1]. -/ +theorem exists_factorial_bound_le (θ L : ℝ) {δ : ℝ} (hδ : 0 < δ) : + ∃ k : ℕ, Real.exp (1 / θ) * (L / θ) ^ k / k.factorial ≤ δ := by + have h := (FloorSemiring.tendsto_pow_div_factorial_atTop (L / θ)).const_mul + (Real.exp (1 / θ)) + rw [mul_zero] at h + obtain ⟨k, hk⟩ := (h.eventually (gt_mem_nhds hδ)).exists + exact ⟨k, by rw [mul_div_assoc]; exact hk.le⟩ + +end Bounds + +end Matrix diff --git a/ComplexityTests/FactorialTruncation.lean b/ComplexityTests/FactorialTruncation.lean new file mode 100644 index 000000000..1a9743119 --- /dev/null +++ b/ComplexityTests/FactorialTruncation.lean @@ -0,0 +1,93 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexity.Foundations.LinearAlgebra.Matrix.FactorialTruncation + +/-! +# Tests for factorial truncation of cutoff corrections +-/ + +namespace ComplexityTests.FactorialTruncation + +open Matrix + +/-- A walk on three time layers: from `0` to `1` and from `1` to `2`, each with probability +`1 / 2`. Its entries are at most `f = 1 / 2`. -/ +private noncomputable def C : Matrix (Fin 3) (Fin 3) ℝ := !![0, 1 / 2, 0; 0, 0, 1 / 2; 0, 0, 0] + +/-- The hard cutoff `t ↦ max (t - θ f) 0` with `θ = 1 / 4`, `f = 1 / 2`: it leaves exactly `1 / 8` +behind. It is monotone and `1`-Lipschitz. -/ +private noncomputable def φ : Fin 3 → ℝ → ℝ := fun _ t => max (t - 1 / 8) 0 + +private theorem hC : C.IsStrictUpperTriangular := by + intro i j h; fin_cases i <;> fin_cases j <;> simp_all [C] + +private theorem hC0 : ∀ x y, 0 ≤ C x y := by + intro x y; fin_cases x <;> fin_cases y <;> norm_num [C] + +private theorem hCf : ∀ x y, C x y ≤ 1 / 2 := by + intro x y; fin_cases x <;> fin_cases y <;> norm_num [C] + +private theorem hC1 : C *ᵥ 1 ≤ 1 := by + intro x; fin_cases x <;> norm_num [C, mulVec, dotProduct, Fin.sum_univ_three] + +private theorem hφ0 : ∀ y t, 0 ≤ φ y t := fun _ _ => le_max_right _ _ + +private theorem hφθ : ∀ y t, φ y t ≤ max (t - 1 / 4 * (1 / 2)) 0 := fun _ t => by + norm_num [φ] + +private theorem hφm : ∀ y, Monotone (φ y) := fun _ _ _ h => max_le_max (by linarith) le_rfl + +private theorem hφL : ∀ y s t, s ≤ t → φ y t - φ y s ≤ 1 * (t - s) := fun _ s t _ => by + simp only [φ, one_mul] + have := le_max_left (s - 1 / 8) 0 + have := le_max_right (s - 1 / 8) 0 + have : max (t - 1 / 8) 0 ≤ max (s - 1 / 8) 0 + (t - s) := max_le (by linarith) (by linarith) + linarith + +/-- The cutoff correction of `C`, computed by hand: `φ (1 / 2) = 3 / 8` on both transitions, +and `φ (3 / 8 * 1 / 2) = 1 / 16` on the corrected two-step entry. -/ +private noncomputable def Estar : Matrix (Fin 3) (Fin 3) ℝ := + !![0, 3 / 8, 1 / 16; 0, 0, 3 / 8; 0, 0, 0] + +-- `Estar` solves the recursion, so it is the cutoff correction. +private theorem Estar_eq : Estar = cutoffCorrectionFix φ C := by + refine eq_cutoffCorrectionFix hC ?_ + ext x y + fin_cases x <;> fin_cases y <;> + norm_num [cutoffCorrection, φ, C, Estar, mul_apply, Fin.sum_univ_three] + +-- One iteration from zero misses the two-step entry entirely. +example : cutoffCorrectionIter φ C 1 0 2 = 0 := by + norm_num [cutoffCorrectionIter, cutoffCorrection, φ, C] + +-- The truncation error after one iteration, `1 / 16`, is within the factorial bound. +example : cutoffCorrectionFix φ C 0 2 - cutoffCorrectionIter φ C 1 0 2 ≤ + 1 / 2 * Real.exp (1 / (1 / 4)) * (1 / (1 / 4)) ^ 1 / (Nat.factorial 1) := + cutoffCorrectionFix_sub_iter_le hC hC0 hCf hC1 hφ0 hφθ hφm hφL (by norm_num) (by norm_num) + (by norm_num) 1 0 2 + +-- After two iterations the iterate has reached the fixed point at `(0, 2)`. +example : cutoffCorrectionIter φ C 2 0 2 = cutoffCorrectionFix φ C 0 2 := by + rw [← Estar_eq] + norm_num [cutoffCorrectionIter, cutoffCorrection, φ, C, Estar, mul_apply, Fin.sum_univ_three] + +-- The corrected matrix of every iterate is nonnegative, and the hard cutoff leaves at most +-- `θ f = 1 / 8` behind in every column. +example (k : ℕ) (x y : Fin 3) : + 0 ≤ (C - cutoffCorrectionIter φ C k + cutoffCorrectionIter φ C k * C) x y := + cutoffCorrection_residual_nonneg hC0 hφ0 hφθ hφm (by norm_num) k x y + +example (k : ℕ) (x y : Fin 3) : + (C - cutoffCorrectionIter φ C k + cutoffCorrectionIter φ C k * C) x y ≤ + 1 / 4 * (1 / 2) + 1 / 2 * Real.exp (1 / (1 / 4)) * (1 / (1 / 4)) ^ k / k.factorial := + cutoffCorrection_residual_le hC hC0 hCf hC1 hφ0 hφθ hφm hφL (by norm_num) (by norm_num) + (by norm_num) (fun t => by norm_num [φ]) k x + +-- A fixed number of iterations gets within `1 / 100` of the factorial bound's limit. +example : ∃ k : ℕ, Real.exp (1 / (1 / 4)) * (1 / (1 / 4)) ^ k / k.factorial ≤ 1 / 100 := + exists_factorial_bound_le _ _ (by norm_num) + +end ComplexityTests.FactorialTruncation From 6e0388d538b591a63b9a59ef5a4337638b31242e Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:17:18 +0000 Subject: [PATCH 5/8] refactor(Foundations): use Nat.sum_Icc_choose for the hockey-stick step Review nit on #1677: drop the private hockey-stick lemma. Co-Authored-By: Claude Opus 5.5 --- .../Matrix/FactorialTruncation.lean | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean b/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean index ad9fe5b9c..d9e81c1ed 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean @@ -180,13 +180,6 @@ private theorem sum_rank_le (S : Finset V) (y : V) {g : ℕ → ℝ} (hg : ∀ j simp only [mem_filter] at hz exact Finset.mem_range.mpr (hlt hz.1 hz.2) -/-- The hockey-stick identity `∑ j < n, (j choose k) = n choose (k + 1)`. -/ -private theorem sum_range_choose_eq (n k : ℕ) : - ∑ j ∈ range n, (j.choose k : ℝ) = (n.choose (k + 1) : ℝ) := by - induction n with - | zero => simp - | succ n ih => rw [sum_range_succ, ih, Nat.choose_succ_succ', Nat.cast_add, add_comm] - variable (hC : C.IsStrictUpperTriangular) (hC0 : ∀ x y, 0 ≤ C x y) (hCf : ∀ x y, C x y ≤ f) (hC1 : C *ᵥ 1 ≤ 1) (hφ0 : ∀ y t, 0 ≤ φ y t) (hφθ : ∀ y t, φ y t ≤ max (t - θ * f) 0) (hφm : ∀ y, Monotone (φ y)) (hφL : ∀ y s t, s ≤ t → φ y t - φ y s ≤ L * (t - s)) @@ -388,7 +381,15 @@ private theorem fix_sub_iter_le_choose (hf : 0 ≤ f) (hθf : 0 ≤ θ * f) (hL gcongr exact sum_rank_le S y (g := fun j => (j.choose k : ℝ)) fun j => by positivity _ = f * (1 + f) ^ #S * (L * f) ^ (k + 1) * (#(S.filter (· < y))).choose (k + 1) := by - rw [sum_range_choose_eq] + -- the hockey-stick identity `∑ j ∈ Icc k n, j.choose k = (n + 1).choose (k + 1)` + congr 1 + rcases hn : #(S.filter (· < y)) with _ | n + · simp + · rw [← Nat.sum_Icc_choose, Nat.cast_sum] + refine (Finset.sum_subset (fun j hj => ?_) fun j hj hjn => ?_).symm + · simp only [mem_Icc, mem_range] at hj ⊢; omega + · simp only [mem_Icc, mem_range, not_and_or, not_le] at hj hjn + rw [Nat.choose_eq_zero_of_lt (by omega), Nat.cast_zero] end Row From 8b3f5725d8ca58892463e9848898ea86e29fdc2a Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:26:24 +0000 Subject: [PATCH 6/8] doc(Foundations): count chains with the integer support size Review of #1677: the module docstring now bounds the chain count by m.choose k for the actual support size m, as the proof does. Co-Authored-By: Claude Opus 5.5 --- .../LinearAlgebra/Matrix/FactorialTruncation.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean b/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean index d9e81c1ed..f94a429ae 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean @@ -32,10 +32,10 @@ iterations every entry is within `f e^(1 / θ) (L / θ)^k / k!` of the fixed poi (`Matrix.cutoffCorrectionFix_sub_iter_le`). The proof counts chains. In a fixed row, every positive entry of the fixed point leaves a residual -at least `θ f`, and the residuals of a row sum to at most one, so the row has at most `1 / (θ f)` -positive entries. Unrolling the recursion `k` times along that row expresses the error as a sum -over increasing chains of `k` of these entries, each weighted by at most `(L f)^k`; there are at -most `binomial (1 / (θ f), k) ≤ (θ f)^(-k) / k!` of them. +at least `θ f`, and the residuals of a row sum to at most one, so the number `m` of positive +entries in the row satisfies `m θ f ≤ 1`. Unrolling the recursion `k` times along that row +expresses the error as a sum over increasing chains of `k` of these entries, each weighted by at +most `(L f)^k`; there are at most `m.choose k ≤ m^k / k! ≤ (θ f)^(-k) / k!` of them. For the finite correction `E = E k`, the corrected matrix `C - E + E C` is nonnegative (`Matrix.cutoffCorrection_residual_nonneg`), and in a column whose cutoff leaves at most `θ₂ f` From 4014d0c1714f65e566c8c01dbfab34e06b72e803 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 00:04:51 +0000 Subject: [PATCH 7/8] fix(Foundations): qualify Matrix apply lemmas for the rc2 Mathlib API Under rc2 the root-namespace add_apply/neg_apply/sub_apply/mul_apply/one_apply no longer apply to matrices; use the Matrix.* versions in CorrectionHierarchy and its test, as #1653 does elsewhere. Co-Authored-By: Claude Opus 5.5 (cherry picked from commit ea663cedbea1caf5e23e6f38b36fed48ed46dda8) --- .../Matrix/CorrectionHierarchy.lean | 18 ++++++++++-------- ComplexityTests/CorrectionHierarchy.lean | 19 ++++++++++--------- 2 files changed, 20 insertions(+), 17 deletions(-) diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean b/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean index 2420fb961..ec5c5825e 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/CorrectionHierarchy.lean @@ -112,15 +112,15 @@ theorem isUpperTriangular [Zero R] (h : M.IsStrictUpperTriangular) : M.IsUpperTr theorem add [AddZeroClass R] (hM : M.IsStrictUpperTriangular) (hN : N.IsStrictUpperTriangular) : (M + N).IsStrictUpperTriangular := fun i j hij => by - simp only [add_apply, hM hij, hN hij, add_zero] + simp only [Matrix.add_apply, hM hij, hN hij, add_zero] theorem neg [SubtractionMonoid R] (hM : M.IsStrictUpperTriangular) : (-M).IsStrictUpperTriangular := fun i j hij => by - simp only [neg_apply, hM hij, neg_zero] + simp only [Matrix.neg_apply, hM hij, neg_zero] theorem sub [SubtractionMonoid R] (hM : M.IsStrictUpperTriangular) (hN : N.IsStrictUpperTriangular) : (M - N).IsStrictUpperTriangular := fun i j hij => by - simp only [sub_apply, hM hij, hN hij, sub_zero] + simp only [Matrix.sub_apply, hM hij, hN hij, sub_zero] theorem mul [Fintype V] [NonUnitalNonAssocSemiring R] (hM : M.IsStrictUpperTriangular) (hN : N.IsStrictUpperTriangular) : (M * N).IsStrictUpperTriangular := fun i j hij => by @@ -134,9 +134,10 @@ theorem mul [Fintype V] [NonUnitalNonAssocSemiring R] (hM : M.IsStrictUpperTrian theorem det_one_add {V : Type*} [Fintype V] [DecidableEq V] [LinearOrder V] [CommRing R] {E : Matrix V V R} (h : E.IsStrictUpperTriangular) : (1 + E).det = 1 := by have hT : (1 + E).IsUpperTriangular := fun i j (hji : j < i) => by - rw [add_apply, one_apply_ne (ne_of_lt hji).symm, h.isUpperTriangular hji, add_zero] + rw [Matrix.add_apply, one_apply_ne (ne_of_lt hji).symm, h.isUpperTriangular hji, add_zero] rw [det_of_isUpperTriangular hT] - exact Finset.prod_eq_one fun i _ => by rw [add_apply, one_apply_eq, h (lt_irrefl i), add_zero] + exact Finset.prod_eq_one fun i _ => by + rw [Matrix.add_apply, one_apply_eq, h (lt_irrefl i), add_zero] end IsStrictUpperTriangular @@ -240,11 +241,12 @@ theorem copySplit_mul_copyWeight [Fintype V] [DecidableEq V] [Fintype ι] [Semir copySplit r s D * copyWeight r = copyWeight r * D := by ext ⟨x, i⟩ z have hL : (copySplit r s D * copyWeight r) (x, i) z = r i x * D x z * ∑ j, s x z j * r j z := by - rw [mul_apply, Fintype.sum_prod_type, Fintype.sum_eq_single z fun y hy => ?_, Finset.mul_sum] + rw [Matrix.mul_apply, Fintype.sum_prod_type, Fintype.sum_eq_single z fun y hy => ?_, + Finset.mul_sum] · simp [copySplit, copyWeight, mul_assoc] · simp [copyWeight, hy] have hR : (copyWeight r * D) (x, i) z = r i x * D x z := by - rw [mul_apply, Fintype.sum_eq_single x fun y hy => ?_] + rw [Matrix.mul_apply, Fintype.sum_eq_single x fun y hy => ?_] · simp [copyWeight] · simp [copyWeight, Ne.symm hy] rw [hL, hR] @@ -358,7 +360,7 @@ variable [Ring R] [PartialOrder R] [IsOrderedRing R] private theorem one_apply_nonneg {n : Type*} [DecidableEq n] (i j : n) : (0 : R) ≤ (1 : Matrix n n R) i j := by - rw [one_apply]; split_ifs <;> simp + rw [Matrix.one_apply]; split_ifs <;> simp private theorem mul_nonneg_entries {m n o : Type*} [Fintype n] {A : Matrix m n R} {B : Matrix n o R} (hA : ∀ i j, 0 ≤ A i j) (hB : ∀ i j, 0 ≤ B i j) (i : m) (k : o) : diff --git a/ComplexityTests/CorrectionHierarchy.lean b/ComplexityTests/CorrectionHierarchy.lean index c6bb668e6..1564bdc7a 100644 --- a/ComplexityTests/CorrectionHierarchy.lean +++ b/ComplexityTests/CorrectionHierarchy.lean @@ -24,7 +24,8 @@ private def e : Fin 3 → ℚ := ![0, 0, 1] private def p : Fin 3 → ℚ := ![1 / 4, 1 / 2, 1] private theorem one_sub_C_mulVec_p : (1 - C) *ᵥ p = e := by - ext i; fin_cases i <;> norm_num [C, p, e, mulVec, dotProduct, Fin.sum_univ_three, one_apply] + ext i; fin_cases i <;> + norm_num [C, p, e, mulVec, dotProduct, Fin.sum_univ_three, Matrix.one_apply] /-- The correction removes the second transition. -/ private def E : Matrix (Fin 3) (Fin 3) ℚ := !![0, 0, 0; 0, 0, 1 / 2; 0, 0, 0] @@ -41,18 +42,18 @@ example : C - E + E * C = !![0, 1 / 2, 0; 0, 0, 0; 0, 0, 0] := by -- equation. example : (1 - (C - E + E * C)) *ᵥ p = ![0, 1 / 2, 1] := by rw [one_sub_correction_mulVec, one_sub_C_mulVec_p] - ext i; fin_cases i <;> simp [E, e, mulVec, dotProduct, Fin.sum_univ_three, one_apply] + ext i; fin_cases i <;> simp [E, e, mulVec, dotProduct, Fin.sum_univ_three, Matrix.one_apply] private theorem inv_one_sub_C : (1 - C)⁻¹ = 1 + C + C * C := inv_eq_left_inv <| by ext i j; fin_cases i <;> fin_cases j <;> - simp [C, mul_apply, Fin.sum_univ_three, one_apply] + simp [C, Matrix.mul_apply, Fin.sum_univ_three, Matrix.one_apply] -- The acceptance probabilities of the corrected walk with the corrected reward are those of -- the original walk: `1 / 4` from `0`. example : ((1 - (C - E + E * C))⁻¹ *ᵥ (e + E *ᵥ e)) 0 = 1 / 4 := by rw [E_strict.inv_one_sub_correction_mulVec, inv_one_sub_C] - simp [C, e, mulVec, dotProduct, Fin.sum_univ_three, one_apply] + simp [C, e, mulVec, dotProduct, Fin.sum_univ_three, Matrix.one_apply] norm_num -- A nonnegative correction does not increase the row sums. @@ -93,7 +94,7 @@ private def Es (l : ℕ) : Matrix (Fin 3) (Fin 3) ℚ := if l = 0 then C + C * C private def Ps (_ : ℕ) : Matrix (Fin 3) (Fin 3) ℚ := 1 private theorem C_cube : C * C * C = 0 := by - ext i j; fin_cases i <;> fin_cases j <;> simp [C, mul_apply, Fin.sum_univ_three] + ext i j; fin_cases i <;> fin_cases j <;> simp [C, Matrix.mul_apply, Fin.sum_univ_three] private theorem hstep (l : ℕ) : Cs (l + 1) * Ps l = Ps l * (Cs l - Es l + Es l * Cs l) := by rcases l with _ | l @@ -108,12 +109,12 @@ private theorem nonneg_C : ∀ i j, 0 ≤ C i j := by -- the row sum of the zero matrix. example : (rewardTransport (V := fun _ => Fin 3) Ps Es 1 *ᵥ e) 0 = 1 / 4 := by have h := sub_rewardTransport_mulVec_mem_Icc (V := fun _ => Fin 3) (C := Cs) (E := Es) - (P := Ps) (z := fun _ => 0) (fun _ i j => by simp [Ps, one_apply]; split_ifs <;> simp) + (P := Ps) (z := fun _ => 0) (fun _ i j => by simp [Ps, Matrix.one_apply]; split_ifs <;> simp) (fun _ => by simp [Ps]) (fun l i j => by unfold Cs; split_ifs <;> simp [nonneg_C]) hstep (p := p) (e := e) (by simpa [Cs] using one_sub_C_mulVec_p) (fun i => by fin_cases i <;> norm_num [p]) (fun i => by fin_cases i <;> norm_num [p]) - (fun _ w => by simp [Ps, one_apply, eq_comm]) 1 + (fun _ w => by simp [Ps, Matrix.one_apply, eq_comm]) 1 have hp0 : p 0 = 1 / 4 := rfl simp only [Cs, Nat.add_one_ne_zero, ↓reduceIte, Matrix.zero_apply, Finset.sum_const_zero, Set.mem_Icc] at h @@ -122,10 +123,10 @@ example : (rewardTransport (V := fun _ => Fin 3) Ps Es 1 *ᵥ e) 0 = 1 / 4 := by -- The transported rewards are nonnegative. example : 0 ≤ rewardTransport (V := fun _ => Fin 3) Ps Es 1 *ᵥ e := rewardTransport_mulVec_nonneg (V := fun _ => Fin 3) - (fun _ i j => by simp only [Ps, one_apply]; split_ifs <;> simp) + (fun _ i j => by simp only [Ps, Matrix.one_apply]; split_ifs <;> simp) (fun l i j => by unfold Es; split_ifs - · fin_cases i <;> fin_cases j <;> norm_num [C, mul_apply, Fin.sum_univ_three] + · fin_cases i <;> fin_cases j <;> norm_num [C, Matrix.mul_apply, Fin.sum_univ_three] · simp) (fun i => by fin_cases i <;> simp [e]) 1 From b0b00058c5845fb44ba7f50f5ec33bf3764cacd9 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 00:10:59 +0000 Subject: [PATCH 8/8] fix(Foundations): qualify Matrix apply lemmas in FactorialTruncation for rc2 Under rc2 the root-namespace add_apply/sub_apply/mul_apply no longer apply to matrices; use the Matrix.* versions in FactorialTruncation and its test, rewrapping lines that crossed 100 columns. Co-Authored-By: Claude Opus 5.5 (cherry picked from commit 19cf8a82f0390c89261196084d1838f498523e73) --- .../Matrix/FactorialTruncation.lean | 26 ++++++++++--------- ComplexityTests/FactorialTruncation.lean | 5 ++-- 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean b/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean index f94a429ae..856f41393 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean @@ -105,7 +105,7 @@ variable [LinearOrder V] private theorem cutoffCorrection_congr (hC : C.IsStrictUpperTriangular) {F G : Matrix V V R} {x y : V} (h : ∀ z < y, F x z = G x z) : cutoffCorrection φ C F x y = cutoffCorrection φ C G x y := by - simp only [cutoffCorrection, of_apply, add_apply, mul_apply] + simp only [cutoffCorrection, of_apply, Matrix.add_apply, Matrix.mul_apply] congr 2 refine Finset.sum_congr rfl fun z _ => ?_ by_cases hz : z < y @@ -191,7 +191,7 @@ include hC0 hφm in private theorem cutoffCorrection_mono {F G : Matrix V V ℝ} (hFG : ∀ x y, F x y ≤ G x y) (x y : V) : cutoffCorrection φ C F x y ≤ cutoffCorrection φ C G x y := by refine hφm y ?_ - simp only [add_apply, mul_apply] + simp only [Matrix.add_apply, Matrix.mul_apply] exact add_le_add_right (Finset.sum_le_sum fun z _ => mul_le_mul_of_nonneg_right (hFG x z) (hC0 z y)) _ @@ -271,7 +271,7 @@ private theorem card_support_mul_le (hθf : 0 ≤ θ * f) : have hE0 : ∀ i j, 0 ≤ E i j := cutoffCorrectionIter_nonneg hφ0 _ have hEfix : ∀ y, E x y = φ y ((C + E * C) x y) := fix_apply hC x have hres : ∀ y, (C - E + E * C) x y = (C + E * C) x y - E x y := fun y => by - simp only [add_apply, sub_apply]; ring + simp only [Matrix.add_apply, Matrix.sub_apply]; ring have hres0 : ∀ y, 0 ≤ (C - E + E * C) x y := fun y => by rw [hres, hEfix y, sub_nonneg] exact cutoff_le_self hφθ hθf y (correctionInput_nonneg hC0 hE0 x y) @@ -317,7 +317,7 @@ private theorem fix_le_pow (hf : 0 ≤ f) (hθf : 0 ≤ θ * f) (y : V) : calc E x y ≤ (C + E * C) x y := by rw [hEfix]; exact cutoff_le_self hφθ hθf y (correctionInput_nonneg hC0 hE0 x y) _ = C x y + ∑ z ∈ S.filter (· < y), E x z * C z y := by - rw [add_apply, mul_apply, hsum] + rw [Matrix.add_apply, Matrix.mul_apply, hsum] _ ≤ f + ∑ z ∈ S.filter (· < y), f * (1 + f) ^ #(S.filter (· < z)) * f := by refine add_le_add (hCf x y) (Finset.sum_le_sum fun z hz => ?_) exact mul_le_mul (ih z (mem_filter.mp hz).2) (hCf z y) (hC0 z y) (by positivity) @@ -353,14 +353,16 @@ private theorem fix_sub_iter_le_choose (hf : 0 ≤ f) (hθf : 0 ≤ θ * f) (hL have hsum : ∑ z, (E - F) x z * C z y = ∑ z ∈ S.filter (· < y), (E - F) x z * C z y := sum_mul_eq_sum_support x hC (fun z hz => by change E x z = 0 at hz - rw [sub_apply, hz, sub_eq_zero] + rw [Matrix.sub_apply, hz, sub_eq_zero] exact le_antisymm (cutoffCorrectionIter_nonneg (C := C) hφ0 k x z) (hz ▸ hFE z)) y have hdiff : (C + E * C) x y - (C + F * C) x y = ∑ z, (E - F) x z * C z y := by - simp only [add_apply, mul_apply, sub_apply, sub_mul, Finset.sum_sub_distrib]; ring + simp only [Matrix.add_apply, Matrix.mul_apply, Matrix.sub_apply, sub_mul, + Finset.sum_sub_distrib] + ring have hle : (C + F * C) x y ≤ (C + E * C) x y := by rw [← sub_nonneg, hdiff] - exact Finset.sum_nonneg fun z _ => mul_nonneg (by rw [sub_apply, sub_nonneg]; exact hFE z) - (hC0 z y) + exact Finset.sum_nonneg fun z _ => + mul_nonneg (by rw [Matrix.sub_apply, sub_nonneg]; exact hFE z) (hC0 z y) calc E x y - cutoffCorrectionIter φ C (k + 1) x y = φ y ((C + E * C) x y) - φ y ((C + F * C) x y) := by rw [hEfix, cutoffCorrectionIter_succ]; rfl @@ -370,7 +372,7 @@ private theorem fix_sub_iter_le_choose (hf : 0 ≤ f) (hθf : 0 ≤ θ * f) (hL _ ≤ L * ∑ z ∈ S.filter (· < y), f * (1 + f) ^ #S * (L * f) ^ k * (#(S.filter (· < z))).choose k * f := by refine mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun z _ => ?_) hL - rw [sub_apply] + rw [Matrix.sub_apply] exact mul_le_mul (ih z) (hCf z y) (hC0 z y) (by positivity) _ = f * (1 + f) ^ #S * (L * f) ^ (k + 1) * ∑ z ∈ S.filter (· < y), ((#(S.filter (· < z))).choose k : ℝ) := by @@ -445,8 +447,8 @@ theorem cutoffCorrection_residual_nonneg (hθf : 0 ≤ θ * f) (k : ℕ) (x y : (cutoffCorrectionIter φ C (k + 1) * C) x y := Finset.sum_le_sum fun z _ => mul_le_mul_of_nonneg_right (cutoffCorrectionIter_le_succ hC0 hφ0 hφm k x z) (hC0 z y) - rw [← hstep, add_apply] at hcut - rw [add_apply, sub_apply] + rw [← hstep, Matrix.add_apply] at hcut + rw [Matrix.add_apply, Matrix.sub_apply] linarith include hC hC0 hCf hC1 hφ0 hφθ hφm hφL in @@ -466,7 +468,7 @@ theorem cutoffCorrection_residual_le (hf : 0 < f) (hθ : 0 < θ) (hL : 0 ≤ L) (cutoffCorrectionIter_le_fix hC hC0 hφ0 hφm k x z) (hC0 z y) have hT := hgood ((C + E * C) x y) rw [← hEfix] at hT - simp only [add_apply, sub_apply] at hT hΔC ⊢ + simp only [Matrix.add_apply, Matrix.sub_apply] at hT hΔC ⊢ linarith /-- **A constant number of iterations suffices**: for every accuracy `δ > 0` there is `k`, depending diff --git a/ComplexityTests/FactorialTruncation.lean b/ComplexityTests/FactorialTruncation.lean index 1a9743119..18bd60c9a 100644 --- a/ComplexityTests/FactorialTruncation.lean +++ b/ComplexityTests/FactorialTruncation.lean @@ -57,7 +57,7 @@ private theorem Estar_eq : Estar = cutoffCorrectionFix φ C := by refine eq_cutoffCorrectionFix hC ?_ ext x y fin_cases x <;> fin_cases y <;> - norm_num [cutoffCorrection, φ, C, Estar, mul_apply, Fin.sum_univ_three] + norm_num [cutoffCorrection, φ, C, Estar, Matrix.mul_apply, Fin.sum_univ_three] -- One iteration from zero misses the two-step entry entirely. example : cutoffCorrectionIter φ C 1 0 2 = 0 := by @@ -72,7 +72,8 @@ example : cutoffCorrectionFix φ C 0 2 - cutoffCorrectionIter φ C 1 0 2 ≤ -- After two iterations the iterate has reached the fixed point at `(0, 2)`. example : cutoffCorrectionIter φ C 2 0 2 = cutoffCorrectionFix φ C 0 2 := by rw [← Estar_eq] - norm_num [cutoffCorrectionIter, cutoffCorrection, φ, C, Estar, mul_apply, Fin.sum_univ_three] + norm_num [cutoffCorrectionIter, cutoffCorrection, φ, C, Estar, Matrix.mul_apply, + Fin.sum_univ_three] -- The corrected matrix of every iterate is nonnegative, and the hard cutoff leaves at most -- `θ f = 1 / 8` behind in every column.