diff --git a/Complexity.lean b/Complexity.lean index 603e806a12..bc9d197805 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -892,7 +892,10 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.KernelProd public import Complexity.Computability.Circuit.Frontier.TensorNetwork.LocalDeformation public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketEntry +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Recursion +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Reindex public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduledRecursion public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TaperedRecovery public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional @@ -2893,6 +2896,7 @@ public import Complexity.Foundations.NumberTheory.AKS.Introspective public import Complexity.Foundations.NumberTheory.AKS.PerfectPower public import Complexity.Foundations.NumberTheory.AKS.SmallR public import Complexity.Foundations.NumberTheory.Harmonic +public import Complexity.Foundations.NumberTheory.Padics.AdjoinRootDigitLift public import Complexity.Foundations.NumberTheory.Padics.AdjoinRootReduction public import Complexity.Foundations.NumberTheory.Padics.AdjoinRootValuation public import Complexity.Foundations.NumberTheory.Padics.RatValuation diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ActiveCall.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ActiveCall.lean index cf9a248fe1..afa5522d4c 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ActiveCall.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ActiveCall.lean @@ -44,17 +44,16 @@ of the products of the contractions of the children. So the values may be comput children's contractions modulo `2 ^ p_t` (`TensorNetwork.exists_recoverFromValues_eq_add_of_mk`). **The packing bridge.** The orientation that the child identity needs is property (2) of -Lemma D.3 for `Cslib.PacketPacking.Packing` (`TensorNetwork.packingGroup_src_tgt`), and the port +Lemma D.3 for `Cslib.PacketPacking.Packing` (`packingGroup_src_tgt`), and the port counts of Lemma D.3 (3) are the group sizes that bound the children -(`TensorNetwork.card_packingGroup_src`, `TensorNetwork.card_packingGroup_tgt`, with +(`card_packingGroup_src`, `card_packingGroup_tgt`, with `TensorNetwork.ModeSplitting.mul_card_edges_child_le`). ## Main definitions * `Cslib.Circuits.Frontier.integerHom`: the inclusion of `ℤ_(2)` into `B`. * `Cslib.Circuits.Frontier.recoverFromValues`: interpolation followed by tapered recovery. -* `Cslib.Circuits.Frontier.TensorNetwork.packingGroup`: the group of a vertex in coordinate `i` - of a packing. +* `Cslib.Circuits.Frontier.packingGroup`: the group of a vertex in coordinate `i` of a packing. ## Main results @@ -66,7 +65,7 @@ counts of Lemma D.3 (3) are the group sizes that bound the children deformation modulo `2 ^ p_t` are deformed contractions along `cauchyValueMatrix`. * `Cslib.Circuits.Frontier.TensorNetwork.exists_recoverFromValues_eq_add_of_mk`: correctness of one active call. -* `Cslib.Circuits.Frontier.TensorNetwork.packingGroup_src_tgt`: the packing bridge, with +* `Cslib.Circuits.Frontier.packingGroup_src_tgt`: the packing bridge, with `packing_slot_lt`, `packing_slot_injective`, `card_packingGroup_src` and `card_packingGroup_tgt`. * `Cslib.Circuits.Frontier.two_pow_padicValInt_dvd_and_not_dvd`: a node of valuation `i` meets @@ -187,56 +186,64 @@ theorem exists_recoverFromValues_eq_add (B : Subring K) hslot htS, coeff_map, coeff_map, hg, coeff_add, coeff_C_mul, map_add, map_mul, map_pow] rfl +end TensorNetwork + /-! ### The packing bridge -/ -/-- The group of a vertex in coordinate `i` of a packing: its row label if it is a row and its -column label if it is a column. -/ -@[expose] def packingGroup {R : Type*} {a r : ℕ} (N : TensorNetwork R Bool V E) (side : V → Bool) - (Q : PacketPacking.Packing N.src N.tgt a r) (i : Fin a) (v : V) : Fin r := +section PackingBridge + +variable {V E : Type*} {src tgt : E → V} {a r : ℕ} + +/-- The group of a vertex in coordinate `i` of a packing of the edges `src e → tgt e`: its row +label if it is a row and its column label if it is a column. -/ +@[expose] def packingGroup (side : V → Bool) (Q : PacketPacking.Packing src tgt a r) (i : Fin a) + (v : V) : Fin r := if side v then Q.rowLabel v i else Q.colLabel v i -omit [Fintype V] [Fintype E] [DecidableEq E] [DecidableEq P] in -/-- **The packing bridge.** For a packing of the edges of a network whose edges run from rows to -columns (Lemma D.3 of [OpenAI2026ETH]), the groups in coordinate `i` are oriented by digit `i` of -the slots (Lemma D.3 (2)): the hypothesis of `TensorNetwork.cauchyModeSplitting`. -/ -theorem packingGroup_src_tgt {R : Type*} {a r : ℕ} (N : TensorNetwork R Bool V E) - (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) - (Q : PacketPacking.Packing N.src N.tgt a r) (i : Fin a) (e : E) : - (packingGroup N side Q i (N.src e), packingGroup N side Q i (N.tgt e)) = +/-- **The packing bridge.** For a packing of edges that run from rows to columns (Lemma D.3 of +[OpenAI2026ETH]), the groups in coordinate `i` are oriented by digit `i` of the slots +(Lemma D.3 (2)): the hypothesis of `TensorNetwork.cauchyModeSplitting`. The edge ends `src` and +`tgt` are arbitrary functions, so the bridge applies to `N.src` and `N.tgt` of any network with +these ends, such as `N.map f`. -/ +theorem packingGroup_src_tgt (side : V → Bool) (hsrc : ∀ e, side (src e) = true) + (htgt : ∀ e, side (tgt e) = false) (Q : PacketPacking.Packing src tgt a r) (i : Fin a) + (e : E) : + (packingGroup side Q i (src e), packingGroup side Q i (tgt e)) = if (Q.slot e : ℕ).testBit i then (Q.symbols (Q.packet e) i).swap else Q.symbols (Q.packet e) i := by simp only [packingGroup, hsrc, htgt, ↓reduceIte, Bool.false_eq_true] exact Q.labels_eq e i -omit [Fintype V] [Fintype E] [DecidableEq E] [DecidableEq P] in /-- The slots of a packing lie below `2 ^ a`. -/ -theorem packing_slot_lt {R : Type*} {a r : ℕ} {N : TensorNetwork R Bool V E} - (Q : PacketPacking.Packing N.src N.tgt a r) (e : E) : (Q.slot e : ℕ) < 2 ^ a := +theorem packing_slot_lt (Q : PacketPacking.Packing src tgt a r) (e : E) : + (Q.slot e : ℕ) < 2 ^ a := (Q.slot e).isLt -omit [Fintype V] [Fintype E] [DecidableEq E] [DecidableEq P] in /-- No two edges share a slot of a packet. -/ -theorem packing_slot_injective {R : Type*} {a r : ℕ} {N : TensorNetwork R Bool V E} - (Q : PacketPacking.Packing N.src N.tgt a r) (e e' : E) (hp : Q.packet e = Q.packet e') - (hs : (Q.slot e : ℕ) = Q.slot e') : e = e' := +theorem packing_slot_injective (Q : PacketPacking.Packing src tgt a r) (e e' : E) + (hp : Q.packet e = Q.packet e') (hs : (Q.slot e : ℕ) = Q.slot e') : e = e' := Q.injective (Prod.ext hp (Fin.ext hs)) -omit [Fintype V] [DecidableEq E] [DecidableEq P] in +variable [Fintype E] + /-- The rows of group `σ` in coordinate `i` of a packing are the rows with symbol `σ`. -/ -theorem card_packingGroup_src {R : Type*} {a r : ℕ} (N : TensorNetwork R Bool V E) - (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) - (Q : PacketPacking.Packing N.src N.tgt a r) (i : Fin a) (σ : Fin r) : - #{e | packingGroup N side Q i (N.src e) = σ} = #{e | Q.rowLabel (N.src e) i = σ} := by +theorem card_packingGroup_src (side : V → Bool) (hsrc : ∀ e, side (src e) = true) + (Q : PacketPacking.Packing src tgt a r) (i : Fin a) (σ : Fin r) : + #{e | packingGroup side Q i (src e) = σ} = #{e | Q.rowLabel (src e) i = σ} := by simp only [packingGroup, hsrc, ↓reduceIte] -omit [Fintype V] [DecidableEq E] [DecidableEq P] in /-- The columns of group `σ` in coordinate `i` of a packing are the columns with symbol `σ`. -/ -theorem card_packingGroup_tgt {R : Type*} {a r : ℕ} (N : TensorNetwork R Bool V E) - (side : V → Bool) (htgt : ∀ e, side (N.tgt e) = false) - (Q : PacketPacking.Packing N.src N.tgt a r) (i : Fin a) (σ : Fin r) : - #{e | packingGroup N side Q i (N.tgt e) = σ} = #{e | Q.colLabel (N.tgt e) i = σ} := by +theorem card_packingGroup_tgt (side : V → Bool) (htgt : ∀ e, side (tgt e) = false) + (Q : PacketPacking.Packing src tgt a r) (i : Fin a) (σ : Fin r) : + #{e | packingGroup side Q i (tgt e) = σ} = #{e | Q.colLabel (tgt e) i = σ} := by simp only [packingGroup, htgt, Bool.false_eq_true, ↓reduceIte] +end PackingBridge + +namespace TensorNetwork + +variable {V E P : Type*} [Fintype V] [Fintype E] [DecidableEq E] [DecidableEq P] + /-- **The values of the local deformation modulo `2 ^ p_t`** are deformed contractions of the reduced network along the Cauchy matrix at `T = t + α ζ` (which the child identity (D.16), `TensorNetwork.deformedContraction_cauchyValueMatrix_eq_sum`, expands). -/ diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Recursion.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Recursion.lean new file mode 100644 index 0000000000..a6606b51b9 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Recursion.lean @@ -0,0 +1,707 @@ +/- +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.ActiveCall +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Reindex +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule + +/-! +# The contraction recursion and its correctness + +This file assembles the recursive contraction algorithm of [OpenAI2026ETH] (§D.4.7, p. 64) from +its active calls, and proves it correct by induction from the leaves. + +**One node** (`TensorNetwork.nodeSplitting`). For a network whose edges run from rows to columns, +a packing `Q` of its edges into packets of `2 ^ a` slots, and a nonzero grid point `t` of +valuation `i < a`, group the vertices by their symbol in coordinate `i` of `Q` (`packingGroup`). +The packing bridge `packingGroup_src_tgt` orients the groups, so the Cauchy matrix at +`T = t + α ζ` has the mode splitting `TensorNetwork.cauchyModeSplitting` (§D.4.5, p. 62). At a call +with input precision `p`, `TensorNetwork.callSplitting` is this splitting for the network reduced +modulo `2 ^ p_t`, `p_t = p + 8 h D_t + 8 M (a + 1)`: the schedule's +`ContractionSchedule.nodePrecision` at the valuation of `t`, the precision of Lemma D.5. + +**One call from its children.** If every value `v t k` reduces modulo `2 ^ p_t` to the sum over +the mode tuples of the products of the contractions of the children (the right side of (D.16)), +then interpolation and tapered recovery return the contraction modulo `2 ^ p` +(`TensorNetwork.exists_recoverFromValues_eq_add_of_children`). The children's contractions may +come from any *contraction oracle* (`TensorNetwork.ContractionOracle`) that is correct modulo the +precision it is given: a child over `B ⧸ (2 ^ p_t)` is lifted to `B` along a section of the +reduction and renumbered by `Fin` (`TensorNetwork.finLift`, +`TensorNetwork.ContractionOracle.evalLift`), and the oracle's value then reduces to its contraction +(`TensorNetwork.ContractionOracle.mk_evalLift`). The value of +an active node is `TensorNetwork.nodeValue`, the values of a call are `TensorNetwork.callValues`, +and the recovered value is `TensorNetwork.callValue` +(`TensorNetwork.exists_callValue_eq_add`). + +**The recursion** (`TensorNetwork.contractRec`). A call receives a network on `Fin n` vertices +and `Fin m` edges, its sides, its depth `d` and its precision `p`. A *schedule* gives the +parameters `a`, `u`, `h` and the degree bound `Δ` of a call from its depth and its number of edges +(`CallParams`), or none at a leaf; the manuscript's schedule is +`ContractionSchedule.callParams`. The call is active when its guard holds (`CallParams.Guard`): +the parameters meet the hypotheses of Lemma D.5 (`CallParams.Admissible`, with `u ≤ a` and enough +interpolation points), and the network runs from rows to columns with at most `Δ` ports at each +end of each vertex (`TensorNetwork.RowsToColumnsLE`). It packs the edges with +`PacketPacking.packing` (Lemma D.3, `r = 64`), takes the first `M (2 L - 1) + 1` of a fixed family +of interpolation points, and evaluates each child by a recursive call at depth `d + 1` and precision +`p_t`. A leaf, an inactive call, and a child that does not have fewer edges than its parent are +evaluated by the contraction itself, the direct summation of the manuscript's leaves. The recursion +is well founded on the number of edges. + +**Correctness** (`TensorNetwork.exists_contractRec_eq_add`). For interpolation points with unit +differences, every call returns the contraction modulo `2 ^ p`, for every schedule: the manuscript's +"induction from the leaves" (p. 64) becomes strong induction on the number of edges. So the +parameter schedule (D.4)–(D.6) matters only for the running time, which this file does not treat. +Under the first inequality of (D.6), every child has at most `M / 16` edges +(`TensorNetwork.mul_card_edges_child_callSplitting_le`, from Lemma D.3 (3)), so an active call with +an edge never falls back for its children, and when `2 L ≤ Δ` the lifted children again run from +rows to columns within the degree bound (`TensorNetwork.rowsToColumnsLE_finLift_child`). In the +manuscript's ring `B = O = ℤ_(2)[U] / (f)`, the binary-coordinate lifts are such points +(`AdjoinRoot.isUnit_integerDigitLift_sub`). + +## Main definitions + +* `Cslib.Circuits.Frontier.TensorNetwork.RowsToColumnsLE`: a network from rows to columns with a + degree bound. +* `Cslib.Circuits.Frontier.TensorNetwork.nodeSplitting`, + `Cslib.Circuits.Frontier.TensorNetwork.callSplitting`: the mode splitting at an active node. +* `Cslib.Circuits.Frontier.TensorNetwork.finLift`: a child lifted to `B` and numbered by `Fin`. +* `Cslib.Circuits.Frontier.TensorNetwork.ContractionOracle`: values for child calls, with + `ContractionOracle.Correct` and `ContractionOracle.evalLift`. +* `Cslib.Circuits.Frontier.TensorNetwork.nodeValue`, + `Cslib.Circuits.Frontier.TensorNetwork.callValues`, + `Cslib.Circuits.Frontier.TensorNetwork.callValue`: one active call from an oracle. +* `Cslib.Circuits.Frontier.TensorNetwork.CallParams`: the parameters of a call, with + `CallParams.Admissible` and the guard `CallParams.Guard`. +* `Cslib.Circuits.Frontier.TensorNetwork.contractRec`: the recursion. + +## Main results + +* `Cslib.Circuits.Frontier.TensorNetwork.exists_recoverFromValues_eq_add_of_children`: one call is + correct when its values are the sums of the products of the children's contractions. +* `Cslib.Circuits.Frontier.TensorNetwork.callSplitting_side`, + `Cslib.Circuits.Frontier.TensorNetwork.callSplitting_group`, + `Cslib.Circuits.Frontier.TensorNetwork.callSplitting_packet`: the fields of the splitting. +* `Cslib.Circuits.Frontier.TensorNetwork.exists_callValue_eq_add`: one call is correct for a + correct oracle. +* `Cslib.Circuits.Frontier.TensorNetwork.mul_card_edges_child_callSplitting_le`: under (D.6), the + children have at most `M / 16` edges. +* `Cslib.Circuits.Frontier.TensorNetwork.ModeSplitting.rowsToColumnsLE_child`, + `Cslib.Circuits.Frontier.TensorNetwork.rowsToColumnsLE_finLift_child`: the children keep the + degree bound. +* `Cslib.Circuits.Frontier.TensorNetwork.contractRec_eq_callValue`, + `Cslib.Circuits.Frontier.TensorNetwork.contractRec_of_sched_eq_none`: an active call and a leaf. +* `Cslib.Circuits.Frontier.TensorNetwork.exists_contractRec_eq_add`, + `Cslib.Circuits.Frontier.TensorNetwork.mk_contractRec`: the recursion returns the contraction + modulo `2 ^ p`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma D.3 (pp. 58–59), + §D.4.4–§D.4.7, pp. 60–64. +-/ + +public section + +open Polynomial Finset + +namespace Cslib.Circuits.Frontier + +open ContractionSchedule (nodePrecision) + +/-- The subring `ℤ_(2)` of rationals with odd denominator. -/ +local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2) + +/-! ### Node precisions -/ + +/-- A node of positive multiplicity has valuation below `u`. -/ +theorem padicValInt_lt_of_taperMult_pos_left {u h : ℕ} {t : ℤ} (hq : 0 < taperMult u h t) : + padicValInt 2 t < u := by + unfold taperMult at hq + by_contra hc + rw [Nat.sub_eq_zero_of_le (not_lt.mp hc), mul_zero] at hq + exact lt_irrefl 0 hq + +/-- A node of positive multiplicity has valuation below `u`, so below `a` when `u ≤ a`. -/ +theorem padicValInt_lt_of_taperMult_pos {u h a : ℕ} {t : ℤ} (hq : 0 < taperMult u h t) + (hua : u ≤ a) : padicValInt 2 t < a := + (padicValInt_lt_of_taperMult_pos_left hq).trans_le hua + +/-- The ideal `(2 ^ n)` of a commutative ring. -/ +abbrev twoPowIdeal (B : Type*) [CommRing B] (n : ℕ) : Ideal B := + Ideal.span {(2 : B) ^ n} + +/-- `2 ^ n = 0` modulo `2 ^ n`. -/ +theorem two_pow_eq_zero_twoPowIdeal (B : Type*) [CommRing B] (n : ℕ) : + (2 : B ⧸ twoPowIdeal B n) ^ n = 0 := by + have : Ideal.Quotient.mk (twoPowIdeal B n) ((2 : B) ^ n) = 0 := + Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self _) + rwa [map_pow, map_ofNat] at this + +/-- The ideal `(2 ^ p_t)` of the node `t` of a call with `M` edges, packets of `2 ^ a` slots, +multiplicity step `h` and input precision `p`. -/ +abbrev nodeIdeal (B : Type*) [CommRing B] (M a h p : ℕ) (t : ℤ) : Ideal B := + twoPowIdeal B (nodePrecision p h a M (padicValInt 2 t)) + +namespace TensorNetwork + +/-! ### Networks from rows to columns -/ + +/-- Every edge of `N` runs from a row (`side v = true`) to a column, and every vertex has at most +`Δ` ports at each end: the bipartite form and the degree bound `Δ` of the networks of the +recursion (§D.4.2, p. 58). -/ +structure RowsToColumnsLE {R U V E : Type*} [Fintype E] [DecidableEq V] + (N : TensorNetwork R U V E) (side : V → Bool) (Δ : ℕ) : Prop where + /-- Edges start at rows. -/ + side_src : ∀ e, side (N.src e) = true + /-- Edges end at columns. -/ + side_tgt : ∀ e, side (N.tgt e) = false + /-- Every vertex is the source of at most `Δ` edges. -/ + src_le : ∀ v, #{e | N.src e = v} ≤ Δ + /-- Every vertex is the target of at most `Δ` edges. -/ + tgt_le : ∀ w, #{e | N.tgt e = w} ≤ Δ + +instance {R U : Type*} {n m : ℕ} (N : TensorNetwork R U (Fin n) (Fin m)) (side : Fin n → Bool) + (Δ : ℕ) : Decidable (N.RowsToColumnsLE side Δ) := + decidable_of_iff ((∀ e, side (N.src e) = true) ∧ (∀ e, side (N.tgt e) = false) ∧ + (∀ v, #{e | N.src e = v} ≤ Δ) ∧ ∀ w, #{e | N.tgt e = w} ≤ Δ) + ⟨fun ⟨h₁, h₂, h₃, h₄⟩ => ⟨h₁, h₂, h₃, h₄⟩, fun ⟨h₁, h₂, h₃, h₄⟩ => ⟨h₁, h₂, h₃, h₄⟩⟩ + +/-! ### The modes of an active node -/ + +section Node + +variable {R V E : Type*} [CommRing R] [Fintype E] {a r : ℕ} + +/-- **The modes of an active node** (§D.4.5). For a network whose edges run from rows to columns, +a packing `Q` of its edges, and a nonzero grid point `t` of valuation `i < a`, the mode splitting +of the Cauchy matrix at `T = t + α ζ` with the vertices grouped by their symbol in coordinate `i` +of `Q` (`cauchyModeSplitting`, oriented by `packingGroup_src_tgt`). -/ +noncomputable def nodeSplitting (N : TensorNetwork R Bool V E) (side : V → Bool) + (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) + (Q : PacketPacking.Packing N.src N.tgt a r) (κ : ℤ₍₂₎ →+* R) (ζ : R) {p : ℕ} + (hp : (2 : R) ^ p = 0) {t : ℤ} (ht : t ∈ recoveryNodes a) (hia : padicValInt 2 t < a) : + N.ModeSplitting (cauchyValueMatrix κ ζ a t Q.packet fun e => Q.slot e) (Fin r) + (Fin Q.numPackets) (Fin Q.numPackets × Fin (2 ^ (padicValInt 2 t + 1)) × Fin p) := + cauchyModeSplitting (group := packingGroup side Q ⟨_, hia⟩) (packet := Q.packet) + (slot := fun e => Q.slot e) (sym := fun q => Q.symbols q ⟨_, hia⟩) (i := padicValInt 2 t) + side hsrc htgt (packingGroup_src_tgt side hsrc htgt Q ⟨_, hia⟩) (packing_slot_lt Q) hia κ ζ hp + (mem_of_mem_erase ht) (two_pow_padicValInt_dvd_and_not_dvd (ne_of_mem_erase ht)).1 + (two_pow_padicValInt_dvd_and_not_dvd (ne_of_mem_erase ht)).2 + +/-- **The child identity at an active node** ((D.16)): the deformed contraction along the Cauchy +matrix at `T = t + α ζ` is the sum, over the mode tuples of weight below `p`, of the products over +the groups of the contractions of the children of `nodeSplitting`. -/ +theorem deformedContraction_eq_sum_nodeSplitting [Fintype V] [DecidableEq V] [DecidableEq E] + (N : TensorNetwork R Bool V E) (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) + (htgt : ∀ e, side (N.tgt e) = false) (Q : PacketPacking.Packing N.src N.tgt a r) + (κ : ℤ₍₂₎ →+* R) (ζ : R) {p : ℕ} (hp : (2 : R) ^ p = 0) {t : ℤ} (ht : t ∈ recoveryNodes a) + (hia : padicValInt 2 t < a) : + N.deformedContraction side (cauchyValueMatrix κ ζ a t Q.packet fun e => Q.slot e) = + ∑ β ∈ modeBudget + (fun Z : Fin Q.numPackets × Fin (2 ^ (padicValInt 2 t + 1)) × Fin p => (Z.2.2 : ℕ) + 1) p, + ∏ g, ((nodeSplitting N side hsrc htgt Q κ ζ hp ht hia).child β g).contraction := + deformedContraction_cauchyValueMatrix_eq_sum (group := packingGroup side Q ⟨_, hia⟩) + (packet := Q.packet) (slot := fun e => Q.slot e) (sym := fun q => Q.symbols q ⟨_, hia⟩) + (i := padicValInt 2 t) side hsrc htgt (packingGroup_src_tgt side hsrc htgt Q ⟨_, hia⟩) + (packing_slot_lt Q) hia κ ζ hp (mem_of_mem_erase ht) + (two_pow_padicValInt_dvd_and_not_dvd (ne_of_mem_erase ht)).1 + (two_pow_padicValInt_dvd_and_not_dvd (ne_of_mem_erase ht)).2 + +end Node + +/-! ### One call from its children -/ + +section Children + +variable {K : Type*} [CommRing K] [Algebra ℚ K] (B : Subring K) + (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) {V E : Type*} [Fintype V] [DecidableEq V] [Fintype E] + [DecidableEq E] + +/-- The mode splitting at the active node `t` and the point `z` of a call with input precision +`p`: `nodeSplitting` for the network reduced modulo `2 ^ p_t`, at the reduction of `z`. -/ +noncomputable def callSplitting (N : TensorNetwork B Bool V E) (side : V → Bool) + (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) {a r : ℕ} + (Q : PacketPacking.Packing N.src N.tgt a r) (p u h : ℕ) (hua : u ≤ a) {t : ℤ} + (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (z : B) : + ModeSplitting + (N.map (Ideal.Quotient.mk (nodeIdeal B (Fintype.card E) a h p t))) + (cauchyValueMatrix + ((Ideal.Quotient.mk (nodeIdeal B (Fintype.card E) a h p t)).comp + (integerHom B hB)) + (Ideal.Quotient.mk (nodeIdeal B (Fintype.card E) a h p t) z) a t + Q.packet fun e => Q.slot e) + (Fin r) (Fin Q.numPackets) + (Fin Q.numPackets × Fin (2 ^ (padicValInt 2 t + 1)) × + Fin (nodePrecision p h a (Fintype.card E) (padicValInt 2 t))) := + nodeSplitting (N.map (Ideal.Quotient.mk (nodeIdeal B (Fintype.card E) a h p t))) + side hsrc htgt Q _ _ (two_pow_eq_zero_twoPowIdeal _ _) ht + (padicValInt_lt_of_taperMult_pos hq hua) + +section Fields + +variable (N : TensorNetwork B Bool V E) (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) + (htgt : ∀ e, side (N.tgt e) = false) {a r : ℕ} (Q : PacketPacking.Packing N.src N.tgt a r) + (p u h : ℕ) (hua : u ≤ a) {t : ℤ} (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (z : B) + +omit [Fintype V] [DecidableEq V] [DecidableEq E] in +/-- The rows of the splitting at an active node are the rows of the call. -/ +@[simp] theorem callSplitting_side : + (callSplitting B hB N side hsrc htgt Q p u h hua ht hq z).side = side := + cauchyModeSplitting_side .. + +omit [Fintype V] [DecidableEq V] [DecidableEq E] in +/-- The groups at an active node of valuation `i` are the symbols in coordinate `i` of the +packing. -/ +@[simp] theorem callSplitting_group : + (callSplitting B hB N side hsrc htgt Q p u h hua ht hq z).group = + packingGroup side Q ⟨_, padicValInt_lt_of_taperMult_pos hq hua⟩ := + cauchyModeSplitting_group .. + +omit [Fintype V] [DecidableEq V] [DecidableEq E] in +/-- The packets of the splitting at an active node are the packets of the packing. -/ +@[simp] theorem callSplitting_packet : + (callSplitting B hB N side hsrc htgt Q p u h hua ht hq z).packet = Q.packet := + cauchyModeSplitting_packet .. + +end Fields + +/-- **Correctness of one active call from its children** ([OpenAI2026ETH], §D.4.4–§D.4.7). Let +`N` have entries in `B`, edges from rows to columns, and a packing `Q` into packets of `2 ^ a` +slots. Let `1 ≤ u ≤ M`, `u ≤ a` and `3 M ≤ h u ≤ 3 M + u` for `M` edges, and let the +`n > M (2 L - 1)` points `ζ k` have unit differences. If at every node `t` of positive +multiplicity each value `v t k` reduces modulo `2 ^ p_t` to the sum, over the mode tuples of +weight below `p_t`, of the products over the groups of the contractions of the children of +`callSplitting` at `ζ k` (the right side of (D.16)), then the recovered value agrees with the +contraction modulo `2 ^ p`. -/ +theorem exists_recoverFromValues_eq_add_of_children (N : TensorNetwork B Bool V E) + (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) + {a r : ℕ} (Q : PacketPacking.Packing N.src N.tgt a r) {u h p : ℕ} (hu : 1 ≤ u) + (huM : u ≤ Fintype.card E) (hua : u ≤ a) (hh : 3 * Fintype.card E ≤ h * u) + (hh' : h * u ≤ 3 * Fintype.card E + u) {n : ℕ} (ζ : Fin n → B) + (hζ : Pairwise fun k l => IsUnit (ζ k - ζ l)) (hn : Fintype.card E * (2 * 2 ^ a - 1) < n) + (v : ℤ → Fin n → B) + (hv : ∀ t (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) k, + Ideal.Quotient.mk (nodeIdeal B (Fintype.card E) a h p t) (v t k) = + ∑ β ∈ modeBudget (fun Z : Fin Q.numPackets × Fin (2 ^ (padicValInt 2 t + 1)) × + Fin (nodePrecision p h a (Fintype.card E) (padicValInt 2 t)) => (Z.2.2 : ℕ) + 1) + (nodePrecision p h a (Fintype.card E) (padicValInt 2 t)), + ∏ g, ((callSplitting B hB N side hsrc htgt Q p u h hua ht hq (ζ k)).child β + g).contraction) : + ∃ b ∈ B, recoverFromValues B a u h ζ v = (N.contraction : K) + 2 ^ p * b := + exists_recoverFromValues_eq_add_of_mk B hB N side (packing_slot_lt Q) + (packing_slot_injective Q) hu huM hh hh' ζ hζ hn v fun t ht hq k => + (hv t ht hq k).trans (deformedContraction_eq_sum_nodeSplitting + (N.map (Ideal.Quotient.mk (nodeIdeal B (Fintype.card E) a h p t))) side + hsrc htgt Q _ _ (two_pow_eq_zero_twoPowIdeal _ _) ht + (padicValInt_lt_of_taperMult_pos hq hua)).symm + +end Children + +/-! ### Lifting child networks -/ + +section FinLift + +variable {B : Type*} [CommRing B] {V E : Type*} [Fintype V] [Fintype E] {p : ℕ} + +/-- A network over `B ⧸ (2 ^ p)` on finite types, lifted to `B` along a section of the reduction +(`TensorNetwork.mapFun`) and numbered by `Fin` (`TensorNetwork.reindex`): the network that a child +call receives. -/ +noncomputable def finLift (N : TensorNetwork (B ⧸ twoPowIdeal B p) Bool V E) : + TensorNetwork B Bool (Fin (Fintype.card V)) (Fin (Fintype.card E)) := + (N.mapFun (Function.surjInv Ideal.Quotient.mk_surjective)).reindex (Fintype.equivFin V) + (Fintype.equivFin E) + +/-- The contraction of a lifted network reduces to the contraction. -/ +theorem mk_contraction_finLift [DecidableEq E] (N : TensorNetwork (B ⧸ twoPowIdeal B p) Bool V E) : + Ideal.Quotient.mk (twoPowIdeal B p) (finLift N).contraction = N.contraction := by + rw [finLift, contraction_reindex, + contraction_map_mapFun _ (Function.surjInv_eq Ideal.Quotient.mk_surjective)] + +/-- Lifting keeps a network running from rows to columns, with its degree bound. -/ +theorem RowsToColumnsLE.finLift [DecidableEq V] {N : TensorNetwork (B ⧸ twoPowIdeal B p) Bool V E} + {side : V → Bool} {Δ : ℕ} (h : N.RowsToColumnsLE side Δ) : + (TensorNetwork.finLift N).RowsToColumnsLE (side ∘ (Fintype.equivFin V).symm) Δ where + side_src e := by + simp only [TensorNetwork.finLift, Function.comp_apply, reindex_src, Equiv.symm_apply_apply] + exact h.side_src _ + side_tgt e := by + simp only [TensorNetwork.finLift, Function.comp_apply, reindex_tgt, Equiv.symm_apply_apply] + exact h.side_tgt _ + src_le v := by + rw [TensorNetwork.finLift, card_reindex_src] + exact h.src_le _ + tgt_le w := by + rw [TensorNetwork.finLift, card_reindex_tgt] + exact h.tgt_le _ + +end FinLift + +/-! ### Contraction oracles -/ + +/-- A *contraction oracle*: a value for every Boolean tensor network on the vertices `Fin n` and the +edges `Fin m`, with its sides, at every precision. A call of the recursion evaluates its children +through an oracle. -/ +abbrev ContractionOracle (B : Type*) : Type _ := + (n m : ℕ) → TensorNetwork B Bool (Fin n) (Fin m) → (Fin n → Bool) → ℕ → B + +namespace ContractionOracle + +variable {B : Type*} [CommRing B] + +/-- An oracle is *correct* when each of its values agrees with the contraction modulo the +precision `2 ^ p` it is given. -/ +@[expose] def Correct (rec : ContractionOracle B) : Prop := + ∀ n m (N : TensorNetwork B Bool (Fin n) (Fin m)) side p, + ∃ c, rec n m N side p = N.contraction + 2 ^ p * c + +/-- The value of an oracle on a network over `B ⧸ (2 ^ p)` on finite types, at precision `p`: the +query on the lifted network `finLift N`. -/ +noncomputable def evalLift (rec : ContractionOracle B) {V E : Type*} [Fintype V] [Fintype E] + {p : ℕ} (N : TensorNetwork (B ⧸ twoPowIdeal B p) Bool V E) (side : V → Bool) : B := + rec _ _ (finLift N) (side ∘ (Fintype.equivFin V).symm) p + +/-- **A correct oracle evaluates a lifted network**: its value reduces modulo `2 ^ p` to the +contraction. -/ +theorem mk_evalLift {rec : ContractionOracle B} (hrec : rec.Correct) {V E : Type*} [Fintype V] + [Fintype E] [DecidableEq E] {p : ℕ} (N : TensorNetwork (B ⧸ twoPowIdeal B p) Bool V E) + (side : V → Bool) : + Ideal.Quotient.mk (twoPowIdeal B p) (rec.evalLift N side) = N.contraction := by + obtain ⟨c, hc⟩ := hrec _ _ (finLift N) (side ∘ (Fintype.equivFin V).symm) p + have h2 : Ideal.Quotient.mk (twoPowIdeal B p) ((2 : B) ^ p) = 0 := + Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self _) + rw [evalLift, hc, map_add, map_mul, h2, zero_mul, add_zero, mk_contraction_finLift] + +end ContractionOracle + +/-! ### One call from an oracle -/ + +section Call + +variable {K : Type*} [CommRing K] [Algebra ℚ K] (B : Subring K) + (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) {V E : Type*} [Fintype V] [DecidableEq V] [Fintype E] + [DecidableEq E] + +/-- **The value at an active node** ((D.16)): the sum, over the mode tuples of weight below `p_t`, +of the products over the groups of the oracle's values on the children of `callSplitting` at `z`. +A child has its old vertices as rows and its packets as columns. -/ +noncomputable def nodeValue (rec : ContractionOracle B) (N : TensorNetwork B Bool V E) + (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) + {a r : ℕ} (Q : PacketPacking.Packing N.src N.tgt a r) (p u h : ℕ) (hua : u ≤ a) {t : ℤ} + (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (z : B) : B := + ∑ β ∈ modeBudget (fun Z : Fin Q.numPackets × Fin (2 ^ (padicValInt 2 t + 1)) × + Fin (nodePrecision p h a (Fintype.card E) (padicValInt 2 t)) => (Z.2.2 : ℕ) + 1) + (nodePrecision p h a (Fintype.card E) (padicValInt 2 t)), + ∏ g, rec.evalLift ((callSplitting B hB N side hsrc htgt Q p u h hua ht hq z).child β g) + Sum.isLeft + +/-- For a correct oracle, the value at an active node reduces modulo `2 ^ p_t` to the right side of +(D.16). -/ +theorem mk_nodeValue {rec : ContractionOracle B} (hrec : rec.Correct) + (N : TensorNetwork B Bool V E) (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) + (htgt : ∀ e, side (N.tgt e) = false) {a r : ℕ} (Q : PacketPacking.Packing N.src N.tgt a r) + (p u h : ℕ) (hua : u ≤ a) {t : ℤ} (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) + (z : B) : + Ideal.Quotient.mk (nodeIdeal B (Fintype.card E) a h p t) + (nodeValue B hB rec N side hsrc htgt Q p u h hua ht hq z) = + ∑ β ∈ modeBudget (fun Z : Fin Q.numPackets × Fin (2 ^ (padicValInt 2 t + 1)) × + Fin (nodePrecision p h a (Fintype.card E) (padicValInt 2 t)) => (Z.2.2 : ℕ) + 1) + (nodePrecision p h a (Fintype.card E) (padicValInt 2 t)), + ∏ g, ((callSplitting B hB N side hsrc htgt Q p u h hua ht hq z).child β g).contraction := by + simp only [nodeValue, map_sum, map_prod, ContractionOracle.mk_evalLift hrec] + +/-- The values of an active call at the nodes and interpolation points: `nodeValue` at the nodes +of positive multiplicity, and zero elsewhere. -/ +noncomputable def callValues (rec : ContractionOracle B) (N : TensorNetwork B Bool V E) + (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) + {a r : ℕ} (Q : PacketPacking.Packing N.src N.tgt a r) (p u h : ℕ) (hua : u ≤ a) {n : ℕ} + (ζ : Fin n → B) (t : ℤ) (k : Fin n) : B := + if hq : t ∈ recoveryNodes a ∧ 0 < taperMult u h t then + nodeValue B hB rec N side hsrc htgt Q p u h hua hq.1 hq.2 (ζ k) + else 0 + +open Classical in +/-- **One active call** (§D.4.7): interpolate and recover (`recoverFromValues`) the values +`callValues` computed from the oracle. The recovered value lies in `B` when the oracle is correct +(`exists_callValue_eq_add`); otherwise the call returns zero. -/ +noncomputable def callValue (rec : ContractionOracle B) (N : TensorNetwork B Bool V E) + (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) + {a r : ℕ} (Q : PacketPacking.Packing N.src N.tgt a r) (p u h : ℕ) (hua : u ≤ a) {n : ℕ} + (ζ : Fin n → B) : B := + if hx : recoverFromValues B a u h ζ (callValues B hB rec N side hsrc htgt Q p u h hua ζ) ∈ B then + ⟨_, hx⟩ + else 0 + +/-- **Correctness of one active call** for a correct oracle: under the hypotheses of +`exists_recoverFromValues_eq_add_of_children`, the call returns the contraction modulo `2 ^ p`. -/ +theorem exists_callValue_eq_add {rec : ContractionOracle B} (hrec : rec.Correct) + (N : TensorNetwork B Bool V E) (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) + (htgt : ∀ e, side (N.tgt e) = false) {a r : ℕ} (Q : PacketPacking.Packing N.src N.tgt a r) + {u h p : ℕ} (hu : 1 ≤ u) (huM : u ≤ Fintype.card E) (hua : u ≤ a) + (hh : 3 * Fintype.card E ≤ h * u) (hh' : h * u ≤ 3 * Fintype.card E + u) {n : ℕ} + (ζ : Fin n → B) (hζ : Pairwise fun k l => IsUnit (ζ k - ζ l)) + (hn : Fintype.card E * (2 * 2 ^ a - 1) < n) : + ∃ c : B, callValue B hB rec N side hsrc htgt Q p u h hua ζ = N.contraction + 2 ^ p * c := by + obtain ⟨b, hb, hx⟩ := exists_recoverFromValues_eq_add_of_children B hB N side hsrc htgt Q hu + huM hua hh hh' ζ hζ hn (callValues B hB rec N side hsrc htgt Q p u h hua ζ) + fun t ht hq k => by + rw [callValues, dite_eq_left ⟨ht, hq⟩] + exact mk_nodeValue B hB hrec N side hsrc htgt Q p u h hua ht hq (ζ k) + have hx' : recoverFromValues B a u h ζ (callValues B hB rec N side hsrc htgt Q p u h hua ζ) = + ((N.contraction + 2 ^ p * ⟨b, hb⟩ : B) : K) := by + rw [hx] + push_cast + rfl + refine ⟨⟨b, hb⟩, ?_⟩ + rw [callValue, dite_eq_left (by rw [hx']; exact (N.contraction + 2 ^ p * ⟨b, hb⟩).2)] + exact Subtype.ext hx' + +end Call + +/-! ### The children of an active call -/ + +namespace ModeSplitting + +variable {R V E G P M : Type*} [CommRing R] [Fintype M] {N : TensorNetwork R Bool V E} + {W : Matrix E E R} (S : N.ModeSplitting W G P M) [Fintype E] [DecidableEq E] [DecidableEq P] + [DecidableEq G] [DecidableEq M] [DecidableEq V] + +/-- **Children run from rows to columns within the degree bound.** If every vertex of `N` has at +most `Δ` ports at each end, and the packets have `2 ^ a` slots with `2 · 2 ^ a ≤ Δ`, then each +child runs from its old vertices to its packets with at most `Δ` ports at each vertex: old +vertices keep their degrees, and a packet vertex has at most `2 L` ports (§D.4.6, p. 63). -/ +theorem rowsToColumnsLE_child {Δ a : ℕ} {slot : E → ℕ} (hrow : ∀ v, #{e | N.src e = v} ≤ Δ) + (hcol : ∀ w, #{e | N.tgt e = w} ≤ Δ) (hslot : ∀ e, slot e < 2 ^ a) + (hinj : ∀ e e', S.packet e = S.packet e' → slot e = slot e' → e = e') (hL : 2 * 2 ^ a ≤ Δ) + (β : M → ℕ) (g : G) : (S.child β g).RowsToColumnsLE Sum.isLeft Δ where + side_src := by rintro (e | e) <;> rfl + side_tgt := by rintro (e | e) <;> rfl + src_le := by + rintro (v | q) + · rw [S.card_child_src_inl] + by_cases hv : S.side v.1 + · have h0 : #{e | N.tgt e = v.1} = 0 := card_eq_zero.mpr <| filter_eq_empty_iff.mpr + fun e _ he => by + have := S.side_tgt e + rw [he, hv] at this + exact absurd this (by decide) + rw [h0, add_zero] + exact hrow _ + · have h0 : #{e | N.src e = v.1} = 0 := card_eq_zero.mpr <| filter_eq_empty_iff.mpr + fun e _ he => by + have := S.side_src e + rw [he] at this + exact hv this + rw [h0, zero_add] + exact hcol _ + · rw [S.card_child_src_inr] + exact Nat.zero_le _ + tgt_le := by + rintro (v | q) + · rw [S.card_child_tgt_inl] + exact Nat.zero_le _ + · exact (S.card_child_tgt_inr_le hslot hinj β g q).trans hL + +end ModeSplitting + +section ChildSize + +variable {K : Type*} [CommRing K] [Algebra ℚ K] (B : Subring K) + (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) {V E : Type*} [Fintype V] [DecidableEq V] [FinEnum V] + [Fintype E] [DecidableEq E] [LinearOrder E] + +omit [Fintype V] [DecidableEq E] in +/-- **Children have at most `M / 16` edges** under the size hypothesis `2 Δ D² ≤ M` of (D.6), +`D = 64 ^ (2 a)`, for the packing of Lemma D.3 with `r = 64` and maximum degree `Δ`: each group has +at most `2 M / 64` ports on each side (`PacketPacking.row_ports_packing_le`), and a child has one +edge per port of its group. The source (§D.4.6, p. 63) bounds a child by `6M/r = 3M/32 < M/8` +edges from the `3M/r` port bound of Lemma D.3 (3); `PacketPacking.packing` has the sharper port +bound `2M/r`. -/ +theorem mul_card_edges_child_callSplitting_le (N : TensorNetwork B Bool V E) (side : V → Bool) + (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) {a Δ : ℕ} + (hrow : ∀ v, #{e | N.src e = v} ≤ Δ) (hcol : ∀ w, #{e | N.tgt e = w} ≤ Δ) + (hM : 2 * Δ * (64 ^ (2 * a)) ^ 2 ≤ Fintype.card E) (p u h : ℕ) (hua : u ≤ a) {t : ℤ} + (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (z : B) (g : Fin 64) : + 64 * Fintype.card + ({e // (callSplitting B hB N side hsrc htgt (PacketPacking.packing N.src N.tgt a 64) p u h + hua ht hq z).group (N.src e) = g} ⊕ + {e // (callSplitting B hB N side hsrc htgt (PacketPacking.packing N.src N.tgt a 64) p u h + hua ht hq z).group (N.tgt e) = g}) ≤ + 4 * Fintype.card E := by + have := ModeSplitting.mul_card_edges_child_le (c := 2) (r := 64) + (callSplitting B hB N side hsrc htgt (PacketPacking.packing N.src N.tgt a 64) p u h hua ht hq z) + g (by + rw [callSplitting_group] + exact (congrArg (64 * ·) (card_packingGroup_src side hsrc _ _ g)).trans_le + (PacketPacking.row_ports_packing_le N.src N.tgt a 64 hrow hcol hM _ g)) (by + rw [callSplitting_group] + exact (congrArg (64 * ·) (card_packingGroup_tgt side htgt _ _ g)).trans_le + (PacketPacking.col_ports_packing_le N.src N.tgt a 64 hrow hcol hM _ g)) + exact this.trans_eq (by ring) + +omit [LinearOrder E] [FinEnum V] in +/-- **The lifted children of an active call run from rows to columns within the degree bound** +`Δ`, when the call does and its packets have `2 · 2 ^ a ≤ Δ` slots: the networks the child calls +receive meet the network part of their guard (`CallParams.Guard`). -/ +theorem rowsToColumnsLE_finLift_child (N : TensorNetwork B Bool V E) (side : V → Bool) + (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) {a r : ℕ} + (Q : PacketPacking.Packing N.src N.tgt a r) (p u h : ℕ) (hua : u ≤ a) {t : ℤ} + (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (z : B) {Δ : ℕ} + (hrow : ∀ v, #{e | N.src e = v} ≤ Δ) (hcol : ∀ w, #{e | N.tgt e = w} ≤ Δ) + (hL : 2 * 2 ^ a ≤ Δ) (β) (g : Fin r) : + (finLift ((callSplitting B hB N side hsrc htgt Q p u h hua ht hq z).child β g)).RowsToColumnsLE + (Sum.isLeft ∘ (Fintype.equivFin _).symm) Δ := + RowsToColumnsLE.finLift <| ModeSplitting.rowsToColumnsLE_child + (callSplitting B hB N side hsrc htgt Q p u h hua ht hq z) hrow hcol (packing_slot_lt Q) + (by rw [callSplitting_packet]; exact packing_slot_injective Q) hL β g + +end ChildSize + +/-! ### The recursion -/ + +/-- The parameters of an active call: packets of `L = 2 ^ a` slots, the tapered multiplicities +`q_t = h max(0, u - v₂ t)` of Lemma D.5, and the degree bound `Δ` of (D.6). -/ +structure CallParams where + /-- The packets have `2 ^ a` slots. -/ + a : ℕ + /-- The number of levels of positive multiplicity. -/ + u : ℕ + /-- The step of the multiplicities between levels. -/ + h : ℕ + /-- The degree bound `Δ`. -/ + degree : ℕ + +/-- The parameters of a call with `M` edges and `n` interpolation points are *admissible* when +they meet the hypotheses of Lemma D.5, `1 ≤ u ≤ M`, `u ≤ a` and `3 M ≤ h u ≤ 3 M + u`, and there +are more than `M (2 L - 1)` points. -/ +structure CallParams.Admissible (θ : CallParams) (M n : ℕ) : Prop where + /-- `1 ≤ u`. -/ + one_le_u : 1 ≤ θ.u + /-- `u ≤ M`. -/ + u_le_edges : θ.u ≤ M + /-- `u ≤ a`. -/ + u_le_a : θ.u ≤ θ.a + /-- `3 M ≤ h u`. -/ + le_h_mul : 3 * M ≤ θ.h * θ.u + /-- `h u ≤ 3 M + u`, as for `h = ⌈3 M / u⌉`. -/ + h_mul_le : θ.h * θ.u ≤ 3 * M + θ.u + /-- There are more than `M (2 L - 1)` interpolation points. -/ + points_lt : M * (2 * 2 ^ θ.a - 1) < n + +instance (θ : CallParams) (M n : ℕ) : Decidable (θ.Admissible M n) := + decidable_of_iff (1 ≤ θ.u ∧ θ.u ≤ M ∧ θ.u ≤ θ.a ∧ 3 * M ≤ θ.h * θ.u ∧ + θ.h * θ.u ≤ 3 * M + θ.u ∧ M * (2 * 2 ^ θ.a - 1) < n) + ⟨fun ⟨h₁, h₂, h₃, h₄, h₅, h₆⟩ => ⟨h₁, h₂, h₃, h₄, h₅, h₆⟩, + fun ⟨h₁, h₂, h₃, h₄, h₅, h₆⟩ => ⟨h₁, h₂, h₃, h₄, h₅, h₆⟩⟩ + +/-- The *guard* of an active call on a network `N` with `m` edges, its sides `side` and `n` +interpolation points: the parameters `θ` are admissible, and `N` runs from rows to columns with +at most `Δ = θ.degree` ports at each end of each vertex, the degree bound under which Lemma D.3 +makes the children smaller (`mul_card_edges_child_callSplitting_le`). Correctness does not use the +degree bound. -/ +structure CallParams.Guard (θ : CallParams) {R : Type*} {n m : ℕ} + (N : TensorNetwork R Bool (Fin n) (Fin m)) (side : Fin n → Bool) (N₀ : ℕ) : Prop + extends N.RowsToColumnsLE side θ.degree where + /-- The parameters are admissible. -/ + admissible : θ.Admissible m N₀ + +instance (θ : CallParams) {R : Type*} {n m : ℕ} (N : TensorNetwork R Bool (Fin n) (Fin m)) + (side : Fin n → Bool) (N₀ : ℕ) : Decidable (θ.Guard N side N₀) := + decidable_of_iff (N.RowsToColumnsLE side θ.degree ∧ θ.Admissible m N₀) + ⟨fun ⟨h₁, h₂⟩ => ⟨h₁, h₂⟩, fun h => ⟨h.toRowsToColumnsLE, h.admissible⟩⟩ + +section Recursion + +variable {K : Type*} [CommRing K] [Algebra ℚ K] (B : Subring K) + (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) (sched : ℕ → ℕ → Option CallParams) {N₀ : ℕ} + (pts : Fin N₀ → B) + +/-- **The contraction recursion** ([OpenAI2026ETH], §D.4.7). A call at depth `d` on a network `N` +with `m` edges, sides `side` and precision `p` asks the schedule for its parameters. When there +are none, or the guard fails (`CallParams.Guard`), it returns the contraction (direct +summation). Otherwise it is an active call (`callValue`) with the packing of Lemma D.3 (`r = 64`) +and the first `M (2 L - 1) + 1` points of `pts`, whose children are recursive calls at depth +`d + 1`; a child that does not have fewer edges returns its contraction. -/ +noncomputable def contractRec (d n m : ℕ) (N : TensorNetwork B Bool (Fin n) (Fin m)) + (side : Fin n → Bool) (p : ℕ) : B := + match sched d m with + | none => N.contraction + | some θ => + if hθ : θ.Guard N side N₀ then + callValue B hB + (fun n' m' N' side' p' => + if hm : m' < m then contractRec (d + 1) n' m' N' side' p' else N'.contraction) + N side hθ.side_src hθ.side_tgt (PacketPacking.packing N.src N.tgt θ.a 64) p θ.u θ.h + hθ.admissible.u_le_a + fun k : Fin (m * (2 * 2 ^ θ.a - 1) + 1) => pts (Fin.castLE hθ.admissible.points_lt k) + else N.contraction +termination_by m + +variable {B hB sched pts} in +/-- **An active call** of the recursion: when the schedule gives parameters whose guard holds, the +call is `callValue` with the packing of Lemma D.3, the first `M (2 L - 1) + 1` points, and +recursive calls at depth `d + 1` for the children with fewer edges. -/ +theorem contractRec_eq_callValue {d n m : ℕ} {N : TensorNetwork B Bool (Fin n) (Fin m)} + {side : Fin n → Bool} {θ : CallParams} (hs : sched d m = some θ) (hθ : θ.Guard N side N₀) + (p : ℕ) : + contractRec B hB sched pts d n m N side p = + callValue B hB + (fun n' m' N' side' p' => + if m' < m then contractRec B hB sched pts (d + 1) n' m' N' side' p' else N'.contraction) + N side hθ.side_src hθ.side_tgt (PacketPacking.packing N.src N.tgt θ.a 64) p θ.u θ.h + hθ.admissible.u_le_a + fun k : Fin (m * (2 * 2 ^ θ.a - 1) + 1) => pts (Fin.castLE hθ.admissible.points_lt k) := by + rw [contractRec.eq_def] + simp only [hs] + rw [dite_eq_left hθ] + rfl + +variable {B hB sched pts} in +/-- **A leaf** of the recursion, where the schedule gives no parameters, is evaluated directly. -/ +theorem contractRec_of_sched_eq_none {d n m : ℕ} {N : TensorNetwork B Bool (Fin n) (Fin m)} + {side : Fin n → Bool} (hs : sched d m = none) (p : ℕ) : + contractRec B hB sched pts d n m N side p = N.contraction := by + rw [contractRec.eq_def] + simp only [hs] + +/-- **Correctness of the recursion** ([OpenAI2026ETH], §D.4.7, p. 64: correctness "by induction +from the leaves"). For interpolation points with unit differences, every call returns the +contraction modulo `2 ^ p`, for every schedule and depth. -/ +theorem exists_contractRec_eq_add (hpts : Pairwise fun k l => IsUnit (pts k - pts l)) (d n m : ℕ) + (N : TensorNetwork B Bool (Fin n) (Fin m)) (side : Fin n → Bool) (p : ℕ) : + ∃ c : B, contractRec B hB sched pts d n m N side p = N.contraction + 2 ^ p * c := by + induction m using Nat.strong_induction_on generalizing d n p with + | _ m ih => + rw [contractRec] + split + · exact ⟨0, by simp⟩ + · rename_i θ _ + split_ifs with hθ + · obtain ⟨hu, huM, hua, hh, hh', hn⟩ := hθ.admissible + refine exists_callValue_eq_add B hB (fun n' m' N' side' p' => ?_) N side hθ.side_src + hθ.side_tgt _ hu (by simpa using huM) hua (by simpa using hh) (by simpa using hh') _ + (fun k l hkl => hpts fun h => hkl (Fin.castLE_injective _ h)) (by simp) + split_ifs with hm + · exact ih m' hm (d + 1) n' N' side' p' + · exact ⟨0, by simp⟩ + · exact ⟨0, by simp⟩ + +/-- **The recursion computes the contraction modulo `2 ^ p`.** -/ +theorem mk_contractRec (hpts : Pairwise fun k l => IsUnit (pts k - pts l)) (d n m : ℕ) + (N : TensorNetwork B Bool (Fin n) (Fin m)) (side : Fin n → Bool) (p : ℕ) : + Ideal.Quotient.mk (twoPowIdeal B p) (contractRec B hB sched pts d n m N side p) = + Ideal.Quotient.mk (twoPowIdeal B p) N.contraction := by + obtain ⟨c, hc⟩ := exists_contractRec_eq_add B hB sched pts hpts d n m N side p + rw [hc, Ideal.Quotient.eq, add_sub_cancel_left] + exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self _) + +end Recursion + +end TensorNetwork + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Reindex.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Reindex.lean new file mode 100644 index 0000000000..468d7f065f --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Reindex.lean @@ -0,0 +1,145 @@ +/- +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 + +/-! +# Renaming and lifting tensor networks + +Two operations that keep the contraction of a tensor network under control while its types or its +coefficient ring change. + +* **Renaming** (`TensorNetwork.reindex`). Transport a network along bijections of its vertices + and of its edges. The contraction is unchanged (`TensorNetwork.contraction_reindex`). The + contraction recursion of [OpenAI2026ETH] (§D.4.6–§D.4.7, pp. 63–64) uses it to number the + vertices and edges of a child network by `Fin`. +* **Lifting the entries** (`TensorNetwork.mapFun`). Apply an arbitrary function to every tensor + entry. When the function is a section of a ring homomorphism `f`, reducing the lifted network + along `f` recovers the original (`TensorNetwork.map_mapFun`), so its contraction reduces to the + original contraction (`TensorNetwork.contraction_map_mapFun`). This is the manuscript's + canonical lift of entries specified modulo `2 ^ p` (§D.4.1, p. 58); any section works. + +## Main definitions + +* `Cslib.Circuits.Frontier.TensorNetwork.reindex`: renaming the vertices and edges. +* `Cslib.Circuits.Frontier.TensorNetwork.mapFun`: mapping every entry by a function. + +## Main results + +* `Cslib.Circuits.Frontier.TensorNetwork.contraction_reindex`: renaming preserves the contraction, + and `card_reindex_src`, `card_reindex_tgt` the degrees. +* `Cslib.Circuits.Frontier.TensorNetwork.map_mapFun`: reducing a lift along `f` recovers the + network. +* `Cslib.Circuits.Frontier.TensorNetwork.contraction_map_mapFun`: the contraction of a lift + reduces to the contraction. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.1 (p. 58) and + §D.4.6 (p. 63). +-/ + +public section + +namespace Cslib.Circuits.Frontier.TensorNetwork + +open Finset + +variable {R S U V E V' E' : Type*} + +/-! ### Renaming the vertices and edges -/ + +section Reindex + +variable (eV : V ≃ V') (eE : E ≃ E') (N : TensorNetwork R U V E) + +/-- The network transported along bijections `eV` of the vertices and `eE` of the edges: edge +`eE e` runs from `eV (N.src e)` to `eV (N.tgt e)`, and vertex `eV v` carries the tensor of `v`. -/ +@[expose] def reindex : TensorNetwork R U V' E' where + src e := eV (N.src (eE.symm e)) + tgt e := eV (N.tgt (eE.symm e)) + tensor v x := N.tensor (eV.symm v) (x ∘ eE) + tensor_congr v x y h := N.tensor_congr _ _ _ fun e he => h (eE e) (by + simp only [Equiv.symm_apply_apply] + rcases he with he | he + · exact Or.inl (by rw [he, Equiv.apply_symm_apply]) + · exact Or.inr (by rw [he, Equiv.apply_symm_apply])) + +@[simp] theorem reindex_src (e : E') : (N.reindex eV eE).src e = eV (N.src (eE.symm e)) := + rfl + +@[simp] theorem reindex_tgt (e : E') : (N.reindex eV eE).tgt e = eV (N.tgt (eE.symm e)) := + rfl + +@[simp] theorem reindex_tensor (v : V') (x : E' → U) : + (N.reindex eV eE).tensor v x = N.tensor (eV.symm v) (x ∘ eE) := + rfl + +/-- Renaming keeps the number of edges leaving each vertex. -/ +theorem card_reindex_src [Fintype E] [Fintype E'] [DecidableEq V] [DecidableEq V'] (v : V') : + #{e | (N.reindex eV eE).src e = v} = #{e | N.src e = eV.symm v} := by + refine Finset.card_equiv eE.symm fun e => ?_ + rw [Finset.mem_filter, Finset.mem_filter] + simp [Equiv.eq_symm_apply] + +/-- Renaming keeps the number of edges entering each vertex. -/ +theorem card_reindex_tgt [Fintype E] [Fintype E'] [DecidableEq V] [DecidableEq V'] (v : V') : + #{e | (N.reindex eV eE).tgt e = v} = #{e | N.tgt e = eV.symm v} := by + refine Finset.card_equiv eE.symm fun e => ?_ + rw [Finset.mem_filter, Finset.mem_filter] + simp [Equiv.eq_symm_apply] + +/-- **Renaming preserves the contraction.** -/ +theorem contraction_reindex [CommSemiring R] [Fintype U] [Fintype V] [Fintype E] [DecidableEq E] + [Fintype V'] [Fintype E'] [DecidableEq E'] : + (N.reindex eV eE).contraction = N.contraction := + Fintype.sum_equiv (eE.symm.arrowCongr (Equiv.refl U)) _ _ fun _ => + Fintype.prod_equiv eV.symm _ _ fun _ => rfl + +end Reindex + +/-! ### Lifting the entries -/ + +section MapFun + +/-- The tensor network with every tensor entry mapped by the function `f`. Unlike +`TensorNetwork.map`, `f` need not be a ring homomorphism; a section of a reduction map lifts the +entries. -/ +@[expose] def mapFun (f : R → S) (N : TensorNetwork R U V E) : TensorNetwork S U V E where + toMultigraph := N.toMultigraph + tensor v x := f (N.tensor v x) + tensor_congr v x y h := by rw [N.tensor_congr v x y h] + +@[simp] theorem mapFun_tensor (f : R → S) (N : TensorNetwork R U V E) (v : V) (x : E → U) : + (N.mapFun f).tensor v x = f (N.tensor v x) := + rfl + +@[simp] theorem toMultigraph_mapFun (f : R → S) (N : TensorNetwork R U V E) : + (N.mapFun f).toMultigraph = N.toMultigraph := + rfl + +variable [CommSemiring R] [CommSemiring S] (f : R →+* S) {σ : S → R} + +/-- **Reducing a lift recovers the network**: for a section `σ` of `f`, mapping the entries by +`σ` and then by `f` changes nothing. -/ +theorem map_mapFun (hσ : ∀ x, f (σ x) = x) (N : TensorNetwork S U V E) : + (N.mapFun σ).map f = N := by + obtain ⟨G, T, hT⟩ := N + simp only [map, mapFun, hσ] + +/-- **The contraction of a lift reduces to the contraction**: for a section `σ` of `f`, `f` maps +the contraction of the lifted network to the contraction of the network. -/ +theorem contraction_map_mapFun [Fintype U] [Fintype V] [Fintype E] [DecidableEq E] + (hσ : ∀ x, f (σ x) = x) (N : TensorNetwork S U V E) : + f (N.mapFun σ).contraction = N.contraction := by + rw [← contraction_map, map_mapFun f hσ] + +end MapFun + +end Cslib.Circuits.Frontier.TensorNetwork diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduledRecursion.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduledRecursion.lean new file mode 100644 index 0000000000..3a70376cc1 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduledRecursion.lean @@ -0,0 +1,206 @@ +/- +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.Recursion + +/-! +# The contraction recursion with the parameter schedule + +This file runs the contraction recursion (`TensorNetwork.contractRec`) with the parameter schedule +of [OpenAI2026ETH] (§D.4.2, (D.4)–(D.6), p. 58) from `Cslib.Circuits.Frontier.ContractionSchedule`, +so that its correctness and the running-time certificate refer to the same calls. + +**The schedule of call parameters** (`ContractionSchedule.callParams s`). For size `s`, a call at +depth `d` with `M` edges is a leaf when `M ≤ H = leafSize s`. Otherwise it has `a = slotBits s d` +slot bits, taper `u = taper s d`, multiplicity step `h = ⌈3 M / u⌉` (`taperStep`), and degree +bound `Δ = degreeBound s`. Its children are recovered at the precisions `p_t = nodePrecision`. +Correctness of the recursion holds for this schedule as for every other +(`TensorNetwork.exists_contractRec_eq_add`). + +**An active call.** At a call with `Active C s d M p` and `ActiveBounds C s d M p` (the certificate +`exists_activeBounds` gives the second from the first for `s ≥ s₀`) on a network that runs from +rows to columns with at most `Δ` ports at each end, and with at least `2 ^ (4 ⌊log₂ s⌋)` +interpolation points: + +* the guard holds, so the call is the active call `callValue` + (`contractRec_callParams_eq_callValue`); +* every lifted child runs from rows to columns within the degree bound + (`TensorNetwork.rowsToColumnsLE_finLift_child`), has at most `M / 16` edges + (`sixteen_mul_card_edges_child_le`), and is evaluated at a precision within the schedule + (`nodePrecision_le_of_taperMult_pos`), so it is a leaf or an active call at depth `d + 1` + (`Active.child`); +* there are at most `2 ^ e_d` mode tuples at each active node (`card_modeBudget_callParams_le`), and + the nodes, points and groups contribute `2 ^ (2 ⌊log₂ s⌋)` (`ActiveBounds.branching_le`). + +These are the per-call facts that a certificate of the running time instantiates along the +recursion tree. + +## Main definitions + +* `Cslib.Circuits.Frontier.ContractionSchedule.taperStep`: `h = ⌈3 M / u⌉`. +* `Cslib.Circuits.Frontier.ContractionSchedule.callParams`: the schedule of call parameters. + +## Main results + +* `Cslib.Circuits.Frontier.ContractionSchedule.ActiveBounds.admissible`: the parameters of an active + call are admissible. +* `Cslib.Circuits.Frontier.ContractionSchedule.contractRec_callParams_eq_callValue`: an active call. +* `Cslib.Circuits.Frontier.ContractionSchedule.sixteen_mul_card_edges_child_le`, + `Cslib.Circuits.Frontier.ContractionSchedule.nodePrecision_le_of_taperMult_pos`, + `Cslib.Circuits.Frontier.ContractionSchedule.card_modeBudget_callParams_le`: its children and + their number. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.2 (p. 58), + §D.4.4–§D.4.7, pp. 60–64. +-/ + +public section + +open Finset + +namespace Cslib.Circuits.Frontier.ContractionSchedule + +open TensorNetwork + +/-- The subring `ℤ_(2)` of rationals with odd denominator. -/ +local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2) + +/-! ### The schedule of call parameters -/ + +/-- The multiplicity step `h = ⌈3 M / u⌉` of Lemma D.5 at depth `d`, with `u = taper s d`. -/ +@[expose] def taperStep (s d M : ℕ) : ℕ := + (3 * M + taper s d - 1) / taper s d + +theorem le_taperStep_mul {s d M : ℕ} (hu : 1 ≤ taper s d) : + 3 * M ≤ taperStep s d M * taper s d := by + have h1 := Nat.lt_div_mul_add (a := 3 * M + taper s d - 1) (b := taper s d) (by omega) + unfold taperStep + generalize (3 * M + taper s d - 1) / taper s d * taper s d = y at h1 ⊢ + omega + +theorem taperStep_mul_le (s d M : ℕ) : taperStep s d M * taper s d ≤ 3 * M + taper s d := + (Nat.div_mul_le_self _ _).trans (Nat.sub_le _ _) + +/-- **The schedule of call parameters** for size `s`: a call at depth `d` with `M` edges is a leaf +when `M ≤ leafSize s`, and otherwise has `a = slotBits s d`, `u = taper s d`, `h = ⌈3 M / u⌉` and +the degree bound `Δ = degreeBound s`. -/ +@[expose] def callParams (s d M : ℕ) : Option CallParams := + if M ≤ leafSize s then none + else some ⟨slotBits s d, taper s d, taperStep s d M, degreeBound s⟩ + +theorem callParams_of_le {s d M : ℕ} (h : M ≤ leafSize s) : callParams s d M = none := + ite_eq_left h + +theorem callParams_of_lt {s d M : ℕ} (h : leafSize s < M) : + callParams s d M = some ⟨slotBits s d, taper s d, taperStep s d M, degreeBound s⟩ := + ite_eq_right (not_le.mpr h) + +/-- **The parameters of an active call are admissible**, given `2 ^ (4 ⌊log₂ s⌋)` interpolation +points. -/ +theorem ActiveBounds.admissible {C s d M p : ℕ} (hB : ActiveBounds C s d M p) {N₀ : ℕ} + (hN₀ : 2 ^ (4 * Nat.log 2 s) ≤ N₀) : + (CallParams.mk (slotBits s d) (taper s d) (taperStep s d M) (degreeBound s)).Admissible M + N₀ where + one_le_u := hB.one_le_taper + u_le_edges := hB.taper_le_edges + u_le_a := by + have := slotBits_eq s d + simp only + omega + le_h_mul := le_taperStep_mul hB.one_le_taper + h_mul_le := taperStep_mul_le s d M + points_lt := by + have := hB.points_le + simp only + omega + +/-! ### An active call -/ + +section Active + +variable {K : Type*} [CommRing K] [Algebra ℚ K] (B : Subring K) + (hB : ∀ c ∈ ℤ₍₂₎, algebraMap ℚ K c ∈ B) {N₀ : ℕ} (pts : Fin N₀ → B) + +/-- **An active call of the scheduled recursion.** At an active call (`Active`, `ActiveBounds`) on a +network that runs from rows to columns within the degree bound, with at least +`2 ^ (4 ⌊log₂ s⌋)` interpolation points, the recursion is the active call `callValue` with the +packing of Lemma D.3 at `a = slotBits s d`, `u = taper s d` and `h = ⌈3 M / u⌉`, and recursive +calls at depth `d + 1` for the children. -/ +theorem contractRec_callParams_eq_callValue {C s d n m p : ℕ} + {N : TensorNetwork B Bool (Fin n) (Fin m)} {side : Fin n → Bool} (hA : Active C s d m p) + (hAB : ActiveBounds C s d m p) (hN : N.RowsToColumnsLE side (degreeBound s)) + (hN₀ : 2 ^ (4 * Nat.log 2 s) ≤ N₀) : + contractRec B hB (callParams s) pts d n m N side p = + callValue B hB + (fun n' m' N' side' p' => + if m' < m then contractRec B hB (callParams s) pts (d + 1) n' m' N' side' p' + else N'.contraction) + N side hN.side_src hN.side_tgt (PacketPacking.packing N.src N.tgt (slotBits s d) 64) p + (taper s d) (taperStep s d m) (hAB.admissible hN₀).u_le_a + fun k : Fin (m * (2 * 2 ^ slotBits s d - 1) + 1) => + pts (Fin.castLE (hAB.admissible hN₀).points_lt k) := + contractRec_eq_callValue (callParams_of_lt hA.leafSize_lt) ⟨hN, hAB.admissible hN₀⟩ p + +variable {C s d n m p : ℕ} {N : TensorNetwork B Bool (Fin n) (Fin m)} {side : Fin n → Bool} + +/-- **The children of an active call have at most `M / 16` edges**, as `Active.child` requires +(Lemma D.3 (3) under (D.6), `TensorNetwork.mul_card_edges_child_callSplitting_le`). -/ +theorem sixteen_mul_card_edges_child_le (hAB : ActiveBounds C s d m p) + (hN : N.RowsToColumnsLE side (degreeBound s)) (hua : taper s d ≤ slotBits s d) {t : ℤ} + (ht : t ∈ recoveryNodes (slotBits s d)) (hq : 0 < taperMult (taper s d) (taperStep s d m) t) + (z : B) (g : Fin 64) : + 16 * Fintype.card + ({e // (callSplitting B hB N side hN.side_src hN.side_tgt + (PacketPacking.packing N.src N.tgt (slotBits s d) 64) p (taper s d) (taperStep s d m) + hua ht hq z).group (N.src e) = g} ⊕ + {e // (callSplitting B hB N side hN.side_src hN.side_tgt + (PacketPacking.packing N.src N.tgt (slotBits s d) 64) p (taper s d) (taperStep s d m) + hua ht hq z).group (N.tgt e) = g}) ≤ + m := by + have h := mul_card_edges_child_callSplitting_le B hB N side hN.side_src hN.side_tgt hN.src_le + hN.tgt_le (by rw [Fintype.card_fin]; exact hAB.degree_mul_pairs_sq_le) p (taper s d) + (taperStep s d m) hua ht hq z g + have := Fintype.card_fin m + omega + +/-- **The children of an active call are evaluated within the precision schedule**: a node of +positive multiplicity passes `p_t ≤ precisionBound C s (d + 1)` to its children. -/ +theorem nodePrecision_le_of_taperMult_pos (hAB : ActiveBounds C s d m p) {t : ℤ} + (hq : 0 < taperMult (taper s d) (taperStep s d m) t) : + nodePrecision p (taperStep s d m) (slotBits s d) (Fintype.card (Fin m)) (padicValInt 2 t) ≤ + precisionBound C s (d + 1) := by + rw [Fintype.card_fin] + exact hAB.nodePrecision_le _ _ (padicValInt_lt_of_taperMult_pos_left hq) (taperStep_mul_le s d m) + +omit [Algebra ℚ K] in +/-- **The mode count (D.15) at an active call**: at a node of positive multiplicity, there are at +most `2 ^ e_d` mode tuples for the packing of Lemma D.3, which has at most `3 M / L` packets. -/ +theorem card_modeBudget_callParams_le (hA : Active C s d m p) (hAB : ActiveBounds C s d m p) + (hN : N.RowsToColumnsLE side (degreeBound s)) {t : ℤ} + (hq : 0 < taperMult (taper s d) (taperStep s d m) t) : + #(modeBudget + (fun Z : Fin (PacketPacking.packing N.src N.tgt (slotBits s d) 64).numPackets × + Fin (2 ^ (padicValInt 2 t + 1)) × + Fin (nodePrecision p (taperStep s d m) (slotBits s d) (Fintype.card (Fin m)) + (padicValInt 2 t)) => (Z.2.2 : ℕ) + 1) + (nodePrecision p (taperStep s d m) (slotBits s d) (Fintype.card (Fin m)) + (padicValInt 2 t))) ≤ + 2 ^ branchExponent C s d := by + have hP := PacketPacking.numPackets_packing_mul_le N.src N.tgt (slotBits s d) 64 hN.src_le + hN.tgt_le (by rw [Fintype.card_fin]; exact hAB.degree_mul_pairs_sq_le) + (by rw [Fintype.card_fin]; exact hAB.slots_mul_pairs_le) + rw [Fintype.card_fin] at hP ⊢ + exact hAB.card_modeBudget_le hA (padicValInt_lt_of_taperMult_pos_left hq) + (taperStep_mul_le s d m) (by rwa [Fintype.card_fin]) + +end Active + +end Cslib.Circuits.Frontier.ContractionSchedule diff --git a/Complexity/Foundations/NumberTheory/Padics/AdjoinRootDigitLift.lean b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootDigitLift.lean new file mode 100644 index 0000000000..9d807df9aa --- /dev/null +++ b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootDigitLift.lean @@ -0,0 +1,117 @@ +/- +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/`) + +public import Complexity.Foundations.NumberTheory.Padics.AdjoinRootValuation +import Complexity.Foundations.RingTheory.AdjoinRoot +import Complexity.Foundations.RingTheory.GaloisRing + +/-! +# Digit lifts in `ℤ_(p)[X] / (f)` + +Let `p` be a prime and `f` a monic integer polynomial that is irreducible modulo `p`, and let +`O = ℤ_(p)[X] / (f)` be the valuation ring of `AdjoinRoot.padicValuation` in `K = ℚ[X] / (f)`. +The *digit lift* of a digit vector `c : Fin (deg f) → ZMod p` is `∑ i, c i * X ^ i` in `O`, with +each digit read as an integer in `{0, …, p - 1}` (`AdjoinRoot.integerDigitLift`). For `p = 2` +these are the binary-coordinate lifts of the residue-field elements of [OpenAI2026ETH] (§D.4.1, +p. 58). + +**Distinct digit lifts differ by a unit of `O`** (`AdjoinRoot.isUnit_integerDigitLift_sub`). The +difference of two lifts is the image of `∑ i, (c i - c' i) * X ^ i ∈ ℤ[X] / (f)`, which is nonzero +modulo `p` because the digit lifts reduce to distinct elements of `𝔽_p[X] / (f)` +(`GaloisRing.residue_digitLift_injective`). So it has valuation one +(`AdjoinRoot.padicValuation_map_eq_one_iff`), and is a unit of the valuation ring +(`AdjoinRoot.isUnit_of_padicValuation_eq_one`). This is the counterpart in `O` of +`GaloisRing.isUnit_digitLift_sub`, and it supplies the interpolation points of the contraction +recursion (`Cslib.Circuits.Frontier.TensorNetwork.exists_contractRec_eq_add`) over `B = O`. + +## Main definitions + +* `AdjoinRoot.integerDigitLift`: the digit lift of a digit vector, in `O`. + +## Main results + +* `AdjoinRoot.coe_integerDigitLift`: the digit lift is `∑ i, c i * X ^ i`. +* `AdjoinRoot.isUnit_integerDigitLift_sub`: distinct digit lifts differ by a unit of `O`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.1, p. 58. +-/ + +public section + +open Polynomial + +namespace AdjoinRoot + +variable {p : ℕ} [Fact p.Prime] {f : ℤ[X]} (hf : f.Monic) + (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) + +variable (p f) in +/-- The integer polynomial `∑ i, c i * X ^ i` of a digit vector, with each digit read as an +integer in `{0, …, p - 1}`. -/ +private noncomputable def digitPoly (c : Fin f.natDegree → ZMod p) : ℤ[X] := + ∑ i, C ((c i).val : ℤ) * X ^ (i : ℕ) + +/-- Modulo `p`, the digit polynomial is `∑ i, c i * X ^ i`. -/ +private theorem map_digitPoly (c : Fin f.natDegree → ZMod p) : + (digitPoly p f c).map (Int.castRingHom (ZMod p)) = ∑ i, C (c i) * X ^ (i : ℕ) := by + simp only [digitPoly, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, + Polynomial.map_pow, Polynomial.map_X] + simp only [eq_intCast, Int.cast_natCast, ZMod.natCast_zmod_val] + +include hf hirr + +/-- The image in `ℚ[X] / (f)` of the class of the digit polynomial lies in the valuation ring. -/ +private theorem map_mk_digitPoly_mem (c : Fin f.natDegree → ZMod p) : + map (Int.castRingHom ℚ) f _ dvd_rfl (mk f (digitPoly p f c)) ∈ + (padicValuation p hf hirr).integer := + padicValuation_map_le_one hf hirr _ + +/-- **The digit lift** of a digit vector `c`: the element `∑ i, c i * X ^ i` of the valuation ring +`O = ℤ_(p)[X] / (f)`, with each digit `c i ∈ ZMod p` read as an integer in `{0, …, p - 1}`. For +`p = 2` these are the binary-coordinate lifts of [OpenAI2026ETH] (§D.4.1, p. 58). -/ +noncomputable def integerDigitLift (c : Fin f.natDegree → ZMod p) : + (padicValuation p hf hirr).integer := + ⟨_, map_mk_digitPoly_mem hf hirr c⟩ + +/-- The digit lift is `∑ i, c i * X ^ i` in `ℚ[X] / (f)`. -/ +theorem coe_integerDigitLift (c : Fin f.natDegree → ZMod p) : + (integerDigitLift hf hirr c : AdjoinRoot (f.map (Int.castRingHom ℚ))) = + ∑ i, ((c i).val : AdjoinRoot (f.map (Int.castRingHom ℚ))) * root _ ^ (i : ℕ) := by + simp only [integerDigitLift, digitPoly, map_sum, map_mul, map_pow, mk_X, map_natCast, map_root] + +/-- **Distinct digit lifts differ by a unit of `O`**: the difference reduces modulo `p` to a +nonzero element of `𝔽_p[X] / (f)`, so it has valuation one. -/ +theorem isUnit_integerDigitLift_sub {c c' : Fin f.natDegree → ZMod p} (h : c ≠ c') : + IsUnit (integerDigitLift hf hirr c - integerDigitLift hf hirr c') := by + have hx : ((integerDigitLift hf hirr c - integerDigitLift hf hirr c' : + (padicValuation p hf hirr).integer) : AdjoinRoot (f.map (Int.castRingHom ℚ))) = + map (Int.castRingHom ℚ) f _ dvd_rfl (mk f (digitPoly p f c - digitPoly p f c')) := by + rw [map_sub, map_sub] + rfl + have h1 : padicValuation p hf hirr + ((integerDigitLift hf hirr c - integerDigitLift hf hirr c' : + (padicValuation p hf hirr).integer) : AdjoinRoot (f.map (Int.castRingHom ℚ))) = 1 := by + rw [hx, padicValuation_map_eq_one_iff hf hirr, map_mk, Polynomial.map_sub, map_digitPoly, + map_digitPoly, map_sub, sub_ne_zero] + intro heq + refine h (GaloisRing.residue_digitLift_injective (n := 1) hf ?_) + simp only [GaloisRing.residue_digitLift] + exact heq + exact isUnit_of_padicValuation_eq_one hf hirr _ h1 + +/-- **Digit lifts are interpolation points**: distinct digit vectors have lifts with unit +differences. -/ +theorem pairwise_isUnit_integerDigitLift_sub : + Pairwise fun c c' : Fin f.natDegree → ZMod p => + IsUnit (integerDigitLift hf hirr c - integerDigitLift hf hirr c') := + fun _ _ h => isUnit_integerDigitLift_sub hf hirr h + +end AdjoinRoot diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkActiveCall.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkActiveCall.lean index dd0a261b1e..d75f5cbbe8 100644 --- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkActiveCall.lean +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkActiveCall.lean @@ -55,14 +55,14 @@ def packing : Cslib.PacketPacking.Packing net.src net.tgt 1 2 where labels_eq e i := by fin_cases e <;> fin_cases i <;> decide example (e : Fin 2) : - (packingGroup net side packing 0 (net.src e), packingGroup net side packing 0 (net.tgt e)) = + (packingGroup side packing 0 (net.src e), packingGroup side packing 0 (net.tgt e)) = if (packing.slot e : ℕ).testBit 0 then (packing.symbols (packing.packet e) 0).swap else packing.symbols (packing.packet e) 0 := - packingGroup_src_tgt net side (fun e => by fin_cases e <;> decide) + packingGroup_src_tgt side (fun e => by fin_cases e <;> decide) (fun e => by fin_cases e <;> decide) packing 0 e -example : Finset.card {e | packingGroup net side packing 0 (net.src e) = 1} = 1 := by - rw [card_packingGroup_src net side (fun e => by fin_cases e <;> decide)] +example : Finset.card {e | packingGroup side packing 0 (net.src e) = 1} = 1 := by + rw [card_packingGroup_src side (fun e => by fin_cases e <;> decide)] decide /-- **Child invariants.** For any mode splitting of `net` along the packets of `packing`, a packet diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkRecursion.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkRecursion.lean new file mode 100644 index 0000000000..624befa8db --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkRecursion.lean @@ -0,0 +1,182 @@ +/- +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.ScheduledRecursion +import Complexity.Foundations.NumberTheory.Padics.AdjoinRootDigitLift +import Mathlib.Algebra.Field.ZMod +import Mathlib.Algebra.Polynomial.SpecificDegree +import Mathlib.Tactic.ComputeDegree +import Mathlib.Tactic.FinCases + +/-! +# Tests for the contraction recursion + +* **Renaming and lifting.** Renaming a two-edge network along a rotation of its vertices and a + swap of its edges keeps its contraction, and the canonical lift of a network over `ℤ / 4` to `ℤ` + (integer representatives in `{0, 1, 2, 3}`) reduces back to it. +* **Interpolation points in `O`.** For `f = U ^ 2 + U + 1`, the four binary-coordinate lifts in + `O = ℤ_(2)[U] / (f)` have unit differences, and `ℤ_(2)` lies in `O`. +* **Correctness of the recursion over `O`**, with those four points and a constant schedule + `a = u = 1`, `h = 3`. On a one-edge network these parameters are admissible (`3 M ≤ h u ≤ 3 M + u` + and `M (2 L - 1) = 3 < 4`), so the root call is active (`contractRec_eq_callValue`); its children + are not smaller and are evaluated directly. Without parameters the call is a leaf. +* **The scheduled recursion** (`ContractionSchedule.callParams`): small calls are leaves, the + recursion is correct, and for large `s` the parameters of every active call are admissible. +-/ + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.Recursion + +open Polynomial Cslib.Circuits.Frontier TensorNetwork + +/-! ### Renaming and lifting -/ + +/-- Edge `e` runs from row `e` to column `e + 2`; the tensor at `v` is `v + 1` when its edge +carries `true`, and `1` otherwise. -/ +def net : TensorNetwork ℤ Bool (Fin 4) (Fin 2) where + src e := ⟨e.val, by omega⟩ + tgt e := ⟨e.val + 2, by omega⟩ + tensor v x := if x ⟨v.val % 2, by omega⟩ then v.val + 1 else 1 + tensor_congr v x y h := by + rw [h ⟨v.val % 2, by omega⟩ (by fin_cases v <;> decide)] + +/-- Renaming the vertices by a rotation and the edges by a swap keeps the contraction. -/ +example : (net.reindex (finRotate 4) (Equiv.swap 0 1)).contraction = net.contraction := + contraction_reindex _ _ _ + +/-- The same network over `ℤ / 4`. -/ +def net₄ : TensorNetwork (ZMod 4) Bool (Fin 4) (Fin 2) := + net.map (Int.castRingHom (ZMod 4)) + +/-- The canonical lift of `net₄` to `ℤ`, by the integer representatives in `{0, …, 3}`, reduces +to `net₄`, so its contraction reduces to the contraction of `net₄`. -/ +example : (net₄.mapFun fun x => (x.val : ℤ)).map (Int.castRingHom (ZMod 4)) = net₄ := + map_mapFun _ (fun x => by simp) _ + +/-! ### Interpolation points in `O = ℤ_(2)[U] / (U ^ 2 + U + 1)` -/ + +/-- `U ^ 2 + U + 1`, irreducible modulo 2. -/ +noncomputable def f : ℤ[X] := X ^ 2 + X + 1 + +theorem f_monic : f.Monic := by unfold f; monicity! + +theorem f_natDegree : f.natDegree = 2 := by unfold f; compute_degree! + +theorem f_irreducible : Irreducible (f.map (Int.castRingHom (ZMod 2))) := by + unfold f + simp only [Polynomial.map_add, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_one] + refine Polynomial.irreducible_of_degree_le_three_of_not_isRoot ?_ ?_ + · have : (X ^ 2 + X + 1 : (ZMod 2)[X]).natDegree = 2 := by compute_degree! + simp [this] + · intro x hx + rw [IsRoot.def, eval_add, eval_add, eval_pow, eval_X, eval_one] at hx + fin_cases x <;> revert hx <;> decide + +/-- The field `K = ℚ[U] / (U ^ 2 + U + 1)`. -/ +abbrev K : Type := AdjoinRoot (f.map (Int.castRingHom ℚ)) + +/-- The ring `O = ℤ_(2)[U] / (U ^ 2 + U + 1)`, the valuation ring of `K`. -/ +noncomputable abbrev O : Subring K := (AdjoinRoot.padicValuation 2 f_monic f_irreducible).integer + +/-- `ℤ_(2)` lies in `O`: the valuation of `K` extends that of `ℚ`. -/ +theorem hO : ∀ c ∈ Valuation.integer (Rat.padicValuation 2), algebraMap ℚ K c ∈ O := fun c hc => by + rw [Valuation.mem_integer_iff, AdjoinRoot.padicValuation_algebraMap] + exact hc + +/-- There are `2 ^ 2 = 4` digit vectors. -/ +theorem card_digits : Fintype.card (Fin f.natDegree → ZMod 2) = 4 := by + rw [Fintype.card_fun, ZMod.card, Fintype.card_fin, f_natDegree] + norm_num + +/-- The four binary-coordinate lifts `0, 1, U, 1 + U`, in some order. -/ +noncomputable def pts (k : Fin 4) : O := + AdjoinRoot.integerDigitLift f_monic f_irreducible + ((Fintype.equivFin (Fin f.natDegree → ZMod 2)).symm (Fin.cast card_digits.symm k)) + +/-- **The binary-coordinate lifts are interpolation points**: their differences are units of `O`. -/ +theorem pts_pairwise : Pairwise fun k l => IsUnit (pts k - pts l) := fun _ _ hkl => + AdjoinRoot.pairwise_isUnit_integerDigitLift_sub f_monic f_irreducible fun h => + hkl (Fin.cast_injective _ ((Fintype.equivFin _).symm.injective h)) + +/-! ### The recursion over `O` -/ + +/-- Direct contraction is a correct oracle. -/ +example : ContractionOracle.Correct (B := O) fun _ _ N _ _ => N.contraction := + fun _ _ _ _ _ => ⟨0, by simp⟩ + +/-- The constant schedule `a = u = 1`, `h = 3`, with degree bound `1`. -/ +def sched (_ _ : ℕ) : Option TensorNetwork.CallParams := some ⟨1, 1, 3, 1⟩ + +/-- On one edge with four points the schedule is admissible. -/ +example : (TensorNetwork.CallParams.mk 1 1 3 1).Admissible 1 4 := by decide + +/-- One edge from row `0` to column `1`, with tensor `(1, 2)` at the row and `(1, 1)` at the +column. -/ +noncomputable def net₁ : TensorNetwork O Bool (Fin 2) (Fin 1) where + src _ := 0 + tgt _ := 1 + tensor v x := if v = 0 ∧ x 0 then 2 else 1 + tensor_congr v x y h := by rw [h 0 (by fin_cases v <;> simp)] + +/-- **The root call is active**: it is the active call of `callValue` with the packing of +Lemma D.3, the four lifts as interpolation points, and recursive calls at depth one for the +children with fewer edges. -/ +example (p : ℕ) : + contractRec O hO sched pts 0 2 1 net₁ (fun v => decide (v = 0)) p = + callValue O hO + (fun n' m' N' side' p' => + if m' < 1 then contractRec O hO sched pts 1 n' m' N' side' p' else N'.contraction) + net₁ (fun v => decide (v = 0)) (fun _ => rfl) (fun _ => rfl) + (Cslib.PacketPacking.packing net₁.src net₁.tgt 1 64) p 1 3 le_rfl pts := + contractRec_eq_callValue (θ := ⟨1, 1, 3, 1⟩) rfl + ⟨⟨fun _ => rfl, fun _ => rfl, fun _ => (Finset.card_filter_le _ _).trans (by simp), + fun _ => (Finset.card_filter_le _ _).trans (by simp)⟩, by decide⟩ p + +/-- With no parameters, a call is a leaf and returns the contraction. -/ +example (p : ℕ) : + contractRec O hO (fun _ _ => none) pts 0 2 1 net₁ (fun v => decide (v = 0)) p = + net₁.contraction := + contractRec_of_sched_eq_none rfl p + +/-- **The recursion is correct**: at every precision, the root call returns the contraction of +`net₁` modulo `2 ^ p`. -/ +example (p : ℕ) : + Ideal.Quotient.mk (twoPowIdeal O p) + (contractRec O hO sched pts 0 2 1 net₁ (fun v => decide (v = 0)) p) = + Ideal.Quotient.mk (twoPowIdeal O p) net₁.contraction := + mk_contractRec O hO sched pts pts_pairwise 0 2 1 net₁ _ p + +/-- The recursion is correct for every schedule and every network. -/ +example (sched' : ℕ → ℕ → Option TensorNetwork.CallParams) (n m p : ℕ) + (N : TensorNetwork O Bool (Fin n) (Fin m)) (side : Fin n → Bool) : + ∃ c : O, contractRec O hO sched' pts 0 n m N side p = N.contraction + 2 ^ p * c := + exists_contractRec_eq_add O hO sched' pts pts_pairwise 0 n m N side p + +/-! ### The scheduled recursion -/ + +open Cslib.Circuits.Frontier.ContractionSchedule in +/-- With the parameter schedule, a call with at most `leafSize s` edges is a leaf. -/ +example (s n m p : ℕ) (hm : m ≤ leafSize s) (N : TensorNetwork O Bool (Fin n) (Fin m)) + (side : Fin n → Bool) : + contractRec O hO (callParams s) pts 0 n m N side p = N.contraction := + contractRec_of_sched_eq_none (callParams_of_le hm) p + +open Cslib.Circuits.Frontier.ContractionSchedule in +/-- With the parameter schedule, the recursion is correct. -/ +example (s n m p : ℕ) (N : TensorNetwork O Bool (Fin n) (Fin m)) (side : Fin n → Bool) : + ∃ c : O, contractRec O hO (callParams s) pts 0 n m N side p = N.contraction + 2 ^ p * c := + exists_contractRec_eq_add O hO (callParams s) pts pts_pairwise 0 n m N side p + +open Cslib.Circuits.Frontier.ContractionSchedule in +/-- For large `s`, the parameters of every active call are admissible with `2 ^ (4 ⌊log₂ s⌋)` +points, so its guard reduces to the network running from rows to columns within the degree +bound. -/ +example (C : ℕ) : ∃ s₀, ∀ s, s₀ ≤ s → ∀ d M p, Active C s d M p → + (TensorNetwork.CallParams.mk (slotBits s d) (taper s d) (taperStep s d M) + (degreeBound s)).Admissible M (2 ^ (4 * Nat.log 2 s)) := by + obtain ⟨s₀, hs₀⟩ := exists_activeBounds C + exact ⟨s₀, fun s hs d M p hA => ((hs₀ s hs).2 d M p hA).admissible le_rfl⟩ + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.Recursion