diff --git a/Complexity.lean b/Complexity.lean index 80489d35d..858510de0 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -873,6 +873,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional @@ -2821,6 +2822,7 @@ public import Complexity.Foundations.NumberTheory.AKS.Criterion public import Complexity.Foundations.NumberTheory.AKS.Introspective public import Complexity.Foundations.NumberTheory.AKS.SmallR public import Complexity.Foundations.NumberTheory.Harmonic +public import Complexity.Foundations.NumberTheory.Padics.RatValuation public import Complexity.Foundations.NumberTheory.PrimeCounting public import Complexity.Foundations.NumberTheory.PrimeWindow public import Complexity.Foundations.NumberTheory.SqrtPrimeWindow diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/IntegralCoordinates.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IntegralCoordinates.lean new file mode 100644 index 000000000..be7ad962d --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IntegralCoordinates.lean @@ -0,0 +1,351 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation +public import Mathlib.Algebra.Polynomial.Lifts +public import Mathlib.NumberTheory.Padics.PadicNumbers +public import Mathlib.RingTheory.Valuation.Integers +import Complexity.Foundations.NumberTheory.Padics.RatValuation +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.LinearCombination + +/-! +# Integral local coordinates for the Cauchy kernel + +This file proves Lemma D.4 of [OpenAI2026ETH] (§D.4.3, p. 59; proof on p. 60): near each grid +point the Cauchy kernel has `2`-integral coefficients. Let `L = 2 ^ a`, so that the grid +`S = {-L, …, L - 1}` is a complete residue system modulo `α = 2 ^ (a + 1)`. For `t, d ∈ S`, the +polynomial `z ↦ W_d(t + α z)` obtained from the Cauchy kernel `W_d = cauchyKernel L d` has +coefficients in `ℤ_(2)`, the rationals with odd denominator +(`Cslib.Circuits.Frontier.cauchyKernel_comp_mem_lifts`); when `d ≠ t` it is moreover divisible by +`2` (`Cslib.Circuits.Frontier.exists_cauchyKernel_comp_eq_two_mul`). Here `ℤ_(2)` is the valuation +ring `(Rat.padicValuation 2).integer`, and "coefficients in `ℤ_(2)`" is membership in +`Polynomial.lifts` of its inclusion. + +The proof is the manuscript's. Since `S` is a complete residue system modulo `2 ^ (a + 1)`, the +nonzero differences `t - q`, `q ∈ S`, have the same `2`-adic valuations for every `t`; so +`C'(t) = ∏_{q ≠ t} (t - q)` has the valuation of `C'(0)` +(`Cslib.Circuits.Frontier.padicValuation_prod_sub_eq`). Each factor `t - q + α z` with `q ≠ t` is +`(t - q) (1 + α / (t - q) z)` with `α / (t - q)` divisible by `2`, and the factor `q = t` is +`α z`. + +Entrywise, the Cauchy matrix has the same property +(`Cslib.Circuits.Frontier.cauchyMatrix_comp_mem_lifts`). Consequently, for tensors with entries in +a subring `B` of a `ℚ`-algebra `R` that contains `ℤ_(2)`, the deformed contraction `F(T)` along the +Cauchy matrix satisfies `F(t + α z) ∈ B[z]` +(`Cslib.Circuits.Frontier.TensorNetwork.deformedContraction_cauchyMatrix_comp_mem_liftsRing`): the +manuscript's `F(t + α z) ∈ A[z]` with `B = O`. Coefficients in `ℤ_(2)` reduce modulo `2 ^ p` +through `Rat.padicIntegerToZModPow`; the valuations of integers that the proof uses are +`Rat.padicValuation_pow_le_of_abs_lt` and `Rat.padicValuation_add_pow_of_abs_lt`. The algorithmic +half of the lemma, evaluating `W_xy(t + α ζ) mod 2 ^ p` in polynomial time, belongs to the +runtime development. + +## Main results + +* `Cslib.Circuits.Frontier.padicValuation_prod_sub_eq`: `v₂(C'(t)) = v₂(C'(0))` on the grid. +* `Cslib.Circuits.Frontier.cauchyKernel_comp_mem_lifts`: `W_d(t + α z)` has `2`-integral + coefficients. +* `Cslib.Circuits.Frontier.exists_cauchyKernel_comp_eq_two_mul`: it is divisible by `2` unless + `d = t`. +* `Cslib.Circuits.Frontier.cauchyMatrix_comp_mem_lifts`: the same for the Cauchy matrix. +* `Cslib.Circuits.Frontier.TensorNetwork.deformedContraction_mem`: a deformed contraction lies in + any subring containing the tensor and matrix entries. +* `Cslib.Circuits.Frontier.TensorNetwork.deformedContraction_cauchyMatrix_comp_mem_liftsRing`: + `F(t + α z)` has coefficients in any subring containing `ℤ_(2)` and the tensor entries. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.3, Lemma D.4, + pp. 59–60. +-/ + +public section + +namespace Cslib.Circuits.Frontier + +open Polynomial +open scoped WithZero + +/-! ### Two-adic valuations on the grid -/ + +/-- The `2`-adic valuation of a power of two. -/ +private theorem padicValuation_two_pow (k : ℕ) : + Rat.padicValuation 2 ((2 : ℚ) ^ k) = WithZero.exp (-(k : ℤ)) := by + exact_mod_cast Rat.padicValuation_pow_self 2 k + +private theorem padicValuation_two_pow_le {a : ℕ} {x : ℤ} (hx : x ≠ 0) + (hlt : |x| < 2 ^ (a + 1)) : + Rat.padicValuation 2 ((2 : ℚ) ^ a) ≤ Rat.padicValuation 2 (x : ℚ) := by + exact_mod_cast Rat.padicValuation_pow_le_of_abs_lt (p := 2) hx (by exact_mod_cast hlt) + +private theorem padicValuation_add_two_pow {a : ℕ} {x : ℤ} (hx : x ≠ 0) + (hlt : |x| < 2 ^ (a + 1)) : + Rat.padicValuation 2 ((x : ℚ) + 2 ^ (a + 1)) = Rat.padicValuation 2 (x : ℚ) := by + exact_mod_cast Rat.padicValuation_add_pow_of_abs_lt (p := 2) hx (by exact_mod_cast hlt) + +/-- **The grid is a complete residue system.** For `t` on the grid of `L = 2 ^ a` slots, the +nonzero differences `t - q`, `q ∈ S`, have the valuations of `1, …, 2 L - 1`: send `q` to the +residue of `t - q` modulo `2 L`. -/ +theorem padicValuation_prod_sub_eq_prod_Ioo {a : ℕ} {t : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) : + Rat.padicValuation 2 (∏ q ∈ (cauchyGrid (2 ^ a)).erase t, ((t : ℚ) - q)) = + ∏ r ∈ Finset.Ioo (0 : ℤ) (2 ^ (a + 1)), Rat.padicValuation 2 (r : ℚ) := by + rw [map_prod] + set L : ℤ := 2 ^ a with hL + have hL2 : (2 : ℤ) ^ (a + 1) = 2 * L := by rw [hL, pow_succ, mul_comm] + have hLpos : 0 < L := by positivity + rw [mem_cauchyGrid] at ht + simp only [cauchyGrid, Nat.cast_pow, Nat.cast_ofNat, ← hL] at ht ⊢ + rw [hL2] + refine Finset.prod_nbij' (fun q => if q < t then t - q else t - q + 2 * L) + (fun r => if -L ≤ t - r then t - r else t - r + 2 * L) ?_ ?_ ?_ ?_ ?_ + · intro q hq + simp only [Finset.mem_erase, Finset.mem_Ico, Finset.mem_Ioo] at hq ⊢ + split_ifs <;> omega + · intro r hr + simp only [Finset.mem_erase, Finset.mem_Ico, Finset.mem_Ioo] at hr ⊢ + split_ifs <;> omega + · intro q hq + simp only [Finset.mem_erase, Finset.mem_Ico] at hq + split_ifs <;> omega + · intro r hr + simp only [Finset.mem_Ioo] at hr + split_ifs <;> omega + · intro q hq + simp only [Finset.mem_erase, Finset.mem_Ico] at hq + have hne : t - q ≠ 0 := by omega + have habs : |t - q| < 2 ^ (a + 1) := by rw [hL2, abs_lt]; omega + have h2L : (2 : ℚ) * (L : ℚ) = 2 ^ (a + 1) := by exact_mod_cast hL2.symm + have hadd := padicValuation_add_two_pow hne habs + push_cast at hadd + split_ifs + · push_cast; rfl + · push_cast + rw [h2L] + exact hadd.symm + +/-- **`v₂(C'(t)) = v₂(C'(0))` on the grid** of `L = 2 ^ a` slots, where +`C'(t) = ∏_{q ∈ S, q ≠ t} (t - q)`. -/ +theorem padicValuation_prod_sub_eq {a : ℕ} {t : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) : + Rat.padicValuation 2 (∏ q ∈ (cauchyGrid (2 ^ a)).erase t, ((t : ℚ) - q)) = + Rat.padicValuation 2 (∏ q ∈ (cauchyGrid (2 ^ a)).erase 0, ((0 : ℚ) - q)) := by + have h0 : (0 : ℤ) ∈ cauchyGrid (2 ^ a) := by + have : (0 : ℤ) < ((2 ^ a : ℕ) : ℤ) := by positivity + rw [mem_cauchyGrid] + exact ⟨by linarith, this⟩ + rw [padicValuation_prod_sub_eq_prod_Ioo ht] + exact_mod_cast (padicValuation_prod_sub_eq_prod_Ioo h0).symm + +/-- Distinct grid points of `L = 2 ^ a` slots differ by at most `a` factors of two. -/ +theorem padicValuation_two_pow_le_sub {a : ℕ} {t q : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) + (hq : q ∈ cauchyGrid (2 ^ a)) (hne : q ≠ t) : + Rat.padicValuation 2 ((2 : ℚ) ^ a) ≤ Rat.padicValuation 2 ((t : ℚ) - q) := by + rw [mem_cauchyGrid] at ht hq + push_cast at ht hq + have hlt : |t - q| < 2 ^ (a + 1) := by + rw [pow_succ, abs_lt] + constructor <;> linarith + exact_mod_cast padicValuation_two_pow_le (sub_ne_zero.mpr hne.symm) hlt + +/-! ### The kernel in local coordinates -/ + +/-- The subring `ℤ_(2)` of rationals with odd denominator. -/ +local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2) + +private theorem C_mem_lifts_of_le_one {c : ℚ} (hc : Rat.padicValuation 2 c ≤ 1) : + C c ∈ lifts (ℤ₍₂₎).subtype := + C_mem_lifts (ℤ₍₂₎).subtype (⟨c, hc⟩ : ℤ₍₂₎) + +/-- A shifted factor `t + α z - q` with `q ≠ t` is `(t - q) (1 + α / (t - q) z)`. -/ +private theorem shift_factor {t q α : ℚ} (h : t - q ≠ 0) : + C t + C α * X - C q = C (t - q) * (1 + C (α / (t - q)) * X) := by + rw [mul_add, mul_one, ← mul_assoc, ← C_mul, mul_div_cancel₀ _ h, C_sub] + ring + +/-- The kernel in local coordinates, as a product of the shifted factors. -/ +private theorem cauchyKernel_comp (L : ℕ) (d : ℤ) (t α : ℚ) : + (cauchyKernel L d).comp (C t + C α * X) = + C ((∏ q ∈ (cauchyGrid L).erase 0, ((0 : ℚ) - q))⁻¹) * + ∏ q ∈ (cauchyGrid L).erase d, (C t + C α * X - C (q : ℚ)) := by + rw [cauchyKernel, Lagrange.eval_nodal, mul_comp, C_comp, Lagrange.nodal, prod_comp] + simp only [sub_comp, X_comp, C_comp] + +/-- The unit factors `1 + α / (t - q) z` with `q ≠ t` are integral. -/ +private theorem prod_one_add_mem_lifts {a : ℕ} {t : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) + (s : Finset ℤ) (hs : s ⊆ (cauchyGrid (2 ^ a)).erase t) : + ∏ q ∈ s, (1 + C ((2 : ℚ) ^ (a + 1) / ((t : ℚ) - q)) * X) ∈ lifts (ℤ₍₂₎).subtype := by + refine Subsemiring.prod_mem _ fun q hq => ?_ + obtain ⟨hqt, hqS⟩ := Finset.mem_erase.mp (hs hq) + refine add_mem (one_mem _) (mul_mem (C_mem_lifts_of_le_one ?_) (X_mem_lifts _)) + have hle := padicValuation_two_pow_le_sub ht hqS hqt + have hne : ((t : ℚ) - q) ≠ 0 := sub_ne_zero.mpr (by exact_mod_cast hqt.symm) + rw [map_div₀, div_le_one₀ ((Rat.padicValuation 2).pos_iff.mpr hne)] + refine le_trans ?_ hle + rw [padicValuation_two_pow, padicValuation_two_pow, WithZero.exp_le_exp] + omega + +/-- A product of differences `t - q` over points `q ≠ t` is nonzero. -/ +private theorem prod_sub_ne_zero {t : ℤ} {s : Finset ℤ} (hs : t ∉ s) : + ∏ q ∈ s, ((t : ℚ) - q) ≠ 0 := + Finset.prod_ne_zero_iff.mpr fun q hq => + sub_ne_zero.mpr fun h => hs (by rw [show t = q by exact_mod_cast h]; exact hq) + +/-- Shifted factors at points `q ≠ t` split into a constant and the unit factors. -/ +private theorem prod_shift {t : ℤ} (α : ℚ) {s : Finset ℤ} (hs : t ∉ s) : + ∏ q ∈ s, (C (t : ℚ) + C α * X - C (q : ℚ)) = + C (∏ q ∈ s, ((t : ℚ) - q)) * ∏ q ∈ s, (1 + C (α / ((t : ℚ) - q)) * X) := by + calc + ∏ q ∈ s, (C (t : ℚ) + C α * X - C (q : ℚ)) = + ∏ q ∈ s, (C ((t : ℚ) - q) * (1 + C (α / ((t : ℚ) - q)) * X)) := + Finset.prod_congr rfl fun (q : ℤ) hq => shift_factor + (sub_ne_zero.mpr fun h => hs (by rw [show t = q by exact_mod_cast h]; exact hq)) + _ = _ := by rw [Finset.prod_mul_distrib, map_prod] + +/-- **Lemma D.4, divisibility.** Away from its own node, `d ≠ t`, the Cauchy kernel in local +coordinates `z ↦ W_d(t + α z)`, `α = 2 ^ (a + 1)`, is twice a polynomial with `2`-integral +coefficients: the factor `α z` survives, and `α / (t - d)` is divisible by `2`. -/ +theorem exists_cauchyKernel_comp_eq_two_mul {a : ℕ} {t d : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) + (hd : d ∈ cauchyGrid (2 ^ a)) (hdt : d ≠ t) : + ∃ P ∈ lifts (ℤ₍₂₎).subtype, + (cauchyKernel (2 ^ a) d).comp (C (t : ℚ) + C ((2 : ℚ) ^ (a + 1)) * X) = C 2 * P := by + have htd : t ∈ (cauchyGrid (2 ^ a)).erase d := Finset.mem_erase.mpr ⟨hdt.symm, ht⟩ + set s := ((cauchyGrid (2 ^ a)).erase d).erase t with hs_def + have hts : t ∉ s := Finset.notMem_erase t _ + have hs : s ⊆ (cauchyGrid (2 ^ a)).erase t := fun q hq => by + simp only [s, Finset.mem_erase] at hq ⊢ + exact ⟨hq.1, hq.2.2⟩ + have htd' : ((t : ℚ) - d) ≠ 0 := sub_ne_zero.mpr (by exact_mod_cast hdt.symm) + have hdt' : d ∈ (cauchyGrid (2 ^ a)).erase t := Finset.mem_erase.mpr ⟨hdt, hd⟩ + have hCt : ∏ q ∈ (cauchyGrid (2 ^ a)).erase t, ((t : ℚ) - q) = + ((t : ℚ) - d) * ∏ q ∈ s, ((t : ℚ) - q) := by + rw [hs_def, Finset.erase_right_comm] + exact (Finset.mul_prod_erase _ (fun q : ℤ => (t : ℚ) - q) hdt').symm + obtain ⟨C₀, hC₀def⟩ : ∃ C₀ : ℚ, C₀ = ∏ q ∈ (cauchyGrid (2 ^ a)).erase 0, ((0 : ℚ) - q) := + ⟨_, rfl⟩ + have hC₀ : C₀ ≠ 0 := by + have := prod_sub_ne_zero (Finset.notMem_erase (0 : ℤ) (cauchyGrid (2 ^ a))) + push_cast at this + rwa [hC₀def] + obtain ⟨c, hc⟩ : ∃ c : ℚ, c = C₀⁻¹ * (2 ^ (a + 1) * ∏ q ∈ s, ((t : ℚ) - q)) := ⟨_, rfl⟩ + refine ⟨C (c / 2) * X * ∏ q ∈ s, (1 + C ((2 : ℚ) ^ (a + 1) / ((t : ℚ) - q)) * X), ?_, ?_⟩ + · refine mul_mem (mul_mem (C_mem_lifts_of_le_one ?_) (X_mem_lifts _)) + (prod_one_add_mem_lifts ht s hs) + have hc2 : c / 2 = + 2 ^ a * (C₀⁻¹ * ∏ q ∈ (cauchyGrid (2 ^ a)).erase t, ((t : ℚ) - q)) / ((t : ℚ) - d) := by + rw [hc, hCt, pow_succ] + field_simp + have hval : + Rat.padicValuation 2 (C₀⁻¹ * ∏ q ∈ (cauchyGrid (2 ^ a)).erase t, ((t : ℚ) - q)) = 1 := by + rw [map_mul, map_inv₀, padicValuation_prod_sub_eq ht, ← hC₀def, + inv_mul_cancel₀ ((Rat.padicValuation 2).ne_zero_iff.mpr hC₀)] + rw [hc2, map_div₀, map_mul, hval, mul_one, + div_le_one₀ ((Rat.padicValuation 2).pos_iff.mpr htd')] + exact padicValuation_two_pow_le_sub ht hd hdt + · rw [cauchyKernel_comp, ← Finset.mul_prod_erase _ _ htd, prod_shift _ hts, ← hC₀def, + show C (t : ℚ) + C ((2 : ℚ) ^ (a + 1)) * X - C (t : ℚ) = C ((2 : ℚ) ^ (a + 1)) * X by ring] + have h2 : C (2 : ℚ) * C (c / 2) = C c := by rw [← C_mul, mul_div_cancel₀ _ two_ne_zero] + have hcC : C c = C C₀⁻¹ * (C ((2 : ℚ) ^ (a + 1)) * C (∏ q ∈ s, ((t : ℚ) - q))) := by + rw [hc, C_mul, C_mul] + linear_combination + (-(X * ∏ q ∈ s, (1 + C ((2 : ℚ) ^ (a + 1) / ((t : ℚ) - q)) * X))) * h2 - + (X * ∏ q ∈ s, (1 + C ((2 : ℚ) ^ (a + 1) / ((t : ℚ) - q)) * X)) * hcC + +/-- **Lemma D.4, integrality.** For grid points `t, d` of `L = 2 ^ a` slots, the Cauchy kernel in +local coordinates `z ↦ W_d(t + α z)`, `α = 2 ^ (a + 1)`, has coefficients in `ℤ_(2)`. At its own +node, `d = t`, its constant term is `C'(t) / C'(0)`, of valuation one, and the other factors are +`1 + α / (t - q) z`. -/ +theorem cauchyKernel_comp_mem_lifts {a : ℕ} {t d : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) + (hd : d ∈ cauchyGrid (2 ^ a)) : + (cauchyKernel (2 ^ a) d).comp (C (t : ℚ) + C ((2 : ℚ) ^ (a + 1)) * X) ∈ + lifts (ℤ₍₂₎).subtype := by + rcases eq_or_ne d t with rfl | hdt + · have hts : d ∉ (cauchyGrid (2 ^ a)).erase d := Finset.notMem_erase d _ + rw [cauchyKernel_comp, prod_shift _ hts, ← mul_assoc, ← C_mul] + refine mul_mem (C_mem_lifts_of_le_one (le_of_eq ?_)) (prod_one_add_mem_lifts ht _ subset_rfl) + have hC₀ := prod_sub_ne_zero (Finset.notMem_erase (0 : ℤ) (cauchyGrid (2 ^ a))) + push_cast at hC₀ + rw [map_mul, map_inv₀, padicValuation_prod_sub_eq ht, + inv_mul_cancel₀ ((Rat.padicValuation 2).ne_zero_iff.mpr hC₀)] + · obtain ⟨P, hP, h⟩ := exists_cauchyKernel_comp_eq_two_mul ht hd hdt + rw [h] + refine mul_mem (C_mem_lifts_of_le_one ?_) hP + have h2 := padicValuation_two_pow 1 + rw [pow_one] at h2 + rw [h2, ← WithZero.exp_zero, WithZero.exp_le_exp] + norm_num + +/-! ### The Cauchy matrix and the deformed contraction -/ + +/-- **Lemma D.4 for the Cauchy matrix.** For a packing into packets of `2 ^ a` slots, every entry +of the Cauchy matrix in local coordinates `z ↦ W(t + α z)` has `2`-integral coefficients. -/ +theorem cauchyMatrix_comp_mem_lifts {E P : Type*} [DecidableEq P] {a : ℕ} {packet : E → P} + {slot : E → ℕ} (hslot : ∀ e, slot e < 2 ^ a) {t : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) + (e e' : E) : + (cauchyMatrix (2 ^ a) packet slot e e').comp (C (t : ℚ) + C ((2 : ℚ) ^ (a + 1)) * X) ∈ + lifts (ℤ₍₂₎).subtype := by + unfold cauchyMatrix + split_ifs + · exact cauchyKernel_comp_mem_lifts ht (sub_mem_cauchyGrid (hslot e) (hslot e')) + · rw [zero_comp] + exact zero_mem _ + +namespace TensorNetwork + +variable {R V E : Type*} [CommRing R] [Fintype V] [Fintype E] [DecidableEq E] + +/-- A deformed contraction lies in every subring that contains the tensor entries and the matrix +entries: it is a polynomial expression in them. -/ +theorem deformedContraction_mem (N : TensorNetwork R Bool V E) (side : V → Bool) + (W : Matrix E E R) (T : Subring R) (hN : ∀ v x, N.tensor v x ∈ T) + (hW : ∀ e e', W e e' ∈ T) : N.deformedContraction side W ∈ T := by + unfold deformedContraction + refine T.sum_mem fun X _ => T.sum_mem fun Y _ => T.mul_mem (T.mul_mem + (T.prod_mem fun v _ => hN v Y) (T.prod_mem fun v _ => hN v X)) (T.prod_mem fun e _ => ?_) + have hv : W.mulVec (fun e' => if X e' then (1 : R) else 0) e ∈ T := by + unfold Matrix.mulVec dotProduct + refine T.sum_mem fun e' _ => T.mul_mem (hW e e') ?_ + dsimp only + split_ifs + exacts [T.one_mem, T.zero_mem] + unfold affineFactor + split_ifs + exacts [hv, T.sub_mem T.one_mem hv] + +/-- **Lemma D.4 for the deformed contraction.** Let `R` be a `ℚ`-algebra and `B` a subring of `R` +containing `ℤ_(2)`, and let the tensors have entries in `B`. Along the Cauchy matrix of a packing +into packets of `2 ^ a` slots, the deformed contraction `F(T)` satisfies `F(t + α z) ∈ B[z]` at +every grid point `t`, with `α = 2 ^ (a + 1)`. For the manuscript, `R = K`, `B = O` and `F(0)` is +the contraction (`eval_zero_deformedContraction_cauchyMatrix`). -/ +theorem deformedContraction_cauchyMatrix_comp_mem_liftsRing [Algebra ℚ R] {P : Type*} + [DecidableEq P] (N : TensorNetwork R Bool V E) (side : V → Bool) {a : ℕ} {packet : E → P} + {slot : E → ℕ} (hslot : ∀ e, slot e < 2 ^ a) {t : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) + (B : Subring R) (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ R c ∈ B) (hN : ∀ v x, N.tensor v x ∈ B) : + ((N.map Polynomial.C).deformedContraction side + ((cauchyMatrix (2 ^ a) packet slot).map (Polynomial.mapRingHom (algebraMap ℚ R)))).comp + (C (t : R) + C (2 ^ (a + 1)) * X) ∈ liftsRing B.subtype := by + have hq : (C (t : R) + C (2 ^ (a + 1)) * X : R[X]) = + (C (t : ℚ) + C ((2 : ℚ) ^ (a + 1)) * X).map (algebraMap ℚ R) := by + rw [Polynomial.map_add, Polynomial.map_mul, Polynomial.map_C, Polynomial.map_C, + Polynomial.map_X] + exact congrArg₂ (· + ·) (congrArg C (map_intCast _ t).symm) + (congrArg (C · * X) (by rw [map_pow, map_ofNat])) + rw [← coe_compRingHom_apply, ← deformedContraction_map] + refine deformedContraction_mem _ side _ _ (fun v x => ?_) (fun e e' => ?_) + · rw [map_tensor, map_tensor, coe_compRingHom_apply, C_comp, ← lifts_iff_liftsRing] + exact C_mem_lifts B.subtype ⟨_, hN v x⟩ + · rw [Matrix.map_apply, Matrix.map_apply, coe_compRingHom_apply, coe_mapRingHom, hq, + ← map_comp, ← lifts_iff_liftsRing, lifts_iff_coeff_lifts] + intro n + obtain ⟨c, hc⟩ := (lifts_iff_coeff_lifts _).mp + (cauchyMatrix_comp_mem_lifts (packet := packet) hslot ht e e') n + rw [coeff_map, ← hc] + exact ⟨⟨_, hB c c.2⟩, rfl⟩ + +end TensorNetwork + +end Cslib.Circuits.Frontier diff --git a/Complexity/Foundations/NumberTheory/Padics/RatValuation.lean b/Complexity/Foundations/NumberTheory/Padics/RatValuation.lean new file mode 100644 index 000000000..3c249ac98 --- /dev/null +++ b/Complexity/Foundations/NumberTheory/Padics/RatValuation.lean @@ -0,0 +1,123 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, `Mathlib/NumberTheory/Padics/RingHoms.lean`) + +public import Complexity.Init +public import Mathlib.NumberTheory.Padics.RingHoms +public import Mathlib.RingTheory.Valuation.Integers +import Mathlib.NumberTheory.Padics.PadicVal.Basic + +/-! +# The `p`-adic valuation of rationals: integers and reduction modulo `p ^ n` + +Two facts about `Rat.padicValuation p`. First, valuations of integers below `p ^ (a + 1)`: such +a nonzero integer has at most `a` factors of `p` (`Rat.padicValuation_pow_le_of_abs_lt`), so adding +`p ^ (a + 1)` does not change its valuation (`Rat.padicValuation_add_pow_of_abs_lt`). + +Second, reduction modulo `p ^ n`. The rationals whose denominator is prime to `p` form the +valuation ring `ℤ_(p)` of `Rat.padicValuation p`. It embeds in the `p`-adic integers +(`Rat.padicIntegerToPadicInt`), so it has reductions modulo every power of `p` +(`Rat.padicIntegerToZModPow`). On `a / b` with `b` prime to `p`, the reduction is `a * b⁻¹`: it +is characterized by `Rat.padicIntegerToZModPow_mul_den`. + +Both serve the integral local coordinates of the Cauchy kernel of [OpenAI2026ETH] (Lemma D.4, +pp. 59–60): the first shows that its grid is a complete residue system for valuations, and the +second reduces its `ℤ_(2)` coefficients modulo the working precision `2 ^ p`. + +## Main definitions + +* `Rat.padicIntegerToPadicInt`: the inclusion `ℤ_(p) → ℤ_[p]`. +* `Rat.padicIntegerToZModPow`: reduction `ℤ_(p) → ZMod (p ^ n)`. + +## Main results + +* `Rat.padicValuation_pow_self`: `v (p ^ k) = exp (-k)`. +* `Rat.padicValuation_pow_le_of_abs_lt`: a nonzero integer below `p ^ (a + 1)` in absolute value + has valuation at least `v (p ^ a)`. +* `Rat.padicValuation_add_pow_of_abs_lt`: adding `p ^ (a + 1)` to it keeps its valuation. +* `Rat.padicIntegerToZModPow_mul_den`: the reduction of `x` times the denominator of `x` is the + numerator of `x`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.3, pp. 59–60. +-/ + +public section + +open scoped WithZero + +namespace Rat + +variable (p : ℕ) [Fact p.Prime] + +/-! ### Valuations of integers -/ + +/-- The `p`-adic valuation of a nonzero integer. -/ +theorem padicValuation_intCast_of_ne_zero {x : ℤ} (hx : x ≠ 0) : + Rat.padicValuation p (x : ℚ) = WithZero.exp (-(padicValInt p x : ℤ)) := by + simp [Rat.padicValuation, hx, padicValRat.of_int] + +/-- The `p`-adic valuation of a power of `p`. -/ +theorem padicValuation_pow_self (k : ℕ) : + Rat.padicValuation p ((p : ℚ) ^ k) = WithZero.exp (-(k : ℤ)) := by + rw [map_pow, Rat.padicValuation_self, ← WithZero.exp_nsmul, nsmul_eq_mul, mul_neg, mul_one] + +variable {p} + +/-- **A nonzero integer below `p ^ (a + 1)` in absolute value has at most `a` factors of `p`.** -/ +theorem padicValuation_pow_le_of_abs_lt {a : ℕ} {x : ℤ} (hx : x ≠ 0) + (hlt : |x| < (p : ℤ) ^ (a + 1)) : + Rat.padicValuation p ((p : ℚ) ^ a) ≤ Rat.padicValuation p (x : ℚ) := by + rw [padicValuation_pow_self, padicValuation_intCast_of_ne_zero p hx, WithZero.exp_le_exp, + neg_le_neg_iff] + by_contra h + have hdvd : (p : ℤ) ^ (a + 1) ∣ x := (padicValInt_dvd_iff (a + 1) x).mpr (Or.inr (by omega)) + exact absurd (Int.le_of_dvd (abs_pos.mpr hx) ((dvd_abs _ _).mpr hdvd)) (not_le.mpr hlt) + +/-- **Adding `p ^ (a + 1)` to a nonzero integer below it in absolute value keeps its valuation.** -/ +theorem padicValuation_add_pow_of_abs_lt {a : ℕ} {x : ℤ} (hx : x ≠ 0) + (hlt : |x| < (p : ℤ) ^ (a + 1)) : + Rat.padicValuation p ((x : ℚ) + (p : ℚ) ^ (a + 1)) = Rat.padicValuation p (x : ℚ) := by + refine (Rat.padicValuation p).map_add_eq_of_lt_left (lt_of_lt_of_le ?_ + (padicValuation_pow_le_of_abs_lt hx hlt)) + rw [padicValuation_pow_self, padicValuation_pow_self, WithZero.exp_lt_exp] + omega + +variable (p) + +/-! ### Reduction modulo `p ^ n` -/ + +/-- The inclusion of the `p`-integral rationals `ℤ_(p)` in the `p`-adic integers. -/ +noncomputable def padicIntegerToPadicInt : (Rat.padicValuation p).integer →+* ℤ_[p] where + toFun x := ⟨(x : ℚ), Padic.norm_rat_le_one (Rat.padicValuation_le_one_iff.mp x.2)⟩ + map_one' := Subtype.ext (by simp) + map_mul' x y := Subtype.ext (by push_cast; rfl) + map_zero' := Subtype.ext (by simp) + map_add' x y := Subtype.ext (by push_cast; rfl) + +@[simp] +theorem coe_padicIntegerToPadicInt (x : (Rat.padicValuation p).integer) : + ((padicIntegerToPadicInt p x : ℤ_[p]) : ℚ_[p]) = ((x : ℚ) : ℚ_[p]) := by + simp only [padicIntegerToPadicInt] + rfl + +/-- Reduction of the `p`-integral rationals modulo `p ^ n`. -/ +noncomputable def padicIntegerToZModPow (n : ℕ) : (Rat.padicValuation p).integer →+* ZMod (p ^ n) := + (PadicInt.toZModPow n).comp (padicIntegerToPadicInt p) + +/-- **The reduction of `a / b` is `a * b⁻¹`**: multiplied by the denominator it gives the +numerator. -/ +theorem padicIntegerToZModPow_mul_den (n : ℕ) (x : (Rat.padicValuation p).integer) : + padicIntegerToZModPow p n x * ((x : ℚ).den : ZMod (p ^ n)) = ((x : ℚ).num : ZMod (p ^ n)) := by + have h : x * ((x : ℚ).den : (Rat.padicValuation p).integer) = + ((x : ℚ).num : (Rat.padicValuation p).integer) := + Subtype.ext (by push_cast; exact Rat.mul_den_eq_num _) + simpa only [map_mul, map_natCast, map_intCast] using congrArg (padicIntegerToZModPow p n) h + +end Rat diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIntegralCoordinates.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIntegralCoordinates.lean new file mode 100644 index 000000000..65ad05b7a --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIntegralCoordinates.lean @@ -0,0 +1,110 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates +import Complexity.Foundations.NumberTheory.Padics.RatValuation + +/-! +# Tests for the integral local coordinates of the Cauchy kernel + +With `L = 2` slots the grid is `{-2, -1, 0, 1}`, `C'(0) = -2` and `α = 4`. The kernel at `1` is +`-(T + 2) (T + 1) T / 2`, whose leading coefficient `-1/2` is not `2`-integral; in the local +coordinate `T = 1 + 4 z` it becomes `2`-integral (Lemma D.4). +-/ + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates + +open Cslib.Circuits.Frontier Polynomial +open scoped WithZero + +/-- The grid of two slots. -/ +theorem cauchyGrid_two : cauchyGrid 2 = {-2, -1, 0, 1} := by decide + +/-- The leading coefficient of the kernel is `C'(0)⁻¹ = -1/2`. -/ +theorem coeff_cauchyKernel_two_one : (cauchyKernel 2 1).coeff 3 = -1 / 2 := by + have hmem : (1 : ℤ) ∈ cauchyGrid 2 := by decide + have hdeg := natDegree_cauchyKernel hmem + have hlead : (cauchyKernel 2 1).leadingCoeff = + ((Lagrange.nodal ((cauchyGrid 2).erase 0) (Int.cast : ℤ → ℚ)).eval 0)⁻¹ := by + rw [cauchyKernel, leadingCoeff_mul, leadingCoeff_C, Lagrange.nodal_monic.leadingCoeff, + mul_one] + rw [leadingCoeff, hdeg] at hlead + rw [show 3 = 2 * 2 - 1 from rfl, hlead, Lagrange.eval_nodal, cauchyGrid_two] + rw [show ({-2, -1, 0, 1} : Finset ℤ).erase 0 = {-2, -1, 1} by decide] + simp only [Finset.prod_insert (by decide : (-2 : ℤ) ∉ ({-1, 1} : Finset ℤ)), + Finset.prod_insert (by decide : (-1 : ℤ) ∉ ({1} : Finset ℤ)), Finset.prod_singleton] + norm_num + +theorem padicValRat_two : padicValRat 2 (2 : ℚ) = 1 := by + exact_mod_cast padicValRat.self (p := 2) one_lt_two + +/-- **The kernel itself is not `2`-integral**: its leading coefficient `-1/2` has a `2` in the +denominator. -/ +example : cauchyKernel 2 1 ∉ lifts (Rat.padicValuation 2).integer.subtype := by + rw [lifts_iff_coeff_lifts] + intro h + obtain ⟨c, hc⟩ := h 3 + have hle := c.2 + rw [Valuation.mem_integer_iff] at hle + change Rat.padicValuation 2 (c : ℚ) ≤ 1 at hle + have hv : Rat.padicValuation 2 (-1 / 2 : ℚ) = WithZero.exp 1 := by + rw [neg_div, Valuation.map_neg] + simp [Rat.padicValuation, padicValRat_two] + rw [show (c : ℚ) = -1 / 2 by rw [← coeff_cauchyKernel_two_one]; exact hc, hv, + ← WithZero.exp_zero, WithZero.exp_le_exp] at hle + exact absurd hle (by norm_num) + +/-- **In the local coordinate `T = 1 + 4 z` it is `2`-integral** (Lemma D.4, with `a = 1`). -/ +example : + (cauchyKernel 2 1).comp (C 1 + C 4 * X) ∈ lifts (Rat.padicValuation 2).integer.subtype := by + have h := cauchyKernel_comp_mem_lifts (a := 1) (t := 1) (d := 1) (by decide) (by decide) + norm_num at h + exact h + +/-- Away from its own node the kernel in local coordinates is divisible by `2`. -/ +example : ∃ P ∈ lifts (Rat.padicValuation 2).integer.subtype, + (cauchyKernel 2 0).comp (C 1 + C 4 * X) = C 2 * P := by + have h := exists_cauchyKernel_comp_eq_two_mul (a := 1) (t := 1) (d := 0) (by decide) + (by decide) (by decide) + norm_num at h + exact h + +/-! ### Reduction modulo `2 ^ p` -/ + +/-- `1 / 3 ≡ 3 (mod 8)`, since `3 * 3 = 9 ≡ 1`. -/ +example (h : Rat.padicValuation 2 ((3 : ℚ)⁻¹) ≤ 1) : + Rat.padicIntegerToZModPow 2 3 ⟨(3 : ℚ)⁻¹, h⟩ = 3 := by + have h3 := Rat.padicIntegerToZModPow_mul_den 2 3 ⟨(3 : ℚ)⁻¹, h⟩ + have hden : ((3 : ℚ)⁻¹).den = 3 := by simp + have hnum : ((3 : ℚ)⁻¹).num = 1 := by simp + simp only [hden, hnum, Nat.cast_ofNat, Int.cast_one] at h3 + have h9 : (3 * 3 : ZMod (2 ^ 3)) = 1 := by decide + calc Rat.padicIntegerToZModPow 2 3 ⟨(3 : ℚ)⁻¹, h⟩ + = Rat.padicIntegerToZModPow 2 3 ⟨(3 : ℚ)⁻¹, h⟩ * (3 * 3) := by rw [h9, mul_one] + _ = 3 := by rw [← mul_assoc, h3, one_mul] + +/-! ### The deformed contraction -/ + +/-- A row vertex `0` and a column vertex `1` joined by one edge, with integer tensors. -/ +def oneEdge : TensorNetwork ℚ Bool (Fin 2) (Fin 1) where + src _ := 0 + tgt _ := 1 + tensor v x := if v = 0 then (if x 0 then 2 else 1) else (if x 0 then 5 else 3) + tensor_congr v x y h := by rw [h 0 (by fin_cases v <;> simp)] + +/-- With one slot (`a = 0`, `α = 2`), `F(-1 + 2 z)` has `2`-integral coefficients. -/ +example : + ((oneEdge.map Polynomial.C).deformedContraction (fun v => v = 0) + ((cauchyMatrix (2 ^ 0) (fun _ : Fin 1 => ()) (fun _ => 0)).map + (Polynomial.mapRingHom (algebraMap ℚ ℚ)))).comp + (C ((-1 : ℤ) : ℚ) + C (2 ^ (0 + 1)) * X) ∈ + liftsRing (Rat.padicValuation 2).integer.subtype := + TensorNetwork.deformedContraction_cauchyMatrix_comp_mem_liftsRing _ _ (fun _ => by norm_num) + (by decide) _ (fun c hc => hc) fun v x => by + simp only [oneEdge] + split_ifs <;> exact (Rat.padicValuation_le_one_iff.mpr (by decide)) + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates