diff --git a/Complexity.lean b/Complexity.lean index aac9106db..387ad2294 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -913,6 +913,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ActiveCall public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.CauchyModes public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildCursor +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildEntries public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildNumbering public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildSize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.CoeffScheme @@ -930,11 +931,13 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketEntr public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketEvaluator public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketTerms public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Recursion +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ReductionLift public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Reindex public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduleCount public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduledRecursion public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TaperedRecovery +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.VertexDesc public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional public import Complexity.Computability.Circuit.Frontier.Witness diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildEntries.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildEntries.lean new file mode 100644 index 000000000..bb3b4b2d1 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildEntries.lean @@ -0,0 +1,308 @@ +/- +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.VertexDesc +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedContraction +import Mathlib.Data.List.GetD + +/-! +# The entries of the child networks from their descriptors + +A child network of the contraction recursion of [OpenAI2026ETH] (`ModeSplitting.child`, §D.4.6, +p. 63) is carried natively as a network of vertex descriptors (`VertexDesc`) with port lists. This +file proves that such a network has the contraction of the child, once each descriptor reads its +ports in the right order. + +* **Port lists** (`DescribedNetwork.contraction_eq_of_ports`). Number the vertices and the edges of + a Boolean tensor network `N`, and give each vertex any list of edges as its ports and a + descriptor. If the evaluator at the descriptor of `v`, read at the bits of an assignment on its + ports, is the tensor of `v` at that assignment, the described network has the contraction of + `N`. +* **Retained vertices** (`ModeSplitting.child_tensor_inl_eq_tensor`). A vertex of group `g` keeps + its tensor in the child of group `g`: a row reads its row ports and a column its column ports. + So a retained vertex keeps its descriptor, and its ports are its parent ports, in the same + order, renumbered as child edges. +* **Packet vertices** (`TensorNetwork.map_val_entry_child_inr`). Let the ports of the packet + vertex `q` be the child edges of packet `q` in any order without repetition, and let its + descriptor tag each port with whether it is a row port and with its slot, in the same order. Then + along any ring map from `A_p` to the coefficient ring of the child, the descriptor's entry at the + bits on its ports is the child's entry (`child_tensor_inr_cauchyModeSplitting`), for the + packet's context matching the node `(t, ζ)`, the group `g`, the symbols of `q` and the exponents + `β`. The tags are computed from the port list itself, so tags and bits align by construction + (`NativePacket.sidePorts_map`). + +## Main results + +* `Cslib.Circuits.Frontier.DescribedNetwork.contraction_eq_of_ports`: a described network with + port lists has the contraction of the network it describes. +* `Cslib.Circuits.Frontier.NativePacket.sidePorts_map`: the ports of one side of a tagged list. +* `Cslib.Circuits.Frontier.TensorNetwork.ModeSplitting.child_tensor_inl_eq_tensor`: the entries + of the retained vertices of a child. +* `Cslib.Circuits.Frontier.TensorNetwork.map_val_entry_child_inr`: the entries of the packet + vertices of a Cauchy child, from their descriptors. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.6, p. 63. +-/ + +public section + +namespace Cslib.Circuits.Frontier + +/-- The subring `ℤ_(2)` of rationals with odd denominator. -/ +local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2) + +open Finset GaloisRingArith NativePacket + +/-! ### Port lists -/ + +namespace DescribedNetwork + +variable {T : Type} {R : Type*} [CommSemiring R] {V E : Type*} [Fintype V] [Fintype E] + [DecidableEq E] + +/-- **A described network with port lists has the contraction of the network it describes.** +Number the vertices of `N` by `ev` and its edges by `ee`, and give each vertex `v` a list of edges +`ports v` and a descriptor `desc v`. If the evaluator at `desc v`, read at the bits of every +assignment on `ports v`, is the tensor of `v` at that assignment, the described network with the +numbered ports and the descriptors has the contraction of `N`. -/ +theorem contraction_eq_of_ports {k l : ℕ} (N : TensorNetwork R Bool V E) (ev : V ≃ Fin k) + (ee : E ≃ Fin l) (ports : V → List E) (desc : V → T) (eval : T → List Bool → R) + (h : ∀ v (x : E → Bool), eval (desc v) ((ports v).map x) = N.tensor v x) : + (⟨l, List.ofFn fun i => ((ports (ev.symm i)).map fun e => (ee e : ℕ), desc (ev.symm i))⟩ : + DescribedNetwork T).contraction eval = N.contraction := by + simp only [contraction, TensorNetwork.contraction, List.map_ofFn, List.prod_ofFn] + rw [← (ee.arrowCongr (Equiv.refl Bool)).symm.sum_comp] + refine sum_congr rfl fun x _ => ?_ + rw [← ev.symm.prod_comp] + refine prod_congr rfl fun v _ => ?_ + simp only [Function.comp_apply] + rw [← h] + congr 1 + simp only [wordBits, List.map_map] + refine List.map_congr_left fun e _ => ?_ + simp only [Function.comp_apply, Equiv.arrowCongr_symm, Equiv.arrowCongr_apply, + Equiv.symm_symm, Equiv.refl_symm, Equiv.coe_refl, id_eq] + rw [List.getD_eq_getElem _ _ (by simp), List.getElem_ofFn] + +end DescribedNetwork + +/-! ### The ports of one side of a tagged list -/ + +namespace NativePacket + +/-- **The ports of one side of a tagged list.** If the ports of a vertex are tagged, in their +order, by whether they are row ports and by their slots, and the bits are read in the same order, +the ports of one side are the ports with that tag, with their slots and bits, in order. -/ +theorem sidePorts_map {α : Type*} (cs : List α) (tag : α → Bool) (sl : α → ℕ) (y : α → Bool) + (side : Bool) : + sidePorts (cs.map fun c => (tag c, sl c)) (cs.map y) side = + (cs.filter fun c => tag c == side).map fun c => (sl c, y c) := by + induction cs with + | nil => rfl + | cons c cs ih => + simp only [sidePorts, List.length_map] at ih + simp only [sidePorts, List.map_cons, List.length_cons, List.length_map, + List.range_succ_eq_map, List.filter_cons, List.filter_map, List.getD_cons_zero, + Function.comp_def, List.getD_cons_succ] + by_cases hc : tag c == side + · rw [ite_eq_left hc, ite_eq_left hc] + simp only [List.map_cons, List.map_map] + rw [← ih] + rfl + · rw [ite_eq_right hc, ite_eq_right hc] + simp only [List.map_map] + rw [← ih] + rfl + +end NativePacket + +namespace TensorNetwork + +/-! ### Retained vertices -/ + +namespace ModeSplitting + +variable {R V E G P M : Type*} [CommRing R] [Fintype M] [DecidableEq V] [Fintype E] + [DecidableEq E] [DecidableEq P] [DecidableEq G] [DecidableEq M] {N : TensorNetwork R Bool V E} + {W : Matrix E E R} (S : ModeSplitting N W G P M) + +/-- **The retained vertices of a child**: a vertex of group `g` keeps its tensor in the child of +group `g`, reading at each of its edges the child edge of that edge: a row its row ports and a +column its column ports. -/ +theorem child_tensor_inl_eq_tensor (β : M → ℕ) (g : G) (v : {v // S.group v = g}) + (y : {e // S.group (N.src e) = g} ⊕ {e // S.group (N.tgt e) = g} → Bool) : + (S.child β g).tensor (.inl v) y = N.tensor v.1 fun e => + if S.side v.1 then (if h : S.group (N.src e) = g then y (.inl ⟨e, h⟩) else false) + else (if h : S.group (N.tgt e) = g then y (.inr ⟨e, h⟩) else false) := by + simp only [child] + by_cases hv : S.side v.1 + · rw [ite_eq_left hv] + refine N.tensor_congr _ _ _ fun e he => ?_ + simp only [ite_eq_left hv] + by_cases hs : N.src e = v.1 + · rw [dite_eq_left hs, dite_eq_left (hs ▸ v.2)] + · have ht : N.tgt e = v.1 := he.resolve_left hs + have := S.side_tgt e + rw [ht, hv] at this + exact absurd this (by decide) + · rw [ite_eq_right hv] + refine N.tensor_congr _ _ _ fun e he => ?_ + simp only [ite_eq_right hv] + by_cases ht : N.tgt e = v.1 + · rw [dite_eq_left ht, dite_eq_left (ht ▸ v.2)] + · have hs : N.src e = v.1 := he.resolve_right ht + have := S.side_src e + rw [hs] at this + exact absurd this hv + +end ModeSplitting + +/-! ### Packet vertices -/ + +section Ports + +variable {R V E G : Type*} [DecidableEq G] {N : TensorNetwork R Bool V E} {group : V → G} + {slot : E → ℕ} + +/-- The row ports of a list of child edges, with their slots and bits. -/ +private theorem filter_isLeft_map {g : G} + (cs : List ({e // group (N.src e) = g} ⊕ {e // group (N.tgt e) = g})) + (y : {e // group (N.src e) = g} ⊕ {e // group (N.tgt e) = g} → Bool) : + (cs.filter fun c => c.isLeft == true).map + (fun c => (slot (Sum.elim Subtype.val Subtype.val c), y c)) = + ((cs.filterMap Sum.getLeft?).map Subtype.val).map fun e => + (slot e, if h : group (N.src e) = g then y (.inl ⟨e, h⟩) else false) := by + induction cs with + | nil => rfl + | cons c cs ih => + rcases c with c | c + · rw [List.filter_cons_of_pos rfl, List.filterMap_cons_some (f := Sum.getLeft?) rfl, + List.map_cons, List.map_cons, List.map_cons, ih, dite_eq_left c.2] + rfl + · rw [List.filter_cons_of_neg (by simp), List.filterMap_cons_none (f := Sum.getLeft?) rfl, ih] + +/-- The column ports of a list of child edges, with their slots and bits. -/ +private theorem filter_isLeft_false_map {g : G} + (cs : List ({e // group (N.src e) = g} ⊕ {e // group (N.tgt e) = g})) + (y : {e // group (N.src e) = g} ⊕ {e // group (N.tgt e) = g} → Bool) : + (cs.filter fun c => c.isLeft == false).map + (fun c => (slot (Sum.elim Subtype.val Subtype.val c), y c)) = + ((cs.filterMap Sum.getRight?).map Subtype.val).map fun e => + (slot e, if h : group (N.tgt e) = g then y (.inr ⟨e, h⟩) else false) := by + induction cs with + | nil => rfl + | cons c cs ih => + rcases c with c | c + · rw [List.filter_cons_of_neg (by simp), List.filterMap_cons_none (f := Sum.getRight?) rfl, + ih] + · rw [List.filter_cons_of_pos rfl, List.filterMap_cons_some (f := Sum.getRight?) rfl, + List.map_cons, List.map_cons, List.map_cons, ih, dite_eq_left c.2] + rfl + +end Ports + +section Cauchy + +variable {R V E G P : Type*} [CommRing R] [Fintype E] [DecidableEq E] [Fintype P] [DecidableEq G] + [DecidableEq P] {N : TensorNetwork R Bool V E} {group : V → G} {packet : E → P} {slot : E → ℕ} + {sym : P → G × G} {i : ℕ} + (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) + (htgt : ∀ e, side (N.tgt e) = false) + (horient : ∀ e, (group (N.src e), group (N.tgt e)) = + if (slot e).testBit i then (sym (packet e)).swap else sym (packet e)) + {a : ℕ} (hslot : ∀ e, slot e < 2 ^ a) (hia : i < a) (κ : ℤ₍₂₎ →+* R) (ζ : R) {p : ℕ} + (hp : (2 : R) ^ p = 0) {t : ℤ} (ht : t ∈ cauchyGrid (2 ^ a)) (hti : (2 : ℤ) ^ i ∣ t) + (hti' : ¬ (2 : ℤ) ^ (i + 1) ∣ t) + +/-- **The packet vertices of a Cauchy child, from their descriptors.** Let the ports of the +packet vertex `q` in the child of group `g` be the child edges of packet `q`, listed without +repetition in any order, and let the descriptor's ports tag each of them, in the same order, with +whether it is a row port and with its slot. Let the packet's context have the node `t` of +valuation `i < a`, `L = 2 ^ a` slots, `2 ^ (i + 1)` tiles and `p` exponents per tile, the symbols +of `q` against `g`, an interpolation value mapping to `ζ`, and the dense exponents of `β` at `q`. +Then along a ring map `ψ` from `A_p`, at the packet's precision, to `R`, the descriptor's entry at +the bits on its ports is the child's entry. -/ +theorem map_val_entry_child_inr [DecidableEq V] (β : P × Fin (2 ^ (i + 1)) × Fin p → ℕ) (g : G) + (q : P) + (cs : List ({e // (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti + hti').group (N.src e) = g} ⊕ + {e // (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').group + (N.tgt e) = g})) + (hcs : cs.Nodup) (hcs' : ∀ c, c ∈ cs ↔ packet (Sum.elim Subtype.val Subtype.val c) = q) + (c : PacketCtx) (βd : List ℕ) (ψ : Ring c.p c.fl →+* R) (hζ : ψ (val c.p c.fl c.ζ) = ζ) + (ha : c.a = a) (hL : c.L = 2 ^ a) (hi : c.i = i) (htiles : c.tiles = 2 ^ (i + 1)) + (ht' : c.t = t) (hnb : c.nb = p) (he₁ : c.e₁ = decide ((sym q).1 = g)) + (he₂ : c.e₂ = decide ((sym q).2 = g)) (hdiffer : c.differ = decide ((sym q).1 ≠ (sym q).2)) + (hβ : ∀ Z : Fin (2 ^ (i + 1)) × Fin p, βd.getD (finProdFinEquiv Z) 0 = β (q, Z)) + (y : {e // (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').group + (N.src e) = g} ⊕ + {e // (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').group + (N.tgt e) = g} → Bool) : + ψ (val c.p c.fl (VertexDesc.entry + (.inr (c, cs.map fun e => (e.isLeft, slot (Sum.elim Subtype.val Subtype.val e)), βd)) + (cs.map y))) = + ((cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').child β g).tensor + (.inr q) y := by + subst ha hi ht' hnb + have hports : ∀ x ∈ cs.map (fun e => (e.isLeft, slot (Sum.elim Subtype.val Subtype.val e))), + x.2 < 2 ^ c.a := by + intro x hx + obtain ⟨e, -, rfl⟩ := List.mem_map.mp hx + exact hslot _ + have key := VertexDesc.map_val_entry_inr (c, cs.map fun e => (e.isLeft, + slot (Sum.elim Subtype.val Subtype.val e)), βd) (cs.map y) ψ hp κ hL hia htiles ht hti hti' + hports + have hgoal : ψ (val c.p c.fl (VertexDesc.entry (.inr (c, cs.map fun e => (e.isLeft, + slot (Sum.elim Subtype.val Subtype.val e)), βd)) (cs.map y))) = _ := key + rw [hgoal] + dsimp only + have hrows : ((cs.filterMap Sum.getLeft?).map Subtype.val).Nodup := + ((hcs.filterMap fun _ _ _ h₁ h₂ => by + rw [Option.mem_def, Sum.getLeft?_eq_some_iff] at h₁ h₂; rw [h₁, h₂])).map + Subtype.val_injective + have hcols : ((cs.filterMap Sum.getRight?).map Subtype.val).Nodup := + ((hcs.filterMap fun _ _ _ h₁ h₂ => by + rw [Option.mem_def, Sum.getRight?_eq_some_iff] at h₁ h₂; rw [h₁, h₂])).map + Subtype.val_injective + have hrows' : ∀ e, e ∈ (cs.filterMap Sum.getLeft?).map Subtype.val ↔ + packet e = q ∧ group (N.src e) = g := by + intro e + simp only [List.mem_map, List.mem_filterMap, Sum.getLeft?_eq_some_iff] + constructor + · rintro ⟨e', ⟨c, hc, rfl⟩, rfl⟩ + exact ⟨(hcs' _).1 hc, by simpa using e'.2⟩ + · rintro ⟨hq, hg⟩ + have hg' : (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').group + (N.src e) = g := by simpa using hg + exact ⟨⟨e, hg'⟩, ⟨_, (hcs' (.inl ⟨e, hg'⟩)).2 hq, rfl⟩, rfl⟩ + have hcols' : ∀ e, e ∈ (cs.filterMap Sum.getRight?).map Subtype.val ↔ + packet e = q ∧ group (N.tgt e) = g := by + intro e + simp only [List.mem_map, List.mem_filterMap, Sum.getRight?_eq_some_iff] + constructor + · rintro ⟨e', ⟨c, hc, rfl⟩, rfl⟩ + exact ⟨(hcs' _).1 hc, by simpa using e'.2⟩ + · rintro ⟨hq, hg⟩ + have hg' : (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').group + (N.tgt e) = g := by simpa using hg + exact ⟨⟨e, hg'⟩, ⟨_, (hcs' (.inr ⟨e, hg'⟩)).2 hq, rfl⟩, rfl⟩ + rw [child_tensor_inr_cauchyModeSplitting side hsrc htgt horient hslot hia κ _ hp ht hti hti' β + g q y hrows hrows' hcols hcols', sidePorts_map, sidePorts_map, filter_isLeft_map, + filter_isLeft_false_map, hζ, he₁, he₂, hdiffer] + congr 1 + funext Z + exact hβ Z + +end Cauchy + +end TensorNetwork + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ReductionLift.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ReductionLift.lean new file mode 100644 index 000000000..423643c61 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ReductionLift.lean @@ -0,0 +1,121 @@ +/- +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.PacketEvaluator +public import Complexity.Foundations.NumberTheory.Padics.AdjoinRootReduction +import Mathlib.Data.ZMod.QuotientRing + +/-! +# The Galois ring maps into `O / 2 ^ n` + +The contraction recursion of [OpenAI2026ETH] reasons over `O = ℤ_(2)[U] / (f)` and its quotients +`O / (2 ^ n)` (the children of a call live over `O / (2 ^ {p_t})`, `TensorNetwork.callSplitting`), +while the native algorithm computes in `A_n = (ℤ / 2 ^ n)[U] / (f)`, the Galois ring +`GaloisRing 2 n f`. Reduction `O → A_n` (`AdjoinRoot.reduction`) factors through `O / (2 ^ n)`; +this file gives the map back, `reductionLift : A_n → O / (2 ^ n)`, with +`reductionLift ∘ reduction = mk` (`reductionLift_comp_reduction`). It sends `U` to the +class of `U` and is the unique ring map from `ℤ / 2 ^ n` on scalars. So a value computed natively +in `A_n` and mapped along `reductionLift` is the class of any element of `O` reducing to it: the +canonical lift of a coefficient list (`reductionLift_reduction`). + +## Main definitions + +* `Cslib.Circuits.Frontier.reductionLift`: the map `A_n → O / (2 ^ n)`. + +## Main results + +* `Cslib.Circuits.Frontier.reductionLift_comp_reduction`: `reductionLift ∘ reduction = mk`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.1, p. 57. +-/ + +public section + +open Polynomial AdjoinRoot + +namespace Cslib.Circuits.Frontier + +variable {f : ℤ[X]} (hf : f.Monic) (hirr : Irreducible (f.map (Int.castRingHom (ZMod 2)))) + (n : ℕ) + +/-- `2 ^ n = 0` in `O / (2 ^ n)`. -/ +private theorem two_pow_eq_zero_quotient : (2 : ((padicValuation 2 hf hirr).integer ⧸ + Ideal.span {(2 : (padicValuation 2 hf hirr).integer) ^ n})) ^ n = 0 := by + have : Ideal.Quotient.mk (Ideal.span {(2 : (padicValuation 2 hf hirr).integer) ^ n}) + ((2 : (padicValuation 2 hf hirr).integer) ^ n) = 0 := + Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self _) + rwa [map_pow, map_ofNat] at this + +/-- The scalars `ℤ / 2 ^ n → O / (2 ^ n)`. -/ +private noncomputable def scalarLift : ZMod (2 ^ n) →+* ((padicValuation 2 hf hirr).integer ⧸ + Ideal.span {(2 : (padicValuation 2 hf hirr).integer) ^ n}) := + (Ideal.Quotient.lift _ (Int.castRingHom _) fun a ha => by + obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton.mp ha + rw [map_mul, eq_intCast, Int.cast_natCast, Nat.cast_pow, Nat.cast_ofNat, + two_pow_eq_zero_quotient hf hirr n, zero_mul]).comp + (Int.quotientSpanNatEquivZMod (2 ^ n)).symm.toRingHom + +/-- The class of `U` in `O / (2 ^ n)`. -/ +private noncomputable def rootClass : ((padicValuation 2 hf hirr).integer ⧸ + Ideal.span {(2 : (padicValuation 2 hf hirr).integer) ^ n}) := + Ideal.Quotient.mk _ (integerEquiv hf hirr (root _)) + +private theorem eval₂_rootClass : + (f.map (Int.castRingHom (ZMod (2 ^ n)))).eval₂ (scalarLift hf hirr n) (rootClass hf hirr n) = + 0 := by + rw [eval₂_map] + have hcomp : (scalarLift hf hirr n).comp (Int.castRingHom (ZMod (2 ^ n))) = + ((Ideal.Quotient.mk _).comp (integerEquiv hf hirr).toRingHom).comp + ((of _).comp (Int.castRingHom (Rat.padicValuation 2).integer)) := + RingHom.ext_int _ _ + rw [hcomp, rootClass, show Ideal.Quotient.mk _ (integerEquiv hf hirr (root _)) = + ((Ideal.Quotient.mk _).comp (integerEquiv hf hirr).toRingHom) (root _) from rfl, + ← Polynomial.hom_eval₂, ← eval₂_map, eval₂_root, map_zero] + +/-- **The Galois ring maps into `O / (2 ^ n)`**: `ℤ / 2 ^ n` by its unique ring map, and `U` to +its class. -/ +noncomputable def reductionLift : GaloisRing 2 n f →+* ((padicValuation 2 hf hirr).integer ⧸ + Ideal.span {(2 : (padicValuation 2 hf hirr).integer) ^ n}) := + lift (scalarLift hf hirr n) (rootClass hf hirr n) (eval₂_rootClass hf hirr n) + +/-- **`reductionLift` undoes reduction modulo `2 ^ n`**: reducing an element of `O` to `A_n` and +mapping back gives its class in `O / (2 ^ n)`. -/ +theorem reductionLift_comp_reduction : + (reductionLift hf hirr n).comp (reduction hf hirr n) = Ideal.Quotient.mk _ := by + -- `U` of `O` is the class of `U` of `ℤ[X] / (f)`. + have hroot : integerEquiv hf hirr (root _) = ⟨map (Int.castRingHom ℚ) f _ dvd_rfl (root f), + (Valuation.mem_integer_iff _ _).mpr (padicValuation_map_le_one hf hirr _)⟩ := by + apply Subtype.ext + change (integerEquiv hf hirr (root _) : AdjoinRoot (f.map (Int.castRingHom ℚ))) = + map (Int.castRingHom ℚ) f _ dvd_rfl (root f) + rw [map_root, coe_integerEquiv] + conv_lhs => rw [← mk_X] + rw [integerMap_mk, Polynomial.map_X, mk_X] + have key : (reductionLift hf hirr n).comp (integerReduction 2 f n) = + (Ideal.Quotient.mk _).comp (integerEquiv hf hirr).toRingHom := by + refine ringHom_ext ?_ ?_ + · exact padicInteger_ringHom_ext + (two_pow_eq_zero_quotient hf hirr n) _ _ + · rw [RingHom.comp_apply, ← reduction_integerEquiv hf hirr, hroot, reduction_toRat hf hirr, + map_root, + reductionLift, lift_root, rootClass] + rfl + ext x + obtain ⟨y, rfl⟩ := (integerEquiv hf hirr).surjective x + rw [RingHom.comp_apply, reduction_integerEquiv, ← RingHom.comp_apply, key] + rfl + +/-- `reductionLift (reduction x)` is the class of `x`. -/ +theorem reductionLift_reduction (x : (padicValuation 2 hf hirr).integer) : + reductionLift hf hirr n (reduction hf hirr n x) = Ideal.Quotient.mk _ x := + RingHom.congr_fun (reductionLift_comp_reduction hf hirr n) x + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/VertexDesc.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/VertexDesc.lean new file mode 100644 index 000000000..3fff52005 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/VertexDesc.lean @@ -0,0 +1,344 @@ +/- +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.PacketTerms +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Sum +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Sum +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeOptionPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListBinaryLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Foundations.Data.BitString.Binary +import Mathlib.Data.List.GetD + +/-! +# Descriptors of the vertices of the recursion's networks + +The networks of the contraction recursion of [OpenAI2026ETH] (§D.4.6–§D.4.7, pp. 63–64) have two +kinds of vertices. The vertices of the input network keep their tables, and they survive into +every child of their group with the same ports. The packet vertices created at a call are +described by "its packet data, the tuple `β`, the interpolation value, and the creation +precision" (p. 63), and from then on they also survive into the children of their group. A +vertex descriptor (`VertexDesc`) is therefore a table or a packet descriptor +(`NativePacket.PacketDesc`), and a retained vertex keeps its descriptor. + +`VertexDesc.entry` evaluates a descriptor at the bits on its ports: the table entry, as a constant +coefficient list, or the native packet entry at the packet's creation precision. A network of the +recursion reads the entries at its own precision `(p, fl)` (`GaloisRingArith.val p fl`), so a +retained packet vertex created at a lower precision is read at the higher one: its coefficients +are those of the same element of `O = ℤ_(2)[U] / (f)`. One native machine evaluates every +descriptor (`VertexDesc.entryCertificate`), with the packet evaluator's bounds: time +`K (m + 2) ^ L Z ^ K` and space `K Z ^ K`, for `m` target modes and `L` row ports of a packet (none +for a table) and `Z` polynomial in the input and the reduced coefficient lists +(`VertexDesc.entryCertificate_le`). It is the evaluator of direct summation over networks of +descriptors at coefficient lists (`DescribedNetwork.contractionCertificate` at `SumOps.galois`). + +## Main definitions + +* `Cslib.Circuits.Frontier.VertexDesc`: a table or a packet descriptor. +* `Cslib.Circuits.Frontier.VertexDesc.entry`: its entry at the bits on its ports. +* `Cslib.Circuits.Frontier.VertexDesc.enc`: its encoding. +* `Cslib.Circuits.Frontier.VertexDesc.entryCertificate`: the native evaluator. + +## Main results + +* `Cslib.Circuits.Frontier.VertexDesc.val_entry_inl`: a table entry is read as a constant. +* `Cslib.Circuits.Frontier.VertexDesc.map_val_entry_inr`: a packet entry is the packet entry in + every ring receiving `A_p` with `2` nilpotent. +* `Cslib.Circuits.Frontier.VertexDesc.entryCertificate_le`: the time and space of the evaluator. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.6–§D.4.7, pp. 63–64. +-/ + +public section + +namespace Cslib.Circuits.Frontier + +/-- The subring `ℤ_(2)` of rationals with odd denominator. -/ +local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2) + +open GaloisRingArith NativePacket TensorNetwork Turing.MultiTapeTM Cslib.GenericRAM + +/-- **The descriptor of a vertex** of a network of the contraction recursion: the table of a +vertex of the input network (`inl`), or the descriptor of a packet vertex (`inr`). -/ +abbrev VertexDesc : Type := List ℕ ⊕ PacketDesc + +namespace VertexDesc + +/-- **The entry of a vertex at the bits on its ports**: the table entry, as a constant coefficient +list, or the native packet entry at the packet's creation precision. -/ +@[expose] def entry : VertexDesc → List Bool → List ℕ + | .inl table, bs => [ExplicitTensorNetwork.entry table bs] + | .inr d, bs => packetVertexEntry d bs + +/-- The encoding of a descriptor: a tag, then the table in binary or the packet descriptor. -/ +abbrev enc : VertexDesc ↪ List Bool := encSum (encList encNat) encPacketDesc + +/-- The number of target modes of a descriptor: those of its packet, and none for a table. -/ +@[expose] def modes : VertexDesc → ℕ + | .inl _ => 0 + | .inr d => (targetModes d.1).length + +/-- The number of row ports of a descriptor at the bits on its ports: those of its packet, and +none for a table. -/ +@[expose] def rowPorts : VertexDesc → List Bool → ℕ + | .inl _, _ => 0 + | .inr d, bs => (sidePorts d.2.1 bs true).length + +/-- The reduced coefficient lists of the creation precision of a descriptor are at most `Rv` bits +long; no condition for a table. -/ +@[expose] def ReducedLE (Rv : ℕ) : VertexDesc → Prop + | .inl _ => True + | .inr d => ∀ y, SumOps.galois.Reduced (d.1.p, d.1.fl) y → (encList encNat y).length ≤ Rv + +/-! ### Values -/ + +@[simp] theorem entry_inl (table : List ℕ) (bs : List Bool) : + entry (.inl table) bs = [ExplicitTensorNetwork.entry table bs] := rfl + +@[simp] theorem entry_inr (d : PacketDesc) (bs : List Bool) : + entry (.inr d) bs = packetVertexEntry d bs := rfl + +/-- **A table entry is read as a constant** at every precision. -/ +theorem val_entry_inl (p : ℕ) (fl table : List ℕ) (bs : List Bool) : + val p fl (entry (.inl table) bs) = + ((ExplicitTensorNetwork.entry table bs : ℕ) : Ring p fl) := by + obtain h | ⟨e, he⟩ : fl.length = 0 ∨ ∃ e, fl.length = e + 1 := + (Nat.eq_zero_or_pos _).imp id fun h => ⟨_, (Nat.succ_pred_eq_of_pos h).symm⟩ + · have := subsingleton_of_length_eq_zero (p := p) h + exact Subsingleton.elim _ _ + · rw [entry_inl, val, he, Finset.sum_range_succ', + Finset.sum_eq_zero fun i _ => by rw [List.getD_cons_succ, List.getD_nil]; simp] + simp + +/-- **A packet entry in every ring receiving `A_p`.** Along a ring map `ψ` from `A_p`, at the +precision `p` of the packet, to a ring in which `2` is nilpotent, the entry of a packet descriptor +at the bits on its ports is `packetEntry` at any ring map `κ : ℤ_(2) → S`, the image of the +interpolation value, the dense exponents, and the row and column ports read from the bits. -/ +theorem map_val_entry_inr {S : Type*} [CommRing S] (d : PacketDesc) (bs : List Bool) + (ψ : Ring d.1.p d.1.fl →+* S) {n : ℕ} (hn : (2 : S) ^ n = 0) (κ : ℤ₍₂₎ →+* S) + (hL : d.1.L = 2 ^ d.1.a) (hia : d.1.i < d.1.a) (htiles : d.1.tiles = 2 ^ (d.1.i + 1)) + (ht : d.1.t ∈ cauchyGrid (2 ^ d.1.a)) (hti : (2 : ℤ) ^ d.1.i ∣ d.1.t) + (hti' : ¬ (2 : ℤ) ^ (d.1.i + 1) ∣ d.1.t) (hports : ∀ x ∈ d.2.1, x.2 < 2 ^ d.1.a) : + ψ (val d.1.p d.1.fl (entry (.inr d) bs)) = + packetEntry (p := d.1.nb) κ (ψ (val d.1.p d.1.fl d.1.ζ)) d.1.a d.1.i d.1.t d.1.e₁ d.1.e₂ + d.1.differ (fun Z => d.2.2.getD (finProdFinEquiv Z) 0) (sidePorts d.2.1 bs true) + (sidePorts d.2.1 bs false) := by + have hside (side : Bool) : ∀ r ∈ sidePorts d.2.1 bs side, r.1 < 2 ^ d.1.a := by + intro r hr + obtain ⟨j, hj, rfl⟩ := List.mem_map.mp hr + have hj' := List.mem_range.mp (List.mem_filter.mp hj).1 + exact hports _ (by rw [List.getD_eq_getElem _ _ hj']; exact List.getElem_mem _) + exact map_val_packetEntryNative { d.1 with cols := sidePorts d.2.1 bs false } ψ hn κ hL hia + htiles ht hti hti' (hside true) (hside false) d.2.2 + +/-- A packet entry is a reduced coefficient list at the packet's precision. -/ +theorem reduced_entry_inr (d : PacketDesc) (bs : List Bool) : + SumOps.galois.Reduced (d.1.p, d.1.fl) (entry (.inr d) bs) := + SumOps.galois.reduced_mul (d.1.p, d.1.fl) _ _ + +/-! ### The native evaluator -/ + +/-- The right summand of a descriptor and its bits. -/ +theorem getRight_polyTime : + ComputableInPolyTime (fun q : VertexDesc × List Bool => q.1.getRight?) (encPair enc encBits) + (encOption encPacketDesc) := + (ComputableInO.getRight?_deg _ _).computableInPolyTime.comp (ComputableInPolyTime.fst _ _) + +/-- The table entry of a descriptor at its bits, the empty table standing for a packet, as a +singleton list. -/ +theorem tableEntry_polyTime : + ComputableInPolyTime (fun q : VertexDesc × List Bool => + [ExplicitTensorNetwork.entry (q.1.getLeft?.getD []) q.2]) (encPair enc encBits) + (encList encNat) := by + have hleft : ComputableInPolyTime (fun q : VertexDesc × List Bool => q.1.getLeft?) + (encPair enc encBits) (encOption (encList encNat)) := + (ComputableInO.getLeft?_deg _ _).computableInPolyTime.comp (ComputableInPolyTime.fst _ _) + have htable : ComputableInPolyTime (fun q : VertexDesc × List Bool => q.1.getLeft?.getD []) + (encPair enc encBits) (encList encNat) := + (ComputableInDegree.getD (enc₁ := encList encNat) (enc := encOption (encList encNat)) + []).computableInPolyTime.comp hleft + have hindex := ComputableInPolyTime.bitsBinaryValue.comp + (ComputableInPolyTime.bitsReverse.comp (ComputableInPolyTime.snd enc encBits)) + have hentry := ComputableInPolyTime.listGetD_binary (encA := encNat) (encL := encList encNat) 0 + htable hindex + exact (ComputableInPolyTime.cons' hentry (ComputableInPolyTime.const [])).of_enc_eq fun q => by + simp only [ExplicitTensorNetwork.entry, BitString.lsbValue_eq_binaryValue_reverse, + Function.comp_apply] + +/-- The input of the packet evaluator from a descriptor's bits and its packet. -/ +theorem packetInput_polyTime : + ComputableInPolyTime (fun p : (VertexDesc × List Bool) × PacketDesc => (p.2, p.1.2)) + (encPair (encPair enc encBits) encPacketDesc) (encPair encPacketDesc encBits) := + (ComputableInPolyTime.snd _ _).prod + ((ComputableInPolyTime.snd enc encBits).comp (ComputableInPolyTime.fst _ _)) + +/-- **One native machine for the entries of all descriptors**: the table lookup for a table, and +the native packet evaluator (`NativePacket.vertexCertificate`) for a packet. -/ +noncomputable def entryCertificate : + NativeCertificate (fun q : VertexDesc × List Bool => entry q.1 q.2) (encPair enc encBits) + (encList encNat) := + (NativeCertificate.option (value := fun q : VertexDesc × List Bool => q.1.getRight?) + (fallback := fun q => [ExplicitTensorNetwork.entry (q.1.getLeft?.getD []) q.2]) + (body := fun p => packetVertexEntry p.2 p.1.2) + (NativeCertificate.ofPolyTime getRight_polyTime) + (NativeCertificate.ofPolyTime tableEntry_polyTime) + ((vertexCertificate.comp (NativeCertificate.ofPolyTime packetInput_polyTime)).congr + fun _ => rfl)).congr fun q => by + rcases q with ⟨d | d, bs⟩ <;> rfl + +/-- `c (y + 1) ^ d ≤ c Z ^ D` when `y + 1 ≤ Z` and `d ≤ D`. -/ +private theorem mul_pow_le_mul_pow {c y d Z D : ℕ} (hy : y + 1 ≤ Z) (hd : d ≤ D) : + c * (y + 1) ^ d ≤ c * Z ^ D := + Nat.mul_le_mul_left _ ((Nat.pow_le_pow_left hy _).trans + (Nat.pow_le_pow_right (by omega) hd)) + +/-- **The resources of the native evaluator of descriptors.** There is `K` such that on a +descriptor and bits of total length `n`, with `m` target modes and `L` row ports (`0` and `0` for a +table), if the reduced coefficient lists of a packet's precision are at most `Rv` bits long, then +with `Z = n + m + Rv + 2` the time is at most `K (m + 2) ^ L Z ^ K` and the space at most +`K Z ^ K`. -/ +theorem entryCertificate_le : + ∃ K : ℕ, ∀ (q : VertexDesc × List Bool) (Rv : ℕ), q.1.ReducedLE Rv → + entryCertificate.time q ≤ K * (q.1.modes + 2) ^ q.1.rowPorts q.2 * + ((encPair enc encBits q).length + q.1.modes + Rv + 2) ^ K ∧ + entryCertificate.space q ≤ + K * ((encPair enc encBits q).length + q.1.modes + Rv + 2) ^ K := by + obtain ⟨K₀, hK₀⟩ := vertexCertificate_le + have hR := NativeCertificate.ofPolyTime_isPolynomial getRight_polyTime + have hT := NativeCertificate.ofPolyTime_isPolynomial tableEntry_polyTime + have hI := NativeCertificate.ofPolyTime_isPolynomial packetInput_polyTime + obtain ⟨cr, dr, hrt⟩ := hR.1.exists_le + obtain ⟨cr', dr', hrs⟩ := hR.2.exists_le + obtain ⟨ct, dt, htt⟩ := hT.1.exists_le + obtain ⟨ct', dt', hts⟩ := hT.2.exists_le + obtain ⟨ci, di, hit⟩ := hI.1.exists_le + obtain ⟨ci', di', his⟩ := hI.2.exists_le + obtain ⟨D, hD⟩ : ∃ D, D = K₀ + dr + dr' + dt + dt' + di + di' + 1 := ⟨_, rfl⟩ + obtain ⟨G, hG⟩ : ∃ G, G = K₀ + 2 * cr + 2 * cr' + ct + ct' + ci * 3 ^ di + ci' * 3 ^ di' + 1 := + ⟨_, rfl⟩ + refine ⟨G + D, fun q Rv hRv => ?_⟩ + obtain ⟨n, hn⟩ : ∃ n, n = (encPair enc encBits q).length := ⟨_, rfl⟩ + obtain ⟨Z, hZ⟩ : ∃ Z, Z = n + q.1.modes + Rv + 2 := ⟨_, rfl⟩ + obtain ⟨P, hP⟩ : ∃ P, P = (q.1.modes + 2) ^ q.1.rowPorts q.2 := ⟨_, rfl⟩ + rw [← hn, ← hZ, ← hP] + have hP1 : 1 ≤ P := hP ▸ Nat.one_le_pow _ _ (by omega) + have hnZ : n + 1 ≤ Z := by omega + have hZD : Z ^ D ≤ Z ^ (G + D) := Nat.pow_le_pow_right (by omega) (by omega) + have hnD : n ≤ Z ^ D := by + calc n ≤ Z := by omega + _ = Z ^ 1 := (pow_one Z).symm + _ ≤ Z ^ D := Nat.pow_le_pow_right (by omega) (by omega) + have hrt' : (NativeCertificate.ofPolyTime getRight_polyTime).time q ≤ cr * Z ^ D := + (hrt q).trans (hn ▸ mul_pow_le_mul_pow hnZ (by omega)) + have hrs' : (NativeCertificate.ofPolyTime getRight_polyTime).space q ≤ cr' * Z ^ D := + (hrs q).trans (hn ▸ mul_pow_le_mul_pow hnZ (by omega)) + rcases q with ⟨d | d, bs⟩ + · -- A table: the lookup alone. + have htt' : (NativeCertificate.ofPolyTime tableEntry_polyTime).time (.inl d, bs) ≤ + ct * Z ^ D := (htt _).trans (hn ▸ mul_pow_le_mul_pow hnZ (by omega)) + have hts' : (NativeCertificate.ofPolyTime tableEntry_polyTime).space (.inl d, bs) ≤ + ct' * Z ^ D := (hts _).trans (hn ▸ mul_pow_le_mul_pow hnZ (by omega)) + have htime : entryCertificate.time (.inl d, bs) = + 2 * (NativeCertificate.ofPolyTime getRight_polyTime).time (.inl d, bs) + n + + (NativeCertificate.ofPolyTime tableEntry_polyTime).time (.inl d, bs) := by + rw [hn]; rfl + have hspace : entryCertificate.space (.inl d, bs) = + 2 * (NativeCertificate.ofPolyTime getRight_polyTime).space (.inl d, bs) + n + + (NativeCertificate.ofPolyTime tableEntry_polyTime).space (.inl d, bs) := by + rw [hn]; rfl + constructor + · rw [htime] + calc _ ≤ G * Z ^ D := by + have : (2 * cr + 1 + ct) * Z ^ D ≤ G * Z ^ D := Nat.mul_le_mul_right _ (by omega) + have e : (2 * cr + 1 + ct) * Z ^ D = 2 * (cr * Z ^ D) + Z ^ D + ct * Z ^ D := by ring + omega + _ ≤ (G + D) * P * Z ^ (G + D) := + Nat.mul_le_mul ((Nat.le_add_right G D).trans (Nat.le_mul_of_pos_right _ hP1)) hZD + · rw [hspace] + calc _ ≤ G * Z ^ D := by + have : (2 * cr' + 1 + ct') * Z ^ D ≤ G * Z ^ D := Nat.mul_le_mul_right _ (by omega) + have e : (2 * cr' + 1 + ct') * Z ^ D = 2 * (cr' * Z ^ D) + Z ^ D + ct' * Z ^ D := by + ring + omega + _ ≤ (G + D) * Z ^ (G + D) := Nat.mul_le_mul (by omega) hZD + · -- A packet: the input of the packet evaluator, then the evaluator. + have hn' : n = 2 * ((encPacketDesc d).length + 1) + 1 + (encBits bs).length := by + rw [hn]; exact length_encPair _ + have hlen : (encPair encPacketDesc encBits (d, bs)).length ≤ n := by + have h3 : (encPair encPacketDesc encBits (d, bs)).length = + 2 * (encPacketDesc d).length + 1 + (encBits bs).length := length_encPair _ + omega + have hlenI : (encPair (encPair enc encBits) encPacketDesc ((.inr d, bs), d)).length + 1 ≤ + 3 * Z := by + have h1 : (encPair (encPair enc encBits) encPacketDesc ((.inr d, bs), d)).length = + 2 * (encPair enc encBits (.inr d, bs)).length + 1 + (encPacketDesc d).length := + length_encPair _ + omega + have hpow3 {c e : ℕ} (he : e ≤ D) : c * (3 * Z) ^ e ≤ c * 3 ^ e * Z ^ D := by + rw [Nat.mul_pow, ← Nat.mul_assoc] + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by omega) he) + have hit' : (NativeCertificate.ofPolyTime packetInput_polyTime).time ((.inr d, bs), d) ≤ + ci * 3 ^ di * Z ^ D := + (hit _).trans ((Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hlenI _)).trans + (hpow3 (by omega))) + have his' : (NativeCertificate.ofPolyTime packetInput_polyTime).space ((.inr d, bs), d) ≤ + ci' * 3 ^ di' * Z ^ D := + (his _).trans ((Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hlenI _)).trans + (hpow3 (by omega))) + obtain ⟨hvt, hvs⟩ := hK₀ (d, bs) Rv hRv + have hZ' : (encPair encPacketDesc encBits (d, bs)).length + (targetModes d.1).length + Rv + 2 + ≤ Z := by rw [hZ]; simp only [modes]; omega + have hpowK : ((encPair encPacketDesc encBits (d, bs)).length + (targetModes d.1).length + Rv + + 2) ^ K₀ ≤ Z ^ D := + (Nat.pow_le_pow_left hZ' _).trans (Nat.pow_le_pow_right (by omega) (by omega)) + have hvt' : vertexCertificate.time (d, bs) ≤ K₀ * P * Z ^ D := by + refine hvt.trans ?_ + rw [hP] + exact Nat.mul_le_mul_left _ hpowK + have hvs' : vertexCertificate.space (d, bs) ≤ K₀ * Z ^ D := + hvs.trans (Nat.mul_le_mul_left _ hpowK) + have htime : entryCertificate.time (.inr d, bs) = + 2 * (NativeCertificate.ofPolyTime getRight_polyTime).time (.inr d, bs) + n + + ((NativeCertificate.ofPolyTime packetInput_polyTime).time ((.inr d, bs), d) + + vertexCertificate.time (d, bs)) := by + rw [hn]; rfl + have hspace : entryCertificate.space (.inr d, bs) = + 2 * (NativeCertificate.ofPolyTime getRight_polyTime).space (.inr d, bs) + n + + ((NativeCertificate.ofPolyTime packetInput_polyTime).space ((.inr d, bs), d) + + vertexCertificate.space (d, bs)) := by + rw [hn]; rfl + constructor + · rw [htime] + have h1 : 2 * (cr * Z ^ D) + Z ^ D + ci * 3 ^ di * Z ^ D ≤ + P * ((2 * cr + 1 + ci * 3 ^ di) * Z ^ D) := by + calc _ = (2 * cr + 1 + ci * 3 ^ di) * Z ^ D := by ring + _ ≤ _ := Nat.le_mul_of_pos_left _ hP1 + have h2 : P * ((2 * cr + 1 + ci * 3 ^ di) * Z ^ D) + K₀ * P * Z ^ D ≤ P * (G * Z ^ D) := by + rw [show K₀ * P * Z ^ D = P * (K₀ * Z ^ D) by ring, ← Nat.mul_add, ← Nat.add_mul] + exact Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ (by omega)) + calc _ ≤ P * (G * Z ^ D) := by omega + _ ≤ (G + D) * P * Z ^ (G + D) := by + rw [show (G + D) * P * Z ^ (G + D) = P * ((G + D) * Z ^ (G + D)) by ring] + exact Nat.mul_le_mul_left _ (Nat.mul_le_mul (by omega) hZD) + · rw [hspace] + calc _ ≤ G * Z ^ D := by + have : (2 * cr' + 1 + ci' * 3 ^ di' + K₀) * Z ^ D ≤ G * Z ^ D := + Nat.mul_le_mul_right _ (by omega) + have e : (2 * cr' + 1 + ci' * 3 ^ di' + K₀) * Z ^ D = + 2 * (cr' * Z ^ D) + Z ^ D + ci' * 3 ^ di' * Z ^ D + K₀ * Z ^ D := by ring + omega + _ ≤ (G + D) * Z ^ (G + D) := Nat.mul_le_mul (by omega) hZD + +end VertexDesc + +end Cslib.Circuits.Frontier diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkVertexDesc.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkVertexDesc.lean new file mode 100644 index 000000000..e3be36554 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkVertexDesc.lean @@ -0,0 +1,95 @@ +/- +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: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildEntries +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ReductionLift + +/-! +# Tests for vertex descriptors and the entries of child networks + +A table descriptor reads its table little-endian and is a constant in `A_p`. A packet descriptor +over the tiny packet of the packet-evaluator tests (`2 ^ 1` slots over +`A_3 = (ℤ / 8)[U] / (U ^ 2 + U + 1)`, `t = 1`, `ζ = U`) with one row port in slot `0` and one +column port in slot `1` evaluates to the kernel value `5 + 2 U` at zero exponents, whatever the +column ports of its context, since they are read from the tags. The ports of one side of a tagged +list come out in order. Reducing an element of `O` to `A_n` and mapping back along +`reductionLift` gives its class modulo `2 ^ n`. +-/ + +@[expose] public section + +namespace ComplexityTests.TensorNetworkVertexDesc + +open Cslib Cslib.Circuits.Frontier Cslib.Circuits.Frontier.NativePacket + +/-! ### Tables -/ + +-- The bits `[true, false]` index the table at `1`. +example : VertexDesc.entry (.inl [3, 5, 7, 9]) [true, false] = [5] := by decide + +example : VertexDesc.entry (.inl [3, 5, 7, 9]) [false, true] = [7] := by decide + +-- A table has no modes and no row ports. +example : VertexDesc.modes (.inl [3, 5]) = 0 := rfl + +example : VertexDesc.rowPorts (.inl [3, 5]) [true] = 0 := rfl + +-- A table entry is a constant in `A_p`. +example : GaloisRingArith.val 3 [1, 1] (VertexDesc.entry (.inl [3, 5]) [true]) = + ((5 : ℕ) : GaloisRingArith.Ring 3 [1, 1]) := + VertexDesc.val_entry_inl 3 [1, 1] [3, 5] [true] + +/-! ### Packets -/ + +/-- The context of the tiny packet, with no column ports of its own. -/ +def ctx : PacketCtx := + ⟨3, [1, 1], 1, 2, 0, 2, 1, 2, true, false, true, [], [0, 1]⟩ + +/-- The descriptor: a row port in slot `0` and a column port in slot `1`, zero exponents. -/ +def desc : VertexDesc := .inr (ctx, [(true, 0), (false, 1)], [0, 0, 0, 0]) + +-- The column ports are read from the tags and the bits: the entry is `W_1(T) = 5 + 2 U`. +example : VertexDesc.entry desc [true, true] = [5, 2] := by decide + +example : VertexDesc.rowPorts desc [true, true] = 1 := by decide + +/-! ### Tagged ports -/ + +example : sidePorts [(true, 3), (false, 1), (true, 2)] [true, false, false] true = + [(3, true), (2, false)] := by decide + +example : sidePorts [(true, 3), (false, 1), (true, 2)] [true, false, false] false = + [(1, false)] := by decide + +-- The same, through `sidePorts_map` on a list tagged by parity. +example : sidePorts ([4, 1, 2].map fun c => (decide (c % 2 = 0), c)) ([4, 1, 2].map fun c => c < 3) + true = [(4, false), (2, true)] := by + rw [sidePorts_map] + decide + +/-! ### Resources -/ + +example : ∃ K : ℕ, ∀ (q : VertexDesc × List Bool) (Rv : ℕ), q.1.ReducedLE Rv → + VertexDesc.entryCertificate.time q ≤ K * (q.1.modes + 2) ^ q.1.rowPorts q.2 * + ((Turing.MultiTapeTM.encPair VertexDesc.enc Turing.MultiTapeTM.encBits q).length + + q.1.modes + Rv + 2) ^ K ∧ + VertexDesc.entryCertificate.space q ≤ + K * ((Turing.MultiTapeTM.encPair VertexDesc.enc Turing.MultiTapeTM.encBits q).length + + q.1.modes + Rv + 2) ^ K := + VertexDesc.entryCertificate_le + +/-! ### Back from `A_n` to `O / (2 ^ n)` -/ + +example {f : Polynomial ℤ} (hf : f.Monic) + (hirr : Irreducible (f.map (Int.castRingHom (ZMod 2)))) (n : ℕ) + (x : (AdjoinRoot.padicValuation 2 hf hirr).integer) : + reductionLift hf hirr n (AdjoinRoot.reduction hf hirr n x) = Ideal.Quotient.mk _ x := + reductionLift_reduction hf hirr n x + +end ComplexityTests.TensorNetworkVertexDesc