From 97dd69ee11f9fff77ee5672411ea6a135f6423e3 Mon Sep 17 00:00:00 2001 From: chris-ai1 Date: Sat, 31 Oct 2026 10:19:41 +0000 Subject: [PATCH] refactor(tensor-network): place reusable lemmas beside their models Move the row-count bound into DescribedNetwork with arbitrary descriptor types, update its three clients, and move the unchanged native-child descriptor theorem to NativeChild. Add concrete generic-descriptor and edgeless boundary clients. Source credit and contraction/resource endpoints are preserved. Independent Codex review approves the final source; focused strict builds, hygiene and aggregate checks pass. Full hosted validation is required before integration. --- .../Frontier/TensorNetwork/DescribedLift.lean | 9 +++ .../TensorNetwork/FastContractionLeaf.lean | 61 ------------------- .../FastContractionSchedule.lean | 2 +- .../TensorNetwork/FastContractionStep.lean | 12 +--- .../Frontier/TensorNetwork/NativeChild.lean | 55 +++++++++++++++++ ComplexityTests/DescribedNetworkRows.lean | 25 ++++++++ 6 files changed, 92 insertions(+), 72 deletions(-) create mode 100644 ComplexityTests/DescribedNetworkRows.lean diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean index 657d320f7e..62bfd5130d 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean @@ -60,6 +60,7 @@ for. * `Cslib.GaloisRingArith.reduction_liftO`, `Cslib.GaloisRingArith.mk_liftO`: reducing a lift. * `Cslib.GaloisRingArith.isUnit_liftO_sub`, `Cslib.GaloisRingArith.pairwise_isUnit_liftO_sub_digits`: binary lists as interpolation points. +* `Cslib.Circuits.Frontier.DescribedNetwork.rows_le_of_isRowsFirstBipartite`: row count bound. * `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. @@ -250,6 +251,14 @@ theorem isRowsFirstBipartite_map {T' : Type} (f : T → T') (r : ℕ) : variable {D} +/-- A rows-first network with an edge has at most as many rows as vertices. -/ +theorem rows_le_of_isRowsFirstBipartite {D : DescribedNetwork T} {r : ℕ} + (hD : D.IsRowsFirstBipartite r) (hM : 1 ≤ D.numEdges) : r ≤ D.vertices.length := by + by_contra h + have h1 := (hD.2 0 hM).2 + rw [List.drop_of_length_le (by omega)] at h1 + simp at h1 + 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] diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean index 785b26d056..5a9865f610 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean @@ -51,8 +51,6 @@ but a polynomial in `n` is a constant. ## Main results * `Cslib.Circuits.Frontier.FastContraction.leafCertificate_le`: the cost of a leaf. -* `Cslib.Circuits.Frontier.NativeChild.desc_of_mem_nativeChild`: the descriptors of a native - child. * `Cslib.Circuits.Frontier.FastContraction.packetShape_root`, `Cslib.Circuits.Frontier.FastContraction.packetShape_child`: the packet shape on the reached calls. @@ -71,65 +69,6 @@ public section namespace Cslib.Circuits.Frontier -/-! ### The descriptors of the native children -/ - -namespace NativeChild - -open ChildNumbering - -variable {D : DescribedNetwork VertexDesc} {r : ℕ} - -/-- **The descriptors of the native child.** A vertex of the native child of a rows-first parent -with at least `64 ^ a` edges keeps the descriptor of a parent vertex, or is the packet `q`, with -the packet context of `q`, the slice of `β` at `q`, and tags whose slots are below `2 ^ a` and -distinct among its row ports. -/ -theorem desc_of_mem_nativeChild (hD : D.IsRowsFirstBipartite r) {fl : List ℕ} {a i : ℕ} - (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64) - {v : List ℕ × VertexDesc} - (hv : v ∈ (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).vertices) : - (∃ w ∈ D.vertices, v.2 = w.2) ∨ - ∃ q tags, v.2 = .inr (packetCtx fl a i pt t ζ g q, tags, betaSlice i pt β q) ∧ - (∀ y ∈ tags, y.2 < 2 ^ a) ∧ ((tags.filter (·.1)).map (·.2)).Nodup := 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 [nativeChild_eq hD _ (parentPacking hD a).packet (fun e => ((parentPacking hD a).slot e : ℕ)) - g fl a i pt t ζ β _ hgroups hpk1 hpk2] at hv - simp only [List.mem_ofFn] at hv - obtain ⟨c, rfl⟩ := hv - rcases hc : (childVertexEquiv (P := (parentPacking hD a).numPackets) - (packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩) g).symm c with w | q - · left - refine ⟨D.vertices[(w.1 : ℕ)], List.getElem_mem _, ?_⟩ - simp only [numberedDesc, Sum.elim_inl] - · right - simp only [numberedDesc, Sum.elim_inr] - refine ⟨q, _, rfl, ?_, ?_⟩ - · intro y hy - simp only [List.mem_map] at hy - obtain ⟨e, -, rfl⟩ := hy - exact Fin.isLt _ - · rw [List.filter_map, List.map_map] - refine List.Nodup.map_on ?_ ((nodup_packetPorts hD _ _ g q).filter _) - intro c₁ hc₁ c₂ hc₂ heq - simp only [List.mem_filter, Function.comp_apply] at hc₁ hc₂ - obtain ⟨hm₁, hl₁⟩ := hc₁ - obtain ⟨hm₂, hl₂⟩ := hc₂ - rw [mem_packetPorts] at hm₁ hm₂ - rcases c₁ with e₁ | e₁ - · rcases c₂ with e₂ | e₂ - · simp only [Function.comp_apply, Sum.elim_inl] at heq hm₁ hm₂ - have hinj := (parentPacking hD a).injective (a₁ := e₁.1) (a₂ := e₂.1) - (Prod.ext (hm₁.trans hm₂.symm) (Fin.ext heq)) - rw [Subtype.ext hinj] - · simp at hl₂ - · simp at hl₁ - -end NativeChild - namespace FastContraction open GaloisRingArith NativePacket ChildCursor NativeRecovery ContractionSchedule NativeChild diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean index e367f44adf..2cf1e3f191 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean @@ -274,7 +274,7 @@ theorem length_children_le (hB : ∀ d M p, Active C m d M p → ActiveBounds C have hK := pow_slots_le_edges_of_active ha have hslots : slots x = slotBits m x.depth := by rw [slots, h.scale_eq] have hlevels : levels x = taper m x.depth := by rw [levels, h.scale_eq] - have hr := rows_le_of_isRowsFirstBipartite h.wf.2 (one_le_edges_of_active ha) + have hr := DescribedNetwork.rows_le_of_isRowsFirstBipartite h.wf.2 (one_le_edges_of_active ha) have hP : (packing x).2.1 * 2 ^ slots x ≤ 3 * x.edges := packing_eq hr ▸ numPackets_nativeParentPacking_mul_le h.wf.2 hK h.degree_le (by rw [hslots]; exact hb.degree_mul_pairs_sq_le) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean index ea5822fb2d..657277b1a1 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean @@ -71,14 +71,6 @@ row and stores the exponents in unary. -/ variable {x : Call} -/-- A rows-first network with an edge has at most as many rows as vertices. -/ -theorem rows_le_of_isRowsFirstBipartite {D : DescribedNetwork VertexDesc} {r : ℕ} - (hD : D.IsRowsFirstBipartite r) (hM : 1 ≤ D.numEdges) : r ≤ D.vertices.length := by - by_contra h - have h1 := (hD.2 0 hM).2 - rw [List.drop_of_length_le (by omega)] at h1 - simp at h1 - /-- The cap of `nativeMk` leaves a tuple of weight below `p` unchanged, for positive weights. -/ theorem map_min_of_mem_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} {β : List ℕ} (hβ : β ∈ BudgetTuples.budgetTuples ws p) : β.map (min · p) = β := by @@ -97,7 +89,7 @@ theorem nativeMk_eq (hx : WF x) (ha : active x = true) {c : State} (hc : c ∈ c nativeChild x.fl (slots x) (level x ((nodes x).getD c.1 0)) (nodePrec x c.1) (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) x.rows x.net (nativeParentPacking x.rows (slots x) x.net) c.2.2.1 c.2.2.2) := by - have hr := rows_le_of_isRowsFirstBipartite hx.2 (one_le_edges_of_active ha) + have hr := DescribedNetwork.rows_le_of_isRowsFirstBipartite hx.2 (one_le_edges_of_active ha) have hβ : c.2.2.1 ∈ BudgetTuples.budgetTuples (weights x c.1) (nodePrec x c.1) := by simp only [children, cursorList, nodeBlock, pointBlock, groupBlock, List.mem_flatMap, List.mem_range, List.mem_map] at hc @@ -154,7 +146,7 @@ theorem stepCorrect_nativeMk : StepCorrect nativeMk WF := by simp only [active, decide_eq_true_eq] at ha' obtain ⟨-, hu, huM, hua, -, -, -⟩ := ha' have hlen : (points x).length = numPoints x := by simp [points] - have hr := rows_le_of_isRowsFirstBipartite hD (one_le_edges_of_active ha) + have hr := DescribedNetwork.rows_le_of_isRowsFirstBipartite hD (one_le_edges_of_active ha) refine NativeCall.val_recover_eq_contraction hirr hD hu huM hua (le_taperStep_mul hu) (taperStep_mul_le _ _ _) (pow_slots_le_edges_of_active ha) ?_ (points x) (pairwise_isUnit_points hirr ha) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean index e90fd66f59..2d0a6a4ae9 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean @@ -67,6 +67,8 @@ vertices as rows (`NativeChild.isRowsFirstBipartite_nativeChild`). * `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. +* `Cslib.Circuits.Frontier.NativeChild.desc_of_mem_nativeChild`: its retained and packet + descriptors. ## References @@ -1022,6 +1024,59 @@ end Child end Parent +/-! ### The descriptors of the native children -/ + +variable {D : DescribedNetwork VertexDesc} {r : ℕ} + +/-- **The descriptors of the native child.** A vertex of the native child of a rows-first parent +with at least `64 ^ a` edges keeps the descriptor of a parent vertex, or is the packet `q`, with +the packet context of `q`, the slice of `β` at `q`, and tags whose slots are below `2 ^ a` and +distinct among its row ports. -/ +theorem desc_of_mem_nativeChild (hD : D.IsRowsFirstBipartite r) {fl : List ℕ} {a i : ℕ} + (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64) + {v : List ℕ × VertexDesc} + (hv : v ∈ (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).vertices) : + (∃ w ∈ D.vertices, v.2 = w.2) ∨ + ∃ q tags, v.2 = .inr (packetCtx fl a i pt t ζ g q, tags, betaSlice i pt β q) ∧ + (∀ y ∈ tags, y.2 < 2 ^ a) ∧ ((tags.filter (·.1)).map (·.2)).Nodup := 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 [nativeChild_eq hD _ (parentPacking hD a).packet (fun e => ((parentPacking hD a).slot e : ℕ)) + g fl a i pt t ζ β _ hgroups hpk1 hpk2] at hv + simp only [List.mem_ofFn] at hv + obtain ⟨c, rfl⟩ := hv + rcases hc : (childVertexEquiv (P := (parentPacking hD a).numPackets) + (packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩) g).symm c with w | q + · left + refine ⟨D.vertices[(w.1 : ℕ)], List.getElem_mem _, ?_⟩ + simp only [numberedDesc, Sum.elim_inl] + · right + simp only [numberedDesc, Sum.elim_inr] + refine ⟨q, _, rfl, ?_, ?_⟩ + · intro y hy + simp only [List.mem_map] at hy + obtain ⟨e, -, rfl⟩ := hy + exact Fin.isLt _ + · rw [List.filter_map, List.map_map] + refine List.Nodup.map_on ?_ ((nodup_packetPorts hD _ _ g q).filter _) + intro c₁ hc₁ c₂ hc₂ heq + simp only [List.mem_filter, Function.comp_apply] at hc₁ hc₂ + obtain ⟨hm₁, hl₁⟩ := hc₁ + obtain ⟨hm₂, hl₂⟩ := hc₂ + rw [mem_packetPorts] at hm₁ hm₂ + rcases c₁ with e₁ | e₁ + · rcases c₂ with e₂ | e₂ + · simp only [Function.comp_apply, Sum.elim_inl] at heq hm₁ hm₂ + have hinj := (parentPacking hD a).injective (a₁ := e₁.1) (a₂ := e₂.1) + (Prod.ext (hm₁.trans hm₂.symm) (Fin.ext heq)) + rw [Subtype.ext hinj] + · simp at hl₂ + · simp at hl₁ + end NativeChild end Cslib.Circuits.Frontier diff --git a/ComplexityTests/DescribedNetworkRows.lean b/ComplexityTests/DescribedNetworkRows.lean new file mode 100644 index 0000000000..8e0511f589 --- /dev/null +++ b/ComplexityTests/DescribedNetworkRows.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedLift + +/-! The row-count API works independently of the algorithm's vertex descriptors. +The edge hypothesis matters: an edgeless network can have a vacuous oversized row prefix. -/ + +namespace ComplexityTests.DescribedNetworkRows + +open Cslib.Circuits.Frontier + +private def edge : DescribedNetwork Unit := ⟨1, [([0], ()), ([0], ())]⟩ + +example : 1 ≤ edge.vertices.length := + DescribedNetwork.rows_le_of_isRowsFirstBipartite + (D := edge) (r := 1) (by decide) (by decide) + +example : (⟨0, []⟩ : DescribedNetwork Unit).IsRowsFirstBipartite 7 := by decide +example : ¬7 ≤ (⟨0, []⟩ : DescribedNetwork Unit).vertices.length := by decide + +end ComplexityTests.DescribedNetworkRows