feat(ExactTriangle): connect prepared matrices to finite adjacency

Complexity.lean

@@ -88,6 +88,7 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.InstancePair
 public import Complexity.Algorithms.WordRAM.ExactTriangle.Instances
 public import Complexity.Algorithms.WordRAM.ExactTriangle.MatrixSpec
 public import Complexity.Algorithms.WordRAM.ExactTriangle.Parameters
+public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationAdjacency
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationBounds
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationInput
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationSpec

Complexity/Algorithms/WordRAM/ExactTriangle/PreparationAdjacency.lean

@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationSpec
+
+/-!
+# Adjacency in prepared native ExactTriangle matrices
+
+These consumer lemmas connect actual prepared memory to the existing finite lopsided graph.
+The source prime window supplies the padding bound, and piece membership supplies each local
+coordinate. Neither is an additional layout certificate for the program.
+
+## Main results
+
+* `PreparationSpec.instance_adjacency`: actual stored cells give the finite adjacency relations
+  and zero padding, with piece coordinates and middle-width admissibility derived.
+
+## References
+
+The adjacency relations are those of the pinned
+[Theorem 17 matrix construction](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean).
+The composition with native memory readback is original.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.PreparationSpec
+
+open Cslib.WordRAM Cslib.Algorithms.ExactTriangle Cslib.Matrix
+
+private theorem prepared_middle_fits {D g p n k : ℕ} (hg : 1 ≤ g)
+    (hp : p ∈ Nat.sqrtPrimeWindow D) :
+    min (pieceSize D g) (n - k * pieceSize D g) * p ≤ D := by
+  have hpS : p ≤ sOf D := Nat.le_sqrt'.mpr (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).2.2.le
+  have hlen : min (pieceSize D g) (n - k * pieceSize D g) ≤ sOf D :=
+    (min_le_left _ _).trans (pieceSize_le_sOf hg)
+  exact (Nat.mul_le_mul hlen hpS).trans (Nat.sqrt_le D)
+
+private theorem piece_coordinate {n D g k : ℕ} (hD : 16 ≤ D) (hg : 1 ≤ g)
+    (c : Fin n) (hc : c ∈ piece n D g k) :
+    k * pieceSize D g + c.val % pieceSize D g = c.val ∧
+      c.val % pieceSize D g < min (pieceSize D g) (n - k * pieceSize D g) := by
+  have hB := pieceSize_pos hD hg
+  have hdiv := (mem_piece c).mp hc
+  have hsplit := Nat.div_add_mod c.val (pieceSize D g)
+  rw [hdiv, Nat.mul_comm] at hsplit
+  have hmod := Nat.mod_lt c.val hB
+  exact ⟨hsplit, lt_min hmod (by have := c.isLt; omega)⟩
+
+/-- The actual prepared matrix cells express the existing finite graph's adjacency, and the
+unused middle positions are zero. The prime-window and piece hypotheses discharge every
+padding and local-coordinate premise of the matrix-entry API. -/
+theorem instance_adjacency {n D g p : ℕ} (values : ℕ → ℤ)
+    (wAB wBC wAC : Fin n → Fin n → ℤ)
+    (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow D)
+    (hAB : ∀ a b, values (pairIndex (a, b)) = wAB a b)
+    (hBC : ∀ b c, values (n * n + pairIndex (b, c)) = wBC b c)
+    (hAC : ∀ a c, values (2 * (n * n) + pairIndex (a, c)) = wAC a c)
+    {initial y : Data 64} (h : Instances.Output n D g p values initial y)
+    (idx : InstanceIndex p) (hidx : idx ∈ instanceIndices wAB D g p) :
+    let N := n * n
+    let C := fun rho => Nat.count (fun q => (values q % (p : ℤ)).toNat = rho) N
+    let H := numPieces n D g
+    let B := pieceSize D g
+    let ord := ChunkCatalogue.before C (queryCap n D) idx.1.val + idx.2.1
+    let base := y.regs Instances.output +
+      (ord * H + idx.2.2) * (6 + 2 * (n * D))
+    let G := lopInstance wAB wBC wAC D g p idx
+    (∀ (a b c : Fin n) (hc : c ∈ piece n D g idx.2.2) (label : Fin p),
+      let middle := c.val % B * p + label.val
+      (y.mem (base + 6 + (a.val * D + middle)) = 1 ↔
+        G.adjA a (⟨c, hc⟩, label)) ∧
+      (y.mem (base + 6 + n * D + (middle * n + b.val)) = 1 ↔
+        G.adjB (⟨c, hc⟩, label) b)) ∧
+    (∀ (a b : Fin n) (middle : Fin D),
+      min B (n - idx.2.2 * B) ≤ middle.val / p →
+        y.mem (base + 6 + (a.val * D + middle.val)) = 0 ∧
+        y.mem (base + 6 + n * D + (middle.val * n + b.val)) = 0) := by
+  let N := n * n
+  let R := fun q => (values q % (p : ℤ)).toNat
+  let C := fun rho => Nat.count (fun q => R q = rho) N
+  let H := numPieces n D g
+  let B := pieceSize D g
+  let K := ChunkCatalogue.before C (queryCap n D) p
+  let ord := ChunkCatalogue.before C (queryCap n D) idx.1.val + idx.2.1
+  let base := 5 + 6 * N + p + 2 * N * p + 3 * K +
+    (ord * H + idx.2.2) * (6 + 2 * (n * D))
+  let A : WriteMatrices.Args :=
+    ⟨5 + 5 * N, base + 6, n, D, p, idx.2.2 * B, min B (n - idx.2.2 * B), idx.1.val⟩
+  let A' := { A with src := 5 + 4 * N, dst := base + 6 + n * D }
+  have hp0 : p ≠ 0 := (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.ne_zero
+  obtain ⟨-, hL, hR⟩ := instance_readback values wAB hp0 hAB hD hDn hg h idx hidx
+  change (Block.mk A.dst (n * D)).Realizes y.mem
+    (fun j => WriteMatrices.entry false A (fun q => R (2 * N + q)) j) at hL
+  change (Block.mk A'.dst (n * D)).Realizes y.mem
+    (fun j => WriteMatrices.entry true A' (fun q => R (N + q)) j) at hR
+  have hpad : A.length * A.p ≤ A.D := prepared_middle_fits hg hp
+  change min B (n - idx.2.2 * B) * p ≤ D at hpad
+  have hloadL (a c : Fin n) :
+      R (2 * N + (a.val * n + c.val)) = (wAC a c).natMod p := by
+    change (values (2 * (n * n) + pairIndex (a, c)) % (p : ℤ)).toNat = _
+    rw [hAC]
+    rfl
+  have hloadR (b c : Fin n) :
+      R (N + (b.val * n + c.val)) = (wBC b c).natMod p := by
+    change (values (n * n + pairIndex (b, c)) % (p : ℤ)).toNat = _
+    rw [hBC]
+    rfl
+  have hout : y.regs Instances.output = 5 + 6 * N + p + 2 * N * p + 3 * K := h.2.2.2.1
+  dsimp only
+  rw [hout]
+  constructor
+  · intro a b c hc label
+    obtain ⟨hvertex, hv⟩ := piece_coordinate hD hg c hc
+    let v : Fin A.length := ⟨c.val % B, hv⟩
+    have hm : v.val * p + label.val < D := by
+      have hstep := Nat.mul_le_mul_right p v.isLt
+      have hl := label.isLt
+      change (v.val + 1) * p ≤ min B (n - idx.2.2 * B) * p at hstep
+      rw [Nat.add_mul, Nat.one_mul] at hstep
+      omega
+    have hli : a.val * D + (v.val * p + label.val) < n * D := by
+      have hi := Nat.mul_le_mul_right D a.isLt
+      rw [Nat.succ_mul] at hi
+      omega
+    have hri : (v.val * p + label.val) * n + b.val < n * D := by
+      have hi := Nat.mul_le_mul_right n (Nat.succ_le_of_lt hm)
+      rw [Nat.succ_mul] at hi
+      have hb := b.isLt
+      rw [Nat.mul_comm n D]
+      omega
+    have hleft := hL ⟨a.val * D + (v.val * p + label.val), hli⟩
+    have hright := hR ⟨(v.val * p + label.val) * n + b.val, hri⟩
+    change y.mem (A.dst + (a.val * D + (v.val * p + label.val))) = _ at hleft
+    change y.mem (A'.dst + ((v.val * p + label.val) * n + b.val)) = _ at hright
+    constructor
+    · rw [hleft]
+      exact MatrixSpec.left_lopInstance A (fun q => R (2 * N + q)) wAB wBC wAC
+        g idx.2.1 idx.2.2 idx.1 rfl a c v label hc hvertex hpad hloadL
+    · rw [hright]
+      exact MatrixSpec.right_lopInstance A' (fun q => R (N + q)) wAB wBC wAC
+        g idx.2.1 idx.2.2 idx.1 b c v label hc hvertex hloadR
+  · intro a b middle hmiddle
+    have hli : a.val * D + middle.val < n * D := by
+      have hi := Nat.mul_le_mul_right D a.isLt
+      rw [Nat.succ_mul] at hi
+      have hm := middle.isLt
+      omega
+    have hri : middle.val * n + b.val < n * D := by
+      have hi := Nat.mul_le_mul_right n (Nat.succ_le_of_lt middle.isLt)
+      rw [Nat.succ_mul] at hi
+      have hb := b.isLt
+      rw [Nat.mul_comm n D]
+      omega
+    have hleft := hL ⟨a.val * D + middle.val, hli⟩
+    have hright := hR ⟨middle.val * n + b.val, hri⟩
+    change y.mem (A.dst + (a.val * D + middle.val)) = _ at hleft
+    change y.mem (A'.dst + (middle.val * n + b.val)) = _ at hright
+    constructor
+    · rw [hleft]
+      exact MatrixSpec.left_padding A (fun q => R (2 * N + q)) a middle hmiddle
+    · rw [hright]
+      exact MatrixSpec.right_padding A' (fun q => R (N + q)) b middle hmiddle
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.PreparationSpec

Complexity/Algorithms/WordRAM/ExactTriangle/PreparationSpec.lean

@@ -18,6 +18,9 @@ The native catalogue enumerates the existing residue classes, chunks and pieces.
 identify its actual output count and per-instance records with that finite construction. Matrix
 meaning and padding reuse `MatrixSpec` and its existing writer-entry formulas.
 
+The [consumer extension](Complexity/Algorithms/WordRAM/ExactTriangle/PreparationAdjacency.html)
+connects these cells to finite adjacency, deriving piece coordinates and the padding bound.
+
 ## Main results
 
 * `PreparationSpec.count_eq_card`: the actual output counter is the finite instance cardinality.

ComplexityTests/WordRAMExactTriangleAdjacency.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationAdjacency
+import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationBounds
+import Complexity.Foundations.Data.List.Lookup
+
+/-! # Native prepared adjacency with signed asymmetric input -/
+
+namespace ComplexityTests.WordRAMExactTriangleAdjacency
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.WordRAM.ExactTriangle
+
+private def weightAt (i : Fin 768) : ℤ :=
+  if i.val = 273 then 1 else if i.val = 513 then -1 else 0
+
+private def values : List ℤ := List.ofFn weightAt
+
+private def wAB (a b : Fin 16) : ℤ := values.getD (pairIndex (a, b)) 0
+private def wBC (b c : Fin 16) : ℤ := values.getD (256 + pairIndex (b, c)) 0
+private def wAC (a c : Fin 16) : ℤ := values.getD (512 + pairIndex (a, c)) 0
+
+private theorem values_bound : ∀ z ∈ values, z.natAbs ≤ 1 := by
+  intro z hz
+  obtain ⟨i, rfl⟩ := List.mem_ofFn.mp hz
+  dsimp only [weightAt]
+  split_ifs <;> decide
+
+private theorem values_get_zero {i : ℕ} (hi : i < 256) : values.getD i 0 = 0 := by
+  rw [values, List.getD_ofFn_of_lt weightAt (by omega)]
+  simp only [weightAt, show i ≠ 273 by omega, show i ≠ 513 by omega, ↓reduceIte]
+
+private theorem wAB_zero (a b : Fin 16) : wAB a b = 0 := by
+  apply values_get_zero
+  change a.val * 16 + b.val < 256
+  have ha := a.isLt
+  have hb := b.isLt
+  omega
+
+private theorem piece_size : pieceSize 16 1 = 4 := by
+  have hs : sOf 16 = 4 := by
+    change Nat.sqrt 16 = 4
+    have hl : 4 ≤ Nat.sqrt 16 := Nat.le_sqrt.mpr (by decide)
+    have hu : Nat.sqrt 16 < 5 := Nat.sqrt_lt.mpr (by decide)
+    omega
+  simp only [pieceSize, hs, ceilDiv_one]
+
+private theorem query_capacity : queryCap 16 16 = 64 := by
+  have hl : 64 ≤ Nat.sqrt 4096 := Nat.le_sqrt.mpr (by decide)
+  have hu : Nat.sqrt 4096 < 65 := Nat.sqrt_lt.mpr (by decide)
+  have hs : Nat.sqrt 4096 = 64 := by omega
+  simpa only [queryCap, Nat.reducePow, Nat.reduceDiv] using hs
+
+private theorem first_index : (0, 0, 0) ∈ instanceIndices wAB 16 1 3 := by
+  rw [mem_instanceIndices]
+  have hclass : (residueClass wAB 3 0).card = 256 := by
+    have hset : residueClass wAB 3 0 = Finset.univ := by
+      ext q
+      simp only [residueClass, Finset.mem_filter, Finset.mem_univ, true_and, wAB_zero]
+      decide
+    rw [hset]
+    simp only [Finset.card_univ, Fintype.card_prod, Fintype.card_fin, Nat.reduceMul]
+  constructor
+  · simp only [numChunks, hclass, query_capacity]
+    norm_num [Nat.ceilDiv_eq_add_pred_div]
+  · norm_num [numPieces, piece_size, Nat.ceilDiv_eq_add_pred_div]
+
+set_option maxRecDepth 4096 in
+-- The actual initialized 768-weight memory witness exceeds the default expression depth.
+/-- Signed asymmetric input gives two actual adjacent cells and two padded zeros in the
+same initialized run. The client supplies neither a run nor a padding/coordinate premise. -/
+example : ∃ y t, t ≤ 2826240 ∧
+    Runs (PreparationInput.width 16 16 1 3 1) PreparationInput.flatProgram
+      (State.init (PreparationInput.input 16 16 1 3 values))
+      ⟨Instances.program.size, y⟩ (t - 1) ∧
+    Executes (PreparationInput.width 16 16 1 3 1) PreparationInput.flatProgram
+      (State.init (PreparationInput.input 16 16 1 3 values))
+      (y.regs Instances.output) t ∧
+    y.mem (y.regs Instances.output + 11) = 1 ∧
+    y.mem (y.regs Instances.output + 343) = 1 ∧
+    y.mem (y.regs Instances.output + 18) = 0 ∧
+    y.mem (y.regs Instances.output + 455) = 0 := by
+  have hp : 3 ∈ Nat.sqrtPrimeWindow 16 :=
+    Nat.mem_sqrtPrimeWindow_iff_sq.mpr ⟨by decide, by decide, by decide⟩
+  obtain ⟨y, t, ht, hr, he, hout, -, -⟩ := PreparationBounds.runs_input
+    (n := 16) (D := 16) (g := 1) (p := 3) (A := 1) values
+    (by simp only [values, List.length_ofFn])
+    (by decide) (by decide) (by decide) hp values_bound le_rfl
+  obtain ⟨hactive, hzero⟩ := PreparationSpec.instance_adjacency
+    (fun q => values.getD q 0) wAB wBC wAC
+    (by decide) (by decide) (by decide) hp
+    (by intro a b; rfl) (by intro b c; rfl) (by intro a c; rfl)
+    hout (0, 0, 0) first_index
+  have hc : (1 : Fin 16) ∈ piece 16 16 1 0 := by
+    rw [mem_piece, piece_size]
+    decide
+  have hAC : wAC 0 1 = -1 := by
+    change values.getD 513 0 = -1
+    rw [values, List.getD_ofFn_of_lt weightAt (by decide)]
+    rfl
+  have hBC : wBC 1 1 = 1 := by
+    change values.getD 273 0 = 1
+    rw [values, List.getD_ofFn_of_lt weightAt (by decide)]
+    rfl
+  have ha := hactive 0 1 1 hc 2
+  norm_num [ChunkCatalogue.before, piece_size] at ha
+  have hz := hzero 0 1 12 (by rw [piece_size]; decide)
+  norm_num [ChunkCatalogue.before] at hz
+  refine ⟨y, t, ht, hr, he, ha.1.mpr ?_, ha.2.mpr ?_, hz.1, hz.2⟩
+  · change (2 : ℤ) ≡ wAC 0 1 + 0 [ZMOD (3 : ℤ)]
+    rw [hAC]
+    decide
+  · change (2 : ℤ) ≡ -wBC 1 1 [ZMOD (3 : ℤ)]
+    rw [hBC]
+    decide
+
+end ComplexityTests.WordRAMExactTriangleAdjacency