diff --git a/Complexity.lean b/Complexity.lean index 49730c8bf0..66e3c77e00 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -893,12 +893,15 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.CoeffSchem public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedContraction +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedLift public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates public import Complexity.Computability.Circuit.Frontier.TensorNetwork.KernelProduct public import Complexity.Computability.Circuit.Frontier.TensorNetwork.LocalDeformation 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.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 new file mode 100644 index 0000000000..e3f6ad7c22 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean @@ -0,0 +1,414 @@ +/- +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.ReductionLift +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.VertexDesc +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Recursion +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +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 Mathlib.Data.List.GetD +import Mathlib.Data.List.Sort + +/-! +# A described network over `O` + +The contraction recursion of [OpenAI2026ETH] (§D.4, pp. 57–64) is proved correct over the valuation +ring `O = ℤ_(2)[U] / (f)`, while the native algorithm carries networks of descriptors +(`DescribedNetwork VertexDesc`) and computes with coefficient lists in +`A_p = (ℤ / 2 ^ p)[U] / (f)`. This file gives the network over `O` that a described network stands +for. + +* **Lifts.** A coefficient list `c` lifts to `∑ i < e, c_i U ^ i` in `O` (`GaloisRingArith.liftO`), + 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. +* **Rows first.** A described network is *rows-first bipartite* at `r` + (`DescribedNetwork.IsRowsFirstBipartite`) when every port names an edge and every edge is a port + of exactly one of the first `r` vertices, once, and of exactly one of the others, once. The ends + of the edges are then computed by listing the vertices at each edge + (`DescribedNetwork.incident`, `DescribedNetwork.edgeEnds`), in polynomial time + (`DescribedNetwork.computableInPolyTime_edgeEnds`). +* **The network** (`DescribedNetwork.toNetwork`). A rows-first described network and an evaluator + give a Boolean tensor network on `Fin k` vertices and `Fin m` edges with these ends, whose + tensor at a vertex is the evaluator at its descriptor and the bits on its ports. It has the + contraction of the described network (`DescribedNetwork.contraction_toNetwork`). Over `O`, with + the lifts of the entries, its contraction reduces modulo `2 ^ p` to the contraction of the + values in `A_p` (`DescribedNetwork.reduction_contraction_toNetwork`). + +## Main definitions + +* `Cslib.GaloisRingArith.liftO`: the lift of a coefficient list to `O`. +* `Cslib.Circuits.Frontier.DescribedNetwork.incident`, + `Cslib.Circuits.Frontier.DescribedNetwork.edgeEnds`: the ends of the edges. +* `Cslib.Circuits.Frontier.DescribedNetwork.toNetwork`: the network of a described network. + +## Main results + +* `Cslib.GaloisRingArith.reduction_liftO`, `Cslib.GaloisRingArith.mk_liftO`: reducing a lift. +* `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. +* `Cslib.Circuits.Frontier.DescribedNetwork.computableInPolyTime_edgeEnds`: polynomial time. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.1 (pp. 57–58) and + §D.4.6 (pp. 63–64). +-/ + +public section + +open Polynomial AdjoinRoot Finset + +/-! ### Lifts of coefficient lists -/ + +namespace AdjoinRoot + +/-- `ℤ_(2)` lies in the valuation ring `O` of `ℚ[U] / (f)`. -/ +theorem algebraMap_mem_integer_padicValuation {f : ℤ[X]} (hf : f.Monic) + (hirr : Irreducible (f.map (Int.castRingHom (ZMod 2)))) : + ∀ c ∈ Valuation.integer (Rat.padicValuation 2), + algebraMap ℚ (AdjoinRoot (f.map (Int.castRingHom ℚ))) c ∈ + (padicValuation 2 hf hirr).integer := fun c hc => by + rw [Valuation.mem_integer_iff, padicValuation_algebraMap] + exact hc + +end AdjoinRoot + +namespace Cslib.GaloisRingArith + +variable {fl : List ℕ} (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) + +/-- The class of `U` in the valuation ring `O = ℤ_(2)[U] / (f)`, `f = monicOf fl`. -/ +noncomputable def rootO : (padicValuation 2 (monic_monicOf fl) hirr).integer := + ⟨map (Int.castRingHom ℚ) (monicOf fl) _ dvd_rfl (root _), + (Valuation.mem_integer_iff _ _).mpr (padicValuation_map_le_one _ hirr _)⟩ + +/-- **The lift of a coefficient list to `O`**: `∑ i < e, c_i U ^ i`, with `e = fl.length`. -/ +noncomputable def liftO (c : List ℕ) : (padicValuation 2 (monic_monicOf fl) hirr).integer := + ∑ i ∈ range fl.length, ((c.getD i 0 : ℕ) : (padicValuation 2 (monic_monicOf fl) hirr).integer) * + rootO hirr ^ i + +/-- Reduction sends `U` to `U`. -/ +theorem reduction_rootO (p : ℕ) : + reduction (monic_monicOf fl) hirr p (rootO hirr) = root _ := by + rw [rootO, reduction_toRat, map_root] + +/-- **Reducing a lift modulo `2 ^ p` gives the value in `A_p`.** -/ +theorem reduction_liftO (p : ℕ) (c : List ℕ) : + reduction (monic_monicOf fl) hirr p (liftO hirr c) = val p fl c := by + simp only [liftO, val, map_sum, map_mul, map_natCast, map_pow, reduction_rootO] + +/-- **The class of a lift modulo `2 ^ p`** is the image of the value in `A_p`. -/ +theorem mk_liftO (p : ℕ) (c : List ℕ) : + Ideal.Quotient.mk _ (liftO hirr c) = + Cslib.Circuits.Frontier.reductionLift (monic_monicOf fl) hirr p (val p fl c) := by + rw [← reduction_liftO hirr p, Cslib.Circuits.Frontier.reductionLift_reduction] + +end Cslib.GaloisRingArith + +namespace Cslib.Circuits.Frontier + +/-! ### Lists of lists with one occurrence -/ + +/-- **One occurrence among the lists.** If an element occurs once in total among a list of +lists, exactly one of the lists contains it, once. -/ +theorem exists_unique_of_sum_count_eq_one {Ls : List (List ℕ)} {j : ℕ} + (h : (Ls.map fun l => l.count j).sum = 1) : + ∃ i, ∃ hi : i < Ls.length, Ls[i].count j = 1 ∧ + ∀ i' (hi' : i' < Ls.length), j ∈ Ls[i'] → i' = i := by + induction Ls with + | nil => simp at h + | cons l Ls ih => + rw [List.map_cons, List.sum_cons] at h + by_cases hj : j ∈ l + · have hl : l.count j = 1 := by + have := List.count_pos_iff.mpr hj + omega + have h0 : (Ls.map fun l => l.count j).sum = 0 := by omega + refine ⟨0, by simp, by simpa using hl, fun i' hi' hm => ?_⟩ + rcases i' with _ | i' + · rfl + · exfalso + have hi'' : i' < Ls.length := by simpa using hi' + simp only [List.getElem_cons_succ] at hm + have hpos := List.count_pos_iff.mpr hm + have hle : Ls[i'].count j ≤ (Ls.map fun l => l.count j).sum := + List.le_sum_of_mem (List.mem_map.mpr ⟨_, List.getElem_mem _, rfl⟩) + omega + · have hl : l.count j = 0 := List.count_eq_zero.mpr hj + obtain ⟨i, hi, hc, hu⟩ := ih (by omega) + refine ⟨i + 1, by simpa using hi, by simpa using hc, fun i' hi' hm => ?_⟩ + rcases i' with _ | i' + · exact absurd hm (by simpa using hj) + · simp only [List.getElem_cons_succ] at hm + rw [hu i' (by simpa using hi') hm] + +namespace DescribedNetwork + +variable {T : Type} (D : DescribedNetwork T) + +/-! ### Rows first -/ + +/-- Being rows-first depends only on the ports, not on the descriptors. -/ +theorem isRowsFirstBipartite_map {T' : Type} (f : T → T') (r : ℕ) : + (⟨D.numEdges, D.vertices.map fun v => (v.1, f v.2)⟩ : + DescribedNetwork T').IsRowsFirstBipartite r ↔ + D.IsRowsFirstBipartite r := by + simp only [IsRowsFirstBipartite, List.forall_mem_map, ← List.map_take, ← List.map_drop, + List.map_map, Function.comp_def] + +/-- The vertices at the edge `j`: those having `j` among their ports, in increasing order. -/ +@[expose] def incident (j : ℕ) : List ℕ := + (List.range D.vertices.length).filter fun v => j ∈ (D.vertices.map Prod.fst).getD v [] + +/-- **The ends of the edges**: for each edge, its first and its second vertex. -/ +@[expose] def edgeEnds : List (ℕ × ℕ) := + (List.range D.numEdges).map fun j => ((D.incident j).getD 0 0, (D.incident j).getD 1 0) + +variable {D} + +theorem getD_map_fst (v : ℕ) (hv : v < D.vertices.length) : + (D.vertices.map Prod.fst).getD v [] = D.vertices[v].1 := by + rw [List.getD_eq_getElem _ _ (by simpa using hv), List.getElem_map] + +/-- **The two ends of an edge** of a rows-first network: a row `s < r` and a column `t ≥ r`, which +are the only vertices with the edge among their ports, each once. -/ +theorem exists_ends {r : ℕ} (hD : D.IsRowsFirstBipartite r) {j : ℕ} (hj : j < D.numEdges) : + ∃ s t, ∃ hs : s < D.vertices.length, ∃ ht : t < D.vertices.length, s < r ∧ r ≤ t ∧ + D.vertices[s].1.count j = 1 ∧ D.vertices[t].1.count j = 1 ∧ + ∀ v (hv : v < D.vertices.length), j ∈ D.vertices[v].1 → v = s ∨ v = t := by + obtain ⟨hrow', hcol'⟩ := hD.2 j hj + have hrow : (((D.vertices.map Prod.fst).take r).map fun l => l.count j).sum = 1 := by + rw [← List.map_take, List.map_map] + exact hrow' + have hcol : (((D.vertices.map Prod.fst).drop r).map fun l => l.count j).sum = 1 := by + rw [← List.map_drop, List.map_map] + exact hcol' + obtain ⟨s, hs, hsc, hsu⟩ := exists_unique_of_sum_count_eq_one hrow + obtain ⟨t, ht, htc, htu⟩ := exists_unique_of_sum_count_eq_one hcol + simp only [List.length_take, List.length_map, List.length_drop] at hs ht + have hs' : s < D.vertices.length := by omega + have hsr : s < r := by omega + have ht' : r + t < D.vertices.length := by omega + refine ⟨s, r + t, hs', ht', hsr, by omega, ?_, ?_, fun v hv hm => ?_⟩ + · simpa using hsc + · simpa using htc + · by_cases hvr : v < r + · left + refine hsu v (by simp; omega) ?_ + simpa [List.getElem_take] using hm + · right + have := htu (v - r) (by simp; omega) (by + simp only [List.getElem_map, List.getElem_drop] + convert hm using 3 + omega) + omega + +/-- **The vertices at an edge** of a rows-first network are its row and its column. -/ +theorem incident_eq {r : ℕ} (hD : D.IsRowsFirstBipartite r) {j : ℕ} (hj : j < D.numEdges) : + ∃ s t, ∃ hs : s < D.vertices.length, ∃ ht : t < D.vertices.length, s < r ∧ r ≤ t ∧ + D.vertices[s].1.count j = 1 ∧ D.vertices[t].1.count j = 1 ∧ D.incident j = [s, t] := by + obtain ⟨s, t, hs, ht, hsr, hrt, hsc, htc, hu⟩ := exists_ends hD hj + refine ⟨s, t, hs, ht, hsr, hrt, hsc, htc, ?_⟩ + have hsorted : (D.incident j).Pairwise (· < ·) := + (List.pairwise_lt_range).filter _ + have hmem : ∀ v, v ∈ D.incident j ↔ v ∈ [s, t] := by + intro v + simp only [incident, List.mem_filter, List.mem_range, decide_eq_true_eq, List.mem_cons, + List.not_mem_nil, or_false] + constructor + · rintro ⟨hv, hm⟩ + rw [getD_map_fst v hv] at hm + exact hu v hv hm + · rintro (rfl | rfl) + · refine ⟨hs, ?_⟩ + rw [getD_map_fst _ hs] + exact List.count_pos_iff.mp (by omega) + · refine ⟨ht, ?_⟩ + rw [getD_map_fst _ ht] + exact List.count_pos_iff.mp (by omega) + have hst : [s, t].Pairwise (· < ·) := by simp; omega + exact hsorted.eq_of_mem_iff hst hmem + +/-- The first vertex at an edge of a rows-first network is a vertex. -/ +theorem getD_incident_zero_lt {r : ℕ} (hD : D.IsRowsFirstBipartite r) {j : ℕ} + (hj : j < D.numEdges) : (D.incident j).getD 0 0 < D.vertices.length := by + obtain ⟨s, t, hs, ht, -, -, -, -, h⟩ := incident_eq hD hj + rw [h] + exact hs + +/-- The second vertex at an edge of a rows-first network is a vertex. -/ +theorem getD_incident_one_lt {r : ℕ} (hD : D.IsRowsFirstBipartite r) {j : ℕ} + (hj : j < D.numEdges) : (D.incident j).getD 1 0 < D.vertices.length := by + obtain ⟨s, t, hs, ht, -, -, -, -, h⟩ := incident_eq hD hj + rw [h] + exact ht + +/-! ### The network of a described network -/ + +/-- The row of an edge of a rows-first network. -/ +@[expose] def srcFin {r : ℕ} (hD : D.IsRowsFirstBipartite r) (j : Fin D.numEdges) : + Fin D.vertices.length := + ⟨(D.incident j).getD 0 0, getD_incident_zero_lt hD j.2⟩ + +/-- The column of an edge of a rows-first network. -/ +@[expose] def tgtFin {r : ℕ} (hD : D.IsRowsFirstBipartite r) (j : Fin D.numEdges) : + Fin D.vertices.length := + ⟨(D.incident j).getD 1 0, getD_incident_one_lt hD j.2⟩ + +/-- **The network of a rows-first described network**, on `Fin k` vertices and `Fin m` edges: the +edge `j` runs from its row to its column, and the tensor of a vertex is the evaluator at its +descriptor and the bits on its ports. -/ +@[expose] noncomputable def toNetwork {r : ℕ} (hD : D.IsRowsFirstBipartite r) {R : Type*} + (eval : T → List Bool → R) : + TensorNetwork R Bool (Fin D.vertices.length) (Fin D.numEdges) where + src := D.srcFin hD + tgt := D.tgtFin hD + tensor v x := eval D.vertices[v].2 (wordBits (List.ofFn x) D.vertices[v].1) + tensor_congr v x y hxy := by + congr 1 + refine List.map_congr_left fun i hi => ?_ + have hi' : i < D.numEdges := hD.1 _ (List.getElem_mem _) i hi + obtain ⟨s, t, hs, ht, -, -, -, -, hinc⟩ := incident_eq hD hi' + have hv : (v : ℕ) ∈ D.incident i := by + simp only [incident, List.mem_filter, List.mem_range, decide_eq_true_eq] + exact ⟨v.2, by rw [getD_map_fst _ v.2]; exact hi⟩ + rw [List.getD_eq_getElem _ _ (by simpa using hi'), + List.getD_eq_getElem _ _ (by simpa using hi'), + List.getElem_ofFn, List.getElem_ofFn] + refine hxy ⟨i, hi'⟩ ?_ + rw [hinc] at hv + simp only [List.mem_cons, List.not_mem_nil, or_false] at hv + rcases hv with hv | hv + · left + exact Fin.ext (by simp [srcFin, hinc, hv]) + · right + exact Fin.ext (by simp [tgtFin, hinc, hv]) + +variable {r : ℕ} (hD : D.IsRowsFirstBipartite r) + +@[simp] theorem toNetwork_src {R : Type*} (eval : T → List Bool → R) : + (D.toNetwork hD eval).src = D.srcFin hD := rfl + +@[simp] theorem toNetwork_tgt {R : Type*} (eval : T → List Bool → R) : + (D.toNetwork hD eval).tgt = D.tgtFin hD := rfl + +/-- The edges run from the rows. -/ +theorem srcFin_lt (j : Fin D.numEdges) : (D.srcFin hD j : ℕ) < r := by + obtain ⟨s, t, -, -, hsr, -, -, -, h⟩ := incident_eq hD j.2 + simp [srcFin, h, hsr] + +/-- The edges end at the columns. -/ +theorem le_tgtFin (j : Fin D.numEdges) : r ≤ (D.tgtFin hD j : ℕ) := by + obtain ⟨s, t, -, -, -, hrt, -, -, h⟩ := incident_eq hD j.2 + simp [tgtFin, h, hrt] + +/-- A vertex has an edge among its ports exactly when it is an end of the edge. -/ +theorem mem_ports_iff (v : Fin D.vertices.length) (j : Fin D.numEdges) : + (j : ℕ) ∈ D.vertices[v].1 ↔ D.srcFin hD j = v ∨ D.tgtFin hD j = v := by + obtain ⟨s, t, hs, ht, -, -, hsc, htc, hinc⟩ := incident_eq hD j.2 + have hmem : (v : ℕ) ∈ D.incident j ↔ (j : ℕ) ∈ D.vertices[v].1 := by + simp only [incident, List.mem_filter, List.mem_range, decide_eq_true_eq] + rw [getD_map_fst _ v.2] + exact ⟨fun h => h.2, fun h => ⟨v.2, h⟩⟩ + rw [← hmem, hinc] + simp only [List.mem_cons, List.not_mem_nil, or_false, Fin.ext_iff, srcFin, tgtFin, hinc, + List.getD_cons_zero, List.getD_cons_succ] + exact ⟨fun h => h.imp Eq.symm Eq.symm, fun h => h.imp Eq.symm Eq.symm⟩ + +/-- **The ends of the edges** are the native `edgeEnds`. -/ +theorem edgeEnds_eq : + D.edgeEnds = List.ofFn fun j => ((D.srcFin hD j : ℕ), (D.tgtFin hD j : ℕ)) := by + rw [edgeEnds, ← List.map_coe_finRange_eq_range, List.map_map, List.ofFn_eq_map] + rfl + +/-- **The network has the contraction of the described network.** -/ +theorem contraction_toNetwork {R : Type*} [CommSemiring R] (eval : T → List Bool → R) : + (D.toNetwork hD eval).contraction = D.contraction eval := by + simp only [TensorNetwork.contraction, contraction] + refine sum_congr rfl fun x _ => ?_ + rw [← List.ofFn_getElem_eq_map, List.prod_ofFn] + rfl + +/-- The network of a described network commutes with maps of the entries. -/ +theorem toNetwork_map {R S : Type*} [CommSemiring R] [CommSemiring S] (eval : T → List Bool → R) + (ψ : R →+* S) : (D.toNetwork hD eval).map ψ = D.toNetwork hD fun t bs => ψ (eval t bs) := + rfl + +/-- **Over `O`, the contraction reduces to the contraction in `A_p`.** For the network with the +lifts of the entries of the descriptors, reduction modulo `2 ^ p` of its contraction is the +contraction of the described network with the values of the entries in `A_p`. -/ +theorem reduction_contraction_toNetwork {fl : List ℕ} + (hirr : Irreducible ((GaloisRingArith.monicOf fl).map (Int.castRingHom (ZMod 2)))) + (eval : T → List Bool → List ℕ) (p : ℕ) : + reduction (GaloisRingArith.monic_monicOf fl) hirr p + (D.toNetwork hD fun t bs => GaloisRingArith.liftO hirr (eval t bs)).contraction = + D.contraction fun t bs => GaloisRingArith.val p fl (eval t bs) := by + rw [contraction_toNetwork, map_contraction] + simp only [GaloisRingArith.reduction_liftO] + +/-! ### Polynomial time -/ + +section PolyTime + +open Turing.MultiTapeTM + +variable {T : Type} (encT : T ↪ List Bool) + +/-- **The vertices at an edge are polynomial-time**, with the edge in unary. -/ +theorem computableInPolyTime_incident : + ComputableInPolyTime (fun q : DescribedNetwork T × ℕ => q.1.incident q.2) + (encPair (encDescribed encT) encUnary) (encList encUnary) := by + have hV : ComputableInPolyTime (fun q : DescribedNetwork T × ℕ => q.1.vertices) + (encPair (encDescribed encT) encUnary) (encList (encPair (encList encNat) encT)) := + vertices_polyTime.comp (ComputableInPolyTime.fst _ _) + have hP : ComputableInPolyTime (fun q : DescribedNetwork T × ℕ => q.1.vertices.map Prod.fst) + (encPair (encDescribed encT) encUnary) (encList (encList encNat)) := + ComputableInPolyTime.mapWithInput (f := fun _ v => v.1) hV + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)) + have hrange : ComputableInPolyTime (fun q : DescribedNetwork T × ℕ => + List.range q.1.vertices.length) (encPair (encDescribed encT) encUnary) (encList encUnary) := + ComputableInPolyTime.range.comp ((ComputableInPolyTime.length_list _).comp hV) + have hports : ComputableInPolyTime (fun z : (DescribedNetwork T × ℕ) × ℕ => + (z.1.1.vertices.map Prod.fst).getD z.2 []) + (encPair (encPair (encDescribed encT) encUnary) encUnary) (encList encNat) := + (ComputableInPolyTime.listGetD (encA := encList encNat) []).comp + ((hP.comp (ComputableInPolyTime.fst _ _)).prod (ComputableInPolyTime.snd _ _)) + have hj : ComputableInPolyTime (fun z : (DescribedNetwork T × ℕ) × ℕ => z.1.2) + (encPair (encPair (encDescribed encT) encUnary) encUnary) encNat := + ComputableInPolyTime.unary_to_binary.comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.fst _ _)) + exact ComputableInPolyTime.filterWithInput + (test := fun q v => decide (q.2 ∈ (q.1.vertices.map Prod.fst).getD v [])) hrange + (ComputableInPolyTime.decide_mem hports hj) + +/-- **The ends of the edges are polynomial-time.** -/ +theorem computableInPolyTime_edgeEnds : + ComputableInPolyTime (fun D : DescribedNetwork T => D.edgeEnds) (encDescribed encT) + (encList (encPair encNat encNat)) := by + have hinc : ComputableInPolyTime (fun q : DescribedNetwork T × ℕ => q.1.incident q.2) + (encPair (encDescribed encT) encUnary) (encList encUnary) := + computableInPolyTime_incident encT + have hget (i : ℕ) : ComputableInPolyTime (fun q : DescribedNetwork T × ℕ => + (q.1.incident q.2).getD i 0) (encPair (encDescribed encT) encUnary) encNat := + ComputableInPolyTime.unary_to_binary.comp + ((ComputableInPolyTime.listGetD (encA := encUnary) 0).comp + (hinc.prod (ComputableInPolyTime.const i))) + exact ComputableInPolyTime.mapWithInput + (f := fun D j => ((D.incident j).getD 0 0, (D.incident j).getD 1 0)) + (ComputableInPolyTime.range.comp numEdges_polyTime) ((hget 0).prod (hget 1)) + +end PolyTime + +end DescribedNetwork + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean index 313760ebfc..a48aad9bc6 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean @@ -37,9 +37,9 @@ entry zero. Its size measures are the number of edges, the number of vertices, the maximum number of ports of a vertex (`ExplicitTensorNetwork.maxDegree`) and the total length of the tables -(`ExplicitTensorNetwork.tableLength`). A network is *rows-first bipartite* with `r` rows -(`ExplicitTensorNetwork.IsRowsFirstBipartite`) when every edge is a port of exactly one of its -first `r` vertices and of exactly one of the others. +(`ExplicitTensorNetwork.tableLength`). A described network is *rows-first bipartite* with `r` +rows (`DescribedNetwork.IsRowsFirstBipartite`) when every port names an edge and every edge is a +port of exactly one of its first `r` vertices and of exactly one of the others. **Writing a network out** (`TensorNetwork.toExplicit`). Given numberings of the vertices and the edges of a Boolean tensor network on finite types, list the edges at each vertex in increasing @@ -55,6 +55,8 @@ one end of every edge below `r` and the other at or above it gives a rows-first the descriptors of its vertices. * `Cslib.Circuits.Frontier.DescribedNetwork.contraction`: its contraction, for an evaluator of the descriptors. +* `Cslib.Circuits.Frontier.DescribedNetwork.IsRowsFirstBipartite`: the bipartition with the first + `r` vertices as rows. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork`: an explicit Boolean tensor network, with tables as descriptors. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.entry`, @@ -63,8 +65,6 @@ one end of every edge below `r` and the other at or above it gives a rows-first * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.contraction`: the contraction. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree`, `Cslib.Circuits.Frontier.ExplicitTensorNetwork.tableLength`: size measures. -* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`: the bipartition with the - first `r` vertices as rows. * `Cslib.Circuits.Frontier.TensorNetwork.explicitPorts`, `Cslib.Circuits.Frontier.TensorNetwork.explicitTable`, `Cslib.Circuits.Frontier.TensorNetwork.toExplicit`: writing a Boolean tensor network out. @@ -137,6 +137,18 @@ theorem map_contraction {R S : Type*} [CommSemiring R] [CommSemiring S] (ψ : R rw [map_list_prod, List.map_map] rfl +/-- **Rows-first bipartite**: the first `r` vertices are the *rows* and the others the *columns*, +every port names an edge, and every edge is a port of the rows exactly once and of the columns +exactly once. So every edge joins a row to a column. -/ +def IsRowsFirstBipartite (d : DescribedNetwork T) (r : ℕ) : Prop := + (∀ v ∈ d.vertices, ∀ i ∈ v.1, i < d.numEdges) ∧ + ∀ i < d.numEdges, ((d.vertices.take r).map fun v => v.1.count i).sum = 1 ∧ + ((d.vertices.drop r).map fun v => v.1.count i).sum = 1 + +instance (d : DescribedNetwork T) (r : ℕ) : Decidable (d.IsRowsFirstBipartite r) := by + unfold IsRowsFirstBipartite + infer_instance + end DescribedNetwork /-- An *explicit Boolean tensor network* over `R`: a network whose descriptors are *tables*. The @@ -190,18 +202,6 @@ theorem length_le_maxDegree {v : List ℕ × List R} (hv : v ∈ d.vertices) : v.1.length ≤ d.maxDegree := d.maxDegree_le_iff.mp le_rfl v hv -/-- **Rows-first bipartite**: the first `r` vertices are the *rows* and the others the *columns*, -every port names an edge, and every edge is a port of the rows exactly once and of the columns -exactly once. So every edge joins a row to a column. -/ -def IsRowsFirstBipartite (r : ℕ) : Prop := - (∀ v ∈ d.vertices, ∀ i ∈ v.1, i < d.numEdges) ∧ - ∀ i < d.numEdges, ((d.vertices.take r).map fun v => v.1.count i).sum = 1 ∧ - ((d.vertices.drop r).map fun v => v.1.count i).sum = 1 - -instance (r : ℕ) : Decidable (d.IsRowsFirstBipartite r) := by - unfold IsRowsFirstBipartite - infer_instance - end ExplicitTensorNetwork private theorem getD_ofFn {n : ℕ} (x : Fin n → Bool) (i : ℕ) : diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeCall.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeCall.lean new file mode 100644 index 0000000000..82af1b001c --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeCall.lean @@ -0,0 +1,169 @@ +/- +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 +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeRecovery +import Mathlib.Data.List.GetD + +/-! +# Correctness of one native active call + +An active call of the native contraction recursion of [OpenAI2026ETH] (§D.4.4–§D.4.7, +pp. 60–64) on a rows-first network of descriptors stores, for each node index `k` of positive +multiplicity and each interpolation point `i`, a value in `A_{p_t}`, and recovers its own value +with native tapered recovery (`NativeRecovery.recover`). This file proves the call correct from +the correctness of its stored values (`NativeCall.val_recover_eq_contraction`): if each stored value +is, in `A_{p_t}`, the sum over the exponent tuples of the products over the groups of the +contractions of the native children (`NativeChild.nativeChild`), then the recovered value is the +contraction of the network in `A_p`. + +**The proof** is carried over `O = ℤ_(2)[U] / (f)` with the canonical lifts of the entries +(`DescribedNetwork.toNetwork`, `GaloisRingArith.liftO`), as in §D.4.1 (p. 58). The values at the +nodes are the lifts of the stored lists, so + +* modulo `2 ^ {p_t}` they are the right side of (D.16) for the children of `callSplitting`: the + native children have these contractions (`NativeChild.contraction_nativeChild`), and the sum over + the exponent lists is the sum over the mode budget (`BudgetTuples.sum_filter_weight_lt_eq`); +* so interpolation and Lemma D.5 recover the contraction modulo `2 ^ p` + (`TensorNetwork.exists_recoverFromValues_eq_add_of_children`); +* and the lifts reduce in `A_{p + Δ}` to exactly the stored lists, so native recovery computes the + reduction of the contraction (`NativeRecovery.val_recover_of_eq_add`), with no condition on + `p_t` beyond Lemma D.5's. + +The call's precision `p_t` of the node of valuation `i` is `nodePrecision p h a M i`, and the +shift `Δ` only needs `(a + 1) ∑_t q_t ≤ Δ`. + +## Main results + +* `Cslib.Circuits.Frontier.NativeCall.val_recover_eq_contraction`: one native active call is + correct when its stored values are. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.4–§D.4.7, pp. 60–64. +-/ + +public section + +namespace Cslib.Circuits.Frontier.NativeCall + +open Finset GaloisRingArith NativeChild NativeRecovery +open ContractionSchedule (nodePrecision) + +/-- The node index of a node: `t + 2 ^ a`. -/ +theorem toNat_node_add (a k : ℕ) : (node a k + 2 ^ a).toNat = k := by + rw [node, sub_add_cancel, Int.toNat_natCast] + +/-- A product over a range as a list is a product over `Fin`. -/ +theorem prod_map_range {M : Type*} [CommMonoid M] (F : ℕ → M) (n : ℕ) : + ((List.range n).map F).prod = ∏ g : Fin n, F g := by + rw [← List.map_coe_finRange_eq_range, List.map_map, ← List.ofFn_eq_map, List.prod_ofFn] + rfl + +variable {fl : List ℕ} (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) + {D : DescribedNetwork VertexDesc} {r : ℕ} (hD : D.IsRowsFirstBipartite r) + +include hD in +/-- **One native active call is correct when its stored values are** ([OpenAI2026ETH], +§D.4.4–§D.4.7). Let `D` be a rows-first network of descriptors with `M` edges, and let +`(a, u, h)` meet the hypotheses of Lemma D.5 (`1 ≤ u ≤ M`, `u ≤ a`, `3 M ≤ h u ≤ 3 M + u`), with +`64 ^ a ≤ M` and `(a + 1) ∑_t q_t ≤ Δ`. Let the interpolation values `ζl` have lifts with unit +differences, and more than `M (2 L - 1)` of them. Suppose that at every node index `k` of positive +multiplicity, with the node `t = k - 2 ^ a` of valuation `i` and precision `p_t`, each stored value +`W[k][i']` is, in `A_{p_t}`, the sum over the exponent lists of the packet-major modes of the +products over the `64` groups of the contractions in `A_{p_t}` of the native children. Then native +recovery returns the contraction of `D` in `A_p`. -/ +theorem val_recover_eq_contraction {a u h p Δ : ℕ} (hu : 1 ≤ u) (huM : u ≤ D.numEdges) + (hua : u ≤ a) (hh : 3 * D.numEdges ≤ h * u) (hh' : h * u ≤ 3 * D.numEdges + u) + (hK : 64 ^ a ≤ D.numEdges) + (hΔ : (a + 1) * ∑ t ∈ recoveryNodes a, taperMult u h t ≤ Δ) (ζl : List (List ℕ)) + (hζ : Pairwise fun i j : Fin ζl.length => + IsUnit (liftO hirr (ζl.getD i []) - liftO hirr (ζl.getD j []))) + (hn : D.numEdges * (2 * 2 ^ a - 1) < ζl.length) (W : List (List (List ℕ))) + (hW : ∀ k < 2 ^ (a + 1), k ≠ 2 ^ a → 0 < mult a u h k → ∀ i < ζl.length, + val (nodePrecision p h a D.numEdges (padicValInt 2 (node a k))) fl + ((W.getD k []).getD i []) = + ((BudgetTuples.budgetTuples + (modeWeights (nativeParentPacking r a D).2.1 (2 ^ (padicValInt 2 (node a k) + 1)) + (nodePrecision p h a D.numEdges (padicValInt 2 (node a k)))) + (nodePrecision p h a D.numEdges (padicValInt 2 (node a k)))).map fun β => + ((List.range 64).map fun g => + (nativeChild fl a (padicValInt 2 (node a k)) + (nodePrecision p h a D.numEdges (padicValInt 2 (node a k))) (node a k) + (ζl.getD i []) r D (nativeParentPacking r a D) β g).contraction + fun d bs => val (nodePrecision p h a D.numEdges (padicValInt 2 (node a k))) fl + (d.entry bs)).prod).sum) : + val p fl (recover p Δ fl a u h ζl W) = + D.contraction fun d bs => val p fl (d.entry bs) := by + have hB := AdjoinRoot.algebraMap_mem_integer_padicValuation (monic_monicOf fl) hirr + have hcard : Fintype.card (Fin D.numEdges) = D.numEdges := Fintype.card_fin _ + have hpk1 : (nativeParentPacking r a D).2.1 = (parentPacking hD a).numPackets := by + rw [nativeParentPacking_eq hD hK] + -- The points and the values over `O`: the lifts of the native lists. + let ζ : Fin ζl.length → RingO hirr := fun i => liftO hirr (ζl.getD i []) + let v : ℤ → Fin ζl.length → RingO hirr := fun t i => + liftO hirr ((W.getD (t + 2 ^ a).toNat []).getD i []) + -- Modulo `2 ^ {p_t}` the values are the right side of (D.16). + have hv : ∀ t (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (k : Fin ζl.length), + Ideal.Quotient.mk (nodeIdeal (RingO hirr) (Fintype.card (Fin D.numEdges)) a h p t) (v t k) = + ∑ β ∈ TensorNetwork.modeBudget (fun Z : Fin (parentPacking hD a).numPackets × + Fin (2 ^ (padicValInt 2 t + 1)) × + Fin (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t)) => + (Z.2.2 : ℕ) + 1) + (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t)), + ∏ g, ((parentSplitting hirr hD a p u h hua ht hq (ζl.getD k [])).child β + g).contraction := by + intro t ht hq k + obtain ⟨kk, hkk, hkt⟩ : ∃ kk, (kk < 2 ^ (a + 1) ∧ kk ≠ 2 ^ a) ∧ node a kk = t := by + rw [recoveryNodes_eq_image, mem_image] at ht + obtain ⟨kk, hk, e⟩ := ht + exact ⟨kk, by simpa using hk, e⟩ + subst hkt + have hmult : 0 < mult a u h kk := by rw [mult_eq u h hkk.1]; exact hq + have hWk := hW kk hkk.1 hkk.2 hmult k k.2 + rw [← hcard] at hWk + simp only [v, toNat_node_add] + rw [mk_liftO hirr, hWk, map_list_sum, List.map_map, TensorNetwork.modeBudget, + BudgetTuples.sum_filter_weight_lt_eq (nodup_modeList _ _ _) mem_modeList + (fun Z => Nat.succ_pos _), map_modeList_weight, hpk1] + refine congrArg List.sum (List.map_congr_left fun β _ => ?_) + simp only [Function.comp_apply] + rw [map_list_prod, List.map_map, prod_map_range] + refine Fintype.prod_congr _ _ fun g => ?_ + simp only [Function.comp_apply] + rw [DescribedNetwork.map_contraction] + exact contraction_nativeChild hirr hD hK hua ht hq (ζl.getD k []) β g + obtain ⟨b, hb, hx⟩ := TensorNetwork.exists_recoverFromValues_eq_add_of_children (RingO hirr) hB + (parentNetwork hirr hD) (parentSide r) (parentSide_src hD) (parentSide_tgt hD) + (parentPacking hD a) (p := p) hu (by rwa [hcard]) hua (by rwa [hcard]) (by rwa [hcard]) ζ hζ + (by rwa [hcard]) v hv + -- Native recovery computes the reduction of the recovered value. + have hpt : ∀ t ∈ recoveryNodes a, 0 < taperMult u h t → + p + 6 * h * 2 ^ (a - padicValInt 2 t) + taperMult u h t * (a + 1) ≤ + nodePrecision p h a D.numEdges (padicValInt 2 t) := by + intro t _ _ + have h1 : h * (u - padicValInt 2 t) ≤ 8 * D.numEdges := + (Nat.mul_le_mul_left _ (Nat.sub_le _ _)).trans (by omega) + have e1 : 6 * h * 2 ^ (a - padicValInt 2 t) ≤ 8 * h * 2 ^ (a - padicValInt 2 t) := + Nat.mul_le_mul_right _ (by omega) + have e2 : h * (u - padicValInt 2 t) * (a + 1) ≤ 8 * D.numEdges * (a + 1) := + Nat.mul_le_mul_right _ h1 + simp only [nodePrecision, taperMult] + omega + have hrec := val_recover_of_eq_add hirr (RingO hirr) hB + (AdjoinRoot.reduction (monic_monicOf fl) hirr (p + Δ)) hΔ + (fun t => nodePrecision p h a D.numEdges (padicValInt 2 t)) hpt ζ hζ ζl rfl + (fun i => (reduction_liftO hirr _ _).symm) v W + (fun k _ _ _ i => ⟨0, by simp only [v, toNat_node_add, reduction_liftO, mul_zero, add_zero]⟩) + (parentNetwork hirr hD).contraction hb hx + rw [hrec, ← DescribedNetwork.reduction_contraction_toNetwork hD hirr (fun d bs => d.entry bs) p] + exact RingHom.congr_fun (AdjoinRoot.castHom_comp_reduction (monic_monicOf fl) hirr + (Nat.le_add_right p Δ)) _ + +end Cslib.Circuits.Frontier.NativeCall diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean new file mode 100644 index 0000000000..e90fd66f59 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean @@ -0,0 +1,1027 @@ +/- +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.DescribedLift +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildEntries +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildNumbering +public import Complexity.Computability.PolyTime.PacketPacking +public import Complexity.Foundations.Combinatorics.BudgetTuples +import Complexity.Foundations.Data.List.Lookup +import Mathlib.Data.List.GetD + +/-! +# The native child networks of an active call + +An active call of the contraction recursion of [OpenAI2026ETH] (§D.4.5–§D.4.7, pp. 62–64) on a +network of vertex descriptors evaluates, for each node `t`, each interpolation value `ζ`, each +exponent tuple `β` and each group `g`, the child network of group `g`. This file builds that child +natively as a network of descriptors (`NativeChild.nativeChild`), from the parent, the native +packing of its edges (`Cslib.PacketPacking.nativePacking`) and `(t, ζ, β, g)`, and proves that it +has the contraction of the child of the mode splitting at the node (`TensorNetwork.callSplitting`). + +**The child.** Its vertices are numbered as in `ChildNumbering.childVertexEquiv` and its edges as +in `ChildNumbering.childEdgeEquiv`: + +* the vertices of group `g`, in order, keep their descriptors, and their ports are their parent + ports, *in the parent's order*, each renumbered to its child edge: a row port by its position + among the row ports of group `g`, a column port by the number of row ports plus its position + among the column ports (`NativeChild.childEdgeOf`). A retained vertex reads its ports in its own + order, so its ports are not sorted; +* the packet `q` is a new vertex whose ports are its child edges in increasing order + (`ChildNumbering.childPorts`), each tagged with whether it is a row port and with the slot of its + parent edge, and whose descriptor carries the node, the value `ζ`, the symbols of `q` against + `g` and the slice of `β` at `q` (`NativeChild.packetCtx`, `NativeChild.betaSlice`), at the + child's precision `p_t`. + +The modes of the node are listed packet-major (`NativeChild.modeList`): the mode `(q, y, b)` is at +`q · 2 ^ (i + 1) · p_t + y · p_t + b`, so the dense exponents of packet `q` are a slice of `β`, and +`β` stands for the mode tuple `BudgetTuples.ofList (modeList …) β`. + +**Correctness** (`NativeChild.contraction_nativeChild`). Over `O = ℤ_(2)[U] / (f)` the parent is +the network `DescribedNetwork.toNetwork` with the lifts of its entries, and its packing is the +native packing, which is `PacketPacking.packing` of its edges (`PacketPacking.nativePacking_eq`), +moved to the ends of the parent (`NativeChild.parentPacking`). Along `reductionLift`, the entries of +the native child in `A_{p_t}` give the contraction of the child of `callSplitting` at the lift of +`ζ` and the mode tuple of `β`: the retained vertices by `ModeSplitting.child_tensor_inl_eq_tensor` +and the packets by `TensorNetwork.map_val_entry_child_inr`, assembled by +`DescribedNetwork.contraction_eq_of_ports`. The native child is again rows-first, with its retained +vertices as rows (`NativeChild.isRowsFirstBipartite_nativeChild`). + +## Main definitions + +* `Cslib.PacketPacking.Packing.relabel`: a packing moved to other ends of the edges. +* `Cslib.Circuits.Frontier.NativeChild.nativeChild`: the native child. +* `Cslib.Circuits.Frontier.NativeChild.childRows`: its number of rows. +* `Cslib.Circuits.Frontier.NativeChild.modeList`, `Cslib.Circuits.Frontier.NativeChild.modeWeights`: + the modes of a node, packet-major, and their weights. +* `Cslib.Circuits.Frontier.NativeChild.parentPacking`: the packing of the parent over `O`. + +## Main results + +* `Cslib.Circuits.Frontier.NativeChild.contraction_nativeChild`: the native child has the + contraction of the child. +* `Cslib.Circuits.Frontier.NativeChild.isRowsFirstBipartite_nativeChild`: it is rows-first. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.5–§D.4.7, pp. 62–64. +-/ + +public section + +/-! ### Moving a packing to other ends -/ + +namespace Cslib.PacketPacking + +variable {E R C R' C' : Type*} {rowOf : E → R} {colOf : E → C} {a r : ℕ} + +/-- **A packing moved to other ends of the edges**: the same packets, slots and symbols, with the +labels of the new ends read through `ρ` and `κ`, which agree with the old labels at the ends of +every edge. -/ +@[expose] def Packing.relabel (P : Packing rowOf colOf a r) (rowOf' : E → R') (colOf' : E → C') + (ρ : R' → Fin a → Fin r) (κ : C' → Fin a → Fin r) + (hρ : ∀ e, ρ (rowOf' e) = P.rowLabel (rowOf e)) + (hκ : ∀ e, κ (colOf' e) = P.colLabel (colOf e)) : + Packing rowOf' colOf' a r where + rowLabel := ρ + colLabel := κ + numPackets := P.numPackets + packet := P.packet + slot := P.slot + symbols := P.symbols + injective := P.injective + labels_eq e i := by rw [hρ, hκ]; exact P.labels_eq e i + +end Cslib.PacketPacking + +namespace Cslib.Circuits.Frontier + +/-- The subring `ℤ_(2)` of rationals with odd denominator. -/ +local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2) + +namespace NativeChild + +open ChildNumbering GaloisRingArith NativePacket +open ContractionSchedule (nodePrecision) + +/-! ### The native child -/ + +/-- **The groups of the vertices** in coordinate `i`: digit `i` of the row word of a row +(`v < r`), and of the column word of a column. -/ +@[expose] def groupsOf (r i k : ℕ) (words : List (List ℕ) × List (List ℕ)) : List ℕ := + (List.range k).map fun v => + if v < r then (words.1.getD v []).getD i 0 else (words.2.getD (v - r) []).getD i 0 + +/-- The parent edges whose end `sel` is in group `g`, in order: the row ports of group `g` for +`sel = Prod.fst`, its column ports for `sel = Prod.snd`. -/ +@[expose] def portEdges (groups : List ℕ) (g : ℕ) (ends : List (ℕ × ℕ)) (sel : ℕ × ℕ → ℕ) : + List ℕ := + (List.range ends.length).filter fun e => groups.getD (sel (ends.getD e (0, 0))) 0 = g + +/-- The position of the edge `e` among the parent edges whose end `sel` is in group `g`. -/ +@[expose] def portRank (groups : List ℕ) (g : ℕ) (ends : List (ℕ × ℕ)) (sel : ℕ × ℕ → ℕ) + (e : ℕ) : ℕ := + (List.range e).countP fun e' => groups.getD (sel (ends.getD e' (0, 0))) 0 = g + +/-- **The child edge of the parent port `e` of the vertex `v`**: for a row, its position among the +row ports of group `g`; for a column, the number of row ports plus its position among the column +ports. -/ +@[expose] def childEdgeOf (r : ℕ) (groups : List ℕ) (g : ℕ) (ends : List (ℕ × ℕ)) (v e : ℕ) : ℕ := + if v < r then portRank groups g ends Prod.fst e + else (portEdges groups g ends Prod.fst).length + portRank groups g ends Prod.snd e + +/-- **The parent edge of the child edge `j`**: the `j`-th row port of group `g`, or the +`(j - R)`-th column port for `R` row ports. -/ +@[expose] def parentEdge (groups : List ℕ) (g : ℕ) (ends : List (ℕ × ℕ)) (j : ℕ) : ℕ := + if j < (portEdges groups g ends Prod.fst).length then + (portEdges groups g ends Prod.fst).getD j 0 + else (portEdges groups g ends Prod.snd).getD (j - (portEdges groups g ends Prod.fst).length) 0 + +/-- **The context of the packet `q`** in the child of group `g` at the node `t` of valuation `i` +and the interpolation value `ζ`: the precision `p_t` and `p_t` exponents per tile, `2 ^ a` slots, +`2 ^ (i + 1)` tiles, and the symbols of `q` in coordinate `i` against `g`. -/ +@[expose] def packetCtx (fl : List ℕ) (a i pt : ℕ) (t : ℤ) (ζ : List ℕ) (g q : ℕ) : PacketCtx where + p := pt + fl := fl + a := a + L := 2 ^ a + i := i + tiles := 2 ^ (i + 1) + t := t + nb := pt + e₁ := decide ((PacketPacking.packetSymbols a 64 q i).1 = g) + e₂ := decide ((PacketPacking.packetSymbols a 64 q i).2 = g) + differ := decide ((PacketPacking.packetSymbols a 64 q i).1 ≠ + (PacketPacking.packetSymbols a 64 q i).2) + cols := [] + ζ := ζ + +/-- **The dense exponents of the packet `q`**: its slice of the packet-major list `β`. -/ +@[expose] def betaSlice (i pt : ℕ) (β : List ℕ) (q : ℕ) : List ℕ := + (β.drop (q * (2 ^ (i + 1) * pt))).take (2 ^ (i + 1) * pt) + +/-- The default vertex: no ports and the empty table. -/ +abbrev defaultVertex : List ℕ × VertexDesc := ([], .inl []) + +/-- **The native child** of group `g` at the node `t` of valuation `i`, the interpolation value +`ζ`, the precision `p_t` and the packet-major exponents `β`, of the rows-first parent `D` with `r` +rows and the native packing `pk` of its edges: the vertices of group `g` with their descriptors +and renumbered ports, then one packet vertex per packet. -/ +@[expose] def nativeChild (fl : List ℕ) (a i pt : ℕ) (t : ℤ) (ζ : List ℕ) (r : ℕ) + (D : DescribedNetwork VertexDesc) + (pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)) (β : List ℕ) (g : ℕ) : + DescribedNetwork VertexDesc := + let groups := groupsOf r i D.vertices.length pk.1 + let cedges := childEdgeList groups g D.edgeEnds (pk.2.2.map Prod.fst) + ⟨cedges.length, + ((List.range D.vertices.length).filter fun v => groups.getD v 0 = g).map (fun v => + (((D.vertices.getD v defaultVertex).1.map (childEdgeOf r groups g D.edgeEnds v)), + (D.vertices.getD v defaultVertex).2)) ++ + (List.range pk.2.1).map fun q => + (childPorts cedges (groups.count g + q), + .inr (packetCtx fl a i pt t ζ g q, + (childPorts cedges (groups.count g + q)).map fun j => + (decide (j < (portEdges groups g D.edgeEnds Prod.fst).length), + (pk.2.2.getD (parentEdge groups g D.edgeEnds j) (0, 0)).2), + betaSlice i pt β q))⟩ + +/-- **The number of rows of the native child**: the number of vertices of group `g`. -/ +@[expose] def childRows (r i : ℕ) (D : DescribedNetwork VertexDesc) + (pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)) (g : ℕ) : ℕ := + (groupsOf r i D.vertices.length pk.1).count g + +/-! ### The modes of a node -/ + +/-- The packet-major numbering of the modes `(q, y, b)`: `q · T p + y · p + b`. -/ +@[expose] def modeEquiv (P T p : ℕ) : Fin P × Fin T × Fin p ≃ Fin (P * (T * p)) := + (Equiv.prodCongr (Equiv.refl _) finProdFinEquiv).trans finProdFinEquiv + +/-- **The modes of a node, packet-major.** -/ +@[expose] def modeList (P T p : ℕ) : List (Fin P × Fin T × Fin p) := + List.ofFn (modeEquiv P T p).symm + +/-- **The weights of the modes, packet-major**: the mode `(q, y, b)` has weight `b + 1`. -/ +@[expose] def modeWeights (P T p : ℕ) : List ℕ := + (List.range (P * (T * p))).map fun j => j % p + 1 + +theorem modeEquiv_apply_val {P T p : ℕ} (Z : Fin P × Fin T × Fin p) : + (modeEquiv P T p Z : ℕ) = Z.1 * (T * p) + (Z.2.1 * p + Z.2.2) := by + simp only [modeEquiv, Equiv.trans_apply, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map, + id_eq, finProdFinEquiv_apply_val] + ring + +theorem nodup_modeList (P T p : ℕ) : (modeList P T p).Nodup := + List.nodup_ofFn.mpr (modeEquiv P T p).symm.injective + +theorem mem_modeList {P T p : ℕ} (Z : Fin P × Fin T × Fin p) : Z ∈ modeList P T p := + List.mem_ofFn.mpr ⟨modeEquiv P T p Z, by simp⟩ + +theorem idxOf_modeList {P T p : ℕ} (Z : Fin P × Fin T × Fin p) : + (modeList P T p).idxOf Z = modeEquiv P T p Z := by + have h : (modeList P T p)[(modeEquiv P T p Z : ℕ)]'(by simp [modeList]) = Z := by + simp [modeList] + have := List.Nodup.idxOf_getElem (nodup_modeList P T p) (modeEquiv P T p Z : ℕ) + (by simp [modeList]) + rwa [h] at this + +/-- The last coordinate of a mode is its number modulo `p`. -/ +theorem val_modeEquiv_symm_snd_snd {P T p : ℕ} (j : Fin (P * (T * p))) : + (((modeEquiv P T p).symm j).2.2 : ℕ) = j % p := by + obtain ⟨Z, hZ⟩ : ∃ Z, (modeEquiv P T p).symm j = Z := ⟨_, rfl⟩ + have hj : (j : ℕ) = Z.1 * (T * p) + (Z.2.1 * p + Z.2.2) := by + rw [← modeEquiv_apply_val, ← hZ, Equiv.apply_symm_apply] + rw [hZ, hj, show (Z.1 : ℕ) * (T * p) + (Z.2.1 * p + Z.2.2) = Z.2.2 + p * (Z.1 * T + Z.2.1) by + ring, Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt Z.2.2.2] + +/-- The weights listed along the modes are `modeWeights`. -/ +theorem map_modeList_weight (P T p : ℕ) : + (modeList P T p).map (fun Z => (Z.2.2 : ℕ) + 1) = modeWeights P T p := by + apply List.ext_getElem (by simp [modeList, modeWeights]) + intro j h₁ h₂ + simp only [modeList, List.getElem_map, List.getElem_ofFn, modeWeights, List.getElem_range, + val_modeEquiv_symm_snd_snd] + +/-- **The slice of a packet** reads the mode tuple of `β`: entry `b + p y` of the slice of `q` is +the exponent of the mode `(q, y, b)`. -/ +theorem getD_betaSlice {P i pt : ℕ} (β : List ℕ) (q : Fin P) (Z : Fin (2 ^ (i + 1)) × Fin pt) : + (betaSlice i pt β q).getD (finProdFinEquiv Z) 0 = + BudgetTuples.ofList (modeList P (2 ^ (i + 1)) pt) β (q, Z) := by + have hZ : (finProdFinEquiv Z : ℕ) < 2 ^ (i + 1) * pt := (finProdFinEquiv Z).2 + rw [BudgetTuples.ofList, idxOf_modeList, modeEquiv_apply_val, betaSlice, + List.getD_eq_getElem?_getD, List.getElem?_take_of_lt hZ, List.getElem?_drop, + ← List.getD_eq_getElem?_getD, finProdFinEquiv_apply_val] + congr 2 + ring + +/-! ### The native lists in a numbered network -/ + +section Bridge + +variable {m k s : ℕ} (src tgt : Fin m → Fin k) (group : Fin k → Fin s) (g : Fin s) + +/-- Reading the group of an end of an edge from the lists. -/ +theorem getD_ofFn_group (sel : ℕ × ℕ → ℕ) (endF : Fin m → Fin k) + (hsel : ∀ e, sel ((src e : ℕ), (tgt e : ℕ)) = endF e) (e : Fin m) : + (List.ofFn fun v => (group v : ℕ)).getD + (sel ((List.ofFn fun e => ((src e : ℕ), (tgt e : ℕ))).getD e (0, 0))) 0 = + group (endF e) := by + rw [List.getD_ofFn, hsel, List.getD_ofFn] + +/-- **The native ports of group `g` at the end `sel`** are its members, in order. -/ +theorem portEdges_eq (sel : ℕ × ℕ → ℕ) (endF : Fin m → Fin k) + (hsel : ∀ e, sel ((src e : ℕ), (tgt e : ℕ)) = endF e) : + portEdges (List.ofFn fun v => (group v : ℕ)) g (List.ofFn fun e => ((src e : ℕ), (tgt e : ℕ))) + sel = (members fun e => group (endF e) = g).map Fin.val := by + rw [portEdges, List.length_ofFn, ← List.map_coe_finRange_eq_range, List.filter_map, members] + congr 1 + refine List.filter_congr fun e _ => ?_ + simp only [Function.comp_apply, getD_ofFn_group src tgt group sel endF hsel, Fin.val_inj] + +/-- **The native position of a port** is its position among the members. -/ +theorem portRank_eq (sel : ℕ × ℕ → ℕ) (endF : Fin m → Fin k) + (hsel : ∀ e, sel ((src e : ℕ), (tgt e : ℕ)) = endF e) (e : Fin m) : + portRank (List.ofFn fun v => (group v : ℕ)) g (List.ofFn fun e => ((src e : ℕ), (tgt e : ℕ))) + sel e = rank (fun e => group (endF e) = g) e := by + have hr : List.range e = ((List.finRange m).take e).map Fin.val := by + rw [List.map_take, List.map_coe_finRange_eq_range, List.take_range, min_eq_left e.2.le] + rw [portRank, rank, hr, List.countP_map] + refine List.countP_congr fun u _ => ?_ + simp only [Function.comp_apply, getD_ofFn_group src tgt group sel endF hsel, Fin.val_inj, + decide_eq_true_eq] + +/-- Counting a group among the groups of the vertices gives the number of its vertices. -/ +theorem count_ofFn_group : + (List.ofFn fun v => (group v : ℕ)).count (g : ℕ) = (members fun v => group v = g).length := by + rw [List.ofFn_eq_map, List.count, List.countP_map, members, ← List.countP_eq_length_filter] + refine List.countP_congr fun u _ => ?_ + simp [Fin.val_inj] + +/-- The native vertices of group `g` are its members, in order. -/ +theorem filter_range_group : + (List.range k).filter (fun v => (List.ofFn fun v => (group v : ℕ)).getD v 0 = (g : ℕ)) = + (members fun v => group v = g).map Fin.val := by + rw [← List.map_coe_finRange_eq_range, List.filter_map, members] + congr 1 + refine List.filter_congr fun v _ => ?_ + simp only [Function.comp_apply, List.getD_ofFn, Fin.val_inj] + +variable {r : ℕ} (hsrc : ∀ e, (src e : ℕ) < r) (htgt : ∀ e, r ≤ (tgt e : ℕ)) +include hsrc + +/-- **The child edge of a row port** is its number in `childEdgeEquiv`. -/ +theorem childEdgeOf_src (e : Fin m) (h : group (src e) = g) : + childEdgeOf r (List.ofFn fun v => (group v : ℕ)) g + (List.ofFn fun e => ((src e : ℕ), (tgt e : ℕ))) (src e) e = + (childEdgeEquiv src tgt group g (.inl ⟨e, h⟩) : ℕ) := by + rw [childEdgeOf, ite_eq_left (hsrc e), portRank_eq src tgt group g Prod.fst src (fun _ => rfl)] + simp [childEdgeEquiv] + +omit hsrc in +include htgt in +/-- **The child edge of a column port** is its number in `childEdgeEquiv`. -/ +theorem childEdgeOf_tgt (e : Fin m) (h : group (tgt e) = g) : + childEdgeOf r (List.ofFn fun v => (group v : ℕ)) g + (List.ofFn fun e => ((src e : ℕ), (tgt e : ℕ))) (tgt e) e = + (childEdgeEquiv src tgt group g (.inr ⟨e, h⟩) : ℕ) := by + rw [childEdgeOf, ite_eq_right (by have := htgt e; omega), + portRank_eq src tgt group g Prod.snd tgt (fun _ => rfl), + portEdges_eq src tgt group g Prod.fst src (fun _ => rfl), List.length_map] + simp [childEdgeEquiv] + +omit hsrc in +/-- **The parent edge of a numbered child edge.** -/ +theorem parentEdge_childEdgeEquiv (c : ChildEdge src tgt group g) : + parentEdge (List.ofFn fun v => (group v : ℕ)) g + (List.ofFn fun e => ((src e : ℕ), (tgt e : ℕ))) (childEdgeEquiv src tgt group g c) = + (Sum.elim (fun e => (e.1 : ℕ)) (fun e => (e.1 : ℕ)) c) := by + rw [parentEdge, portEdges_eq src tgt group g Prod.fst src (fun _ => rfl), + portEdges_eq src tgt group g Prod.snd tgt (fun _ => rfl), List.length_map] + rcases c with c | c + · have hlt := rank_lt (fun e => group (src e) = g) c.1 c.2 + simp only [childEdgeEquiv, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inl, + finSumFinEquiv_apply_left, Fin.val_castAdd, rankEquiv_apply_val, Sum.elim_inl] + rw [ite_eq_left hlt, List.getD_eq_getElem _ _ (by simpa using hlt), List.getElem_map, + getElem_rank (fun e => group (src e) = g) c.1 c.2] + · have hlt := rank_lt (fun e => group (tgt e) = g) c.1 c.2 + simp only [childEdgeEquiv, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inr, + finSumFinEquiv_apply_right, Fin.val_natAdd, rankEquiv_apply_val, Sum.elim_inr] + rw [ite_eq_right (by omega), Nat.add_sub_cancel_left, + List.getD_eq_getElem _ _ (by simpa using hlt), List.getElem_map, + getElem_rank (fun e => group (tgt e) = g) c.1 c.2] + +omit hsrc in +/-- A numbered child edge is a row port exactly when its number is below the number of row +ports. -/ +theorem lt_length_portEdges_iff (c : ChildEdge src tgt group g) : + (childEdgeEquiv src tgt group g c : ℕ) < + (portEdges (List.ofFn fun v => (group v : ℕ)) g + (List.ofFn fun e => ((src e : ℕ), (tgt e : ℕ))) Prod.fst).length ↔ c.isLeft := by + rw [portEdges_eq src tgt group g Prod.fst src (fun _ => rfl), List.length_map] + rcases c with c | c + · simp only [childEdgeEquiv, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inl, + finSumFinEquiv_apply_left, Fin.val_castAdd, rankEquiv_apply_val, Sum.isLeft_inl, iff_true] + exact rank_lt (fun e => group (src e) = g) c.1 c.2 + · simp only [childEdgeEquiv, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inr, + finSumFinEquiv_apply_right, Fin.val_natAdd, Sum.isLeft_inr, Bool.false_eq_true, iff_false] + omega + +end Bridge + +/-- A filter-map that keeps every entry is a map. -/ +theorem map_filterMap_of_isSome {α β γ : Type*} (f : α → Option β) (y : β → γ) (d : γ) + (l : List α) (h : ∀ x ∈ l, (f x).isSome) : + (l.filterMap f).map y = l.map fun x => ((f x).map y).getD d := by + induction l with + | nil => rfl + | cons x l ih => + obtain ⟨b, hb⟩ := Option.isSome_iff_exists.mp (h x List.mem_cons_self) + rw [List.filterMap_cons_some hb, List.map_cons, List.map_cons, hb, + ih fun x' hx' => h x' (List.mem_cons_of_mem _ hx')] + rfl + +/-! ### The parent over `O` -/ + +section Parent + +variable {fl : List ℕ} (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) + {D : DescribedNetwork VertexDesc} {r : ℕ} (hD : D.IsRowsFirstBipartite r) + +/-- The valuation ring `O = ℤ_(2)[U] / (f)` of `f = monicOf fl`. -/ +noncomputable abbrev RingO : Subring (AdjoinRoot ((monicOf fl).map (Int.castRingHom ℚ))) := + (AdjoinRoot.padicValuation 2 (monic_monicOf fl) hirr).integer + +/-- **The parent over `O`**: the network of the descriptors with the lifts of their entries. -/ +@[expose] noncomputable def parentNetwork : + TensorNetwork (RingO hirr) Bool (Fin D.vertices.length) (Fin D.numEdges) := + D.toNetwork hD fun d bs => liftO hirr (d.entry bs) + +/-- The sides of the parent: the first `r` vertices are the rows. -/ +@[expose] def parentSide (r : ℕ) {k : ℕ} (v : Fin k) : Bool := decide ((v : ℕ) < r) + +theorem parentSide_src (j : Fin D.numEdges) : parentSide r (D.srcFin hD j) = true := + decide_eq_true (DescribedNetwork.srcFin_lt hD j) + +theorem parentSide_tgt (j : Fin D.numEdges) : parentSide r (D.tgtFin hD j) = false := + decide_eq_false (by have := DescribedNetwork.le_tgtFin hD j; omega) + +/-- The row of an edge, among the rows. -/ +@[expose] def rowOfP (j : Fin D.numEdges) : Fin r := + ⟨D.srcFin hD j, DescribedNetwork.srcFin_lt hD j⟩ + +/-- The column of an edge, among the columns. -/ +@[expose] def colOfP (j : Fin D.numEdges) : Fin (D.vertices.length - r) := + ⟨D.tgtFin hD j - r, by + have := DescribedNetwork.le_tgtFin hD j + have := (D.tgtFin hD j).2 + omega⟩ + +/-- **The native packing of the parent**: `nativePacking` of its `(row, column)` edges, with `r` +rows, `k - r` columns, packets of `2 ^ a` slots and `64` symbols. -/ +@[expose] def nativeParentPacking (r a : ℕ) (D : DescribedNetwork VertexDesc) : + (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ) := + PacketPacking.nativePacking r (D.vertices.length - r) a 64 + (D.edgeEnds.map fun e => (e.1, e.2 - r)) + +/-- The `(row, column)` edges of the parent. -/ +theorem edgeEnds_shift : + D.edgeEnds.map (fun e => (e.1, e.2 - r)) = PacketPacking.edgeList (rowOfP hD) (colOfP hD) := by + rw [DescribedNetwork.edgeEnds_eq hD, PacketPacking.edgeList, List.map_ofFn] + rfl + +/-- **The packing of the parent over `O`**: `PacketPacking.packing` of its `(row, column)` edges, +moved to the ends of the parent. -/ +@[expose] noncomputable def parentPacking (a : ℕ) : + PacketPacking.Packing (D.srcFin hD) (D.tgtFin hD) a 64 := + (PacketPacking.packing (rowOfP hD) (colOfP hD) a 64).relabel (D.srcFin hD) (D.tgtFin hD) + (fun v => if h : (v : ℕ) < r then + (PacketPacking.packing (rowOfP hD) (colOfP hD) a 64).rowLabel ⟨v, h⟩ else fun _ => 0) + (fun v => if h : r ≤ (v : ℕ) then + (PacketPacking.packing (rowOfP hD) (colOfP hD) a 64).colLabel ⟨v - r, by omega⟩ + else fun _ => 0) + (fun e => by rw [dite_eq_left (DescribedNetwork.srcFin_lt hD e)]; rfl) + (fun e => by rw [dite_eq_left (DescribedNetwork.le_tgtFin hD e)]; rfl) + +/-- **The native packing of the parent is its packing over `O`** when `64 ^ a` is at most the +number of edges: the words of its labels, its number of packets, and the packet and slot of each +edge. -/ +theorem nativeParentPacking_eq {a : ℕ} (hK : 64 ^ a ≤ D.numEdges) : + nativeParentPacking r a D = + ((List.ofFn fun v => BalancedSchedules.scheduleToWord + ((PacketPacking.packing (rowOfP hD) (colOfP hD) a 64).rowLabel v), + List.ofFn fun w => BalancedSchedules.scheduleToWord + ((PacketPacking.packing (rowOfP hD) (colOfP hD) a 64).colLabel w)), + (parentPacking hD a).numPackets, + List.ofFn fun e => (((parentPacking hD a).packet e : ℕ), + ((parentPacking hD a).slot e : ℕ))) := by + rw [nativeParentPacking, edgeEnds_shift hD, PacketPacking.nativePacking_eq _ _ hK] + rfl + +/-- **The native groups of the parent** in coordinate `i < a` are the groups of the packing. -/ +theorem groupsOf_eq {a i : ℕ} (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) : + groupsOf r i D.vertices.length (nativeParentPacking r a D).1 = + List.ofFn fun v => (packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩ v : ℕ) := by + rw [nativeParentPacking_eq hD hK] + apply List.ext_getElem (by simp [groupsOf]) + intro v h₁ h₂ + simp only [groupsOf, List.getElem_map, List.getElem_range, List.getElem_ofFn, packingGroup, + parentSide, parentPacking, PacketPacking.Packing.relabel] + have hvk : v < D.vertices.length := by simpa using h₂ + by_cases hv : v < r + · rw [ite_eq_left hv, decide_eq_true hv, ite_eq_left rfl, dite_eq_left hv, + List.getD_ofFn (fun v : Fin r => BalancedSchedules.scheduleToWord _) ⟨v, hv⟩, + BalancedSchedules.scheduleToWord, List.getD_ofFn (fun t : Fin a => _) ⟨i, hia⟩] + · have hvr : r ≤ v := by omega + have hlt : v - r < D.vertices.length - r := by omega + rw [ite_eq_right hv, decide_eq_false hv, ite_eq_right (by simp), dite_eq_left hvr, + List.getD_ofFn (fun w : Fin (D.vertices.length - r) => BalancedSchedules.scheduleToWord _) + ⟨v - r, hlt⟩, BalancedSchedules.scheduleToWord, + List.getD_ofFn (fun t : Fin a => _) ⟨i, hia⟩] + +/-- **The mode splitting at a node of the parent** over `O`: `callSplitting` of the parent with +its packing, at the node `t`, the precision `p`, and the lift of the interpolation value `ζ`. -/ +@[expose] noncomputable def parentSplitting (a p u h : ℕ) (hua : u ≤ a) {t : ℤ} + (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (ζ : List ℕ) := + TensorNetwork.callSplitting (RingO hirr) + (AdjoinRoot.algebraMap_mem_integer_padicValuation _ hirr) (parentNetwork hirr hD) + (parentSide r) (parentSide_src hD) (parentSide_tgt hD) (parentPacking hD a) p u h hua ht hq + (liftO hirr ζ) + +section Fields + +variable {a p u h : ℕ} (hua : u ≤ a) {t : ℤ} (ht : t ∈ recoveryNodes a) + (hq : 0 < taperMult u h t) (ζ : List ℕ) + +/-- The rows of the splitting are the first `r` vertices. -/ +theorem parentSplitting_side : (parentSplitting hirr hD a p u h hua ht hq ζ).side = parentSide r := + TensorNetwork.callSplitting_side (RingO hirr) _ (parentNetwork hirr hD) (parentSide r) _ _ + (parentPacking hD a) p u h hua ht hq (liftO hirr ζ) + +/-- The groups of the splitting are the groups of the packing in coordinate `v₂(t)`. -/ +theorem parentSplitting_group : (parentSplitting hirr hD a p u h hua ht hq ζ).group = + packingGroup (parentSide r) (parentPacking hD a) + ⟨_, padicValInt_lt_of_taperMult_pos hq hua⟩ := + TensorNetwork.callSplitting_group (RingO hirr) _ (parentNetwork hirr hD) (parentSide r) _ _ + (parentPacking hD a) p u h hua ht hq (liftO hirr ζ) + +/-- The packets of the splitting are the packets of the packing. -/ +theorem parentSplitting_packet : + (parentSplitting hirr hD a p u h hua ht hq ζ).packet = (parentPacking hD a).packet := + TensorNetwork.callSplitting_packet (RingO hirr) _ (parentNetwork hirr hD) (parentSide r) _ _ + (parentPacking hD a) p u h hua ht hq (liftO hirr ζ) + +end Fields + +section Numbered + +variable {P : ℕ} (group : Fin D.vertices.length → Fin 64) (packet : Fin D.numEdges → Fin P) + (slot : Fin D.numEdges → ℕ) (g : Fin 64) + +/-- The ports of a retained vertex: its parent ports, each as its child edge. -/ +@[expose] def retainedPort (v : {v // group v = g}) (j : ℕ) : + Option (ChildEdge (D.srcFin hD) (D.tgtFin hD) group g) := + if hj : j < D.numEdges then + if (v.1 : ℕ) < r then + if hg : group (D.srcFin hD ⟨j, hj⟩) = g then some (.inl ⟨⟨j, hj⟩, hg⟩) else none + else if hg : group (D.tgtFin hD ⟨j, hj⟩) = g then some (.inr ⟨⟨j, hj⟩, hg⟩) else none + else none + +/-- **A parent port of a retained vertex is a child edge**, numbered by `childEdgeOf`. -/ +theorem retainedPort_spec (v : {v // group v = g}) {j : ℕ} + (hj : j ∈ (D.vertices[(v.1 : ℕ)]'v.1.2).1) : + ∃ c, retainedPort hD group g v j = some c ∧ + (childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g c : ℕ) = + childEdgeOf r (List.ofFn fun v => (group v : ℕ)) g + (List.ofFn fun e => ((D.srcFin hD e : ℕ), (D.tgtFin hD e : ℕ))) v j := by + have hjm : j < D.numEdges := hD.1 _ (List.getElem_mem _) j hj + have hends := (DescribedNetwork.mem_ports_iff hD v.1 ⟨j, hjm⟩).mp hj + have hsrcr := DescribedNetwork.srcFin_lt hD + have htgtr := DescribedNetwork.le_tgtFin hD + by_cases hvr : (v.1 : ℕ) < r + · have hs : D.srcFin hD ⟨j, hjm⟩ = v.1 := hends.resolve_right fun h => by + have := htgtr ⟨j, hjm⟩ + rw [h] at this + omega + have hg : group (D.srcFin hD ⟨j, hjm⟩) = g := hs ▸ v.2 + refine ⟨.inl ⟨⟨j, hjm⟩, hg⟩, ?_, ?_⟩ + · simp only [retainedPort, dite_eq_left hjm, ite_eq_left hvr, dite_eq_left hg] + · have := childEdgeOf_src (D.srcFin hD) (D.tgtFin hD) group g hsrcr ⟨j, hjm⟩ hg + rw [show ((v.1 : Fin _) : ℕ) = (D.srcFin hD ⟨j, hjm⟩ : ℕ) by rw [hs]] + exact this.symm + · have ht : D.tgtFin hD ⟨j, hjm⟩ = v.1 := hends.resolve_left fun h => by + have := hsrcr ⟨j, hjm⟩ + rw [h] at this + exact hvr this + have hg : group (D.tgtFin hD ⟨j, hjm⟩) = g := ht ▸ v.2 + refine ⟨.inr ⟨⟨j, hjm⟩, hg⟩, ?_, ?_⟩ + · simp only [retainedPort, dite_eq_left hjm, ite_eq_right hvr, dite_eq_left hg] + · have := childEdgeOf_tgt (D.srcFin hD) (D.tgtFin hD) group g htgtr ⟨j, hjm⟩ hg + rw [show ((v.1 : Fin _) : ℕ) = (D.tgtFin hD ⟨j, hjm⟩ : ℕ) by rw [ht]] + exact this.symm + +/-- **The ports of the packet vertex `q`**: the child edges of packet `q`, in increasing order of +their numbers. -/ +@[expose] def packetPorts (q : Fin P) : List (ChildEdge (D.srcFin hD) (D.tgtFin hD) group g) := + ((List.finRange _).filter fun j => + childTgt (D.srcFin hD) (D.tgtFin hD) group packet g + ((childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g).symm j) = .inr q).map + (childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g).symm + +/-- **The ports of the numbered child vertices**: the renumbered parent ports of a retained +vertex, and the child edges of a packet. -/ +@[expose] def numberedPorts : + ChildVertex group g P → List (ChildEdge (D.srcFin hD) (D.tgtFin hD) group g) := + Sum.elim (fun v => (D.vertices[(v.1 : ℕ)]'v.1.2).1.filterMap (retainedPort hD group g v)) + (packetPorts hD group packet g) + +/-- **The descriptors of the numbered child vertices**: the parent descriptor of a retained +vertex, and the packet descriptor of a packet. -/ +@[expose] def numberedDesc (fl : List ℕ) (a i pt : ℕ) (t : ℤ) (ζ β : List ℕ) : + ChildVertex group g P → VertexDesc := + Sum.elim (fun v => (D.vertices[(v.1 : ℕ)]'v.1.2).2) fun q => + .inr (packetCtx fl a i pt t ζ g q, + (packetPorts hD group packet g q).map fun c => + (c.isLeft, slot (Sum.elim Subtype.val Subtype.val c)), + betaSlice i pt β q) + +/-- The bit that a retained vertex reads at a parent port. -/ +theorem getD_map_retainedPort (v : {v // group v = g}) {j : ℕ} + (hj : j ∈ (D.vertices[(v.1 : ℕ)]'v.1.2).1) + (y : ChildEdge (D.srcFin hD) (D.tgtFin hD) group g → Bool) : + ((retainedPort hD group g v j).map y).getD false = + if parentSide r v.1 then + (if hg : group (D.srcFin hD ⟨j, hD.1 _ (List.getElem_mem _) j hj⟩) = g then + y (.inl ⟨_, hg⟩) else false) + else + (if hg : group (D.tgtFin hD ⟨j, hD.1 _ (List.getElem_mem _) j hj⟩) = g then + y (.inr ⟨_, hg⟩) else false) := by + have hjm : j < D.numEdges := hD.1 _ (List.getElem_mem _) j hj + by_cases hvr : (v.1 : ℕ) < r + · simp only [retainedPort, dite_eq_left hjm, ite_eq_left hvr, parentSide, decide_eq_true hvr, + ite_true] + split_ifs <;> rfl + · simp only [retainedPort, dite_eq_left hjm, ite_eq_right hvr, parentSide, + decide_eq_false hvr, Bool.false_eq_true, ite_false] + split_ifs <;> rfl + +/-- The ports of a packet are its child edges. -/ +theorem mem_packetPorts (q : Fin P) (c : ChildEdge (D.srcFin hD) (D.tgtFin hD) group g) : + c ∈ packetPorts hD group packet g q ↔ packet (Sum.elim Subtype.val Subtype.val c) = q := by + simp only [packetPorts, List.mem_map, List.mem_filter, List.mem_finRange, true_and, + decide_eq_true_eq] + constructor + · rintro ⟨j, hj, rfl⟩ + rcases hc : (childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g).symm j with c | c <;> + rw [hc] at hj <;> simpa [childTgt] using hj + · intro hc + refine ⟨childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g c, ?_, by simp⟩ + rw [Equiv.symm_apply_apply] + rcases c with c | c <;> simpa [childTgt] using hc + +/-- The ports of a packet are distinct. -/ +theorem nodup_packetPorts (q : Fin P) : (packetPorts hD group packet g q).Nodup := + ((List.nodup_finRange _).filter _).map (Equiv.injective _) + +/-- **The native ports of a packet** are its numbered ports. -/ +theorem childPorts_packet (q : Fin P) : + childPorts (List.ofFn fun j => + (((childVertexEquiv (P := P) group g) (childSrc (D.srcFin hD) (D.tgtFin hD) group g + ((childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g).symm j)) : ℕ), + ((childVertexEquiv (P := P) group g) (childTgt (D.srcFin hD) (D.tgtFin hD) group packet g + ((childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g).symm j)) : ℕ))) + ((List.ofFn fun v => (group v : ℕ)).count (g : ℕ) + q) = + (packetPorts hD group packet g q).map fun c => + (childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g c : ℕ) := by + have h1 : (List.ofFn fun v => (group v : ℕ)).count (g : ℕ) + q = + ((childVertexEquiv (P := P) group g) (.inr q) : ℕ) := by + rw [count_ofFn_group] + simp [childVertexEquiv] + rw [h1, childPorts, List.length_ofFn, ← List.map_coe_finRange_eq_range, List.filter_map, + packetPorts, List.map_map] + congr 1 + · funext j + simp + · refine List.filter_congr fun j _ => ?_ + simp only [Function.comp_apply, List.getD_ofFn, Fin.val_inj, Equiv.apply_eq_iff_eq, + decide_eq_decide] + constructor + · rintro (h | h) + · rcases hc : (childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g).symm j with c | c <;> + rw [hc] at h <;> simp [childSrc] at h + · exact h + · exact Or.inr + +/-- **The native child is the numbered child**: with the groups, packets and slots of the native +packing given by functions, the native child lists the numbered child vertices with their +numbered ports and descriptors. -/ +theorem nativeChild_eq (fl : List ℕ) (a i pt : ℕ) (t : ℤ) (ζ β : List ℕ) + (pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)) + (hgroups : groupsOf r i D.vertices.length pk.1 = List.ofFn fun v => (group v : ℕ)) + (hpk1 : pk.2.1 = P) (hpk2 : pk.2.2 = List.ofFn fun e => ((packet e : ℕ), slot e)) : + nativeChild fl a i pt t ζ r D pk β g = + ⟨(members fun e => group (D.srcFin hD e) = g).length + + (members fun e => group (D.tgtFin hD e) = g).length, + List.ofFn fun c => + ((numberedPorts hD group packet g ((childVertexEquiv (P := P) group g).symm c)).map + fun e => (childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) group g e : ℕ), + numberedDesc hD group packet slot g fl a i pt t ζ β + ((childVertexEquiv (P := P) group g).symm c))⟩ := by + have hpackets : pk.2.2.map Prod.fst = List.ofFn fun e => (packet e : ℕ) := by + rw [hpk2, List.map_ofFn] + rfl + have hcedges := childEdgeList_eq (P := P) (D.srcFin hD) (D.tgtFin hD) group packet g + have hsrcr := DescribedNetwork.srcFin_lt hD + have htgtr := DescribedNetwork.le_tgtFin hD + simp only [nativeChild] + rw [hgroups, DescribedNetwork.edgeEnds_eq hD, hpackets, hpk1, hpk2, hcedges] + simp only [DescribedNetwork.mk.injEq, List.length_ofFn, true_and] + refine Eq.trans ?_ (List.ofFn_add (n := (members fun v => group v = g).length) (m := P)).symm + congr 1 + · rw [filter_range_group, List.map_map] + apply List.ext_getElem (by simp) + intro n h₁ h₂ + have hn : n < (members fun v => group v = g).length := by simpa using h₁ + have hmem : group (members fun v => group v = g)[n] = g := + of_decide_eq_true (List.mem_filter.mp (List.getElem_mem hn)).2 + have hevl : (childVertexEquiv (P := P) group g).symm + (Fin.castLE (Nat.le_add_right _ _) ⟨n, hn⟩) = + .inl ⟨(members fun v => group v = g)[n], hmem⟩ := by + rw [childVertexEquiv, Equiv.symm_trans_apply, + show Fin.castLE (Nat.le_add_right _ _) ⟨n, hn⟩ = Fin.castAdd _ ⟨n, hn⟩ from rfl, + finSumFinEquiv_symm_apply_castAdd] + rfl + simp only [List.getElem_map, List.getElem_ofFn, Function.comp_apply] + rw [hevl] + refine Prod.ext ?_ ?_ + · simp only [numberedPorts, Sum.elim_inl] + rw [List.getD_eq_getElem _ _ ((members fun v => group v = g)[n]).2] + rw [map_filterMap_of_isSome _ _ 0 _ fun j hj => by + obtain ⟨c, hc, -⟩ := retainedPort_spec hD group g ⟨_, hmem⟩ hj + rw [hc] + rfl] + refine List.map_congr_left fun j hj => ?_ + obtain ⟨c, hc, hce⟩ := retainedPort_spec hD group g ⟨_, hmem⟩ hj + rw [hc] + exact hce.symm + · simp only [numberedDesc, Sum.elim_inl] + rw [List.getD_eq_getElem _ _ ((members fun v => group v = g)[n]).2] + · apply List.ext_getElem (by simp) + intro n h₁ h₂ + have hn : n < P := by simpa using h₁ + have hevr : (childVertexEquiv (P := P) group g).symm (Fin.natAdd _ ⟨n, hn⟩) = + .inr ⟨n, hn⟩ := by + rw [childVertexEquiv, Equiv.symm_trans_apply, finSumFinEquiv_symm_apply_natAdd] + rfl + simp only [List.getElem_map, List.getElem_range, List.getElem_ofFn] + rw [hevr] + have hcpq := childPorts_packet hD group packet g ⟨n, hn⟩ + simp only at hcpq + refine Prod.ext hcpq ?_ + simp only [numberedDesc, Sum.elim_inr] + congr 2 + refine Prod.ext ?_ rfl + rw [hcpq, List.map_map] + refine List.map_congr_left fun c _ => ?_ + refine Prod.ext ?_ ?_ + · simp only [Function.comp_apply] + rw [Bool.eq_iff_iff, decide_eq_true_iff] + exact lt_length_portEdges_iff (D.srcFin hD) (D.tgtFin hD) group g c + · simp only [Function.comp_apply] + rw [parentEdge_childEdgeEquiv] + rcases c with c | c <;> simp + +/-- **The ports of a retained vertex are its child edges.** -/ +theorem mem_filterMap_retainedPort (x : {v // group v = g}) + (c : ChildEdge (D.srcFin hD) (D.tgtFin hD) group g) : + c ∈ (D.vertices[(x.1 : ℕ)]'x.1.2).1.filterMap (retainedPort hD group g x) ↔ + childSrc (P := P) (D.srcFin hD) (D.tgtFin hD) group g c = .inl x := by + have hsrcr := DescribedNetwork.srcFin_lt hD + have htgtr := DescribedNetwork.le_tgtFin hD + rw [List.mem_filterMap] + rcases c with ⟨e, he⟩ | ⟨e, he⟩ + · simp only [childSrc, Sum.elim_inl, Sum.inl.injEq, Subtype.ext_iff] + constructor + · rintro ⟨j, hj, hc⟩ + simp only [retainedPort] at hc + split_ifs at hc with hjm hxr hg hg <;> + simp only [Option.some.injEq, Sum.inl.injEq, reduceCtorEq, + Subtype.mk.injEq] at hc + subst hc + rcases (DescribedNetwork.mem_ports_iff hD x.1 ⟨j, hjm⟩).mp hj with h | h + · exact h + · have := htgtr ⟨j, hjm⟩ + rw [h] at this + omega + · intro hs + refine ⟨e.val, (DescribedNetwork.mem_ports_iff hD x.1 e).mpr (Or.inl hs), ?_⟩ + have hxr : (x.1 : ℕ) < r := hs ▸ hsrcr e + simp only [retainedPort, dite_eq_left e.2, ite_eq_left hxr, Fin.eta] + rw [dite_eq_left he] + · simp only [childSrc, Sum.elim_inr, Sum.inl.injEq, Subtype.ext_iff] + constructor + · rintro ⟨j, hj, hc⟩ + simp only [retainedPort] at hc + split_ifs at hc with hjm hxr hg hg <;> + simp only [Option.some.injEq, Sum.inr.injEq, reduceCtorEq, + Subtype.mk.injEq] at hc + subst hc + rcases (DescribedNetwork.mem_ports_iff hD x.1 ⟨j, hjm⟩).mp hj with h | h + · have := hsrcr ⟨j, hjm⟩ + rw [h] at this + exact absurd this hxr + · exact h + · intro ht + refine ⟨e.val, (DescribedNetwork.mem_ports_iff hD x.1 e).mpr (Or.inr ht), ?_⟩ + have hxr : ¬ (x.1 : ℕ) < r := by have := htgtr e; rw [ht] at this; omega + simp only [retainedPort, dite_eq_left e.2, ite_eq_right hxr, Fin.eta] + rw [dite_eq_left he] + +/-- A retained port names its parent edge. -/ +theorem val_of_retainedPort_eq_some {x : {v // group v = g}} {j : ℕ} + {c : ChildEdge (D.srcFin hD) (D.tgtFin hD) group g} (h : retainedPort hD group g x j = some c) : + (Sum.elim (fun e => (e.1 : ℕ)) (fun e => (e.1 : ℕ)) c) = j := by + simp only [retainedPort] at h + split_ifs at h <;> simp only [Option.some.injEq] at h <;> subst h <;> rfl + +include hD in +/-- The ports of a vertex of a rows-first network are distinct. -/ +theorem nodup_ports (v : Fin D.vertices.length) : (D.vertices[v]).1.Nodup := by + refine List.nodup_iff_count_le_one.mpr fun j => ?_ + by_cases hj : j ∈ (D.vertices[v]).1 + · have hjm : j < D.numEdges := hD.1 _ (List.getElem_mem _) j hj + obtain ⟨s, t, hs, ht, -, -, hsc, htc, hinc⟩ := DescribedNetwork.incident_eq hD hjm + rcases (DescribedNetwork.mem_ports_iff hD v ⟨j, hjm⟩).mp hj with h | h + · have hv : (v : ℕ) = s := by + rw [← h] + simp [DescribedNetwork.srcFin, hinc] + have : (D.vertices[v]).1 = (D.vertices[s]).1 := by simp only [Fin.getElem_fin, hv] + rw [this, hsc] + · have hv : (v : ℕ) = t := by + rw [← h] + simp [DescribedNetwork.tgtFin, hinc] + have : (D.vertices[v]).1 = (D.vertices[t]).1 := by simp only [Fin.getElem_fin, hv] + rw [this, htc] + · rw [List.count_eq_zero.mpr hj] + exact Nat.zero_le _ + +/-- **The numbered ports of a child vertex are its child edges**, without repetition. -/ +theorem mem_numberedPorts (v : ChildVertex group g P) + (c : ChildEdge (D.srcFin hD) (D.tgtFin hD) group g) : + c ∈ numberedPorts hD group packet g v ↔ + childSrc (D.srcFin hD) (D.tgtFin hD) group g c = v ∨ + childTgt (D.srcFin hD) (D.tgtFin hD) group packet g c = v := by + rcases v with x | q + · rw [numberedPorts, Sum.elim_inl, mem_filterMap_retainedPort] + refine ⟨Or.inl, fun h => h.resolve_right ?_⟩ + rcases c with c | c <;> simp [childTgt] + · rw [numberedPorts, Sum.elim_inr, mem_packetPorts] + rcases c with c | c <;> simp [childSrc, childTgt] + +theorem nodup_numberedPorts (v : ChildVertex group g P) : + (numberedPorts hD group packet g v).Nodup := by + rcases v with x | q + · exact (nodup_ports hD x.1).filterMap fun j j' c hc hc' => by + rw [← val_of_retainedPort_eq_some hD group g hc, ← val_of_retainedPort_eq_some hD group g hc'] + · exact nodup_packetPorts hD group packet g q + +end Numbered + +/-- **Being rows-first depends only on the multisets of ports.** -/ +theorem isRowsFirstBipartite_ofFn_iff {T T' : Type} {k l r : ℕ} (F : Fin k → List ℕ × T) + (F' : Fin k → List ℕ × T') (h : ∀ x, (F x).1.Perm (F' x).1) : + (⟨l, List.ofFn F⟩ : DescribedNetwork T).IsRowsFirstBipartite r ↔ + (⟨l, List.ofFn F'⟩ : DescribedNetwork T').IsRowsFirstBipartite r := by + have hc (i : ℕ) : (List.ofFn F).map (fun v => v.1.count i) = + (List.ofFn F').map (fun v => v.1.count i) := by + simp only [List.map_ofFn] + congr 1 + funext x + exact (h x).count_eq i + have hm : (∀ v ∈ List.ofFn F, ∀ i ∈ v.1, i < l) ↔ (∀ v ∈ List.ofFn F', ∀ i ∈ v.1, i < l) := by + simp only [List.mem_ofFn, forall_exists_index, forall_apply_eq_imp_iff] + exact forall_congr' fun x => forall_congr' fun i => imp_congr_left (h x).mem_iff + simp only [DescribedNetwork.IsRowsFirstBipartite, List.map_take, List.map_drop, hc, hm] + +section Rows + +variable {a i : ℕ} (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) + +include hD hK hia in +/-- **The native child is rows-first**, with its retained vertices as its rows. -/ +theorem isRowsFirstBipartite_nativeChild (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64) : + (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).IsRowsFirstBipartite + (childRows r i D (nativeParentPacking r a D) g) := by + have hgroups := groupsOf_eq hD hK hia + have hpk1 : (nativeParentPacking r a D).2.1 = (parentPacking hD a).numPackets := by + rw [nativeParentPacking_eq hD hK] + have hpk2 : (nativeParentPacking r a D).2.2 = List.ofFn fun e => + (((parentPacking hD a).packet e : ℕ), ((parentPacking hD a).slot e : ℕ)) := by + rw [nativeParentPacking_eq hD hK] + rw [childRows, hgroups, count_ofFn_group, + nativeChild_eq hD _ (parentPacking hD a).packet (fun e => ((parentPacking hD a).slot e : ℕ)) g + fl a i pt t ζ β _ hgroups hpk1 hpk2] + -- The incidence of the numbered child, with zero tensors. + let N : TensorNetwork ℕ Bool + (ChildVertex (packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩) g + (parentPacking hD a).numPackets) + (ChildEdge (D.srcFin hD) (D.tgtFin hD) + (packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩) g) := + { src := childSrc (D.srcFin hD) (D.tgtFin hD) _ g + tgt := childTgt (D.srcFin hD) (D.tgtFin hD) _ (parentPacking hD a).packet g + tensor := fun _ _ => 0 + tensor_congr := fun _ _ _ _ => rfl } + have hside : ∀ e, ((childVertexEquiv (P := (parentPacking hD a).numPackets) _ g (N.src e) : + Fin _) : ℕ) < (members fun v => + packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩ v = g).length ↔ + ¬ ((childVertexEquiv (P := (parentPacking hD a).numPackets) _ g (N.tgt e) : Fin _) : ℕ) < + (members fun v => + packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩ v = g).length := by + rintro (e | e) <;> simp only [N, childSrc, childTgt, childVertexEquiv, Sum.elim_inl, + Sum.elim_inr, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inl, Equiv.refl_apply, + finSumFinEquiv_apply_left, finSumFinEquiv_apply_right, Fin.val_castAdd, Fin.val_natAdd, + rankEquiv_apply_val, Sum.map_inr] + · exact ⟨fun _ => by omega, fun _ => rank_lt _ _ e.2⟩ + · exact ⟨fun _ => by omega, fun _ => rank_lt _ _ e.2⟩ + have hexp := TensorNetwork.isRowsFirstBipartite_toExplicit N + (childVertexEquiv (P := (parentPacking hD a).numPackets) _ g) + (childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) _ g) _ hside + refine (isRowsFirstBipartite_ofFn_iff _ _ fun c => ?_).mpr hexp + set v := (childVertexEquiv (P := (parentPacking hD a).numPackets) _ g).symm c + refine (List.perm_ext_iff_of_nodup ((nodup_numberedPorts hD _ _ g v).map + (Fin.val_injective.comp (Equiv.injective _))) + ((N.nodup_explicitPorts _ v).map Fin.val_injective)).mpr fun n => ?_ + simp only [List.mem_map, TensorNetwork.mem_explicitPorts, mem_numberedPorts] + constructor + · rintro ⟨e, he, rfl⟩ + exact ⟨_, by simpa [N] using he, rfl⟩ + · rintro ⟨j, hj, rfl⟩ + exact ⟨_, by simpa [N] using hj, by simp⟩ + +end Rows + + +section Child + +variable {a p u h : ℕ} (hK : 64 ^ a ≤ D.numEdges) (hua : u ≤ a) {t : ℤ} + (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (ζ β : List ℕ) (g : Fin 64) + +/-- The valuation of the node. -/ +local notation "iₜ" => padicValInt 2 t +/-- The precision of the node. -/ +local notation "ptₜ" => nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t) +/-- The mode splitting at the node. -/ +local notation "S₀" => parentSplitting hirr hD a p u h hua ht hq ζ +/-- The mode tuple of `β`. -/ +local notation "β₀" => BudgetTuples.ofList + (modeList (PacketPacking.Packing.numPackets (parentPacking hD a)) + (2 ^ (padicValInt 2 t + 1)) (nodePrecision p h a (Fintype.card (Fin D.numEdges)) + (padicValInt 2 t))) β +/-- The numbering of the child vertices. -/ +local notation "ev₀" => + childVertexEquiv (P := PacketPacking.Packing.numPackets (parentPacking hD a)) + (TensorNetwork.ModeSplitting.group (parentSplitting hirr hD a p u h hua ht hq ζ)) g +/-- The numbering of the child edges. -/ +local notation "ee₀" => childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) + (TensorNetwork.ModeSplitting.group (parentSplitting hirr hD a p u h hua ht hq ζ)) g + +/-- **The entries of the retained vertices** of the numbered child are the tensors of the child. -/ +theorem entry_numbered_inl (v : {v // (S₀).group v = g}) + (y : ChildEdge (D.srcFin hD) (D.tgtFin hD) (S₀).group g → Bool) : + reductionLift (monic_monicOf fl) hirr ptₜ (val ptₜ fl + ((numberedDesc hD (S₀).group (S₀).packet (fun e => ((parentPacking hD a).slot e : ℕ)) g + fl a iₜ ptₜ t ζ β (.inl v)).entry + ((numberedPorts hD (S₀).group (S₀).packet g (.inl v)).map y))) = + ((S₀).child β₀ g).tensor (.inl v) y := by + rw [TensorNetwork.ModeSplitting.child_tensor_inl_eq_tensor (S₀) β₀ g v y, + TensorNetwork.map_tensor, + ← mk_liftO, parentSplitting_side hirr hD hua ht hq ζ] + simp only [numberedDesc, numberedPorts, Sum.elim_inl, parentNetwork, + DescribedNetwork.toNetwork, DescribedNetwork.wordBits] + congr 3 + rw [map_filterMap_of_isSome _ _ false _ fun j hj => by + obtain ⟨c, hc, -⟩ := retainedPort_spec hD (S₀).group g v hj + rw [hc] + rfl] + refine List.map_congr_left fun j hj => ?_ + rw [getD_map_retainedPort hD (S₀).group g v hj y, + List.getD_ofFn_of_lt _ (hD.1 _ (List.getElem_mem _) j hj)] + rfl + +/-- **The entries of the packet vertices** of the numbered child are the tensors of the child. -/ +theorem entry_numbered_inr (q : Fin (parentPacking hD a).numPackets) + (y : ChildEdge (D.srcFin hD) (D.tgtFin hD) (S₀).group g → Bool) : + reductionLift (monic_monicOf fl) hirr ptₜ (val ptₜ fl + ((numberedDesc hD (S₀).group (S₀).packet (fun e => ((parentPacking hD a).slot e : ℕ)) g + fl a iₜ ptₜ t ζ β (.inr q)).entry + ((numberedPorts hD (S₀).group (S₀).packet g (.inr q)).map y))) = + ((S₀).child β₀ g).tensor (.inr q) y := by + have hia : iₜ < a := padicValInt_lt_of_taperMult_pos hq hua + have hsym := PacketPacking.packetSymbols_eq (rowOfP hD) (colOfP hD) _ _ q ⟨iₜ, hia⟩ + simp only [numberedDesc, numberedPorts, Sum.elim_inr] + exact TensorNetwork.map_val_entry_child_inr (N := (parentNetwork hirr hD).map + (Ideal.Quotient.mk (nodeIdeal (RingO hirr) (Fintype.card (Fin D.numEdges)) a h p t))) + (parentSide r) (parentSide_src hD) (parentSide_tgt hD) + (packingGroup_src_tgt (parentSide r) (parentSide_src hD) (parentSide_tgt hD) + (parentPacking hD a) ⟨iₜ, hia⟩) + (packing_slot_lt (parentPacking hD a)) hia _ _ (two_pow_eq_zero_twoPowIdeal _ _) + (Finset.mem_of_mem_erase ht) (two_pow_padicValInt_dvd_and_not_dvd (Finset.ne_of_mem_erase ht)).1 + (two_pow_padicValInt_dvd_and_not_dvd (Finset.ne_of_mem_erase ht)).2 β₀ g q _ + (nodup_packetPorts hD (S₀).group (S₀).packet g q) + (fun c => (mem_packetPorts hD (S₀).group (S₀).packet g q c).trans (by + rw [parentSplitting_packet hirr hD hua ht hq ζ] + exact Iff.rfl)) + (packetCtx fl a iₜ ptₜ t ζ g q) (betaSlice iₜ ptₜ β q) + (reductionLift (monic_monicOf fl) hirr ptₜ) (mk_liftO hirr ptₜ ζ).symm rfl rfl rfl rfl rfl rfl + (by simp only [packetCtx, hsym, Fin.val_inj]; rfl) + (by simp only [packetCtx, hsym, Fin.val_inj]; rfl) + (by simp only [packetCtx, hsym, ne_eq, Fin.val_inj]; rfl) + (getD_betaSlice β q) y + +include hK in +/-- **The native child has the contraction of the child** ([OpenAI2026ETH], §D.4.6). For a +rows-first parent with `64 ^ a` at most its number of edges, a node `t` of positive multiplicity +with `u ≤ a`, an interpolation value `ζ`, packet-major exponents `β` and a group `g`, the native +child at the precision `p_t` of the node, with the entries of its descriptors in `A_{p_t}` mapped +along `reductionLift` to `O / (2 ^ {p_t})`, has the contraction of the child of group `g` of the +mode splitting at `t` (`parentSplitting`) at the mode tuple of `β`. -/ +theorem contraction_nativeChild : + (nativeChild fl a (padicValInt 2 t) + (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t)) t ζ r D + (nativeParentPacking r a D) β g).contraction + (fun d bs => reductionLift (monic_monicOf fl) hirr + (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t)) + (val (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t)) fl + (d.entry bs))) = + ((parentSplitting hirr hD a p u h hua ht hq ζ).child + (BudgetTuples.ofList (modeList (parentPacking hD a).numPackets (2 ^ (padicValInt 2 t + 1)) + (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t))) β) + g).contraction := by + have hia : iₜ < a := padicValInt_lt_of_taperMult_pos hq hua + have hgroups : groupsOf r iₜ D.vertices.length (nativeParentPacking r a D).1 = + List.ofFn fun v => ((S₀).group v : ℕ) := by + rw [parentSplitting_group hirr hD hua ht hq ζ] + exact groupsOf_eq hD hK hia + have hpk1 : (nativeParentPacking r a D).2.1 = (parentPacking hD a).numPackets := by + rw [nativeParentPacking_eq hD hK] + have hpk2 : (nativeParentPacking r a D).2.2 = + List.ofFn fun e => (((S₀).packet e : ℕ), ((parentPacking hD a).slot e : ℕ)) := by + rw [nativeParentPacking_eq hD hK, parentSplitting_packet hirr hD hua ht hq ζ] + rw [nativeChild_eq hD (S₀).group (S₀).packet (fun e => ((parentPacking hD a).slot e : ℕ)) g + fl a iₜ ptₜ t ζ β _ hgroups hpk1 hpk2] + refine DescribedNetwork.contraction_eq_of_ports ((S₀).child β₀ g) _ _ _ _ _ ?_ + rintro (v | q) y + · exact entry_numbered_inl hirr hD hua ht hq ζ β g v y + · exact entry_numbered_inr hirr hD hua ht hq ζ β g q y + +end Child + +end Parent + +end NativeChild + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Recursion.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Recursion.lean index a6606b51b9..46ead171a8 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Recursion.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Recursion.lean @@ -182,7 +182,7 @@ variable {R V E : Type*} [CommRing R] [Fintype E] {a r : ℕ} a packing `Q` of its edges, and a nonzero grid point `t` of valuation `i < a`, the mode splitting of the Cauchy matrix at `T = t + α ζ` with the vertices grouped by their symbol in coordinate `i` of `Q` (`cauchyModeSplitting`, oriented by `packingGroup_src_tgt`). -/ -noncomputable def nodeSplitting (N : TensorNetwork R Bool V E) (side : V → Bool) +@[expose] noncomputable def nodeSplitting (N : TensorNetwork R Bool V E) (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) (Q : PacketPacking.Packing N.src N.tgt a r) (κ : ℤ₍₂₎ →+* R) (ζ : R) {p : ℕ} (hp : (2 : R) ^ p = 0) {t : ℤ} (ht : t ∈ recoveryNodes a) (hia : padicValInt 2 t < a) : @@ -225,7 +225,7 @@ variable {K : Type*} [CommRing K] [Algebra ℚ K] (B : Subring K) /-- The mode splitting at the active node `t` and the point `z` of a call with input precision `p`: `nodeSplitting` for the network reduced modulo `2 ^ p_t`, at the reduction of `z`. -/ -noncomputable def callSplitting (N : TensorNetwork B Bool V E) (side : V → Bool) +@[expose] noncomputable def callSplitting (N : TensorNetwork B Bool V E) (side : V → Bool) (hsrc : ∀ e, side (N.src e) = true) (htgt : ∀ e, side (N.tgt e) = false) {a r : ℕ} (Q : PacketPacking.Packing N.src N.tgt a r) (p u h : ℕ) (hua : u ≤ a) {t : ℤ} (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (z : B) : diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Admissible.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Admissible.lean index d1afe23004..80fd8c882e 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Admissible.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Admissible.lean @@ -22,7 +22,7 @@ explicit Boolean tensor networks with a number of row vertices, networks are built (milestone H3) and the contraction theorem consumes them (milestone T2). A network `(r, G)` is admissible at size `s` with constant `C` when `G` is bipartite with its -first `r` vertices as rows (`Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`), +first `r` vertices as rows (`Cslib.Circuits.Frontier.DescribedNetwork.IsRowsFirstBipartite`), it has at most `C s` edges and at most `C s` vertices, its maximum degree is at most `C ⌊log₂ s⌋`, every table lists the values at all bit strings on its ports, and it has at least `s` edges. The last two conditions spare the contraction algorithm short tables and networks much smaller than diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean index 56ed22be45..da05642876 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean @@ -43,7 +43,7 @@ accepting count (`Turing.MultiTapePTM.sum_contraction_explicitBlockNetwork`). `2 * (q * (3 * k + 1) * m)` edges and maximum degree at most `2 * (3 * k + 1) * m`, both `O(b)` per interval. Its first `q * (3 * k + 2)` vertices are the rows of a bipartition: every edge has exactly one port at a row and one at a column -(`Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`). Every table has length +(`Cslib.Circuits.Frontier.DescribedNetwork.IsRowsFirstBipartite`). Every table has length `2 ^ (number of ports)`, and its entries are at most `2 ^ b`. These are the inputs of the Boolean tensor contraction theorem [OpenAI2026ETH, Theorem D.1] diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean index 9206e0547a..dcde7ed35a 100644 --- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean @@ -103,7 +103,7 @@ example : ¬ parallel.IsRowsFirstBipartite 2 := by decide example : ¬ (cycle eqTable).IsRowsFirstBipartite 2 := by decide /-- A port naming no edge is excluded. -/ -example : ¬ ExplicitTensorNetwork.IsRowsFirstBipartite +example : ¬ DescribedNetwork.IsRowsFirstBipartite (⟨1, [([0], [1, 1]), ([0, 5], [1, 1, 1, 1])]⟩ : ExplicitTensorNetwork ℕ) 1 := by decide /-- Written out with the old vertices first, the subdivision of `parallelNetwork` is rows-first diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChild.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChild.lean new file mode 100644 index 0000000000..1431e819e9 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChild.lean @@ -0,0 +1,64 @@ +/- +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.NativeCall + +public section + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.NativeChild + +namespace Cslib.Tests.TensorNetworkNativeChild + +/-! ### A path with one row and two columns + +The row `0` joins the columns `1` and `2` by the edges `0` and `1`, and the vertices carry tables. +The network is rows-first at `1`, and the ends of its edges are computed from the ports. -/ + +/-- The tables of the vertices. -/ +def table (n : ℕ) : VertexDesc := .inl (List.replicate n 1) + +/-- The row `0` with ports `1, 0` (not in edge order), the columns `1` and `2`. -/ +def path : DescribedNetwork VertexDesc := + ⟨2, [([1, 0], table 4), ([0], table 2), ([1], table 2)]⟩ + +example : path.IsRowsFirstBipartite 1 := by decide + +example : ¬ path.IsRowsFirstBipartite 2 := by decide + +example : path.edgeEnds = [(0, 1), (0, 2)] := by decide + +/-- The native child of group `0` for a packing that puts the row and the column `1` in group `0`, +the column `2` in group `1`, and both edges in packet `0` with slots `0` and `1`. -/ +def child : DescribedNetwork VertexDesc := + nativeChild [1] 1 0 3 (-1) [0] 1 path (([[0]], [[0], [1]]), 1, [(0, 0), (0, 1)]) [] 0 + +/-- The child keeps the row and the column `1`, and adds the packet: three child edges, the two +row ports of group `0` and the column port of edge `0`. -/ +example : child.numEdges = 3 := by decide + +/-- The row keeps its parent's port order, renumbered (edge `1` is row port `1`, edge `0` row port +`0`); the column `1` reads the column port `2`; the packet reads all three child edges in order. -/ +example : child.vertices.map Prod.fst = [[1, 0], [2], [0, 1, 2]] := by decide + +/-- The packet tags its ports as row ports, row ports and a column port, with the slots of their +parent edges. -/ +example : (child.vertices.getD 2 ([], .inl [])).2.getRight?.map (fun d => d.2.1) = + some [(true, 0), (true, 1), (false, 0)] := by decide + +example : childRows 1 0 path (([[0]], [[0], [1]]), 1, [(0, 0), (0, 1)]) 0 = 2 := by decide + +example : child.IsRowsFirstBipartite 2 := by decide + +/-! ### The modes of a node -/ + +example : modeWeights 2 2 3 = [1, 2, 3, 1, 2, 3, 1, 2, 3, 1, 2, 3] := by decide + +example : betaSlice 0 3 [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12] 1 = [7, 8, 9, 10, 11, 12] := by + decide + +end Cslib.Tests.TensorNetworkNativeChild