From 22c839875da94d8f1a207f905192940f82c2fc4e Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:16:02 +0000 Subject: [PATCH] feat(probability): bound computable hierarchy stage parameters Replace the arbitrary prime witness in stageModulus with computable least-prime search. Expose primality, both lower bounds and minimality; derive the factor-of-two Bertrand bound and explicit log2 and Nat.size bounds. Compute stageSide by natural ceiling division and prove equality with its former real-ceiling specification. Preserve the channel and hierarchy theorem statements and Christian Reitwiessner's source credit. This advances #1721's concrete hierarchy parameter work. The arithmetic refinement is separate from the paper's estimator and supplies no machine space certificate. The existing source mapping to OpenAI2026LogSpace Sections 2-3 and 4.5 is unchanged; the new prime bound uses Mathlib's Bertrand theorem rather than importing an OpenAI Lean implementation. Validation: the changed library module and complete hierarchy-channel test module compile with the pinned Lean 4.36.0-rc2 toolchain and strict repository options, using shared dependencies read-only and private outputs. Executable checks return [2, 11, 17, 2, 2] for boundary, composite-bound, prime-bound and ceiling-division cases. Formal tests check prime minimality, a linear bit-length specialization, the exact ceil(5/4) side and the actual retention interface at rate 1/4 with density 2/5. All previous three-layer hierarchy tests are retained and pass. Focused proof hygiene with --check-simp and git diff --check pass. Full six-gate integration validation and independent review are pending. Implemented with AI assistance by worker /root/compression_review on feat/logspace-bounded-stage-primes; coordinator /root owns integration. Independent non-author source/API review by lean_environment approved exact source revision f7400570ede09f783a5c24ecc7d13e9d9fe5c51c and independently compiled the full affected module/test. Reviewed source files are unchanged after integration. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- .../HierarchyChannels.lean | 117 ++++++++++++++---- ComplexityTests/HierarchyChannels.lean | 49 +++++++- 2 files changed, 138 insertions(+), 28 deletions(-) diff --git a/Complexity/Probability/PairwiseIndependentHash/HierarchyChannels.lean b/Complexity/Probability/PairwiseIndependentHash/HierarchyChannels.lean index 3de37d9d29..27264de25d 100644 --- a/Complexity/Probability/PairwiseIndependentHash/HierarchyChannels.lean +++ b/Complexity/Probability/PairwiseIndependentHash/HierarchyChannels.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Copyright (c) 2026 Christian Reitwiessner and Samuel Schlesinger. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Christian Reitwiessner +Authors: Christian Reitwiessner, Samuel Schlesinger -/ module @@ -9,7 +9,11 @@ module public import Complexity.Foundations.Probability.DetectedHierarchy public import Complexity.Probability.PairwiseIndependentHash.DetectorChannels +public import Mathlib.Algebra.Order.Floor.Div +public import Mathlib.Data.Nat.Size +import Mathlib.Data.Nat.Log import Mathlib.Data.Nat.Prime.Infinite +import Mathlib.NumberTheory.Bertrand /-! # Affine channels for every stage of the hierarchy @@ -31,18 +35,27 @@ With these channels the stage bound holds without any channel hypothesis gives a fully concrete instance of the hierarchy and its bound (`Matrix.sub_hierarchyReward_le_radix`). This instantiates the reduced algebraic-stage bound; the preprint's full threshold ladder and later-estimation root/complement regularity for `Q` -and all step cutoffs remain separate requirements. The prime at each stage is chosen -noncomputably; no prime-size or machine-resource bound is supplied. +and the cutoffs remain separate requirements. The modulus is the least prime at least +`max (2 ^ l) (M l)`, obtained by computable natural-number search. Bertrand's postulate gives +`P_l ≤ 2 * max (2 ^ l) (M l)`, hence explicit logarithm and binary-length bounds. The side is +computed by natural ceiling division and proved equal to the real-ceiling formula above. +These arithmetic definitions and value bounds do not certify a machine-space implementation. ## Main definitions -* `Cslib.Probability.stageModulus`, `Cslib.Probability.stageChannel`: the affine channel of stage - `l` on identifiers below `M l`. +* `Cslib.Probability.stageModulus`, `Cslib.Probability.stageSide`: the least-prime modulus and + natural ceiling-division side of stage `l`. +* `Cslib.Probability.stageChannel`: the affine channel on identifiers below `M l`. ## Main results * `Cslib.Probability.retentionChannels_stageChannel`: the channel interface at rate `(2 ^ H)⁻¹ ^ l` with uniform constants. +* `Cslib.Probability.le_stageModulus`, `Cslib.Probability.stageModulus_le_of_prime`: the modulus + meets both lower bounds and is the least prime that does so. +* `Cslib.Probability.stageModulus_le_two_mul`, `Cslib.Probability.log2_stageModulus_le`, + `Cslib.Probability.size_stageModulus_le`: quantitative modulus and binary-length bounds. +* `Cslib.Probability.stageSide_eq_ceil`: the exact real-ceiling identity for the computable side. * `Matrix.sub_hierarchyReward_le_affine`: the stage bound with these channels. * `Matrix.sub_hierarchyReward_le_radix`: the stage bound on radix identifiers. @@ -58,29 +71,81 @@ open Finset namespace Cslib.Probability -/-- A prime at least `n` (Euclid). -/ -private noncomputable def primeAtLeast (n : ℕ) : ℕ := - Classical.choose (Nat.exists_infinite_primes n) - -private theorem le_primeAtLeast (n : ℕ) : n ≤ primeAtLeast n := - (Classical.choose_spec (Nat.exists_infinite_primes n)).1 - -private theorem primeAtLeast_prime (n : ℕ) : (primeAtLeast n).Prime := - (Classical.choose_spec (Nat.exists_infinite_primes n)).2 - -private instance (n : ℕ) : Fact (primeAtLeast n).Prime := ⟨primeAtLeast_prime n⟩ - variable (H : ℕ) (M : ℕ → ℕ) -/-- The prime modulus of stage `l`: at least `2 ^ l` and at least the identifier bound `M l`. -/ -noncomputable def stageModulus (l : ℕ) : ℕ := primeAtLeast (max (2 ^ l) (M l)) +/-- The least prime modulus of stage `l`: at least `2 ^ l` and the identifier bound `M l`. +The definition is computable natural-number search; no machine-space bound is asserted. -/ +def stageModulus (l : ℕ) : ℕ := + Nat.find (Nat.exists_infinite_primes (max (2 ^ l) (M l))) + +theorem stageModulus_prime (l : ℕ) : (stageModulus M l).Prime := + (Nat.find_spec (Nat.exists_infinite_primes (max (2 ^ l) (M l)))).2 + +/-- The modulus meets both the stage-rate and identifier bounds. -/ +theorem le_stageModulus (l : ℕ) : max (2 ^ l) (M l) ≤ stageModulus M l := + (Nat.find_spec (Nat.exists_infinite_primes (max (2 ^ l) (M l)))).1 + +/-- No larger prime is selected when a smaller prime already meets both bounds. -/ +theorem stageModulus_le_of_prime (l : ℕ) {p : ℕ} (hp : p.Prime) + (hbound : max (2 ^ l) (M l) ≤ p) : stageModulus M l ≤ p := + Nat.find_min' (Nat.exists_infinite_primes (max (2 ^ l) (M l))) ⟨hbound, hp⟩ + +/-- Bertrand's postulate bounds the least admissible prime by twice the lower bound. -/ +theorem stageModulus_le_two_mul (l : ℕ) : stageModulus M l ≤ 2 * max (2 ^ l) (M l) := by + have hbound : 0 < max (2 ^ l) (M l) := (pow_pos (by norm_num) l).trans_le (le_max_left _ _) + obtain ⟨p, hp, hlt, hle⟩ := Nat.exists_prime_lt_and_le_two_mul _ hbound.ne' + exact (stageModulus_le_of_prime M l hp hlt.le).trans hle + +/-- The base-two logarithm costs at most one above the larger input logarithm. -/ +theorem log2_stageModulus_le (l : ℕ) : + (stageModulus M l).log2 ≤ max l (M l).log2 + 1 := by + have hbound : 0 < max (2 ^ l) (M l) := (pow_pos (by norm_num) l).trans_le (le_max_left _ _) + simp only [Nat.log2_eq_log_two] + calc Nat.log 2 (stageModulus M l) ≤ Nat.log 2 (2 * max (2 ^ l) (M l)) := + Nat.log_monotone (stageModulus_le_two_mul M l) + _ = Nat.log 2 (max (2 ^ l) (M l)) + 1 := by + rw [Nat.mul_comm, Nat.log_mul_base (by norm_num) hbound.ne'] + _ = max l (Nat.log 2 (M l)) + 1 := by + rw [(Nat.log_monotone (b := 2)).map_max, Nat.log_pow (by norm_num)] + +/-- The binary length is at most one more than the larger input length. -/ +theorem size_stageModulus_le (l : ℕ) : + (stageModulus M l).size ≤ max (l + 1) (M l).size + 1 := by + have hbound : 0 < max (2 ^ l) (M l) := (pow_pos (by norm_num) l).trans_le (le_max_left _ _) + have hsize : Monotone Nat.size := fun _ _ h => Nat.size_le_size h + calc (stageModulus M l).size ≤ (2 * max (2 ^ l) (M l)).size := + Nat.size_le_size (stageModulus_le_two_mul M l) + _ = (max (2 ^ l) (M l) <<< 1).size := by rw [Nat.shiftLeft_eq]; norm_num [Nat.mul_comm] + _ = (max (2 ^ l) (M l)).size + 1 := Nat.size_shiftLeft hbound.ne' 1 + _ = max (l + 1) (M l).size + 1 := by rw [hsize.map_max, Nat.size_pow] /-- The stage modulus is prime, so its finite-field and seed instances are available to importers. -/ -instance (l : ℕ) : Fact (stageModulus M l).Prime := ⟨primeAtLeast_prime _⟩ - -/-- The side `⌈P_l 2^(-l)⌉` of the retention box of stage `l`. -/ -noncomputable abbrev stageSide (l : ℕ) : ℕ := ⌈(stageModulus M l : ℝ) * (2⁻¹ : ℝ) ^ l⌉₊ +instance (l : ℕ) : Fact (stageModulus M l).Prime := ⟨stageModulus_prime M l⟩ + +/-- The retention-box side, computed by natural ceiling division `P_l ⌈/⌉ 2^l`. -/ +abbrev stageSide (l : ℕ) : ℕ := stageModulus M l ⌈/⌉ (2 ^ l) + +/-- Natural ceiling division gives exactly the original real-ceiling retention-box side. -/ +theorem stageSide_eq_ceil (l : ℕ) : + stageSide M l = ⌈(stageModulus M l : ℝ) * (2⁻¹ : ℝ) ^ l⌉₊ := by + apply eq_of_forall_ge_iff + intro n + rw [stageSide, ceilDiv_le_iff_le_mul (by positivity : 0 < (2 : ℕ) ^ l), Nat.ceil_le, + inv_pow, ← div_eq_mul_inv, div_le_iff₀ (by positivity : 0 < (2 : ℝ) ^ l)] + norm_cast + rw [Nat.mul_comm] + +theorem stageSide_le_stageModulus (l : ℕ) : stageSide M l ≤ stageModulus M l := by + apply (ceilDiv_le_iff_le_mul (by positivity : 0 < (2 : ℕ) ^ l)).2 + exact Nat.le_mul_of_pos_left _ (by positivity) + +theorem stageSide_pos (l : ℕ) : 0 < stageSide M l := by + by_contra h + have hz : stageSide M l ≤ 0 := Nat.le_of_not_gt h + have hp := (ceilDiv_le_iff_le_mul (by positivity : 0 < (2 : ℕ) ^ l)).1 hz + have hprime := (stageModulus_prime M l).pos + omega /-- The seeds of the affine channel of stage `l`: affine maps `𝔽_(P_l) → 𝔽_(P_l) ^ H`. -/ abbrev stageSeed (l : ℕ) : Type := @@ -104,7 +169,7 @@ theorem retentionChannels_stageChannel {V : ℕ → Type*} {ident : ∀ l, V l (((2 : ℝ) ^ H)⁻¹ ^ l) ((((stageSide M l : ℕ) : ℝ) / stageModulus M l) ^ H) 1 (2 ^ H) (2 ^ H) 4 := by set P := stageModulus M l - have hP : max (2 ^ l) (M l) ≤ P := le_primeAtLeast _ + have hP : max (2 ^ l) (M l) ≤ P := le_stageModulus M l have hinj : Function.Injective fun v => ((ident l v : ℕ) : ZMod P) := by intro a b hab have h := congrArg ZMod.val hab @@ -121,6 +186,8 @@ theorem retentionChannels_stageChannel {V : ℕ → Type*} {ident : ∀ l, V l have hrate : ((2⁻¹ : ℝ) ^ l) ^ H = ((2 : ℝ) ^ H)⁻¹ ^ l := by rw [← pow_mul, ← inv_pow, ← pow_mul, mul_comm] rw [hrate] at h + unfold stageChannel + rw [stageSide_eq_ceil] exact h end Cslib.Probability diff --git a/ComplexityTests/HierarchyChannels.lean b/ComplexityTests/HierarchyChannels.lean index 021dc64524..ce35f0a362 100644 --- a/ComplexityTests/HierarchyChannels.lean +++ b/ComplexityTests/HierarchyChannels.lean @@ -1,19 +1,62 @@ /- -Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Christian Reitwiessner +Authors: Christian Reitwiessner, Samuel Schlesinger -/ import Complexity.Probability.PairwiseIndependentHash.HierarchyChannels import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum /-! -# Tests for the hierarchy with affine channels on radix identifiers +# Tests for the hierarchy with bounded computable affine channels on radix identifiers + +Evaluation checks exercise least-prime search at the zero-identifier boundary, a composite lower +bound, and a prime lower bound. The formal examples use minimality and binary-length bounds and +verify the retained channel interface with the new computable side. -/ namespace ComplexityTests.HierarchyChannels open Finset Matrix Cslib.Probability +-- Both parameters execute using natural arithmetic: these checks do not evaluate a real ceiling. +/-- info: [2, 11, 17, 2, 2] -/ +#guard_msgs in +#eval [stageModulus (fun _ => 0) 0, stageModulus (fun _ => 0) 3, + stageModulus (fun _ => 17) 3, stageSide (fun _ => 0) 0, stageSide (fun _ => 5) 2] + +-- A prime identifier bound above the power-of-two bound is selected exactly. +example : stageModulus (fun _ => 17) 3 = 17 := by + apply le_antisymm (stageModulus_le_of_prime _ _ (by norm_num) (by norm_num)) + simpa using le_stageModulus (fun _ => 17) 3 + +private theorem modulus_five : stageModulus (fun _ => 5) 2 = 5 := by + apply le_antisymm (stageModulus_le_of_prime _ _ (by norm_num) (by norm_num)) + simpa using le_stageModulus (fun _ => 5) 2 + +-- The arithmetic side agrees with the nonintegral mathematical ratio ceil(5/4). +example : stageSide (fun _ => 5) 2 = 2 ∧ + ⌈(stageModulus (fun _ => 5) 2 : ℝ) * (2⁻¹ : ℝ) ^ 2⌉₊ = 2 := by + have h : stageSide (fun _ => 5) 2 = 2 := by + norm_num [stageSide, modulus_five, Nat.ceilDiv_eq_add_pred_div] + exact ⟨h, (stageSide_eq_ceil (fun _ => 5) 2).symm.trans h⟩ + +-- An identifier bound exponential in the stage index needs only a linear binary-length bound. +example (r l : ℕ) : + (stageModulus (fun i => 2 ^ (r * i)) l).size ≤ max (l + 1) (r * l + 1) + 1 := by + simpa only [Nat.size_pow] using size_stageModulus_le (fun i => 2 ^ (r * i)) l + +-- At stage two, identifiers below five use modulus five and side two: the actual retention +-- density is 2/5, while the requested stage rate is 1/4. The original uniform constants apply. +example : + let X := stageChannel 1 (fun _ => 5) (V := fun _ => Fin 5) (fun _ v => v.val) 2 + RetentionChannels X X (1 / 4) (2 / 5) 1 2 2 4 := by + intro X + have h := retentionChannels_stageChannel (H := 1) (M := fun _ => 5) + (V := fun _ => Fin 5) (ident := fun _ v => v.val) + (fun _ => Fin.val_injective) (fun _ v => v.isLt) 2 + convert h using 1 <;> norm_num [stageSide, modulus_five, Nat.ceilDiv_eq_add_pred_div] + /-- A walk on three time layers: from `0` to `1` and from `1` to `2`, each with probability `1 / 2`. -/ private noncomputable def C : Matrix (Fin 3) (Fin 3) ℝ := !![0, 1 / 2, 0; 0, 0, 1 / 2; 0, 0, 0]