diff --git a/Complexity.lean b/Complexity.lean index ce9efdf650..f6e3b68073 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -899,6 +899,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectCont public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContraction public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionMachine +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionPolyTime public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates public import Complexity.Computability.Circuit.Frontier.TensorNetwork.KernelProduct @@ -906,6 +907,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.LocalDefor public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeCall public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeChild +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeChildPolyTime public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeRecovery public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketEntry public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketEvaluator diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean index e0d0e1a0da..decff167be 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean @@ -14,6 +14,8 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Li import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.PolyTime.GaloisRingUnits +import Complexity.Foundations.NumberTheory.Padics.AdjoinRootDigitLift import Mathlib.Data.List.GetD import Mathlib.Data.List.Sort @@ -30,6 +32,9 @@ for. and reducing the lift modulo `2 ^ p` gives the value of `c` in `A_p` (`GaloisRingArith.reduction_liftO`). This is the canonical lifting of representatives of §D.4.1 (p. 58): a retained vertex is read through the lift of its entry at every later precision. + Lifts of distinct lists with binary coordinates differ by a unit + (`GaloisRingArith.isUnit_liftO_sub`); in particular the binary digits of `0, …, n - 1` are + interpolation points when `n ≤ 2 ^ e` (`GaloisRingArith.pairwise_isUnit_liftO_sub_digits`). * **Rows first.** A described network is *rows-first bipartite* at `r` (`DescribedNetwork.IsRowsFirstBipartite`, the condition of `ExplicitTensorNetwork.IsRowsFirstBipartite`) when every port names an edge and every edge is a @@ -55,6 +60,8 @@ for. ## Main results * `Cslib.GaloisRingArith.reduction_liftO`, `Cslib.GaloisRingArith.mk_liftO`: reducing a lift. +* `Cslib.GaloisRingArith.isUnit_liftO_sub`, + `Cslib.GaloisRingArith.pairwise_isUnit_liftO_sub_digits`: binary lists as interpolation points. * `Cslib.Circuits.Frontier.DescribedNetwork.incident_eq`: the vertices at an edge. * `Cslib.Circuits.Frontier.DescribedNetwork.contraction_toNetwork`, `Cslib.Circuits.Frontier.DescribedNetwork.reduction_contraction_toNetwork`: the contraction. @@ -115,6 +122,73 @@ theorem mk_liftO (p : ℕ) (c : List ℕ) : Cslib.Circuits.Frontier.reductionLift (monic_monicOf fl) hirr p (val p fl c) := by rw [← reduction_liftO hirr p, Cslib.Circuits.Frontier.reductionLift_reduction] +/-! ### Binary lists as interpolation points -/ + +/-- A lift of a list with binary coordinates is a digit lift. -/ +private theorem liftO_eq_integerDigitLift {c : List ℕ} (hc : ∀ i < fl.length, c.getD i 0 < 2) : + liftO hirr c = AdjoinRoot.integerDigitLift (monic_monicOf fl) hirr + fun i => ((c.getD i 0 : ℕ) : ZMod 2) := by + apply Subtype.ext + rw [AdjoinRoot.coe_integerDigitLift, Fin.sum_univ_eq_sum_range + (fun i => ((((c.getD i 0 : ℕ) : ZMod 2)).val : AdjoinRoot ((monicOf fl).map + (Int.castRingHom ℚ))) * AdjoinRoot.root _ ^ i), natDegree_monicOf, liftO] + push_cast + refine Finset.sum_congr rfl fun i hi => ?_ + rw [ZMod.val_natCast, Nat.mod_eq_of_lt (hc i (mem_range.mp hi))] + exact congrArg (_ * · ^ i) (AdjoinRoot.map_root _ _ _ _) + +/-- **Lifts of distinct binary lists differ by a unit.** If two lists have binary coordinates +below `e = fl.length` and differ at one of them, their lifts to `O` differ by a unit: they are +digit lifts (`AdjoinRoot.isUnit_integerDigitLift_sub`). -/ +theorem isUnit_liftO_sub {c c' : List ℕ} (hc : ∀ i < fl.length, c.getD i 0 < 2) + (hc' : ∀ i < fl.length, c'.getD i 0 < 2) + (hne : ∃ i < fl.length, c.getD i 0 ≠ c'.getD i 0) : + IsUnit (liftO hirr c - liftO hirr c') := by + rw [liftO_eq_integerDigitLift hirr hc, liftO_eq_integerDigitLift hirr hc'] + refine AdjoinRoot.isUnit_integerDigitLift_sub _ hirr fun h => ?_ + obtain ⟨i, hi, hne⟩ := hne + have h2 := congrArg ZMod.val (congrFun h ⟨i, by rwa [natDegree_monicOf]⟩) + rw [ZMod.val_natCast, ZMod.val_natCast, Nat.mod_eq_of_lt (hc i hi), + Nat.mod_eq_of_lt (hc' i hi)] at h2 + exact hne h2 + +/-- Coordinate `i < e` of the binary digits of `k` below `e`. -/ +theorem getD_map_testBit (e k i : ℕ) (hi : i < e) : + ((List.range e).map fun j => if k.testBit j then 1 else 0).getD i 0 = + if k.testBit i then 1 else 0 := by + rw [List.getD_eq_getElem _ _ (by simpa using hi), List.getElem_map, List.getElem_range] + +/-- **Binary-digit points are interpolation points.** The lists of the binary digits below +`e = fl.length` of `0, …, n - 1`, for `n ≤ 2 ^ e`, have lifts to `O` with unit differences. -/ +theorem pairwise_isUnit_liftO_sub_digits {n : ℕ} (hn : n ≤ 2 ^ fl.length) : + Pairwise fun i j : Fin ((List.range n).map fun k => + (List.range fl.length).map fun j => if k.testBit j then 1 else 0).length => + IsUnit (liftO hirr (((List.range n).map fun k => + (List.range fl.length).map fun j => if k.testBit j then 1 else 0).getD i []) - + liftO hirr (((List.range n).map fun k => + (List.range fl.length).map fun j => if k.testBit j then 1 else 0).getD j [])) := by + intro i j hij + have hi : (i : ℕ) < n := by simpa using i.2 + have hj : (j : ℕ) < n := by simpa using j.2 + rw [List.getD_eq_getElem _ _ i.2, List.getD_eq_getElem _ _ j.2, List.getElem_map, + List.getElem_map, List.getElem_range, List.getElem_range] + have hbin (k : ℕ) : ∀ b < fl.length, + ((List.range fl.length).map fun j => if k.testBit j then 1 else 0).getD b 0 < 2 := by + intro b hb + rw [getD_map_testBit _ _ _ hb] + split <;> omega + refine isUnit_liftO_sub hirr (hbin _) (hbin _) ?_ + by_contra hall + simp only [not_exists, not_and, not_not] at hall + refine hij (Fin.ext (Nat.eq_of_testBit_eq fun b => ?_)) + rcases lt_or_ge b fl.length with hb | hb + · have := hall b hb + rw [getD_map_testBit _ _ _ hb, getD_map_testBit _ _ _ hb] at this + revert this + cases (i : ℕ).testBit b <;> cases (j : ℕ).testBit b <;> simp + · have h2 : 2 ^ fl.length ≤ 2 ^ b := Nat.pow_le_pow_right (by norm_num) hb + rw [Nat.testBit_lt_two_pow (by omega), Nat.testBit_lt_two_pow (by omega)] + end Cslib.GaloisRingArith namespace Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContraction.lean index 915b801846..aab15a930b 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContraction.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContraction.lean @@ -162,9 +162,26 @@ theorem edges_lt_bound_of_active {x : Call} (h : active x = true) : x.edges < x. @[expose] def nodePrec (i : ℕ) : ℕ := nodePrecision x.prec (step x) (slots x) x.edges (level x ((nodes x).getD i 0)) -/-- **The packing of Lemma D.3**, natively (`nativeParentPacking`, `r = 64`). -/ +/-- The number of rows capped at the number of vertices. The packing and the child builder use it +in place of the number of rows: it changes nothing for a rows-first network with an edge +(`FastContraction.rowCap_eq`), and it keeps them polynomial-time on every call, since the number +of rows is stored in binary and the packing lists one word per row. -/ +@[expose] def rowCap : ℕ := min x.rows x.net.vertices.length + +/-- The cap on the rows is inactive when there are at most as many rows as vertices. -/ +theorem rowCap_eq {x : Call} (h : x.rows ≤ x.net.vertices.length) : rowCap x = x.rows := + min_eq_left h + +/-- **The packing of Lemma D.3**, natively (`nativeParentPacking`, `r = 64`), with the rows +capped (`FastContraction.rowCap`). -/ @[expose] def packing : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ) := - nativeParentPacking x.rows (slots x) x.net + nativeParentPacking (rowCap x) (slots x) x.net + +/-- The packing is the native packing of the rows when there are at most as many rows as +vertices. -/ +theorem packing_eq {x : Call} (h : x.rows ≤ x.net.vertices.length) : + packing x = nativeParentPacking x.rows (slots x) x.net := by + rw [packing, rowCap_eq h] /-- **The weights of the modes of the `i`-th node**, packet-major over `(q, y₀, b)` with `y₀ < 2 ^ (v₂ t + 1)` and `b < p_t`: mode `(q, y₀, b)` has weight `b + 1`. -/ diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionPolyTime.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionPolyTime.lean new file mode 100644 index 0000000000..4d83637e21 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionPolyTime.lean @@ -0,0 +1,872 @@ +/- +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.FastContractionMachine +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeChildPolyTime +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep +import Complexity.Computability.PolyTime.BudgetTuples +import Complexity.Computability.PolyTime.GaloisRingArithmetic +import Complexity.Computability.PolyTime.GaloisRingSeries +import Mathlib.Data.List.GetD +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.SqrtLog +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Sqrt +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPower +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeRadix + +/-! +# The components of the native contraction recursion in polynomial time + +The scheme `Cslib.Circuits.Frontier.FastContraction.scheme mk` of the contraction recursion of +[OpenAI2026ETH] has polynomial-time components (`Cslib.GenericRAM.StackRecursion.Scheme.PolyTime`) +for the encodings `FastContraction.encCall`, `encFrame` and `encValue` whenever the child builder +`mk` is polynomial-time (`FastContraction.scheme_polyTime`). The native child builder is +(`FastContraction.nativeMk_polyTime`), so the scheme of `FastContraction.nativeMk` has +polynomial-time components (`FastContraction.scheme_nativeMk_polyTime`). + +**Every call.** The components compute the data of a call on every call and every frame, not only +on the active calls and the cursor's states. The scale `s`, the depth, the edge bound, the +precision and the number `M` of edges are in unary, so the schedule's quantities are polynomial in +the input: +* `a = slotBits s d ≤ ⌊log₂ s⌋ / 32768`, so `2 ^ a ≤ s + 1` + (`ContractionSchedule.two_pow_slotBits_le`); +* the multiplicity step `h = ⌈3 M / u⌉` is at most `3 M + u`; +* every level is at most `a + 1` (`FastContraction.level_le`), so a node has at most `4 (s + 1)` + tiles; +* the native packing has at most `M (2 ^ a) ^ 12` packets + (`NativeChild.numPackets_nativeParentPacking_le`), which bounds the mode weights and the + cursor's exponent tuples. + +The number of rows and the cursor's exponents are stored in binary, so the packing and the child +builder cap them, at the number of vertices (`FastContraction.rowCap`) and at the node's precision. +The caps change nothing on well-formed active calls (`FastContraction.nativeMk_eq`). + +## Main results + +* `Cslib.Circuits.Frontier.ContractionSchedule.taper_polyTime`, + `Cslib.Circuits.Frontier.ContractionSchedule.slotBits_polyTime`, + `Cslib.Circuits.Frontier.ContractionSchedule.taperStep_polyTime`, + `Cslib.Circuits.Frontier.ContractionSchedule.leafSize_polyTime`, + `Cslib.Circuits.Frontier.ContractionSchedule.degreeBound_polyTime`: the schedule. +* `Cslib.Circuits.Frontier.FastContraction.active_polyTime`, `nodePrec_polyTime`, + `packets_polyTime`, `weights_polyTime`, `points_polyTime`, `table_polyTime`: the data of a call. +* `Cslib.Circuits.Frontier.FastContraction.scheme_polyTime`: the components of the scheme, for a + polynomial-time child builder. +* `Cslib.Circuits.Frontier.FastContraction.nativeMk_polyTime`, + `Cslib.Circuits.Frontier.FastContraction.scheme_nativeMk_polyTime`: the native child builder and + the components of its scheme. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH]. +-/ + +public section + +open Turing.MultiTapeTM + +namespace Cslib.Circuits.Frontier.ContractionSchedule + +/-! ### The schedule -/ + +/-- `⌊log₂ s⌋` in unary from `s` in unary. -/ +private theorem log_polyTime : ComputableInPolyTime (Nat.log 2) encUnary encUnary := + ComputableInPolyTime.binary_log_two.comp ComputableInPolyTime.unary_to_binary + +/-- **The taper is polynomial-time**, in unary from the scale and the depth in unary. -/ +theorem taper_polyTime : ComputableInPolyTime (fun q : ℕ × ℕ => taper q.1 q.2) + (encPair encUnary encUnary) encUnary := by + have hlog := log_polyTime.comp (ComputableInPolyTime.fst encUnary encUnary) + exact ComputableInPolyTime.binary_to_unary_bounded + (ComputableInPolyTime.binary_div.comp ((ComputableInPolyTime.unary_to_binary.comp hlog).prod + (ComputableInPolyTime.binary_two_pow.comp (ComputableInPolyTime.unary_add' + (ComputableInPolyTime.const 17) (ComputableInPolyTime.snd encUnary encUnary))))) + hlog fun q => Nat.div_le_self _ _ + +/-- A sum over `Finset.range` as the sum of a list. -/ +private theorem sum_range_eq_list (f : ℕ → ℕ) (n : ℕ) : + ∑ j ∈ Finset.range n, f j = ((List.range n).map f).sum := by + induction n with + | zero => simp + | succ n ih => + rw [Finset.sum_range_succ, List.range_succ, List.map_append, List.sum_append, ih] + simp + +/-- **The number of label coordinates is polynomial-time**, in unary from the scale and the depth +in unary. -/ +theorem slotBits_polyTime : ComputableInPolyTime (fun q : ℕ × ℕ => slotBits q.1 q.2) + (encPair encUnary encUnary) encUnary := by + have hd := ComputableInPolyTime.snd encUnary encUnary + have hlog := log_polyTime.comp (ComputableInPolyTime.fst encUnary encUnary) + have hterm : ComputableInPolyTime (fun p : (ℕ × ℕ) × ℕ => taper p.1.1 p.2) + (encPair (encPair encUnary encUnary) encUnary) encNat := + ComputableInPolyTime.unary_to_binary.comp (taper_polyTime.comp + (((ComputableInPolyTime.fst encUnary encUnary).comp (ComputableInPolyTime.fst _ _)).prod + (ComputableInPolyTime.snd _ _))) + have hterms : ComputableInPolyTime (fun q : ℕ × ℕ => (List.range (q.2 + 1)).map (taper q.1)) + (encPair encUnary encUnary) (encList encNat) := + ComputableInPolyTime.mapWithInput (f := fun q j => taper q.1 j) + (ComputableInPolyTime.range.comp + (ComputableInPolyTime.unary_add' hd (ComputableInPolyTime.const 1))) hterm + have hsum := (ComputableInPolyTime.of_tidy ComputableTidilyInPolyTime.binary_sum).comp hterms + have hval (q : ℕ × ℕ) : slotBits q.1 q.2 = 2 * ((List.range (q.2 + 1)).map (taper q.1)).sum := by + simp only [slotBits, prefixBits, sum_range_eq_list] + refine (ComputableInPolyTime.binary_to_unary_bounded + (ComputableInPolyTime.binary_mul' (ComputableInPolyTime.const 2) hsum) hlog + fun q => ?_).of_enc_eq fun q => ?_ + · simp only [Function.comp_apply, ← hval] + exact (slotBits_le q.1 q.2).trans (Nat.div_le_self _ _) + · simp only [Function.comp_apply, hval] + +/-- `2 ^ a ≤ s + 1` for the number `a = slotBits s d` of label coordinates. -/ +theorem two_pow_slotBits_le (s d : ℕ) : 2 ^ slotBits s d ≤ s + 1 := by + have ha := slotBits_le s d + rcases Nat.eq_zero_or_pos s with rfl | hs + · simp only [Nat.log_zero_right, Nat.zero_div, Nat.le_zero] at ha + simp [ha] + · calc 2 ^ slotBits s d ≤ 2 ^ Nat.log 2 s := + Nat.pow_le_pow_right (by norm_num) (ha.trans (Nat.div_le_self _ _)) + _ ≤ s := Nat.pow_log_le_self 2 hs.ne' + _ ≤ s + 1 := Nat.le_succ s + +/-- **The multiplicity step is polynomial-time**, in unary from the scale, the depth and the number +of edges in unary. -/ +theorem taperStep_polyTime : + ComputableInPolyTime (fun q : ℕ × ℕ × ℕ => taperStep q.1 q.2.1 q.2.2) + (encPair encUnary (encPair encUnary encUnary)) encUnary := by + have hs := ComputableInPolyTime.fst encUnary (encPair encUnary encUnary) + have hr := ComputableInPolyTime.snd encUnary (encPair encUnary encUnary) + have hd := (ComputableInPolyTime.fst encUnary encUnary).comp hr + have hM := (ComputableInPolyTime.snd encUnary encUnary).comp hr + have hu := taper_polyTime.comp (hs.prod hd) + exact ComputableInPolyTime.unary_div.comp ((ComputableInPolyTime.unary_sub' + (ComputableInPolyTime.unary_add' (ComputableInPolyTime.unary_mul' + (ComputableInPolyTime.const 3) hM) hu) (ComputableInPolyTime.const 1)).prod hu) + +/-- **The leaf size is polynomial-time**, in unary from the scale in unary. -/ +theorem leafSize_polyTime : ComputableInPolyTime leafSize encUnary encUnary := + ComputableInPolyTime.binary_to_unary_bounded + (ComputableInPolyTime.binary_div.comp (ComputableInPolyTime.unary_to_binary.prod + (ComputableInPolyTime.binary_sqrt' (ComputableInPolyTime.unary_to_binary.comp log_polyTime)))) + (ComputableInPolyTime.id' (encIn := encUnary)) fun _ => Nat.div_le_self _ _ + +/-- **The degree bound is polynomial-time**: `2 ^ (9 ⌊log₂ s⌋ / 10 + 2)` in binary from `s` in +unary. -/ +theorem degreeBound_polyTime : ComputableInPolyTime degreeBound encUnary encNat := by + have hb := ComputableInPolyTime.unary_to_binary + have hlog := ComputableInPolyTime.binary_log_two.comp hb + have he : ComputableInPolyTime (fun m => 9 * Nat.log 2 m / 10 + 2) encUnary encUnary := + ComputableInPolyTime.binary_to_unary_bounded + (ComputableInPolyTime.binary_add.comp ((ComputableInPolyTime.binary_div.comp + ((ComputableInPolyTime.binary_mul' (ComputableInPolyTime.const 9) (hb.comp hlog)).prod + (ComputableInPolyTime.const 10))).prod (ComputableInPolyTime.const 2))) + (ComputableInPolyTime.unary_add' hlog (ComputableInPolyTime.const 2)) fun m => by + simp only [Function.comp_apply]; omega + exact ComputableInPolyTime.binary_two_pow.comp he + +end Cslib.Circuits.Frontier.ContractionSchedule + +namespace Cslib.Circuits.Frontier.FastContraction + +open GaloisRingArith ChildCursor NativeRecovery ContractionSchedule NativeChild + Cslib.GenericRAM Cslib.GenericRAM.StackRecursion + +/-! ### The parameters of a call -/ + +/-- The scale is polynomial-time. -/ +theorem scale_polyTime : ComputableInPolyTime Call.scale encCall encUnary := by + unfold Call.scale; fun_prop + +/-- The edge bound is polynomial-time. -/ +theorem bound_polyTime : ComputableInPolyTime Call.bound encCall encUnary := by + unfold Call.bound; fun_prop + +/-- The precision is polynomial-time. -/ +theorem prec_polyTime : ComputableInPolyTime Call.prec encCall encUnary := by + unfold Call.prec; fun_prop + +/-- The coefficients of the modulus are polynomial-time. -/ +theorem fl_polyTime : ComputableInPolyTime Call.fl encCall (encList encNat) := by + unfold Call.fl; fun_prop + +/-- The number of rows is polynomial-time. -/ +theorem rows_polyTime : ComputableInPolyTime Call.rows encCall encNat := by + unfold Call.rows; fun_prop + +/-- The network is polynomial-time. -/ +theorem net_polyTime : + ComputableInPolyTime Call.net encCall (DescribedNetwork.encDescribed VertexDesc.enc) := by + unfold Call.net; fun_prop + +/-- The number of edges is polynomial-time, in unary. -/ +theorem edges_polyTime : ComputableInPolyTime Call.edges encCall encUnary := + DescribedNetwork.numEdges_polyTime.comp net_polyTime + +/-- The vertices are polynomial-time. -/ +theorem vertices_polyTime : ComputableInPolyTime (fun x : Call => x.net.vertices) encCall + (encList (encPair (encList encNat) VertexDesc.enc)) := + DescribedNetwork.vertices_polyTime.comp net_polyTime + +/-! ### The schedule of a call -/ + +/-- The number of label coordinates is polynomial-time. -/ +theorem slots_polyTime : ComputableInPolyTime slots encCall encUnary := + slotBits_polyTime.comp (scale_polyTime.prod depth_polyTime) + +/-- `2 ^ a ≤ s + 1` at every call. -/ +theorem two_pow_slots_le (x : Call) : 2 ^ slots x ≤ x.scale + 1 := two_pow_slotBits_le _ _ + +/-- The number `2 ^ a` of slots is polynomial-time, in unary. -/ +theorem twoPowSlots_polyTime : ComputableInPolyTime (fun x => 2 ^ slots x) encCall encUnary := + ComputableInPolyTime.binary_to_unary_bounded + (ComputableInPolyTime.binary_two_pow.comp slots_polyTime) + (ComputableInPolyTime.unary_add' scale_polyTime (ComputableInPolyTime.const 1)) + two_pow_slots_le + +/-- The number `2 ^ (a + 1)` of grid indices is polynomial-time, in unary. -/ +theorem twoPowSlotsSucc_polyTime : + ComputableInPolyTime (fun x => 2 ^ (slots x + 1)) encCall encUnary := + (ComputableInPolyTime.unary_add' twoPowSlots_polyTime twoPowSlots_polyTime).of_enc_eq fun x => by + rw [pow_succ, mul_two] + +/-- The number of levels is polynomial-time. -/ +theorem levels_polyTime : ComputableInPolyTime levels encCall encUnary := + taper_polyTime.comp (scale_polyTime.prod depth_polyTime) + +/-- The multiplicity step is polynomial-time. -/ +theorem step_polyTime : ComputableInPolyTime step encCall encUnary := + taperStep_polyTime.comp (scale_polyTime.prod (depth_polyTime.prod edges_polyTime)) + +/-- The number of interpolation points is polynomial-time, in unary. -/ +theorem numPoints_polyTime : ComputableInPolyTime numPoints encCall encUnary := + ComputableInPolyTime.unary_add' (ComputableInPolyTime.unary_mul' edges_polyTime + (ComputableInPolyTime.unary_sub' (ComputableInPolyTime.unary_mul' + (ComputableInPolyTime.const 2) twoPowSlots_polyTime) (ComputableInPolyTime.const 1))) + (ComputableInPolyTime.const 1) + +/-- The shift `Δ'` is polynomial-time, in unary. -/ +theorem shift_polyTime : ComputableInPolyTime shift encCall encUnary := + ComputableInPolyTime.unary_add' (ComputableInPolyTime.unary_add' + (ComputableInPolyTime.unary_mul' (ComputableInPolyTime.unary_mul' + (ComputableInPolyTime.unary_mul' + (ComputableInPolyTime.unary_add' slots_polyTime (ComputableInPolyTime.const 1)) + twoPowSlotsSucc_polyTime) step_polyTime) levels_polyTime) + (ComputableInPolyTime.unary_mul' (ComputableInPolyTime.unary_mul' + (ComputableInPolyTime.const 8) step_polyTime) twoPowSlots_polyTime)) + (ComputableInPolyTime.unary_mul' (ComputableInPolyTime.unary_mul' + (ComputableInPolyTime.const 8) edges_polyTime) + (ComputableInPolyTime.unary_add' slots_polyTime (ComputableInPolyTime.const 1))) + +/-- The common precision `N = p + Δ'` is polynomial-time, in unary. -/ +theorem wide_polyTime : ComputableInPolyTime wide encCall encUnary := + ComputableInPolyTime.unary_add' prec_polyTime shift_polyTime + +/-! ### Nodes, levels and precisions -/ + +/-- The capped valuation `twoVal b d` is at most `b`. -/ +private theorem twoVal_le (b d : ℕ) : twoVal b d ≤ b := by + unfold twoVal + split_ifs + · exact Nat.zero_le _ + · exact (List.length_filter_le _ _).trans (List.length_range (n := b)).le + +/-- Every level is at most `a + 1`. -/ +theorem level_le (x : Call) (k : ℕ) : level x k ≤ slots x + 1 := twoVal_le _ _ + +/-- The level of a grid index is polynomial-time, in unary. -/ +theorem level_polyTime : + ComputableInPolyTime (fun q : Call × ℕ => level q.1 q.2) (encPair encCall encUnary) + encUnary := by + have hx := ComputableInPolyTime.fst encCall encUnary + have hk := ComputableInPolyTime.snd encCall encUnary + have hL := twoPowSlots_polyTime.comp hx + have h := computableInPolyTime_twoVal + (ComputableInPolyTime.unary_add' (slots_polyTime.comp hx) (ComputableInPolyTime.const 1)) + (ComputableInPolyTime.unary_add' (ComputableInPolyTime.unary_sub' hk hL) + (ComputableInPolyTime.unary_sub' hL hk)) + exact h + +/-- The nodes of positive multiplicity are polynomial-time, as unary grid indices. -/ +theorem nodes_polyTime : ComputableInPolyTime nodes encCall (encList encUnary) := by + have hx := ComputableInPolyTime.fst encCall encUnary + have hk := ComputableInPolyTime.snd encCall encUnary + have hL := twoPowSlots_polyTime.comp hx + have hmult := computableInPolyTime_mult (slots_polyTime.comp hx) hL (levels_polyTime.comp hx) + (step_polyTime.comp hx) hk + have htest : ComputableInPolyTime (fun q : Call × ℕ => + decide (q.2 ≠ 2 ^ slots q.1 ∧ 0 < mult (slots q.1) (levels q.1) (step q.1) q.2)) + (encPair encCall encUnary) encBool := + (ComputableInPolyTime.bool_and' (ComputableInPolyTime.bool_not.comp + (ComputableInPolyTime.decide_eq' hk hL)) + (ComputableInPolyTime.unary_lt' (ComputableInPolyTime.const 0) hmult)).of_enc_eq fun q => by + simp only [Function.comp_apply, Bool.decide_and, decide_not] + have h := ComputableInPolyTime.filterWithInput + (test := fun (x : Call) k => + decide (k ≠ 2 ^ slots x ∧ 0 < mult (slots x) (levels x) (step x) k)) + (ComputableInPolyTime.range.comp twoPowSlotsSucc_polyTime) htest + exact h + +/-- The grid index of the `i`-th node is polynomial-time, in unary. -/ +theorem node_polyTime : + ComputableInPolyTime (fun q : Call × ℕ => (nodes q.1).getD q.2 0) (encPair encCall encUnary) + encUnary := by + have h := ComputableInPolyTime.listGetDWithInput + (nodes_polyTime.comp (ComputableInPolyTime.fst encCall encUnary)) + (ComputableInPolyTime.snd encCall encUnary) 0 + exact h + +/-- The level of the `i`-th node is polynomial-time, in unary. -/ +theorem nodeLevel_polyTime : + ComputableInPolyTime (fun q : Call × ℕ => level q.1 ((nodes q.1).getD q.2 0)) + (encPair encCall encUnary) encUnary := by + have h := level_polyTime.comp ((ComputableInPolyTime.fst encCall encUnary).prod node_polyTime) + exact h + +/-- The number `2 ^ (v₂ t + 1)` of tiles of the `i`-th node is polynomial-time, in unary. -/ +theorem tiles_polyTime : + ComputableInPolyTime (fun q : Call × ℕ => 2 ^ (level q.1 ((nodes q.1).getD q.2 0) + 1)) + (encPair encCall encUnary) encUnary := by + have hv := ComputableInPolyTime.binary_two_pow.comp + (ComputableInPolyTime.unary_add' nodeLevel_polyTime (ComputableInPolyTime.const 1)) + have hb := ComputableInPolyTime.unary_mul' (ComputableInPolyTime.const 4) + (twoPowSlots_polyTime.comp (ComputableInPolyTime.fst encCall encUnary)) + have h := ComputableInPolyTime.binary_to_unary_bounded hv hb fun q => by + simp only [Function.comp_apply] + calc 2 ^ (level q.1 ((nodes q.1).getD q.2 0) + 1) ≤ 2 ^ (slots q.1 + 2) := + Nat.pow_le_pow_right (by norm_num) + (by have := level_le q.1 ((nodes q.1).getD q.2 0); omega) + _ = 4 * 2 ^ slots q.1 := by rw [pow_add]; ring + exact h + +/-- **The precision of the `i`-th node is polynomial-time**, in unary. -/ +theorem nodePrec_polyTime : + ComputableInPolyTime (fun q : Call × ℕ => nodePrec q.1 q.2) (encPair encCall encUnary) + encUnary := by + have hx := ComputableInPolyTime.fst encCall encUnary + have hpow : ComputableInPolyTime + (fun q : Call × ℕ => 2 ^ (slots q.1 - level q.1 ((nodes q.1).getD q.2 0))) + (encPair encCall encUnary) encUnary := by + have h := ComputableInPolyTime.binary_to_unary_bounded (ComputableInPolyTime.binary_two_pow.comp + (ComputableInPolyTime.unary_sub' (slots_polyTime.comp hx) nodeLevel_polyTime)) + (twoPowSlots_polyTime.comp hx) + fun q => Nat.pow_le_pow_right (by norm_num) (Nat.sub_le _ _) + exact h + have h := ComputableInPolyTime.unary_add' (ComputableInPolyTime.unary_add' (prec_polyTime.comp hx) + (ComputableInPolyTime.unary_mul' (ComputableInPolyTime.unary_mul' + (ComputableInPolyTime.const 8) (step_polyTime.comp hx)) hpow)) + (ComputableInPolyTime.unary_mul' (ComputableInPolyTime.unary_mul' + (ComputableInPolyTime.const 8) (edges_polyTime.comp hx)) + (ComputableInPolyTime.unary_add' (slots_polyTime.comp hx) (ComputableInPolyTime.const 1))) + exact h + +/-! ### The packing and the weights -/ + +/-- The capped number of rows is polynomial-time, in unary. -/ +theorem rowCap_polyTime : ComputableInPolyTime rowCap encCall encUnary := + (ComputableInPolyTime.binary_min_unary.comp + (((ComputableInPolyTime.length_list _).comp vertices_polyTime).prod rows_polyTime)).of_enc_eq + fun x => by simp only [Function.comp_apply, rowCap, min_comm] + +/-- **The packing is polynomial-time** on every call. -/ +theorem packing_polyTime : ComputableInPolyTime packing encCall PacketPacking.encNativePacking := + computableInPolyTime_nativeParentPacking rowCap_polyTime slots_polyTime net_polyTime + +/-- **The number of packets is polynomial-time**, in unary, on every call: there are at most +`M (2 ^ a) ^ 12 ≤ M (s + 1) ^ 12` of them (`NativeChild.numPackets_nativeParentPacking_le`). -/ +theorem packets_polyTime : + ComputableInPolyTime (fun x : Call => (packing x).2.1) encCall encUnary := + computableInPolyTime_numPackets_nativeParentPacking rowCap_polyTime slots_polyTime + twoPowSlots_polyTime net_polyTime + +/-- **The weights of the modes of the `i`-th node are polynomial-time.** -/ +theorem weights_polyTime : + ComputableInPolyTime (fun q : Call × ℕ => weights q.1 q.2) (encPair encCall encUnary) + (encList encNat) := by + have hx := ComputableInPolyTime.fst encCall encUnary + have hp := nodePrec_polyTime + have hlen := ComputableInPolyTime.unary_mul' (packets_polyTime.comp hx) + (ComputableInPolyTime.unary_mul' tiles_polyTime hp) + have hj := ComputableInPolyTime.snd (encPair encCall encUnary) encUnary + have hpj := hp.comp (ComputableInPolyTime.fst (encPair encCall encUnary) encUnary) + have hf : ComputableInPolyTime (fun r : (Call × ℕ) × ℕ => r.2 % nodePrec r.1.1 r.1.2 + 1) + (encPair (encPair encCall encUnary) encUnary) encNat := by + have h := ComputableInPolyTime.unary_to_binary.comp (ComputableInPolyTime.unary_add' + (ComputableInPolyTime.unary_mod.comp (hj.prod hpj)) (ComputableInPolyTime.const 1)) + exact h + have h := ComputableInPolyTime.mapWithInput + (f := fun (q : Call × ℕ) j => j % nodePrec q.1 q.2 + 1) + (ComputableInPolyTime.range.comp hlen) hf + exact h + +/-- The number of modes of the `i`-th node is polynomial-time, in unary. -/ +theorem weightsLength_polyTime : + ComputableInPolyTime (fun q : Call × ℕ => (weights q.1 q.2).length) (encPair encCall encUnary) + encUnary := by + have h := (ComputableInPolyTime.length_list _).comp weights_polyTime + exact h + +/-! ### Points and the table -/ + +/-- The binary digits are polynomial-time, from the length and the number in unary. -/ +theorem digits_polyTime : + ComputableInPolyTime (fun q : ℕ × ℕ => digits q.1 q.2) (encPair encUnary encUnary) + (encList encNat) := by + have hk := (ComputableInPolyTime.snd encUnary encUnary).comp + (ComputableInPolyTime.fst (encPair encUnary encUnary) encUnary) + have hf : ComputableInPolyTime (fun r : (ℕ × ℕ) × ℕ => if r.1.2.testBit r.2 then 1 else 0) + (encPair (encPair encUnary encUnary) encUnary) encNat := by + have h := ComputableInPolyTime.ite (encMid := encNat) (ComputableInPolyTime.binary_testBit + (ComputableInPolyTime.unary_to_binary.comp hk) (ComputableInPolyTime.snd _ _)) + (ComputableInPolyTime.const 1) (ComputableInPolyTime.const 0) + exact h + have h := ComputableInPolyTime.mapWithInput + (f := fun (q : ℕ × ℕ) i => if q.2.testBit i then 1 else 0) + (ComputableInPolyTime.range.comp (ComputableInPolyTime.fst encUnary encUnary)) hf + exact h + +/-- **The interpolation points are polynomial-time.** -/ +theorem points_polyTime : ComputableInPolyTime points encCall (encList (encList encNat)) := by + have hf : ComputableInPolyTime (fun r : Call × ℕ => digits r.1.fl.length r.2) + (encPair encCall encUnary) (encList encNat) := by + have h := digits_polyTime.comp ((((ComputableInPolyTime.length_list _).comp fl_polyTime).comp + (ComputableInPolyTime.fst encCall encUnary)).prod (ComputableInPolyTime.snd _ _)) + exact h + have h := ComputableInPolyTime.mapWithInput (f := fun (x : Call) k => digits x.fl.length k) + (ComputableInPolyTime.range.comp numPoints_polyTime) hf + exact h + +/-- **The table of native recovery is polynomial-time**, from a call and the stored values. -/ +theorem table_polyTime : + ComputableInPolyTime (fun q : Call × List (List ℕ) => table q.1 q.2) + (encPair encCall (encList (encList encNat))) (encList (encList (encList encNat))) := by + let e := encPair encCall (encList (encList encNat)) + have hx := ComputableInPolyTime.fst encCall (encList (encList encNat)) + have hx' := hx.comp (ComputableInPolyTime.fst e encUnary) + have hV' := (ComputableInPolyTime.snd encCall (encList (encList encNat))).comp + (ComputableInPolyTime.fst e encUnary) + have hk := ComputableInPolyTime.snd e encUnary + have hn := numPoints_polyTime.comp hx' + have hmem := ComputableInPolyTime.decide_mem (nodes_polyTime.comp hx') hk + have hidx := ComputableInPolyTime.idxOfWithInput (nodes_polyTime.comp hx') hk + have hdrop : ComputableInPolyTime (fun r : (Call × List (List ℕ)) × ℕ => + r.1.2.drop ((nodes r.1.1).idxOf r.2 * numPoints r.1.1)) (encPair e encUnary) + (encList (encList encNat)) := + .of_tidy (ComputableTidilyInPolyTime.listDropWithInput hV'.tidy + (ComputableInPolyTime.unary_mul' hidx hn).tidy) + have htake : ComputableInPolyTime (fun r : (Call × List (List ℕ)) × ℕ => + (r.1.2.drop ((nodes r.1.1).idxOf r.2 * numPoints r.1.1)).take (numPoints r.1.1)) + (encPair e encUnary) (encList (encList encNat)) := + .of_tidy (ComputableTidilyInPolyTime.listTakeWithInput hdrop.tidy hn.tidy) + have hf : ComputableInPolyTime (fun r : (Call × List (List ℕ)) × ℕ => + if r.2 ∈ nodes r.1.1 then + (r.1.2.drop ((nodes r.1.1).idxOf r.2 * numPoints r.1.1)).take (numPoints r.1.1) + else []) (encPair e encUnary) (encList (encList encNat)) := by + have h := ComputableInPolyTime.ite hmem htake (ComputableInPolyTime.const []) + refine h.of_enc_eq fun r => ?_ + simp only [Function.comp_apply, decide_eq_true_eq] + have h := ComputableInPolyTime.mapWithInput (f := fun (q : Call × List (List ℕ)) k => + if k ∈ nodes q.1 then + (q.2.drop ((nodes q.1).idxOf k * numPoints q.1)).take (numPoints q.1) else []) + (ComputableInPolyTime.range.comp (twoPowSlotsSucc_polyTime.comp hx)) hf + exact h + +/-! ### Active calls -/ + +/-- Whether a call is active, as a conjunction of tests. -/ +theorem active_eq (x : Call) : active x = + (decide (leafSize x.scale < x.edges) && decide (1 ≤ levels x) && decide (levels x ≤ x.edges) && + decide (levels x ≤ slots x) && + x.net.vertices.all (fun v => decide (v.1.length ≤ degreeBound x.scale)) && + decide (numPoints x ≤ 2 ^ x.fl.length) && decide (x.edges < x.bound)) := by + simp only [active, Bool.decide_and, List.all_eq, decide_eq_true_eq, Bool.and_assoc] + +/-- **Whether a call is active is polynomial-time.** -/ +theorem active_polyTime : ComputableInPolyTime active encCall encBool := by + have hdeg : ComputableInPolyTime (fun x : Call => + x.net.vertices.all (fun v => decide (v.1.length ≤ degreeBound x.scale))) encCall encBool := + ComputableInPolyTime.allWithInput vertices_polyTime + (ComputableInPolyTime.binary_le' (ComputableInPolyTime.unary_to_binary.comp + ((ComputableInPolyTime.length_list _).comp ((ComputableInPolyTime.fst _ _).comp + (ComputableInPolyTime.snd _ _)))) + (degreeBound_polyTime.comp (scale_polyTime.comp (ComputableInPolyTime.fst _ _)))) + have h := ComputableInPolyTime.bool_and' (ComputableInPolyTime.bool_and' + (ComputableInPolyTime.bool_and' (ComputableInPolyTime.bool_and' + (ComputableInPolyTime.bool_and' (ComputableInPolyTime.bool_and' + (ComputableInPolyTime.unary_lt' (leafSize_polyTime.comp scale_polyTime) edges_polyTime) + (ComputableInPolyTime.unary_le' (ComputableInPolyTime.const 1) levels_polyTime)) + (ComputableInPolyTime.unary_le' levels_polyTime edges_polyTime)) + (ComputableInPolyTime.unary_le' levels_polyTime slots_polyTime)) hdeg) + (ComputableInPolyTime.binary_le' + (ComputableInPolyTime.unary_to_binary.comp numPoints_polyTime) + (ComputableInPolyTime.binary_two_pow.comp + ((ComputableInPolyTime.length_list _).comp fl_polyTime)))) + (ComputableInPolyTime.unary_lt' edges_polyTime bound_polyTime) + refine h.of_enc_eq fun x => ?_ + rw [active_eq] + rfl + +/-! ### The components of the scheme -/ + +section Scheme + +variable (mk : Call → State → ℕ × DescribedNetwork VertexDesc) + +/-- **The leaf test is polynomial-time.** -/ +theorem isLeaf_polyTime : ComputableInPolyTime (scheme mk).isLeaf encCall encBool := by + have h := ComputableInPolyTime.bool_not.comp active_polyTime + exact h + +/-- **The initial accumulator is polynomial-time.** -/ +theorem start_polyTime : ComputableInPolyTime (scheme mk).start encCall encFrame := by + have hlen : ComputableInPolyTime (fun x : Call => (weights x 0).length) encCall encUnary := by + have h := weightsLength_polyTime.comp + ((ComputableInPolyTime.id' (encIn := encCall)).prod (ComputableInPolyTime.const 0)) + exact h + have hst : ComputableInPolyTime (fun x : Call => cursorStart (weights x)) encCall + (encPair encUnary (encPair encUnary (encPair (encList encNat) encUnary))) := + (ComputableInPolyTime.const 0).prod ((ComputableInPolyTime.const 0).prod + ((ComputableInPolyTime.replicate hlen (ComputableInPolyTime.const 0)).prod + (ComputableInPolyTime.const 0))) + have hst' : ComputableInPolyTime (fun x : Call => cursorStart (weights x)) encCall + ChildCursor.encState := hst + have h : ComputableInPolyTime (scheme mk).start encCall + (encPair (encOption ChildCursor.encState) + (encPair (encList encNat) (encPair (encList encNat) (encList (encList encNat))))) := + ((ComputableInPolyTime.optionSome _).comp hst').prod + ((computableInPolyTime_one fl_polyTime).prod ((computableInPolyTime_zero fl_polyTime).prod + (ComputableInPolyTime.const []))) + exact h + +/-- The node index of a cursor state is polynomial-time. -/ +private theorem stateNode_polyTime : + ComputableInPolyTime (fun c : State => c.1) ChildCursor.encState encUnary := by + unfold ChildCursor.encState; fun_prop + +/-- The point index of a cursor state is polynomial-time. -/ +private theorem statePoint_polyTime : + ComputableInPolyTime (fun c : State => c.2.1) ChildCursor.encState encUnary := by + unfold ChildCursor.encState; fun_prop + +/-- The exponents of a cursor state are polynomial-time, in binary. -/ +private theorem stateExps_polyTime : + ComputableInPolyTime (fun c : State => c.2.2.1) ChildCursor.encState (encList encNat) := by + unfold ChildCursor.encState; fun_prop + +/-- The group of a cursor state is polynomial-time. -/ +private theorem stateGroup_polyTime : + ComputableInPolyTime (fun c : State => c.2.2.2) ChildCursor.encState encUnary := by + unfold ChildCursor.encState; fun_prop + +variable {mk} + +/-- **The child call at a cursor state is polynomial-time**, given a polynomial-time builder. -/ +theorem child_polyTime + (hmk : ComputableInPolyTime (fun q : Call × State => mk q.1 q.2) + (encPair encCall ChildCursor.encState) + (encPair encNat (DescribedNetwork.encDescribed VertexDesc.enc))) : + ComputableInPolyTime (fun q : Call × State => child q.1 mk q.2) + (encPair encCall ChildCursor.encState) encCall := by + have hx := ComputableInPolyTime.fst encCall ChildCursor.encState + have ht := stateNode_polyTime.comp (ComputableInPolyTime.snd encCall ChildCursor.encState) + have hprec : ComputableInPolyTime (fun q : Call × State => nodePrec q.1 q.2.1) + (encPair encCall ChildCursor.encState) encUnary := by + have h := nodePrec_polyTime.comp (hx.prod ht) + exact h + have h : ComputableInPolyTime (fun q : Call × State => child q.1 mk q.2) + (encPair encCall ChildCursor.encState) + (encPair (encPair encUnary (encPair encUnary (encPair encUnary (encPair encUnary + (encPair (encList encNat) encNat))))) (DescribedNetwork.encDescribed VertexDesc.enc)) := + ((scale_polyTime.comp hx).prod ((ComputableInPolyTime.unary_add' (depth_polyTime.comp hx) + (ComputableInPolyTime.const 1)).prod ((edges_polyTime.comp hx).prod (hprec.prod + ((fl_polyTime.comp hx).prod ((ComputableInPolyTime.fst _ _).comp hmk)))))).prod + ((ComputableInPolyTime.snd _ _).comp hmk) + exact h + +/-- **Child generation is polynomial-time**, given a polynomial-time builder. -/ +theorem next_polyTime + (hmk : ComputableInPolyTime (fun q : Call × State => mk q.1 q.2) + (encPair encCall ChildCursor.encState) + (encPair encNat (DescribedNetwork.encDescribed VertexDesc.enc))) : + ComputableInPolyTime (fun p : Call × Frame => (scheme mk).next p.1 p.2) + (encPair encCall encFrame) (encOption encCall) := by + have hc : ComputableInPolyTime (fun p : Call × Frame => p.2.1) (encPair encCall encFrame) + (encOption ChildCursor.encState) := + (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd encCall encFrame) + have hbody : ComputableInPolyTime (fun r : (Call × Frame) × State => some (child r.1.1 mk r.2)) + (encPair (encPair encCall encFrame) ChildCursor.encState) (encOption encCall) := by + have h := (ComputableInPolyTime.optionSome encCall).comp ((child_polyTime hmk).comp + (((ComputableInPolyTime.fst encCall encFrame).comp (ComputableInPolyTime.fst _ _)).prod + (ComputableInPolyTime.snd _ _))) + exact h + have h := ComputableInPolyTime.optionElimWithInput + (body := fun (p : Call × Frame) (c : State) => some (child p.1 mk c)) hc + (ComputableInPolyTime.const (encOut := encOption encCall) none) hbody + refine h.of_enc_eq fun p => ?_ + rcases p with ⟨x, _ | c, acc⟩ <;> rfl + +variable (mk) + +/-- The inputs of `absorb` at a cursor state: the call, its frame, the child's value and the +state. -/ +private abbrev AbsorbIn : Type := ((Call × Frame) × (ℕ × List ℕ)) × State + +/-- The encoding of `AbsorbIn`. -/ +private abbrev encAbsorbIn : AbsorbIn ↪ List Bool := + encPair (encPair (encPair encCall encFrame) encValue) ChildCursor.encState + +/-- The call of an input of `absorb`. -/ +private theorem absorbCall_polyTime : + ComputableInPolyTime (fun r : AbsorbIn => r.1.1.1) encAbsorbIn encCall := + (ComputableInPolyTime.fst encCall encFrame).comp ((ComputableInPolyTime.fst _ encValue).comp + (ComputableInPolyTime.fst _ ChildCursor.encState)) + +/-- The state of an input of `absorb`. -/ +private theorem absorbState_polyTime : + ComputableInPolyTime (fun r : AbsorbIn => r.2) encAbsorbIn ChildCursor.encState := + ComputableInPolyTime.snd _ _ + +/-- **The cursor step of `absorb` is polynomial-time.** -/ +private theorem absorbCursor_polyTime : + ComputableInPolyTime (fun r : AbsorbIn => cursorNext (weights r.1.1.1) (nodePrec r.1.1.1) + (nodes r.1.1.1).length (numPoints r.1.1.1) 64 r.2) encAbsorbIn (encOption encState) := by + have hx := absorbCall_polyTime + have hc := absorbState_polyTime + have ht := stateNode_polyTime.comp hc + have hT := (ComputableInPolyTime.length_list _).comp (nodes_polyTime.comp hx) + have hn := numPoints_polyTime.comp hx + have hwt : ComputableInPolyTime (fun r : AbsorbIn => weights r.1.1.1 r.2.1) encAbsorbIn + (encList encNat) := by + have h := weights_polyTime.comp (hx.prod ht) + exact h + have hpt : ComputableInPolyTime (fun r : AbsorbIn => nodePrec r.1.1.1 r.2.1) encAbsorbIn + encNat := by + have h := ComputableInPolyTime.unary_to_binary.comp (nodePrec_polyTime.comp (hx.prod ht)) + exact h + have hnext : ComputableInPolyTime (fun r : AbsorbIn => (weights r.1.1.1 (r.2.1 + 1)).length) + encAbsorbIn encUnary := by + have h := weightsLength_polyTime.comp + (hx.prod (ComputableInPolyTime.unary_add' ht (ComputableInPolyTime.const 1))) + exact h + have hin : ComputableInPolyTime (fun r : AbsorbIn => + (((((nodes r.1.1.1).length, numPoints r.1.1.1, (64 : ℕ)), (weights r.1.1.1 r.2.1, + nodePrec r.1.1.1 r.2.1, (weights r.1.1.1 (r.2.1 + 1)).length)), r.2) : StepInput)) + encAbsorbIn (encPair (encPair (encPair encUnary (encPair encUnary encUnary)) + (encPair (encList encNat) (encPair encNat encUnary))) ChildCursor.encState) := + ((hT.prod (hn.prod (ComputableInPolyTime.const 64))).prod (hwt.prod (hpt.prod hnext))).prod hc + have hin' : ComputableInPolyTime (fun r : AbsorbIn => + (((((nodes r.1.1.1).length, numPoints r.1.1.1, (64 : ℕ)), (weights r.1.1.1 r.2.1, + nodePrec r.1.1.1 r.2.1, (weights r.1.1.1 (r.2.1 + 1)).length)), r.2) : StepInput)) + encAbsorbIn encStepInput := hin + refine (computableInPolyTime_cursorStep.comp hin').of_enc_eq fun r => ?_ + rw [cursorNext_eq_cursorStep] + rfl + +/-- **The accumulator step of `absorb` is polynomial-time.** -/ +private theorem absorbAcc_polyTime : + ComputableInPolyTime (fun r : AbsorbIn => absorbAt (weights r.1.1.1) (nodePrec r.1.1.1) 64 + (mul (wide r.1.1.1) r.1.1.1.fl) (add (wide r.1.1.1) r.1.1.1.fl) (one r.1.1.1.fl) + (zero r.1.1.1.fl) r.2 r.1.1.2.2 r.1.2.2) encAbsorbIn + (encPair (encList encNat) (encPair (encList encNat) (encList (encList encNat)))) := by + have hx := absorbCall_polyTime + have hc := absorbState_polyTime + have ht := stateNode_polyTime.comp hc + have hN := wide_polyTime.comp hx + have hfl := fl_polyTime.comp hx + have hacc : ComputableInPolyTime (fun r : AbsorbIn => r.1.1.2.2) encAbsorbIn + (encPair (encList encNat) (encPair (encList encNat) (encList (encList encNat)))) := + (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd encCall encFrame).comp + ((ComputableInPolyTime.fst _ encValue).comp + (ComputableInPolyTime.fst _ ChildCursor.encState))) + have hprod := (ComputableInPolyTime.fst _ _).comp hacc + have hsum := (ComputableInPolyTime.fst _ _).comp ((ComputableInPolyTime.snd _ _).comp hacc) + have hstored := (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp hacc) + have hy : ComputableInPolyTime (fun r : AbsorbIn => r.1.2.2) encAbsorbIn (encList encNat) := + (ComputableInPolyTime.snd encUnary (encList encNat)).comp ((ComputableInPolyTime.snd _ _).comp + (ComputableInPolyTime.fst _ ChildCursor.encState)) + have hpy := computableInPolyTime_mul hN hfl hprod hy + have hnew := computableInPolyTime_add hN hfl hsum hpy + have hone := computableInPolyTime_one hfl + have hzero := computableInPolyTime_zero hfl + have hlast : ComputableInPolyTime (fun r : AbsorbIn => + (BudgetTuples.budgetNext (weights r.1.1.1 r.2.1) (nodePrec r.1.1.1 r.2.1) r.2.2.2.1).isNone) + encAbsorbIn encBool := by + have hwt : ComputableInPolyTime (fun r : AbsorbIn => weights r.1.1.1 r.2.1) encAbsorbIn + (encList encNat) := by + have h := weights_polyTime.comp (hx.prod ht) + exact h + have hpt : ComputableInPolyTime (fun r : AbsorbIn => nodePrec r.1.1.1 r.2.1) encAbsorbIn + encNat := by + have h := ComputableInPolyTime.unary_to_binary.comp (nodePrec_polyTime.comp (hx.prod ht)) + exact h + have hin : ComputableInPolyTime (fun r : AbsorbIn => + (weights r.1.1.1 r.2.1, nodePrec r.1.1.1 r.2.1, r.2.2.2.1)) encAbsorbIn + (encPair (encList encNat) (encPair encNat (encList encNat))) := + hwt.prod (hpt.prod (stateExps_polyTime.comp hc)) + have hin' : ComputableInPolyTime (fun r : AbsorbIn => + (weights r.1.1.1 r.2.1, nodePrec r.1.1.1 r.2.1, r.2.2.2.1)) encAbsorbIn + BudgetTuples.encBudgetInput := hin + have h := ComputableInPolyTime.bool_not.comp (ComputableInPolyTime.optionIsSome + (BudgetTuples.computableInPolyTime_budgetNext.comp hin')) + refine h.of_enc_eq fun r => ?_ + simp only [Function.comp_apply] + cases BudgetTuples.budgetNext (weights r.1.1.1 r.2.1) (nodePrec r.1.1.1 r.2.1) r.2.2.2.1 <;> rfl + have hg : ComputableInPolyTime (fun r : AbsorbIn => decide (r.2.2.2.2 + 1 < 64)) encAbsorbIn + encBool := + ComputableInPolyTime.unary_lt' (ComputableInPolyTime.unary_add' (stateGroup_polyTime.comp hc) + (ComputableInPolyTime.const 1)) (ComputableInPolyTime.const 64) + have h := ComputableInPolyTime.ite hg (hpy.prod (hsum.prod hstored)) + (ComputableInPolyTime.ite hlast (hone.prod (hzero.prod (ComputableInPolyTime.listAppend' hstored + (ComputableInPolyTime.cons' hnew (ComputableInPolyTime.const []))))) + (hone.prod (hnew.prod hstored))) + refine h.of_enc_eq fun r => ?_ + simp only [absorbAt, decide_eq_true_eq, Function.comp_apply] + +/-- **Absorbing a child's value is polynomial-time.** -/ +theorem absorb_polyTime : + ComputableInPolyTime + (fun p : (Call × Frame) × (ℕ × List ℕ) => (scheme mk).absorb p.1.1 p.1.2 p.2) + (encPair (encPair encCall encFrame) encValue) encFrame := by + have hc : ComputableInPolyTime (fun p : (Call × Frame) × (ℕ × List ℕ) => p.1.2.1) + (encPair (encPair encCall encFrame) encValue) (encOption ChildCursor.encState) := + (ComputableInPolyTime.fst _ _).comp ((ComputableInPolyTime.snd encCall encFrame).comp + (ComputableInPolyTime.fst _ encValue)) + have hfallback : ComputableInPolyTime (fun p : (Call × Frame) × (ℕ × List ℕ) => p.1.2) + (encPair (encPair encCall encFrame) encValue) encFrame := + (ComputableInPolyTime.snd encCall encFrame).comp (ComputableInPolyTime.fst _ encValue) + have hbody : ComputableInPolyTime (fun r : AbsorbIn => + ((cursorNext (weights r.1.1.1) (nodePrec r.1.1.1) (nodes r.1.1.1).length (numPoints r.1.1.1) + 64 r.2, absorbAt (weights r.1.1.1) (nodePrec r.1.1.1) 64 + (mul (wide r.1.1.1) r.1.1.1.fl) (add (wide r.1.1.1) r.1.1.1.fl) (one r.1.1.1.fl) + (zero r.1.1.1.fl) r.2 r.1.1.2.2 r.1.2.2) : Frame)) encAbsorbIn encFrame := + absorbCursor_polyTime.prod (absorbAcc_polyTime) + have h := ComputableInPolyTime.optionElimWithInput + (body := fun (p : (Call × Frame) × (ℕ × List ℕ)) (c : State) => + ((cursorNext (weights p.1.1) (nodePrec p.1.1) (nodes p.1.1).length (numPoints p.1.1) 64 c, + absorbAt (weights p.1.1) (nodePrec p.1.1) 64 (mul (wide p.1.1) p.1.1.fl) + (add (wide p.1.1) p.1.1.fl) (one p.1.1.fl) (zero p.1.1.fl) c p.1.2.2 p.2.2) : Frame)) + hc hfallback hbody + refine h.of_enc_eq fun p => ?_ + rcases p with ⟨⟨x, _ | c, acc⟩, y⟩ <;> rfl + +/-- **The value of a call is polynomial-time.** -/ +theorem finish_polyTime : + ComputableInPolyTime (fun p : Call × Frame => (scheme mk).finish p.1 p.2) + (encPair encCall encFrame) encValue := by + have hx := ComputableInPolyTime.fst encCall encFrame + have hV : ComputableInPolyTime (fun p : Call × Frame => p.2.2.2.2) (encPair encCall encFrame) + (encList (encList encNat)) := + (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd encCall encFrame))) + have htab : ComputableInPolyTime (fun p : Call × Frame => table p.1 p.2.2.2.2) + (encPair encCall encFrame) (encList (encList (encList encNat))) := by + have h := table_polyTime.comp (hx.prod hV) + exact h + have hrec := computableInPolyTime_recover (prec_polyTime.comp hx) (shift_polyTime.comp hx) + (fl_polyTime.comp hx) (slots_polyTime.comp hx) (twoPowSlots_polyTime.comp hx) + (levels_polyTime.comp hx) (step_polyTime.comp hx) (points_polyTime.comp hx) htab + have h := (depth_polyTime.comp hx).prod hrec + exact h + +variable {mk} + +/-- **The components of the scheme are polynomial-time**, for a polynomial-time child builder. -/ +theorem scheme_polyTime + (hmk : ComputableInPolyTime (fun q : Call × State => mk q.1 q.2) + (encPair encCall ChildCursor.encState) + (encPair encNat (DescribedNetwork.encDescribed VertexDesc.enc))) : + (scheme mk).PolyTime encCall encFrame encValue := + ⟨isLeaf_polyTime mk, start_polyTime mk, next_polyTime hmk, absorb_polyTime mk, + finish_polyTime mk⟩ + +end Scheme + +/-! ### The native child builder -/ + +/-- **The native child builder is polynomial-time** on every call and cursor state +(`NativeChild.computableInPolyTime_nativeChild_nativeParentPacking`). The rows are capped at the +number of vertices and the exponents at the node's precision, so both are polynomial in unary; the +number `2 ^ a` of slots is at most `s + 1` and the number `2 ^ (v₂ t + 1)` of tiles at most +`4 (s + 1)`. -/ +theorem nativeMk_polyTime : + ComputableInPolyTime (fun q : Call × State => nativeMk q.1 q.2) + (encPair encCall ChildCursor.encState) + (encPair encNat (DescribedNetwork.encDescribed VertexDesc.enc)) := by + have hx := ComputableInPolyTime.fst encCall ChildCursor.encState + have hc := ComputableInPolyTime.snd encCall ChildCursor.encState + have ht := stateNode_polyTime.comp hc + have hj := statePoint_polyTime.comp hc + have hβ := stateExps_polyTime.comp hc + have hg := ComputableInPolyTime.unary_to_binary.comp (stateGroup_polyTime.comp hc) + have hr := rowCap_polyTime.comp hx + have ha := slots_polyTime.comp hx + have hL := twoPowSlots_polyTime.comp hx + have hfl := fl_polyTime.comp hx + have hD := net_polyTime.comp hx + have hi : ComputableInPolyTime (fun q : Call × State => level q.1 ((nodes q.1).getD q.2.1 0)) + (encPair encCall ChildCursor.encState) encUnary := by + have h := nodeLevel_polyTime.comp (hx.prod ht) + exact h + have hT : ComputableInPolyTime + (fun q : Call × State => 2 ^ (level q.1 ((nodes q.1).getD q.2.1 0) + 1)) + (encPair encCall ChildCursor.encState) encUnary := by + have h := tiles_polyTime.comp (hx.prod ht) + exact h + have hpt : ComputableInPolyTime (fun q : Call × State => nodePrec q.1 q.2.1) + (encPair encCall ChildCursor.encState) encUnary := by + have h := nodePrec_polyTime.comp (hx.prod ht) + exact h + have hnode : ComputableInPolyTime + (fun q : Call × State => node (slots q.1) ((nodes q.1).getD q.2.1 0)) + (encPair encCall ChildCursor.encState) encIntBin := by + have h := ComputableInPolyTime.intBin_subNatNat.comp + ((ComputableInPolyTime.unary_to_binary.comp (node_polyTime.comp (hx.prod ht))).prod + (ComputableInPolyTime.unary_to_binary.comp hL)) + refine h.of_enc_eq fun q => ?_ + simp only [Function.comp_apply, node, Int.subNatNat_eq_coe, Nat.cast_pow, Nat.cast_ofNat] + have hζ : ComputableInPolyTime (fun q : Call × State => (points q.1).getD q.2.2.1 []) + (encPair encCall ChildCursor.encState) (encList encNat) := by + have h := ComputableInPolyTime.listGetDWithInput (points_polyTime.comp hx) hj [] + exact h + have hcap : ComputableInPolyTime + (fun q : Call × State => q.2.2.2.1.map (min · (nodePrec q.1 q.2.1))) + (encPair encCall ChildCursor.encState) (encList encUnary) := by + have hf : ComputableInPolyTime (fun r : (Call × State) × ℕ => min r.2 (nodePrec r.1.1 r.1.2.1)) + (encPair (encPair encCall ChildCursor.encState) encNat) encUnary := by + have h := ComputableInPolyTime.binary_min_unary.comp + ((hpt.comp (ComputableInPolyTime.fst _ _)).prod (ComputableInPolyTime.snd _ _)) + refine h.of_enc_eq fun r => ?_ + simp only [Function.comp_apply, min_comm] + have h := ComputableInPolyTime.mapWithInput + (f := fun (q : Call × State) (b : ℕ) => min b (nodePrec q.1 q.2.1)) hβ hf + exact h + have hrows := computableInPolyTime_childRows_nativeParentPacking hr ha hi hD hg + have hchild := computableInPolyTime_nativeChild_nativeParentPacking hfl ha hL hi hT hpt hnode hζ + hr hD hcap hg + have h := hrows.prod hchild + exact h + +/-- **The components of the native contraction recursion are polynomial-time**: the hypothesis +`hpoly` of `CountingSimulation.contractionAlgorithmOfNative`. -/ +theorem scheme_nativeMk_polyTime : (scheme nativeMk).PolyTime encCall encFrame encValue := + scheme_polyTime nativeMk_polyTime + +end Cslib.Circuits.Frontier.FastContraction diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean index 1ff9edf83f..ea5822fb2d 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean @@ -16,11 +16,13 @@ import Mathlib.Data.List.GetD The child builder of the recursion of `Cslib.Circuits.Frontier.FastContraction.scheme` is the native child (`FastContraction.nativeMk`: `NativeChild.childRows` and `NativeChild.nativeChild` at the -cursor state), and a call is well-formed (`FastContraction.WF`) when its modulus is irreducible -modulo `2` and its network is rows-first. The step of an active call is then correct -(`FastContraction.stepCorrect_nativeMk`) whenever its interpolation points have lifts with unit -differences: the values the call stores are the sums of (D.16) at each node -(`FastContraction.val_table_runLoop`), which is the hypothesis of the correctness of one native call +cursor state, with the rows and the exponents capped so that it is polynomial-time on every state), +and a call is well-formed (`FastContraction.WF`) when its modulus is irreducible modulo `2` and its +network is rows-first. The step of an active call is then correct +(`FastContraction.stepCorrect_nativeMk`): its interpolation points, the binary digits of +`0, …, n - 1`, have lifts with unit differences (`FastContraction.pairwise_isUnit_points`), and the +values the call stores are the sums of (D.16) at each node (`FastContraction.val_table_runLoop`), +which is the hypothesis of the correctness of one native call (`NativeCall.val_recover_eq_contraction`, [OpenAI2026ETH], §D.4.4–§D.4.7). ## Main definitions @@ -30,8 +32,11 @@ differences: the values the call stores are the sums of (D.16) at each node ## Main results -* `Cslib.Circuits.Frontier.FastContraction.stepCorrect_nativeMk`: the step is correct, given the - points. +* `Cslib.Circuits.Frontier.FastContraction.pairwise_isUnit_points`: the points have lifts with unit + differences. +* `Cslib.Circuits.Frontier.FastContraction.nativeMk_eq`: the caps of the builder are inactive on + well-formed active calls. +* `Cslib.Circuits.Frontier.FastContraction.stepCorrect_nativeMk`: the step is correct. * `Cslib.Circuits.Frontier.FastContraction.wfChildren_nativeMk`: well-formedness passes to the children. @@ -47,12 +52,17 @@ namespace Cslib.Circuits.Frontier.FastContraction open Finset GaloisRingArith ChildCursor NativeRecovery ContractionSchedule NativeChild /-- **The native child builder**: at the cursor state `(j, i, β, g)`, the rows and the native -child of group `g` at the `j`-th node, the `i`-th point and the exponents `β`. -/ +child of group `g` at the `j`-th node, the `i`-th point and the exponents `β`. The rows are capped +at the number of vertices (`FastContraction.rowCap`) and the exponents at the node's precision +`p_j`. On a well-formed active call and the cursor's states neither cap changes anything +(`FastContraction.nativeMk_eq`); on every call and state they keep the builder polynomial-time, +since the number of rows and the exponents are stored in binary but the child lists one word per +row and stores the exponents in unary. -/ @[expose] def nativeMk (x : Call) (c : State) : ℕ × DescribedNetwork VertexDesc := - (childRows x.rows (level x ((nodes x).getD c.1 0)) x.net (packing x) c.2.2.2, + (childRows (rowCap x) (level x ((nodes x).getD c.1 0)) x.net (packing x) c.2.2.2, nativeChild x.fl (slots x) (level x ((nodes x).getD c.1 0)) (nodePrec x c.1) - (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) x.rows x.net - (packing x) c.2.2.1 c.2.2.2) + (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) (rowCap x) x.net + (packing x) (c.2.2.1.map (min · (nodePrec x c.1))) c.2.2.2) /-- **A well-formed call**: its modulus is irreducible modulo `2` and its network is rows-first. -/ @[expose] def WF (x : Call) : Prop := @@ -61,6 +71,40 @@ child of group `g` at the `j`-th node, the `i`-th point and the exponents `β`. variable {x : Call} +/-- A rows-first network with an edge has at most as many rows as vertices. -/ +theorem rows_le_of_isRowsFirstBipartite {D : DescribedNetwork VertexDesc} {r : ℕ} + (hD : D.IsRowsFirstBipartite r) (hM : 1 ≤ D.numEdges) : r ≤ D.vertices.length := by + by_contra h + have h1 := (hD.2 0 hM).2 + rw [List.drop_of_length_le (by omega)] at h1 + simp at h1 + +/-- The cap of `nativeMk` leaves a tuple of weight below `p` unchanged, for positive weights. -/ +theorem map_min_of_mem_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} {β : List ℕ} + (hβ : β ∈ BudgetTuples.budgetTuples ws p) : β.map (min · p) = β := by + calc β.map (min · p) = β.map id := List.map_congr_left fun b hb => by + have := BudgetTuples.lt_of_mem_budgetTuples hw hβ hb + simp only [id] + omega + _ = β := List.map_id β + +/-- **The caps of `nativeMk` are inactive** at a well-formed active call and a state of its cursor: +the builder is the native child of the rows and the exponents of the state. -/ +theorem nativeMk_eq (hx : WF x) (ha : active x = true) {c : State} (hc : c ∈ children x) : + nativeMk x c = + (childRows x.rows (level x ((nodes x).getD c.1 0)) x.net + (nativeParentPacking x.rows (slots x) x.net) c.2.2.2, + nativeChild x.fl (slots x) (level x ((nodes x).getD c.1 0)) (nodePrec x c.1) + (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) x.rows x.net + (nativeParentPacking x.rows (slots x) x.net) c.2.2.1 c.2.2.2) := by + have hr := rows_le_of_isRowsFirstBipartite hx.2 (one_le_edges_of_active ha) + have hβ : c.2.2.1 ∈ BudgetTuples.budgetTuples (weights x c.1) (nodePrec x c.1) := by + simp only [children, cursorList, nodeBlock, pointBlock, groupBlock, List.mem_flatMap, + List.mem_range, List.mem_map] at hc + obtain ⟨j, -, i, -, β, hβ, g, -, rfl⟩ := hc + exact hβ + rw [nativeMk, packing_eq hr, rowCap_eq hr, map_min_of_mem_budgetTuples (weights_pos _) hβ] + /-- The level of a node index is the `2`-adic valuation of its node. -/ theorem level_eq {k : ℕ} (hk : k < 2 ^ (slots x + 1)) : level x k = padicValInt 2 (node (slots x) k) := by @@ -89,22 +133,31 @@ theorem mem_children {j i : ℕ} {β : List ℕ} {g : ℕ} (hj : j < (nodes x).l List.mem_range, List.mem_map] exact ⟨j, hj, i, hi, β, hβ, g, hg, rfl⟩ +/-- **The interpolation points of an active call have lifts with unit differences**: they are the +binary digits of `0, …, n - 1` with `n ≤ 2 ^ e` +(`GaloisRingArith.pairwise_isUnit_liftO_sub_digits`). -/ +theorem pairwise_isUnit_points (hirr : Irreducible ((monicOf x.fl).map (Int.castRingHom (ZMod 2)))) + (ha : active x = true) : + Pairwise fun i j : Fin (points x).length => + IsUnit (liftO hirr ((points x).getD i []) - liftO hirr ((points x).getD j [])) := by + have hn : numPoints x ≤ 2 ^ x.fl.length := by + simp only [active, decide_eq_true_eq] at ha + exact ha.2.2.2.2.2.1 + exact pairwise_isUnit_liftO_sub_digits hirr hn + /-- **The step of an active call is correct**, for the native child builder and well-formed -calls, whenever the interpolation points of every well-formed active call have lifts with unit -differences. -/ -theorem stepCorrect_nativeMk - (hζ : ∀ x (hirr : Irreducible ((monicOf x.fl).map (Int.castRingHom (ZMod 2)))), - active x = true → Pairwise fun i j : Fin (points x).length => - IsUnit (liftO hirr ((points x).getD i []) - liftO hirr ((points x).getD j []))) : - StepCorrect nativeMk WF := by +calls. -/ +theorem stepCorrect_nativeMk : StepCorrect nativeMk WF := by intro x hx ha vals hvals obtain ⟨hirr, hD⟩ := hx have ha' := ha simp only [active, decide_eq_true_eq] at ha' obtain ⟨-, hu, huM, hua, -, -, -⟩ := ha' have hlen : (points x).length = numPoints x := by simp [points] + have hr := rows_le_of_isRowsFirstBipartite hD (one_le_edges_of_active ha) refine NativeCall.val_recover_eq_contraction hirr hD hu huM hua (le_taperStep_mul hu) - (taperStep_mul_le _ _ _) (pow_slots_le_edges_of_active ha) ?_ (points x) (hζ x hirr ha) + (taperStep_mul_le _ _ _) (pow_slots_le_edges_of_active ha) ?_ (points x) + (pairwise_isUnit_points hirr ha) (by rw [hlen]; exact Nat.lt_succ_self _) _ ?_ · calc (slots x + 1) * ∑ t ∈ recoveryNodes (slots x), taperMult (levels x) (step x) t ≤ (slots x + 1) * (2 ^ (slots x + 1) * (step x * levels x)) := @@ -127,14 +180,15 @@ theorem stepCorrect_nativeMk have hw : weights x j = modeWeights (nativeParentPacking x.rows (slots x) x.net).2.1 (2 ^ (padicValInt 2 (node (slots x) k) + 1)) (nodePrecision x.prec (step x) (slots x) x.edges (padicValInt 2 (node (slots x) k))) := by - rw [weights, packing, hgetD, hlev, hprec] + rw [weights, packing_eq hr, hgetD, hlev, hprec] have hstore := val_table_runLoop ha vals hj hi rw [hjk, hw, hprec] at hstore refine hstore.trans ?_ refine congrArg List.sum (List.map_congr_left fun β hβ => ?_) refine congrArg List.prod (List.map_congr_left fun g hg => ?_) - have hmem := mem_children hj (by omega) (by rw [hw, hprec]; exact hβ) - (List.mem_range.mp hg) + have hβ' : β ∈ BudgetTuples.budgetTuples (weights x j) (nodePrec x j) := by + rw [hw, hprec]; exact hβ + have hmem := mem_children hj (by omega) hβ' (List.mem_range.mp hg) have key : ∀ v P, level x k = v → nodePrec x j = P → val P x.fl (vals (j, i, β, g)) = (nativeChild x.fl (slots x) v P (node (slots x) k) ((points x).getD i []) x.rows x.net @@ -142,7 +196,8 @@ theorem stepCorrect_nativeMk fun d bs => val P x.fl (d.entry bs) := by rintro v P rfl rfl have h := hvals _ hmem - simp only [nativeMk, packing] at h + rw [nativeMk_eq ⟨hirr, hD⟩ ha hmem] at h + simp only at h rw [hgetD] at h exact h exact key _ _ hlev hprec @@ -176,7 +231,10 @@ theorem wfChildren_nativeMk : WFChildren nativeMk WF := by have hia : level x ((nodes x).getD c.1 0) < slots x := by rw [level_eq hk] exact padicValInt_lt_of_taperMult_pos (by rwa [← mult_eq _ _ hk]) hua - exact isRowsFirstBipartite_nativeChild (fl := x.fl) hD (pow_slots_le_edges_of_active ha) hia - (nodePrec x c.1) _ ((points x).getD c.2.1 []) c.2.2.1 ⟨c.2.2.2, hg⟩ + have h := isRowsFirstBipartite_nativeChild (fl := x.fl) hD (pow_slots_le_edges_of_active ha) hia + (nodePrec x c.1) (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) + c.2.2.1 ⟨c.2.2.2, hg⟩ + simp only [child, nativeMk_eq ⟨hirr, hD⟩ ha hc] + exact h end Cslib.Circuits.Frontier.FastContraction diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildPolyTime.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildPolyTime.lean new file mode 100644 index 0000000000..a58650892b --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildPolyTime.lean @@ -0,0 +1,734 @@ +/- +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.NativeChild +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Sum +import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListBinaryLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +import Mathlib.Data.List.GetD + +/-! +# The native child networks in polynomial time + +The native child of group `g` of an active call of the contraction recursion of [OpenAI2026ETH] +(§D.4.6, p. 63), `NativeChild.nativeChild`, and its number of rows, `NativeChild.childRows`, are +computable in polynomial time over the encodings of the native recursion. The counts are unary, +the node `t` is in binary sign-magnitude form, and the lists are binary, except the exponents +`β`, which are unary as in a packet descriptor. The parent is encoded by +`DescribedNetwork.encDescribed VertexDesc.enc` and its packing by +`PacketPacking.encNativePacking`. + +The theorems are stated in composition form, for components computed from any input. Besides the +components themselves, they ask for `2 ^ a`, `2 ^ (i + 1)` and the number of packets in unary. +Every packet vertex stores `2 ^ a` and `2 ^ (i + 1)` in unary in its context, and the child has +one packet vertex per packet. For the native parent packing +(`NativeChild.nativeParentPacking`), the packing itself and its number of packets, at most +`M (2 ^ a) ^ 12` for `M` edges, are computed here, with the number of rows in unary. + +**The pieces.** +* The groups of the vertices are looked up in the label words, one vertex at a time. +* The child edges are `ChildNumbering.childEdgeList`, and the ports of a packet are + `ChildNumbering.childPorts`. +* A retained vertex renumbers its ports by counting the earlier edges with an end in its group. + `NativeChild.portRank_eq_countP` puts that count in a form without a unary loop over the port. +* A packet vertex tags each port with the slot of the parent edge, read off the ports of the + group. + +**The shape of the child**, for size bounds along the recursion: +* the child has at most twice as many edges as the parent; +* it has `childRows + P` vertices; +* each vertex is either a parent vertex, with its descriptor and its number of ports, or the + vertex of a packet `q`, with its context, its tags and its slice of `β`. + +## Main results + +* `Cslib.Circuits.Frontier.NativeChild.computableInPolyTime_nativeChild`, + `Cslib.Circuits.Frontier.NativeChild.computableInPolyTime_childRows`: the native child and its + number of rows are polynomial-time. +* `Cslib.Circuits.Frontier.NativeChild.computableInPolyTime_nativeChild_nativeParentPacking`, + `Cslib.Circuits.Frontier.NativeChild.computableInPolyTime_childRows_nativeParentPacking`: the + same for the native parent packing. +* `Cslib.Circuits.Frontier.NativeChild.numPackets_nativeParentPacking_le`: the number of packets. +* `Cslib.Circuits.Frontier.NativeChild.numEdges_nativeChild_le`, + `Cslib.Circuits.Frontier.NativeChild.length_vertices_nativeChild`, + `Cslib.Circuits.Frontier.NativeChild.mem_vertices_nativeChild`: the shape of the child. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.6, p. 63. +-/ + +public section + +namespace Cslib.Circuits.Frontier.NativeChild + +open Turing.MultiTapeTM ChildNumbering NativePacket + +/-- **The rank of a port without a loop over the port**: the edges before `e` with an end in group +`g`, the edges past the list counting as `(0, 0)`. -/ +theorem portRank_eq_countP (groups : List ℕ) (g : ℕ) (ends : List (ℕ × ℕ)) (sel : ℕ × ℕ → ℕ) + (e : ℕ) : + portRank groups g ends sel e = + (List.range (min ends.length e)).countP + (fun e' => decide (groups.getD (sel (ends.getD e' (0, 0))) 0 = g)) + + (e - ends.length) * (if groups.getD (sel (0, 0)) 0 = g then 1 else 0) := by + induction e with + | zero => simp [portRank] + | succ e ih => + have hstep : portRank groups g ends sel (e + 1) = portRank groups g ends sel e + + if groups.getD (sel (ends.getD e (0, 0))) 0 = g then 1 else 0 := by + simp only [portRank, List.range_succ, List.countP_append, List.countP_singleton, + decide_eq_true_eq] + rw [hstep, ih] + rcases lt_or_ge e ends.length with h | h + · rw [min_eq_right h.le, min_eq_right (show e + 1 ≤ ends.length by omega), List.range_succ, + List.countP_append, List.countP_singleton, Nat.sub_eq_zero_of_le h.le, + Nat.sub_eq_zero_of_le (show e + 1 ≤ ends.length by omega)] + simp only [zero_mul, add_zero, decide_eq_true_eq] + · rw [min_eq_left h, min_eq_left (show ends.length ≤ e + 1 by omega), + List.getD_eq_default _ _ h, show e + 1 - ends.length = e - ends.length + 1 by omega] + split_ifs <;> ring + +section PolyTime + +variable {δ : Type} {encIn : δ ↪ List Bool} {groups : δ → List ℕ} {g : δ → ℕ} + {ends : δ → List (ℕ × ℕ)} + +/-- Whether the end `sel` of the edge `e`, in unary, is in group `g`. -/ +private theorem test_polyTime (sel : ℕ × ℕ → ℕ) + (hsel : ComputableInPolyTime sel (encPair encNat encNat) encNat) + (hgroups : ComputableInPolyTime groups encIn (encList encNat)) + (hg : ComputableInPolyTime g encIn encNat) + (hends : ComputableInPolyTime ends encIn (encList (encPair encNat encNat))) : + ComputableInPolyTime (fun p : δ × ℕ => + decide ((groups p.1).getD (sel ((ends p.1).getD p.2 (0, 0))) 0 = g p.1)) + (encPair encIn encUnary) encBool := by + have hentry : ComputableInPolyTime (fun p : δ × ℕ => (ends p.1).getD p.2 (0, 0)) + (encPair encIn encUnary) (encPair encNat encNat) := + (ComputableInPolyTime.listGetD (0, 0)).comp + ((hends.comp (ComputableInPolyTime.fst _ _)).prod (ComputableInPolyTime.snd _ _)) + exact ComputableInPolyTime.decide_eq' + (ComputableInPolyTime.listGetD_binary 0 (hgroups.comp (ComputableInPolyTime.fst _ _)) + (hsel.comp hentry)) + (hg.comp (ComputableInPolyTime.fst _ _)) + +/-- **The ports of a group are polynomial-time.** -/ +theorem computableInPolyTime_portEdges (sel : ℕ × ℕ → ℕ) + (hsel : ComputableInPolyTime sel (encPair encNat encNat) encNat) + (hgroups : ComputableInPolyTime groups encIn (encList encNat)) + (hg : ComputableInPolyTime g encIn encNat) + (hends : ComputableInPolyTime ends encIn (encList (encPair encNat encNat))) : + ComputableInPolyTime (fun x => portEdges (groups x) (g x) (ends x) sel) encIn + (encList encUnary) := + ComputableInPolyTime.filterWithInput + (test := fun x e => decide ((groups x).getD (sel ((ends x).getD e (0, 0))) 0 = g x)) + (ComputableInPolyTime.range.comp ((ComputableInPolyTime.length_list _).comp hends)) + (test_polyTime sel hsel hgroups hg hends) + +/-- **The rank of a port is polynomial-time**, with the port in binary. -/ +theorem computableInPolyTime_portRank (sel : ℕ × ℕ → ℕ) + (hsel : ComputableInPolyTime sel (encPair encNat encNat) encNat) + (hgroups : ComputableInPolyTime groups encIn (encList encNat)) + (hg : ComputableInPolyTime g encIn encNat) + (hends : ComputableInPolyTime ends encIn (encList (encPair encNat encNat))) + {e : δ → ℕ} (he : ComputableInPolyTime e encIn encNat) : + ComputableInPolyTime (fun x => portRank (groups x) (g x) (ends x) sel (e x)) encIn encNat := by + have hlen : ComputableInPolyTime (fun x => (ends x).length) encIn encUnary := + (ComputableInPolyTime.length_list _).comp hends + have hcount := ComputableInPolyTime.countPWithInput + (test := fun x e' => decide ((groups x).getD (sel ((ends x).getD e' (0, 0))) 0 = g x)) + (ComputableInPolyTime.range.comp (ComputableInPolyTime.binary_min_unary' hlen he)) + (test_polyTime sel hsel hgroups hg hends) + have hdefault : ComputableInPolyTime (fun x => decide ((groups x).getD (sel (0, 0)) 0 = g x)) + encIn encBool := + ComputableInPolyTime.decide_eq' + (ComputableInPolyTime.listGetD_binary 0 hgroups (ComputableInPolyTime.const (sel (0, 0)))) + hg + have hextra : ComputableInPolyTime (fun x => + (e x - (ends x).length) * (if decide ((groups x).getD (sel (0, 0)) 0 = g x) then 1 else 0)) + encIn encNat := + ComputableInPolyTime.binary_mul' + (ComputableInPolyTime.binary_sub' he (ComputableInPolyTime.unary_to_binary.comp hlen)) + (ComputableInPolyTime.ite hdefault (ComputableInPolyTime.const 1) + (ComputableInPolyTime.const 0)) + refine (ComputableInPolyTime.binary_add.comp + ((ComputableInPolyTime.unary_to_binary.comp hcount).prod hextra)).of_enc_eq fun x => ?_ + rw [portRank_eq_countP] + simp only [decide_eq_true_eq, Function.comp_apply] + +/-- **The child edge of a port is polynomial-time**, with the vertex and the port in binary. -/ +theorem computableInPolyTime_childEdgeOf {r v e : δ → ℕ} + (hr : ComputableInPolyTime r encIn encNat) + (hgroups : ComputableInPolyTime groups encIn (encList encNat)) + (hg : ComputableInPolyTime g encIn encNat) + (hends : ComputableInPolyTime ends encIn (encList (encPair encNat encNat))) + (hv : ComputableInPolyTime v encIn encNat) (he : ComputableInPolyTime e encIn encNat) : + ComputableInPolyTime (fun x => childEdgeOf (r x) (groups x) (g x) (ends x) (v x) (e x)) + encIn encNat := by + have hR : ComputableInPolyTime (fun x => (portEdges (groups x) (g x) (ends x) Prod.fst).length) + encIn encNat := + ComputableInPolyTime.unary_to_binary.comp ((ComputableInPolyTime.length_list _).comp + (computableInPolyTime_portEdges Prod.fst (ComputableInPolyTime.fst _ _) hgroups hg hends)) + refine (ComputableInPolyTime.ite (ComputableInPolyTime.binary_lt' hv hr) + (computableInPolyTime_portRank Prod.fst (ComputableInPolyTime.fst _ _) hgroups hg hends he) + (ComputableInPolyTime.binary_add.comp (hR.prod (computableInPolyTime_portRank Prod.snd + (ComputableInPolyTime.snd _ _) hgroups hg hends he)))).of_enc_eq fun x => ?_ + simp only [childEdgeOf, decide_eq_true_eq, Function.comp_apply] + +/-- **The parent edge of a child edge is polynomial-time**, with the child edge in binary and the +parent edge in unary. -/ +theorem computableInPolyTime_parentEdge {j : δ → ℕ} + (hgroups : ComputableInPolyTime groups encIn (encList encNat)) + (hg : ComputableInPolyTime g encIn encNat) + (hends : ComputableInPolyTime ends encIn (encList (encPair encNat encNat))) + (hj : ComputableInPolyTime j encIn encNat) : + ComputableInPolyTime (fun x => parentEdge (groups x) (g x) (ends x) (j x)) encIn + encUnary := by + have hfst := computableInPolyTime_portEdges Prod.fst (ComputableInPolyTime.fst _ _) hgroups hg + hends + have hsnd := computableInPolyTime_portEdges Prod.snd (ComputableInPolyTime.snd _ _) hgroups hg + hends + have hR : ComputableInPolyTime (fun x => (portEdges (groups x) (g x) (ends x) Prod.fst).length) + encIn encNat := + ComputableInPolyTime.unary_to_binary.comp ((ComputableInPolyTime.length_list _).comp hfst) + refine (ComputableInPolyTime.ite (ComputableInPolyTime.binary_lt' hj hR) + (ComputableInPolyTime.listGetD_binary (encA := encUnary) 0 hfst hj) + (ComputableInPolyTime.listGetD_binary (encA := encUnary) 0 hsnd + (ComputableInPolyTime.binary_sub' hj hR))).of_enc_eq fun x => ?_ + simp only [parentEdge, decide_eq_true_eq] + +/-- **The groups of the vertices are polynomial-time.** -/ +theorem computableInPolyTime_groupsOf {r i k : δ → ℕ} + {words : δ → List (List ℕ) × List (List ℕ)} + (hr : ComputableInPolyTime r encIn encNat) (hi : ComputableInPolyTime i encIn encUnary) + (hk : ComputableInPolyTime k encIn encUnary) + (hwords : ComputableInPolyTime words encIn + (encPair (encList (encList encNat)) (encList (encList encNat)))) : + ComputableInPolyTime (fun x => groupsOf (r x) (i x) (k x) (words x)) encIn + (encList encNat) := by + let e := encPair encIn encUnary + have hx : ComputableInPolyTime (fun p : δ × ℕ => p.1) e encIn := ComputableInPolyTime.fst _ _ + have hv : ComputableInPolyTime (fun p : δ × ℕ => p.2) e encNat := + ComputableInPolyTime.unary_to_binary.comp (ComputableInPolyTime.snd _ _) + have hw₁ := (ComputableInPolyTime.fst _ _).comp (hwords.comp hx) + have hw₂ := (ComputableInPolyTime.snd _ _).comp (hwords.comp hx) + have hrow : ComputableInPolyTime (fun p : δ × ℕ => + (((words p.1).1.getD p.2 []).getD (i p.1) 0)) e encNat := + (ComputableInPolyTime.listGetD (encA := encNat) (encL := encList encNat) 0).comp + (((ComputableInPolyTime.listGetD (encA := encList encNat) (encL := encList (encList encNat)) + []).comp (hw₁.prod (ComputableInPolyTime.snd _ _))).prod (hi.comp hx)) + have hcol : ComputableInPolyTime (fun p : δ × ℕ => + (((words p.1).2.getD (p.2 - r p.1) []).getD (i p.1) 0)) e encNat := + (ComputableInPolyTime.listGetD (encA := encNat) (encL := encList encNat) 0).comp + ((ComputableInPolyTime.listGetD_binary (encA := encList encNat) [] hw₂ + (ComputableInPolyTime.binary_sub' hv (hr.comp hx))).prod (hi.comp hx)) + have h := ComputableInPolyTime.mapWithInput + (f := fun x v => if decide (v < r x) then ((words x).1.getD v []).getD (i x) 0 + else ((words x).2.getD (v - r x) []).getD (i x) 0) + (ComputableInPolyTime.range.comp hk) + (ComputableInPolyTime.ite (ComputableInPolyTime.binary_lt' hv (hr.comp hx)) hrow hcol) + refine h.of_enc_eq fun x => ?_ + simp only [groupsOf, decide_eq_true_eq, Function.comp_apply] + +/-- Taking a unary number of elements of a list. -/ +private theorem listTake {α : Type} {encA : α ↪ List Bool} {l : δ → List α} {n : δ → ℕ} + (hl : ComputableInPolyTime l encIn (encList encA)) + (hn : ComputableInPolyTime n encIn encUnary) : + ComputableInPolyTime (fun x => (l x).take (n x)) encIn (encList encA) := by + have hrev := ComputableInPolyTime.listReverseWithInput hl + have hdrop := (ComputableInPolyTime.dropUnary (encA := encA) (encL := encList encA)).comp + (hrev.prod (ComputableInPolyTime.unary_sub' + ((ComputableInPolyTime.length_list _).comp hl) hn)) + refine (ComputableInPolyTime.listReverseWithInput hdrop).of_enc_eq fun x => ?_ + change encList encA ((l x).take (n x)) = + encList encA (((l x).reverse.drop ((l x).length - n x)).reverse) + rw [List.drop_reverse, List.reverse_reverse] + rcases le_total (l x).length (n x) with h | h + · rw [Nat.sub_eq_zero_of_le h, Nat.sub_zero, List.take_length, List.take_of_length_le h] + · rw [Nat.sub_sub_self h] + +/-- Counting a group among the groups, in binary. -/ +private theorem count_polyTime (hgroups : ComputableInPolyTime groups encIn (encList encNat)) + (hg : ComputableInPolyTime g encIn encNat) : + ComputableInPolyTime (fun x => (groups x).count (g x)) encIn encNat := by + have h := ComputableInPolyTime.countPWithInput (test := fun x v => decide (v = g x)) hgroups + (ComputableInPolyTime.decide_eq' (ComputableInPolyTime.snd _ _) + (hg.comp (ComputableInPolyTime.fst _ _))) + refine (ComputableInPolyTime.unary_to_binary.comp h).of_enc_eq fun x => ?_ + rw [List.count] + congr 2 + +/-- **The retained vertices**: the vertices of group `g` with their renumbered ports. -/ +private theorem retained_polyTime {r : δ → ℕ} {V : δ → List (List ℕ × VertexDesc)} + (hr : ComputableInPolyTime r encIn encNat) + (hV : ComputableInPolyTime V encIn (encList (encPair (encList encNat) VertexDesc.enc))) + (hgroups : ComputableInPolyTime groups encIn (encList encNat)) + (hg : ComputableInPolyTime g encIn encNat) + (hends : ComputableInPolyTime ends encIn (encList (encPair encNat encNat))) : + ComputableInPolyTime (fun x => + ((List.range (V x).length).filter fun v => decide ((groups x).getD v 0 = g x)).map fun v => + (((V x).getD v defaultVertex).1.map (childEdgeOf (r x) (groups x) (g x) (ends x) v), + ((V x).getD v defaultVertex).2)) + encIn (encList (encPair (encList encNat) VertexDesc.enc)) := by + let e₁ := encPair encIn encUnary + have hx : ComputableInPolyTime (fun p : δ × ℕ => p.1) e₁ encIn := ComputableInPolyTime.fst _ _ + have hy : ComputableInPolyTime (fun p : δ × ℕ => p.2) e₁ encUnary := + ComputableInPolyTime.snd _ _ + have hfilter : ComputableInPolyTime (fun x => (List.range (V x).length).filter + fun v => decide ((groups x).getD v 0 = g x)) encIn (encList encUnary) := + ComputableInPolyTime.filterWithInput (test := fun x v => decide ((groups x).getD v 0 = g x)) + (ComputableInPolyTime.range.comp ((ComputableInPolyTime.length_list _).comp hV)) + (ComputableInPolyTime.decide_eq' + ((ComputableInPolyTime.listGetD (encA := encNat) (encL := encList encNat) 0).comp + ((hgroups.comp hx).prod hy)) (hg.comp hx)) + have hvtx : ComputableInPolyTime (fun p : δ × ℕ => (V p.1).getD p.2 defaultVertex) e₁ + (encPair (encList encNat) VertexDesc.enc) := + (ComputableInPolyTime.listGetD (encA := encPair (encList encNat) VertexDesc.enc) + (encL := encList (encPair (encList encNat) VertexDesc.enc)) defaultVertex).comp + ((hV.comp hx).prod hy) + have hxx : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => q.1.1) (encPair e₁ encNat) encIn := + hx.comp (ComputableInPolyTime.fst _ _) + have hr' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => r q.1.1) (encPair e₁ encNat) encNat := + hr.comp hxx + have hgroups' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => groups q.1.1) (encPair e₁ encNat) + (encList encNat) := hgroups.comp hxx + have hg' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => g q.1.1) (encPair e₁ encNat) encNat := + hg.comp hxx + have hends' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => ends q.1.1) (encPair e₁ encNat) + (encList (encPair encNat encNat)) := hends.comp hxx + have hv' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => q.1.2) (encPair e₁ encNat) encNat := + ComputableInPolyTime.unary_to_binary.comp (hy.comp (ComputableInPolyTime.fst _ _)) + have he' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => q.2) (encPair e₁ encNat) encNat := + ComputableInPolyTime.snd _ _ + have hce : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => + childEdgeOf (r q.1.1) (groups q.1.1) (g q.1.1) (ends q.1.1) q.1.2 q.2) + (encPair e₁ encNat) encNat := + computableInPolyTime_childEdgeOf hr' hgroups' hg' hends' hv' he' + have hports : ComputableInPolyTime (fun p : δ × ℕ => + ((V p.1).getD p.2 defaultVertex).1.map (childEdgeOf (r p.1) (groups p.1) (g p.1) + (ends p.1) p.2)) e₁ (encList encNat) := + ComputableInPolyTime.mapWithInput + (f := fun p e => childEdgeOf (r p.1) (groups p.1) (g p.1) (ends p.1) p.2 e) + ((ComputableInPolyTime.fst _ _).comp hvtx) hce + exact ComputableInPolyTime.mapWithInput + (f := fun x v => (((V x).getD v defaultVertex).1.map + (childEdgeOf (r x) (groups x) (g x) (ends x) v), ((V x).getD v defaultVertex).2)) + hfilter (hports.prod ((ComputableInPolyTime.snd _ _).comp hvtx)) + +variable {fl ζ β : δ → List ℕ} {a i pt r : δ → ℕ} {t : δ → ℤ} + {D : δ → DescribedNetwork VertexDesc} + {pk : δ → (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)} + +/-- **The context of a packet** is polynomial-time, with the packet in unary. -/ +private theorem packetCtx_polyTime (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (ha : ComputableInPolyTime a encIn encUnary) + (hL : ComputableInPolyTime (fun x => 2 ^ a x) encIn encUnary) + (hi : ComputableInPolyTime i encIn encUnary) + (hT : ComputableInPolyTime (fun x => 2 ^ (i x + 1)) encIn encUnary) + (hpt : ComputableInPolyTime pt encIn encUnary) (ht : ComputableInPolyTime t encIn encIntBin) + (hζ : ComputableInPolyTime ζ encIn (encList encNat)) + (hg : ComputableInPolyTime g encIn encNat) : + ComputableInPolyTime (fun p : δ × ℕ => + packetCtx (fl p.1) (a p.1) (i p.1) (pt p.1) (t p.1) (ζ p.1) (g p.1) p.2) + (encPair encIn encUnary) PacketCtx.enc := by + let e₁ := encPair encIn encUnary + have hx : ComputableInPolyTime (fun p : δ × ℕ => p.1) e₁ encIn := ComputableInPolyTime.fst _ _ + have hsym : ComputableInPolyTime (fun p : δ × ℕ => + PacketPacking.packetSymbols (a p.1) 64 p.2 (i p.1)) e₁ (encPair encNat encNat) := + PacketPacking.computableInPolyTime_packetSymbols (ha.comp hx) (ComputableInPolyTime.const 64) + (ComputableInPolyTime.unary_to_binary.comp (ComputableInPolyTime.snd _ _)) (hi.comp hx) + have hs₁ := (ComputableInPolyTime.fst _ _).comp hsym + have hs₂ := (ComputableInPolyTime.snd _ _).comp hsym + have htuple : ComputableInPolyTime (fun p : δ × ℕ => + PacketCtx.equivProd (packetCtx (fl p.1) (a p.1) (i p.1) (pt p.1) (t p.1) (ζ p.1) (g p.1) p.2)) + e₁ PacketCtx.encProd := + ((hpt.comp hx).prod (hfl.comp hx)).prod (((ha.comp hx).prod (hL.comp hx)).prod + (((hi.comp hx).prod (hT.comp hx)).prod ((ht.comp hx).prod ((hpt.comp hx).prod + (((ComputableInPolyTime.decide_eq' hs₁ (hg.comp hx)).prod + ((ComputableInPolyTime.decide_eq' hs₂ (hg.comp hx)).prod + (ComputableInPolyTime.decide_not (ComputableInPolyTime.decide_eq' hs₁ hs₂)))).prod + ((ComputableInPolyTime.const []).prod (hζ.comp hx))))))) + have hsymm : ComputableInPolyTime PacketCtx.equivProd.symm PacketCtx.encProd PacketCtx.enc := + ComputableInPolyTime.of_eq fun y => by + rw [PacketCtx.enc, encOfEquiv_apply, Equiv.apply_symm_apply] + exact (hsymm.comp htuple).of_enc_eq fun p => by + rw [Function.comp_apply, Equiv.symm_apply_apply] + +/-- **The packet vertices**: one per packet, with its ports, their tags, its context and its slice +of the exponents. -/ +private theorem packetVertices_polyTime {P : δ → ℕ} {cedges : δ → List (ℕ × ℕ)} + {place : δ → List (ℕ × ℕ)} + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (ha : ComputableInPolyTime a encIn encUnary) + (hL : ComputableInPolyTime (fun x => 2 ^ a x) encIn encUnary) + (hi : ComputableInPolyTime i encIn encUnary) + (hT : ComputableInPolyTime (fun x => 2 ^ (i x + 1)) encIn encUnary) + (hpt : ComputableInPolyTime pt encIn encUnary) (ht : ComputableInPolyTime t encIn encIntBin) + (hζ : ComputableInPolyTime ζ encIn (encList encNat)) + (hβ : ComputableInPolyTime β encIn (encList encUnary)) + (hg : ComputableInPolyTime g encIn encNat) + (hgroups : ComputableInPolyTime groups encIn (encList encNat)) + (hends : ComputableInPolyTime ends encIn (encList (encPair encNat encNat))) + (hP : ComputableInPolyTime P encIn encUnary) + (hcedges : ComputableInPolyTime cedges encIn (encList (encPair encNat encNat))) + (hplace : ComputableInPolyTime place encIn (encList (encPair encNat encNat))) : + ComputableInPolyTime (fun x => (List.range (P x)).map fun q => + (childPorts (cedges x) ((groups x).count (g x) + q), + (Sum.inr (packetCtx (fl x) (a x) (i x) (pt x) (t x) (ζ x) (g x) q, + (childPorts (cedges x) ((groups x).count (g x) + q)).map fun j => + (decide (j < (portEdges (groups x) (g x) (ends x) Prod.fst).length), + ((place x).getD (parentEdge (groups x) (g x) (ends x) j) (0, 0)).2), + betaSlice (i x) (pt x) (β x) q) : VertexDesc))) + encIn (encList (encPair (encList encNat) VertexDesc.enc)) := by + let e₁ := encPair encIn encUnary + have hx : ComputableInPolyTime (fun p : δ × ℕ => p.1) e₁ encIn := ComputableInPolyTime.fst _ _ + have hy : ComputableInPolyTime (fun p : δ × ℕ => p.2) e₁ encUnary := + ComputableInPolyTime.snd _ _ + -- The ports. + have hpq : ComputableInPolyTime (fun p : δ × ℕ => + childPorts (cedges p.1) ((groups p.1).count (g p.1) + p.2)) e₁ (encList encUnary) := + computableInPolyTime_childPorts.comp ((hcedges.comp hx).prod + (ComputableInPolyTime.binary_add.comp (((count_polyTime hgroups hg).comp hx).prod + (ComputableInPolyTime.unary_to_binary.comp hy)))) + have hpqb : ComputableInPolyTime (fun p : δ × ℕ => + childPorts (cedges p.1) ((groups p.1).count (g p.1) + p.2)) e₁ (encList encNat) := + (ComputableInPolyTime.mapWithInput (f := fun _ j => j) hpq + (ComputableInPolyTime.unary_to_binary.comp (ComputableInPolyTime.snd _ _))).of_enc_eq + fun p => by rw [List.map_id'] + -- The tags of the ports. + have hR : ComputableInPolyTime (fun x => (portEdges (groups x) (g x) (ends x) Prod.fst).length) + encIn encUnary := + (ComputableInPolyTime.length_list _).comp (computableInPolyTime_portEdges Prod.fst + (ComputableInPolyTime.fst _ _) hgroups hg hends) + have hxu : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => q.1.1) (encPair e₁ encUnary) encIn := + hx.comp (ComputableInPolyTime.fst _ _) + have hgroups' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => groups q.1.1) (encPair e₁ encUnary) + (encList encNat) := hgroups.comp hxu + have hg' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => g q.1.1) (encPair e₁ encUnary) encNat := + hg.comp hxu + have hends' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => ends q.1.1) (encPair e₁ encUnary) + (encList (encPair encNat encNat)) := hends.comp hxu + have hj' : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => q.2) (encPair e₁ encUnary) encNat := + ComputableInPolyTime.unary_to_binary.comp (ComputableInPolyTime.snd _ _) + have hpe : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => + parentEdge (groups q.1.1) (g q.1.1) (ends q.1.1) q.2) (encPair e₁ encUnary) encUnary := + computableInPolyTime_parentEdge hgroups' hg' hends' hj' + have htag : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => + (decide (q.2 < (portEdges (groups q.1.1) (g q.1.1) (ends q.1.1) Prod.fst).length), + ((place q.1.1).getD (parentEdge (groups q.1.1) (g q.1.1) (ends q.1.1) q.2) (0, 0)).2)) + (encPair e₁ encUnary) (encPair encBool encNat) := + (ComputableInPolyTime.unary_lt' (ComputableInPolyTime.snd _ _) (hR.comp hxu)).prod + ((ComputableInPolyTime.snd _ _).comp + ((ComputableInPolyTime.listGetD (encA := encPair encNat encNat) + (encL := encList (encPair encNat encNat)) (0, 0)).comp ((hplace.comp hxu).prod hpe))) + have htags := ComputableInPolyTime.mapWithInput + (f := fun p j => (decide (j < (portEdges (groups p.1) (g p.1) (ends p.1) Prod.fst).length), + ((place p.1).getD (parentEdge (groups p.1) (g p.1) (ends p.1) j) (0, 0)).2)) hpq htag + -- The exponents. + have hTp := ComputableInPolyTime.unary_mul' hT hpt + have hdrop : ComputableInPolyTime (fun p : δ × ℕ => + (β p.1).drop (p.2 * (2 ^ (i p.1 + 1) * pt p.1))) e₁ (encList encUnary) := + (ComputableInPolyTime.dropUnary (encA := encUnary) (encL := encList encUnary)).comp + ((hβ.comp hx).prod (ComputableInPolyTime.unary_mul' hy (hTp.comp hx))) + have hslice : ComputableInPolyTime (fun p : δ × ℕ => betaSlice (i p.1) (pt p.1) (β p.1) p.2) + e₁ (encList encUnary) := listTake hdrop (hTp.comp hx) + have hpacket := hpqb.prod ((ComputableInPolyTime.sumInr (encList encNat) encPacketDesc).comp + ((packetCtx_polyTime hfl ha hL hi hT hpt ht hζ hg).prod (htags.prod hslice))) + exact ComputableInPolyTime.mapWithInput (ComputableInPolyTime.range.comp hP) hpacket + +/-- The parts of a native packing. -/ +private theorem packing_parts (hpk : ComputableInPolyTime pk encIn PacketPacking.encNativePacking) : + ComputableInPolyTime (fun x => (pk x).1) encIn + (encPair (encList (encList encNat)) (encList (encList encNat))) ∧ + ComputableInPolyTime (fun x => (pk x).2.2) encIn (encList (encPair encNat encNat)) := by + have hpk' : ComputableInPolyTime pk encIn + (encPair (encPair (encList (encList encNat)) (encList (encList encNat))) + (encPair encNat (encList (encPair encNat encNat)))) := hpk + exact ⟨(ComputableInPolyTime.fst _ _).comp hpk', + (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp hpk')⟩ + +/-- **The number of rows of the native child is polynomial-time.** -/ +theorem computableInPolyTime_childRows (hr : ComputableInPolyTime r encIn encNat) + (hi : ComputableInPolyTime i encIn encUnary) + (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc)) + (hpk : ComputableInPolyTime pk encIn PacketPacking.encNativePacking) + (hg : ComputableInPolyTime g encIn encNat) : + ComputableInPolyTime (fun x => childRows (r x) (i x) (D x) (pk x) (g x)) encIn encNat := + count_polyTime (computableInPolyTime_groupsOf hr hi ((ComputableInPolyTime.length_list _).comp + (DescribedNetwork.vertices_polyTime.comp hD)) (packing_parts hpk).1) hg + +/-- **The native child is polynomial-time.** The counts `a`, `i` and `p_t` are unary, the node +`t` is in binary sign-magnitude form, the lists `fl` and `ζ`, the number of rows `r` and the group +`g` are in binary, and the exponents `β` are unary. The child stores `2 ^ a` and `2 ^ (i + 1)` in +unary in every packet vertex and has one packet vertex per packet, so these and the number of +packets are asked for in unary. -/ +theorem computableInPolyTime_nativeChild (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (ha : ComputableInPolyTime a encIn encUnary) + (hL : ComputableInPolyTime (fun x => 2 ^ a x) encIn encUnary) + (hi : ComputableInPolyTime i encIn encUnary) + (hT : ComputableInPolyTime (fun x => 2 ^ (i x + 1)) encIn encUnary) + (hpt : ComputableInPolyTime pt encIn encUnary) (ht : ComputableInPolyTime t encIn encIntBin) + (hζ : ComputableInPolyTime ζ encIn (encList encNat)) + (hr : ComputableInPolyTime r encIn encNat) + (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc)) + (hpk : ComputableInPolyTime pk encIn PacketPacking.encNativePacking) + (hP : ComputableInPolyTime (fun x => (pk x).2.1) encIn encUnary) + (hβ : ComputableInPolyTime β encIn (encList encUnary)) + (hg : ComputableInPolyTime g encIn encNat) : + ComputableInPolyTime (fun x => + nativeChild (fl x) (a x) (i x) (pt x) (t x) (ζ x) (r x) (D x) (pk x) (β x) (g x)) + encIn (DescribedNetwork.encDescribed VertexDesc.enc) := by + obtain ⟨hwords, hplace⟩ := packing_parts hpk + have hV := DescribedNetwork.vertices_polyTime.comp hD + have hends := (DescribedNetwork.computableInPolyTime_edgeEnds VertexDesc.enc).comp hD + have hgroups := computableInPolyTime_groupsOf hr hi + ((ComputableInPolyTime.length_list _).comp hV) hwords + have hpackets : ComputableInPolyTime (fun x => (pk x).2.2.map Prod.fst) encIn + (encList encNat) := + ComputableInPolyTime.mapWithInput (f := fun _ q => q.1) hplace + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)) + have hcedges : ComputableInPolyTime (fun x => + childEdgeList (groupsOf (r x) (i x) (D x).vertices.length (pk x).1) (g x) (D x).edgeEnds + ((pk x).2.2.map Prod.fst)) encIn (encList (encPair encNat encNat)) := + computableInPolyTime_childEdgeList.comp ((hgroups.prod hg).prod (hends.prod hpackets)) + have hpair := ((ComputableInPolyTime.length_list _).comp hcedges).prod + (ComputableInPolyTime.listAppend' (retained_polyTime hr hV hgroups hg hends) + (packetVertices_polyTime hfl ha hL hi hT hpt ht hζ hβ hg hgroups hends hP hcedges hplace)) + have hsymm : ComputableInPolyTime (DescribedNetwork.equivProd (T := VertexDesc)).symm + (encPair encUnary (encList (encPair (encList encNat) VertexDesc.enc))) + (DescribedNetwork.encDescribed VertexDesc.enc) := + ComputableInPolyTime.of_eq fun y => by + rw [DescribedNetwork.encDescribed, encOfEquiv_apply, Equiv.apply_symm_apply] + exact (hsymm.comp hpair).of_enc_eq fun x => by + rw [Function.comp_apply] + rfl + +end PolyTime + +/-! ### The child of the native parent packing -/ + +/-- A left fold of `max` over numbers at most `n`, from at most `n`, is at most `n`. -/ +private theorem foldl_max_le {l : List ℕ} {m n : ℕ} (hm : m ≤ n) (hl : ∀ x ∈ l, x ≤ n) : + l.foldl max m ≤ n := by + induction l generalizing m with + | nil => exact hm + | cons x l ih => + exact ih (max_le hm (hl x List.mem_cons_self)) fun y hy => hl y (List.mem_cons_of_mem _ hy) + +/-- **At most `M (2 ^ a) ^ 12` packets**: the native parent packing of a network with `M` edges +has at most one block of `2 ^ a` slots per edge, times the `4096 ^ a` words of pairs of +symbols. -/ +theorem numPackets_nativeParentPacking_le (r a : ℕ) (D : DescribedNetwork VertexDesc) : + (nativeParentPacking r a D).2.1 ≤ D.numEdges * (2 ^ a) ^ 12 := by + set pairs := PacketPacking.edgeWordPairs (PacketPacking.labelWords r (D.vertices.length - r) a 64 + (D.edgeEnds.map fun e => (e.1, e.2 - r))).1 (PacketPacking.labelWords r + (D.vertices.length - r) a 64 (D.edgeEnds.map fun e => (e.1, e.2 - r))).2 + (D.edgeEnds.map fun e => (e.1, e.2 - r)) with hpairs + have hlen : pairs.length = D.numEdges := by + simp [hpairs, PacketPacking.edgeWordPairs, DescribedNetwork.edgeEnds] + have hload : PacketPacking.maxLoadOf (PacketPacking.classIndices pairs) ≤ D.numEdges := by + refine foldl_max_le (Nat.zero_le _) fun x hx => ?_ + simp only [PacketPacking.classIndices, List.map_map, List.mem_map, List.mem_range, + Function.comp_apply] at hx + obtain ⟨j, hj, rfl⟩ := hx + have := List.countP_le_length (l := List.range j) + (p := fun j' => decide (pairs.getD j' ([], []) = pairs.getD j ([], []))) + rw [List.length_range] at this + omega + have hblocks : (PacketPacking.maxLoadOf (PacketPacking.classIndices pairs) + (2 ^ a - 1)) / + 2 ^ a ≤ D.numEdges := by + have hL : 1 ≤ 2 ^ a := Nat.one_le_two_pow + rcases Nat.eq_zero_or_pos D.numEdges with h0 | hpos + · rw [h0] at hload ⊢ + rw [Nat.le_zero.mp hload, zero_add] + exact (Nat.div_eq_of_lt (by omega)).le + · refine Nat.div_le_of_le_mul ?_ + have : 2 ^ a - 1 ≤ (2 ^ a - 1) * D.numEdges := Nat.le_mul_of_pos_right _ hpos + have e : 2 ^ a * D.numEdges = D.numEdges + (2 ^ a - 1) * D.numEdges := by + rw [Nat.sub_mul, one_mul] + have : D.numEdges ≤ 2 ^ a * D.numEdges := Nat.le_mul_of_pos_left _ (by omega) + omega + omega + have h64 : (64 * 64) ^ a = (2 ^ a) ^ 12 := by + rw [← pow_mul, mul_comm a 12, pow_mul] + norm_num + change (PacketPacking.maxLoadOf (PacketPacking.classIndices pairs) + (2 ^ a - 1)) / 2 ^ a * + (64 * 64) ^ a ≤ _ + rw [h64] + exact Nat.mul_le_mul_right _ hblocks + +section PolyTime + +variable {δ : Type} {encIn : δ ↪ List Bool} {fl ζ β : δ → List ℕ} {a i pt r g : δ → ℕ} + {t : δ → ℤ} {D : δ → DescribedNetwork VertexDesc} + +/-- **The native parent packing is polynomial-time**, with the number of rows and `a` in +unary. -/ +theorem computableInPolyTime_nativeParentPacking (hr : ComputableInPolyTime r encIn encUnary) + (ha : ComputableInPolyTime a encIn encUnary) + (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc)) : + ComputableInPolyTime (fun x => nativeParentPacking (r x) (a x) (D x)) encIn + PacketPacking.encNativePacking := by + have hends := (DescribedNetwork.computableInPolyTime_edgeEnds VertexDesc.enc).comp hD + have hrb := ComputableInPolyTime.unary_to_binary.comp hr + have hshift : ComputableInPolyTime (fun x => (D x).edgeEnds.map fun e => (e.1, e.2 - r x)) + encIn (encList (encPair encNat encNat)) := + ComputableInPolyTime.mapWithInput (f := fun x e => (e.1, e.2 - r x)) hends + (((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)).prod + (ComputableInPolyTime.binary_sub' ((ComputableInPolyTime.snd _ _).comp + (ComputableInPolyTime.snd _ _)) (hrb.comp (ComputableInPolyTime.fst _ _)))) + have hnC : ComputableInPolyTime (fun x => (D x).vertices.length - r x) encIn encUnary := + ComputableInPolyTime.unary_sub' ((ComputableInPolyTime.length_list _).comp + (DescribedNetwork.vertices_polyTime.comp hD)) hr + have hin : ComputableInPolyTime (fun x => (((r x, (D x).vertices.length - r x, a x), 64, + (D x).edgeEnds.map fun e => (e.1, e.2 - r x)) : PacketPacking.PackingInput)) encIn + (encPair (encPair encUnary (encPair encUnary encUnary)) + (encPair encNat (encList (encPair encNat encNat)))) := + (hr.prod (hnC.prod ha)).prod ((ComputableInPolyTime.const 64).prod hshift) + have h := PacketPacking.computableInPolyTime_nativePacking.comp hin + refine h.of_enc_eq fun x => ?_ + simp only [Function.comp_apply, nativeParentPacking] + +/-- **The number of packets of the native parent packing in unary** is polynomial-time, with `a` +and `2 ^ a` in unary. -/ +theorem computableInPolyTime_numPackets_nativeParentPacking + (hr : ComputableInPolyTime r encIn encUnary) (ha : ComputableInPolyTime a encIn encUnary) + (hL : ComputableInPolyTime (fun x => 2 ^ a x) encIn encUnary) + (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc)) : + ComputableInPolyTime (fun x => (nativeParentPacking (r x) (a x) (D x)).2.1) encIn + encUnary := by + have hpk : ComputableInPolyTime (fun x => nativeParentPacking (r x) (a x) (D x)) encIn + (encPair (encPair (encList (encList encNat)) (encList (encList encNat))) + (encPair encNat (encList (encPair encNat encNat)))) := + computableInPolyTime_nativeParentPacking hr ha hD + exact ComputableInPolyTime.binary_to_unary_bounded + ((ComputableInPolyTime.fst _ _).comp ((ComputableInPolyTime.snd _ _).comp hpk)) + (ComputableInPolyTime.unary_mul' (DescribedNetwork.numEdges_polyTime.comp hD) + ((ComputableInPolyTime.unary_pow 12).comp hL)) + fun x => numPackets_nativeParentPacking_le (r x) (a x) (D x) + +/-- **The native child of the native parent packing is polynomial-time**, with the number of rows +in unary (`computableInPolyTime_nativeChild` for `nativeParentPacking`). -/ +theorem computableInPolyTime_nativeChild_nativeParentPacking + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (ha : ComputableInPolyTime a encIn encUnary) + (hL : ComputableInPolyTime (fun x => 2 ^ a x) encIn encUnary) + (hi : ComputableInPolyTime i encIn encUnary) + (hT : ComputableInPolyTime (fun x => 2 ^ (i x + 1)) encIn encUnary) + (hpt : ComputableInPolyTime pt encIn encUnary) (ht : ComputableInPolyTime t encIn encIntBin) + (hζ : ComputableInPolyTime ζ encIn (encList encNat)) + (hr : ComputableInPolyTime r encIn encUnary) + (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc)) + (hβ : ComputableInPolyTime β encIn (encList encUnary)) + (hg : ComputableInPolyTime g encIn encNat) : + ComputableInPolyTime (fun x => nativeChild (fl x) (a x) (i x) (pt x) (t x) (ζ x) (r x) (D x) + (nativeParentPacking (r x) (a x) (D x)) (β x) (g x)) + encIn (DescribedNetwork.encDescribed VertexDesc.enc) := + computableInPolyTime_nativeChild hfl ha hL hi hT hpt ht hζ + (ComputableInPolyTime.unary_to_binary.comp hr) hD + (computableInPolyTime_nativeParentPacking hr ha hD) + (computableInPolyTime_numPackets_nativeParentPacking hr ha hL hD) hβ hg + +/-- **The number of rows of the native child of the native parent packing is polynomial-time.** -/ +theorem computableInPolyTime_childRows_nativeParentPacking + (hr : ComputableInPolyTime r encIn encUnary) (ha : ComputableInPolyTime a encIn encUnary) + (hi : ComputableInPolyTime i encIn encUnary) + (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc)) + (hg : ComputableInPolyTime g encIn encNat) : + ComputableInPolyTime (fun x => childRows (r x) (i x) (D x) + (nativeParentPacking (r x) (a x) (D x)) (g x)) encIn encNat := + computableInPolyTime_childRows (ComputableInPolyTime.unary_to_binary.comp hr) hi hD + (computableInPolyTime_nativeParentPacking hr ha hD) hg + +end PolyTime + +/-! ### The shape of the native child -/ + +section Shape + +variable (fl : List ℕ) (a i pt : ℕ) (t : ℤ) (ζ : List ℕ) (r : ℕ) (D : DescribedNetwork VertexDesc) + (pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)) (β : List ℕ) (g : ℕ) + +/-- **The child has at most twice as many edges as the parent**: one per end of a parent edge in +group `g`. -/ +theorem numEdges_nativeChild_le : + (nativeChild fl a i pt t ζ r D pk β g).numEdges ≤ 2 * D.numEdges := by + have hends : D.edgeEnds.length = D.numEdges := by simp [DescribedNetwork.edgeEnds] + have hzip : (D.edgeEnds.zip (pk.2.2.map Prod.fst)).length ≤ D.numEdges := by + rw [List.length_zip] + omega + simp only [nativeChild, childEdgeList, List.length_append, List.length_map] + have h₁ := List.length_filter_le (fun q : (ℕ × ℕ) × ℕ => + decide ((groupsOf r i D.vertices.length pk.1).getD q.1.1 0 = g)) + (D.edgeEnds.zip (pk.2.2.map Prod.fst)) + have h₂ := List.length_filter_le (fun q : (ℕ × ℕ) × ℕ => + decide ((groupsOf r i D.vertices.length pk.1).getD q.1.2 0 = g)) + (D.edgeEnds.zip (pk.2.2.map Prod.fst)) + omega + +/-- **The vertices of the child**: its rows, the parent vertices of group `g`, then one packet +vertex per packet. -/ +theorem length_vertices_nativeChild : + (nativeChild fl a i pt t ζ r D pk β g).vertices.length = childRows r i D pk g + pk.2.1 := by + simp only [nativeChild, childRows, List.length_append, List.length_map, List.length_range] + congr 1 + rw [List.count_eq_countP, List.countP_eq_length_filter, groupsOf, List.filter_map, + List.length_map] + congr 1 + refine List.filter_congr fun v hv => ?_ + rw [List.mem_range] at hv + simp only [Function.comp_apply] + rw [List.getD_eq_getElem _ _ (by simpa using hv), List.getElem_map, List.getElem_range, + beq_eq_decide] + +/-- **Every vertex of the child is a parent vertex or a packet vertex.** A vertex of the child is +either a parent vertex with renumbered ports, with the same descriptor and the same number of +ports, or the vertex of a packet `q`, whose descriptor is its context, tags of its ports with +slots from the packing (or `0`), and its slice of `β`. -/ +theorem mem_vertices_nativeChild {v : List ℕ × VertexDesc} + (hv : v ∈ (nativeChild fl a i pt t ζ r D pk β g).vertices) : + (∃ w ∈ D.vertices, v.2 = w.2 ∧ v.1.length = w.1.length) ∨ + ∃ q < pk.2.1, ∃ tags : List (Bool × ℕ), + v.2 = .inr (packetCtx fl a i pt t ζ g q, tags, betaSlice i pt β q) ∧ + tags.length = v.1.length ∧ ∀ b ∈ tags, b.2 = 0 ∨ ∃ y ∈ pk.2.2, b.2 = y.2 := by + simp only [nativeChild, List.mem_append, List.mem_map, List.mem_filter, List.mem_range] at hv + rcases hv with ⟨u, ⟨hu, -⟩, rfl⟩ | ⟨q, hq, rfl⟩ + · refine Or.inl ⟨D.vertices.getD u defaultVertex, ?_, rfl, List.length_map _⟩ + rw [List.getD_eq_getElem _ _ hu] + exact List.getElem_mem hu + · refine Or.inr ⟨q, hq, _, rfl, List.length_map _, fun b hb => ?_⟩ + obtain ⟨j, -, rfl⟩ := List.mem_map.mp hb + rcases lt_or_ge (parentEdge (groupsOf r i D.vertices.length pk.1) g D.edgeEnds j) + pk.2.2.length with h | h + · rw [List.getD_eq_getElem _ _ h] + exact Or.inr ⟨_, List.getElem_mem h, rfl⟩ + · rw [List.getD_eq_default _ _ h] + exact Or.inl rfl + +/-- The slice of `β` at a packet has at most `2 ^ (i + 1) p_t` exponents. -/ +theorem length_betaSlice_le (q : ℕ) : (betaSlice i pt β q).length ≤ 2 ^ (i + 1) * pt := + List.length_take_le _ _ + +/-- The exponents in the slice of `β` at a packet are exponents of `β`. -/ +theorem mem_of_mem_betaSlice {q b : ℕ} (hb : b ∈ betaSlice i pt β q) : b ∈ β := + List.mem_of_mem_drop (List.mem_of_mem_take hb) + +end Shape + +end Cslib.Circuits.Frontier.NativeChild diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean index 9cb5d17ff7..a498a0ba11 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Gua public import Complexity.Computability.Complexity.Classes.CountingSimulation.Admissible public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionMachine public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionPolyTime import Mathlib.Analysis.SpecificLimits.Normed import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat @@ -51,11 +52,10 @@ finish, and the machine falls back to direct summation, at a constant factor. The guard is polynomial-time (`CountingSimulation.fastGuard_polyTime`). -For the native child builder (`FastContraction.nativeMk`), the step, the passage of -well-formedness to the children and the well-formed roots are proved -(`CountingSimulation.contractionAlgorithmOfNative`); there the remaining obligations are the -components of the scheme in polynomial time, the unit differences of the interpolation points and -the resource analysis. +For the native child builder (`FastContraction.nativeMk`), the components of the scheme are +polynomial-time (`FastContraction.scheme_nativeMk_polyTime`), and the step, the passage of +well-formedness to the children and the well-formed roots are proved; there the one remaining +obligation is the resource analysis (`CountingSimulation.contractionAlgorithmOfNative`). **Remaining obligations** (the hypotheses of `CountingSimulation.contractionAlgorithmOfFast`): the components of the scheme in polynomial time, the correctness of one active call @@ -69,7 +69,7 @@ components of the scheme in polynomial time, the correctness of one active call * `Cslib.Complexity.CountingSimulation.contractionAlgorithmOfFast`: the contraction algorithm from the remaining obligations. * `Cslib.Complexity.CountingSimulation.contractionAlgorithmOfNative`: the same for the native child - builder, with fewer obligations. + builder, from the resource analysis alone. ## Main results @@ -172,19 +172,6 @@ private theorem fastGuard_eq_guardTest (G : ℕ × ExplicitTensorNetwork ℕ) : · rintro ⟨⟨⟨h1, h2⟩, h3⟩, h4⟩ exact ⟨⟨fun v hv i hi => h1 v hv i hi, fun i hi => h2 i hi⟩, h3, h4⟩ -/-- The degree bound `2 ^ (9 ⌊log₂ m⌋ / 10 + 2)`, in binary from `m` in unary. -/ -private theorem degreeBound_polyTime : ComputableInPolyTime degreeBound encUnary encNat := by - have hb := ComputableInPolyTime.unary_to_binary - have hlog := ComputableInPolyTime.binary_log_two.comp hb - have he : ComputableInPolyTime (fun m => 9 * Nat.log 2 m / 10 + 2) encUnary encUnary := - ComputableInPolyTime.binary_to_unary_bounded - (ComputableInPolyTime.binary_add.comp ((ComputableInPolyTime.binary_div.comp - ((ComputableInPolyTime.binary_mul' (ComputableInPolyTime.const 9) (hb.comp hlog)).prod - (ComputableInPolyTime.const 10))).prod (ComputableInPolyTime.const 2))) - (ComputableInPolyTime.unary_add' hlog (ComputableInPolyTime.const 2)) fun m => by - simp only [Function.comp_apply]; omega - exact ComputableInPolyTime.binary_two_pow.comp he - /-- **The guard is polynomial-time.** -/ theorem fastGuard_polyTime : ComputableInPolyTime fastGuard encG encBool := by have hpair : ComputableInPolyTime (DescribedNetwork.equivProd (T := List ℕ)) @@ -650,21 +637,15 @@ theorem wf_root (P : ℕ) {G : ℕ × ExplicitTensorNetwork ℕ} (hg : fastGuard ← List.map_drop, List.map_map, Function.comp_def] at hi ⊢ exact h2 i hi -/-- **The contraction algorithm from the native recursion**, given its remaining obligations: the -components of the scheme in polynomial time, the unit differences of the interpolation points, and -the resource analysis. The step, the passage of well-formedness to the children and the -well-formed roots are proved (`FastContraction.stepCorrect_nativeMk`, +/-- **The contraction algorithm from the native recursion**, given its one remaining obligation, +the resource analysis. The components of the scheme are polynomial-time +(`FastContraction.scheme_nativeMk_polyTime`), and the step, the passage of well-formedness to the +children and the well-formed roots are proved (`FastContraction.stepCorrect_nativeMk`, `FastContraction.wfChildren_nativeMk`, `CountingSimulation.wf_root`). -/ -noncomputable def contractionAlgorithmOfNative - (hpoly : (scheme nativeMk).PolyTime encCall encFrame encValue) - (hζ : ∀ x (hirr : Irreducible ((GaloisRingArith.monicOf x.fl).map - (Int.castRingHom (ZMod 2)))), active x = true → - Pairwise fun i j : Fin (points x).length => IsUnit (GaloisRingArith.liftO hirr - ((points x).getD i []) - GaloisRingArith.liftO hirr ((points x).getD j []))) - (hana : FastAnalysis nativeMk) : +noncomputable def contractionAlgorithmOfNative (hana : FastAnalysis nativeMk) : ContractionAlgorithm (encPair encNat ExplicitTensorNetwork.encExplicitNetwork) (fun G => G.2.contraction) ExplicitAdmissible := - contractionAlgorithmOfFast hpoly (stepCorrect_nativeMk hζ) wfChildren_nativeMk + contractionAlgorithmOfFast scheme_nativeMk_polyTime stepCorrect_nativeMk wfChildren_nativeMk (fun P _ hg => wf_root P hg) hana end Resources diff --git a/Complexity/Foundations/Combinatorics/BudgetTuples.lean b/Complexity/Foundations/Combinatorics/BudgetTuples.lean index 3ed809c732..20d48a9bcd 100644 --- a/Complexity/Foundations/Combinatorics/BudgetTuples.lean +++ b/Complexity/Foundations/Combinatorics/BudgetTuples.lean @@ -55,6 +55,7 @@ along `budgetTuples` (`sum_filter_weight_lt_eq`). * `Cslib.BudgetTuples.mem_budgetTuples`, `Cslib.BudgetTuples.nodup_budgetTuples`: the list holds each tuple of weight below the budget once. +* `Cslib.BudgetTuples.lt_of_mem_budgetTuples`: the entries of these tuples are below the budget. * `Cslib.BudgetTuples.head?_budgetTuples`, `Cslib.BudgetTuples.isChain_budgetTuples`, `Cslib.BudgetTuples.budgetNext_getLast?`: the successor walks the list from the zero tuple. * `Cslib.BudgetTuples.budgetNextScan_eq`: the scan computes the successor. @@ -133,6 +134,26 @@ theorem mem_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} { · simp only [List.length_cons, Nat.add_right_cancel_iff, weight_cons_cons] at hlen hwt exact ⟨b, by omega, γ, ih'.mpr ⟨hlen, by omega⟩, rfl⟩ +/-- Each entry of a tuple is at most its weight, for positive weights. -/ +theorem le_weight_of_mem : ∀ {ws β : List ℕ}, (∀ w ∈ ws, 0 < w) → β.length = ws.length → + ∀ b ∈ β, b ≤ weight ws β + | [], [], _, _, b, hb => by simp at hb + | [], _ :: _, _, hl, _, _ => by simp at hl + | _ :: _, [], _, hl, _, _ => by simp at hl + | w :: ws, b' :: β, hw, hl, b, hb => by + rw [weight_cons_cons] + rcases List.mem_cons.mp hb with rfl | hb + · exact (Nat.le_mul_of_pos_left b (hw w List.mem_cons_self)).trans (Nat.le_add_right _ _) + · have := le_weight_of_mem (fun w' hw' => hw w' (List.mem_cons_of_mem _ hw')) + (by simpa using hl) b hb + omega + +/-- **Every entry of a tuple of weight below `p` is below `p`**, for positive weights. -/ +theorem lt_of_mem_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} {β : List ℕ} + (hβ : β ∈ budgetTuples ws p) {b : ℕ} (hb : b ∈ β) : b < p := by + obtain ⟨hl, hwt⟩ := (mem_budgetTuples hw).mp hβ + exact (le_weight_of_mem hw hl b hb).trans_lt hwt + /-- **Each tuple appears once.** -/ theorem nodup_budgetTuples (ws : List ℕ) (p : ℕ) : (budgetTuples ws p).Nodup := by induction ws generalizing p with diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChildPolyTime.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChildPolyTime.lean new file mode 100644 index 0000000000..5a4e66be69 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChildPolyTime.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: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeChildPolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends + +public section + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.NativeChild Cslib.GaloisRingArith + Turing.MultiTapeTM + +namespace Cslib.Tests.TensorNetworkNativeChildPolyTime + +/-! ### Ranks of ports past the edges + +A port past the edges reads the edge `(0, 0)`, so the rank of a large port counts it. -/ + +example : portRank [0, 1] 0 [(0, 1)] Prod.fst 3 = 3 := by decide + +example : portRank [0, 1] 0 [(0, 1)] Prod.fst 3 = + (List.range (min 1 3)).countP (fun e' => decide ([0, 1].getD (([(0, 1)].getD e' (0, 0)).1) 0 = + 0)) + (3 - 1) * (if [0, 1].getD ((0, 0) : ℕ × ℕ).1 0 = 0 then 1 else 0) := + portRank_eq_countP _ _ _ _ _ + +/-! ### The shape of a small child + +The path of `TensorNetworkNativeChild` with one row joined to two columns. The child of group `0` +keeps the row and the column `1` and adds one packet. -/ + +/-- The tables of the vertices. -/ +def table (n : ℕ) : VertexDesc := .inl (List.replicate n 1) + +/-- The row `0` with ports `1, 0`, the columns `1` and `2`. -/ +def path : DescribedNetwork VertexDesc := + ⟨2, [([1, 0], table 4), ([0], table 2), ([1], table 2)]⟩ + +/-- The packing: the row and the column `1` in group `0`, the column `2` in group `1`, both edges +in packet `0`. -/ +def packing : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ) := + (([[0]], [[0], [1]]), 1, [(0, 0), (0, 1)]) + +example : (nativeChild [1] 1 0 3 (-1) [0] 1 path packing [] 0).numEdges ≤ 2 * path.numEdges := + numEdges_nativeChild_le _ _ _ _ _ _ _ _ _ _ _ + +example : (nativeChild [1] 1 0 3 (-1) [0] 1 path packing [] 0).vertices.length = 3 := by + rw [length_vertices_nativeChild] + decide + +/-! ### Polynomial time on a concrete input + +The composition form applies to an input carrying a parent, its packing words and placements, +and its number of packets in unary, with the other parameters fixed. -/ + +/-- A parent, the packing words, the number of packets and the placements. -/ +abbrev Input : Type := + DescribedNetwork VertexDesc × (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ) + +/-- The encoding of `Input`, with the number of packets in unary. -/ +abbrev encInput : Input ↪ List Bool := + encPair (DescribedNetwork.encDescribed VertexDesc.enc) + (encPair (encPair (encList (encList encNat)) (encList (encList encNat))) + (encPair encUnary (encList (encPair encNat encNat)))) + +example : ComputableInPolyTime (fun x : Input => + nativeChild [1] 1 0 3 (-1) [0] 1 x.1 x.2 [] 0) encInput + (DescribedNetwork.encDescribed VertexDesc.enc) := by + have hpk : ComputableInPolyTime (fun x : Input => x.2) encInput + PacketPacking.encNativePacking := + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)).prod + ((ComputableInPolyTime.unary_to_binary.comp ((ComputableInPolyTime.fst _ _).comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _)))).prod + ((ComputableInPolyTime.snd _ _).comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _)))) + exact computableInPolyTime_nativeChild (ComputableInPolyTime.const _) + (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) + (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) + (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) (ComputableInPolyTime.fst _ _) + hpk ((ComputableInPolyTime.fst _ _).comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _))) + (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) + +/-- With the native parent packing, the number of rows and `a` are the only further inputs. -/ +example : ComputableInPolyTime (fun D : DescribedNetwork VertexDesc => + nativeChild [1] 1 0 3 (-1) [0] 1 D (nativeParentPacking 1 1 D) [] 0) + (DescribedNetwork.encDescribed VertexDesc.enc) + (DescribedNetwork.encDescribed VertexDesc.enc) := + computableInPolyTime_nativeChild_nativeParentPacking (ComputableInPolyTime.const _) + (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) + (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) + (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) ComputableInPolyTime.id' + (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) + +example : (nativeParentPacking 1 0 path).2.1 ≤ 2 := + (numPackets_nativeParentPacking_le 1 0 path).trans (by decide) + +/-! ### Binary-digit points + +The digits below `e = 2` of `0, 1, 2` are the lists of the interpolation points. -/ + +example : ((List.range 3).map fun k => (List.range 2).map fun j => if k.testBit j then 1 else 0) = + [[0, 0], [1, 0], [0, 1]] := by decide + +example (hirr : Irreducible ((monicOf [1, 1]).map (Int.castRingHom (ZMod 2)))) : + Pairwise fun i j : Fin ((List.range 3).map fun k => + (List.range [1, 1].length).map fun j => if k.testBit j then 1 else 0).length => + IsUnit (liftO hirr (((List.range 3).map fun k => + (List.range [1, 1].length).map fun j => if k.testBit j then 1 else 0).getD i []) - + liftO hirr (((List.range 3).map fun k => + (List.range [1, 1].length).map fun j => if k.testBit j then 1 else 0).getD j [])) := + pairwise_isUnit_liftO_sub_digits hirr (by decide) + +end Cslib.Tests.TensorNetworkNativeChildPolyTime diff --git a/ComplexityTests/FastContractionPolyTime.lean b/ComplexityTests/FastContractionPolyTime.lean new file mode 100644 index 0000000000..2b8c3ca973 --- /dev/null +++ b/ComplexityTests/FastContractionPolyTime.lean @@ -0,0 +1,51 @@ +/- +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.Complexity.Classes.CountingSimulation.FastAlgorithm + +/-! # The components of the native contraction recursion in polynomial time: checked instances + +The caps on the rows and the exponents, the schedule's quantities on a call that is not active, +and the instance of the contraction interface from the resource analysis alone. -/ + +namespace ComplexityTests.FastContractionPolyTime + +open Turing.MultiTapeTM Cslib.Circuits.Frontier Cslib.Circuits.Frontier.FastContraction + Cslib.Circuits.Frontier.ContractionSchedule Cslib.Complexity.CountingSimulation + +/-- One row `0` and one column `1` joined by edge `0`, with full tables. -/ +def tiny : ExplicitTensorNetwork ℕ := ⟨1, [([0], [1, 2]), ([0], [3, 4])]⟩ + +-- The number of rows is stored in binary, so a call may claim `2 ^ 100` rows; the cap keeps the +-- two vertices, and on the rows-first root it is inactive. +example : rowCap (root (3, 2 ^ 100, tiny)) = 2 := by decide +example : rowCap (root (3, 1, tiny)) = 1 := by decide + +-- The packing of the root: one packet of `2 ^ 0` slots, within the bound `M (2 ^ a) ^ 12`. +example : slots (root (3, 1, tiny)) = 0 := by decide +example : (packing (root (3, 1, tiny))).2.1 = 1 := by decide +example : (packing (root (3, 1, tiny))).2.1 ≤ + (root (3, 1, tiny)).edges * (2 ^ slots (root (3, 1, tiny))) ^ 12 := + NativeChild.numPackets_nativeParentPacking_le _ _ _ + +-- On every call, `2 ^ a ≤ s + 1`, and the levels are at most `a + 1`. +example (x : Call) : 2 ^ slots x ≤ x.scale + 1 := two_pow_slots_le x +example (x : Call) (k : ℕ) : level x k ≤ slots x + 1 := level_le x k + +-- The cap on the exponents leaves the tuples of weight below the budget unchanged. +example : ([1, 0, 1] : List ℕ).map (min · 3) = [1, 0, 1] := + map_min_of_mem_budgetTuples (ws := [1, 1, 1]) (by decide) (by decide) + +-- The components of the scheme of the native child builder are polynomial-time. +example : (scheme nativeMk).PolyTime encCall encFrame encValue := scheme_nativeMk_polyTime + +-- The contraction interface for admissible explicit networks, from the resource analysis alone. +noncomputable example (hana : FastAnalysis nativeMk) : + ContractionAlgorithm (encPair encNat ExplicitTensorNetwork.encExplicitNetwork) + (fun G => G.2.contraction) ExplicitAdmissible := + contractionAlgorithmOfNative hana + +end ComplexityTests.FastContractionPolyTime