feat(WordRAM): decide ExactTriangle with the fixed-prime native solver

Complexity.lean

@@ -1,6 +1,7 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
 public import Complexity.Algorithms.ExactTriangle.Defs
+public import Complexity.Algorithms.ExactTriangle.FailureAccounting
 public import Complexity.Algorithms.ExactTriangle.Hashing
 public import Complexity.Algorithms.ExactTriangle.Lopsided
 public import Complexity.Algorithms.ExactTriangle.PieceBounds
@@ -94,13 +95,28 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.Catalogue
 public import Complexity.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue
 public import Complexity.Algorithms.WordRAM.ExactTriangle.Chunks
 public import Complexity.Algorithms.WordRAM.ExactTriangle.Classes
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Accounting
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Controller
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Entry
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Flat
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Indexing
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Loop
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Potential
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Record
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.SourceBounds
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Step
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.TimeBound
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Width
 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.PreparationLocality
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationSpec
 public import Complexity.Algorithms.WordRAM.ExactTriangle.QueryScan
 public import Complexity.Algorithms.WordRAM.ExactTriangle.QuerySpec
@@ -127,6 +143,7 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Consume
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Entry
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Exec
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.FailureCount
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Failures
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Flat
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Header

Complexity/Algorithms/ExactTriangle/FailureAccounting.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2026 Anthropic, PBC, Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anthropic, PBC, Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.ExactTriangle.Witnesses
+public import Mathlib.Data.Nat.Count
+import Mathlib.Data.List.GetD
+
+/-!
+# One false-positive budget for distinct record/query occurrences
+
+Lists within distinct existing instances inject into the existing global `failedScans` set.
+Consequently their failed accepted occurrences share one `falsePositiveCount` bound. This
+finite bridge does not multiply that bound by the number of records. A native caller must
+derive list membership, nonrepetition and answers from its actual execution/readback.
+
+The counting argument adapts `Host.FailedScans.sum_fails_le` from
+`anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`, using the existing local
+finite instances and failed-scan API rather than a second host-data model.
+-/
+
+public section
+
+namespace Cslib.Algorithms.ExactTriangle
+
+/-- Failed accepted occurrences across distinct records inject into the single global
+failed-scan set. Lists may be partial chunks, but each occurrence list must be repetition-free. -/
+theorem sum_failed_occurrences_le {n D g p : ℕ}
+    (wAB wBC wAC : Fin n → Fin n → ℤ) (hp : p ≠ 0)
+    (ans : InstanceIndex p → Fin n × Fin n → Bool)
+    (hans : AnswersCorrect wAB wBC wAC D g p ans)
+    (I : Finset (InstanceIndex p)) (hI : I ⊆ instanceIndices wAB D g p)
+    (queries : InstanceIndex p → List (Fin n × Fin n)) (default : Fin n × Fin n)
+    (hnodup : ∀ idx ∈ I, (queries idx).Nodup)
+    (hquery : ∀ idx ∈ I, ∀ q ∈ queries idx, q ∈ (lopInstance wAB wBC wAC D g p idx).W) :
+    (∑ idx ∈ I, Nat.count (fun j => ans idx ((queries idx).getD j default) = true ∧
+      scanPiece wAB wBC wAC D g idx.2.2
+        ((queries idx).getD j default).1 ((queries idx).getD j default).2 = none)
+      (queries idx).length) ≤ falsePositiveCount wAB wBC wAC p := by
+  classical
+  let P := fun idx j => ans idx ((queries idx).getD j default) = true ∧
+    scanPiece wAB wBC wAC D g idx.2.2
+      ((queries idx).getD j default).1 ((queries idx).getD j default).2 = none
+  let occurrences : Finset (Σ _ : InstanceIndex p, ℕ) :=
+    I.sigma fun idx => (Finset.range (queries idx).length).filter (P idx)
+  let failures := failedScans wAB wBC wAC D g p ans
+  have mem_occurrence (z : Σ _ : InstanceIndex p, ℕ) (hz : z ∈ occurrences) :
+      z.1 ∈ I ∧ z.2 < (queries z.1).length ∧ P z.1 z.2 := by
+    simpa only [occurrences, Finset.mem_sigma, Finset.mem_filter, Finset.mem_range,
+      and_assoc] using hz
+  have get_eq (idx : InstanceIndex p) (j : ℕ) (hj : j < (queries idx).length) :
+      (queries idx).getD j default = (queries idx).get ⟨j, hj⟩ := by
+    rw [List.getD_eq_getElem _ _ hj, List.get_eq_getElem]
+  let f : {z // z ∈ occurrences} → {s // s ∈ failures} := fun z =>
+    ⟨(z.val.1, (queries z.val.1).getD z.val.2 default), by
+      obtain ⟨hidx, hj, hacc, hnone⟩ := mem_occurrence z.val z.prop
+      apply Finset.mem_filter.mpr
+      refine ⟨mem_acceptedPairs.mpr ⟨hI hidx, ?_, hacc⟩, hnone⟩
+      exact hquery _ hidx _ (get_eq _ _ hj ▸ List.get_mem _ _)⟩
+  have hf : Function.Injective f := by
+    rintro ⟨⟨idx, j⟩, hx⟩ ⟨⟨idx', j'⟩, hy⟩ hxy
+    have he : idx = idx' := congrArg (fun s => s.val.1) hxy
+    subst idx'
+    obtain ⟨hidx, hj, -⟩ := mem_occurrence ⟨idx, j⟩ hx
+    obtain ⟨-, hj', -⟩ := mem_occurrence ⟨idx, j'⟩ hy
+    have hpair := congrArg (fun s => s.val.2) hxy
+    change (queries idx).getD j default = (queries idx).getD j' default at hpair
+    rw [get_eq idx j hj, get_eq idx j' hj'] at hpair
+    have hpos := List.nodup_iff_injective_get.mp (hnodup idx hidx) hpair
+    exact Subtype.ext (Sigma.ext rfl (heq_of_eq (congrArg Fin.val hpos)))
+  have hcard : (∑ idx ∈ I, Nat.count (P idx) (queries idx).length) = occurrences.card := by
+    simp only [occurrences, Finset.card_sigma, Nat.count_eq_card_filter_range]
+  change (∑ idx ∈ I, Nat.count (P idx) (queries idx).length) ≤ _
+  rw [hcard]
+  calc
+    _ = Fintype.card {z // z ∈ occurrences} := (Fintype.card_coe _).symm
+    _ ≤ Fintype.card {s // s ∈ failures} := Fintype.card_le_of_injective f hf
+    _ = failures.card := Fintype.card_coe _
+    _ ≤ falsePositiveCount wAB wBC wAC p := card_failedScans_le hp hans
+
+end Cslib.Algorithms.ExactTriangle

Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime.lean

@@ -0,0 +1,38 @@
+/-
+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.FixedPrime.SourceBounds
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.TimeBound
+
+/-!
+# Complete native ExactTriangle decision at a fixed admitted prime
+
+`FixedPrime.runs_input` executes one concrete 416-register standard-native program from the
+original signed input, with actual preparation once, all computed catalogue records and
+original-weight witness verification. Its same-state prefix/halt verdict is equivalent to
+original `HasZeroTriangle`; a successful state retains the original coordinates.
+
+`FixedPrime.timeBound_le` derives all-instance queried-product charges and one global
+false-positive scan budget. Preparation costs at most `690n²Dg`, product charges at most
+`138412032(19m+1)n³g/D^(1/18)`, with explicit additional root/query/controller and original
+scan terms. The total actual scans satisfy `S ≤ F(p)+returnedFlag`: empty/failed records do
+not each receive a successful-scan allowance. The runtime order is the producer's actual
+chunk-major order, without a precomputed record list or a clean-workspace premise.
+
+All initialized results require `D=4^m≥16`, `n≥D^18`, `g≥1`, the stated prime window and the
+original signed magnitude bound. The original-input threshold is positive, logarithmic for
+polynomial weights and bounded scalar headers, and works at every wider physical width.
+`FixedPrime.bounded_reachable_original` derives polynomial words and zero support above an
+original-input envelope independent of that larger width. The code never reads word width,
+has at most 133152 flat slots including halt, and performs no whole-window clear or snapshot.
+
+Global parameter/prime selection, unrestricted small geometry and the complete aggregate
+source exponent remain separate. This component does not complete ordinary 3SUM 1.9992.
+The stage execution lemmas in the submodules are internal implementation interfaces.
+-/

Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Accounting.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2026 Anthropic, PBC, Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anthropic, PBC, Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.ExactTriangle.FailureAccounting
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Indexing
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Failures
+
+/-!
+# Global accounting for actual catalogue query blocks
+
+Each block is decoded from the real protected producer memory, in its original rank order.
+The mathematical products are those computed by the concrete native product; their answer
+correctness is proved, not assumed. Failed occurrences in distinct records therefore share
+one global false-positive budget. These value lemmas supply the native loop invariant.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Existing original-weight witness condition restricted to one existing chunk and piece. -/
+@[expose] def recordHit {m n g p : ℕ} (values : ℕ → ℤ) (idx : InstanceIndex p) : Prop :=
+  ∃ q ∈ chunkOf (fun u v : Fin n => values (pairIndex (u, v))) (D m) p idx.1 idx.2.1,
+    ∃ c ∈ piece n (D m) g idx.2.2,
+      weightSum (fun u v : Fin n => values (pairIndex (u, v)))
+        (fun b c => values (n * n + pairIndex (b, c)))
+        (fun u c => values (2 * (n * n) + pairIndex (u, c))) q.1 q.2 c = 0
+
+/-- Real per-record product, root, query and controller charges, excluding interval scans.
+The constant includes the outer loop's two control instructions. -/
+@[expose] noncomputable def recordBase {m n p : ℕ} (hn : 0 < n)
+    (values : ℕ → ℤ) (mem : ℕ → ℕ) (idx : InstanceIndex p) : ℕ :=
+  let Q := RecordProduct.recordQueryCount n (D m) p values idx
+  let qs := RecordProduct.decodedQueries hn mem (RecordProduct.recordQueries n (D m) p idx) Q
+  RecordProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q + 61
+
+/-- Number of accepted queries without an original witness in one actual producer block.
+This is a value specification for charged native scans, not an executable scan oracle. -/
+@[expose] noncomputable def recordFailures {m n g p : ℕ} (hn : 0 < n)
+    (values : ℕ → ℤ) (mem : ℕ → ℕ) (idx : InstanceIndex p) : ℕ :=
+  let qs := RecordProduct.decodedQueries hn mem (RecordProduct.recordQueries n (D m) p idx)
+    (RecordProduct.recordQueryCount n (D m) p values idx)
+  let default : Fin n × Fin n := (⟨0, hn⟩, ⟨0, hn⟩)
+  Nat.count (fun i =>
+    (RecordProduct.leftMatrix m n g p values idx * RecordProduct.rightMatrix m n g p values idx)
+        (qs.getD i default).1 (qs.getD i default).2 ≠ 0 ∧
+      scanPiece (fun a b => values (pairIndex (a, b)))
+        (fun b c => values (n * n + pairIndex (b, c)))
+        (fun a c => values (2 * (n * n) + pairIndex (a, c))) (D m) g idx.2.2
+        (qs.getD i default).1 (qs.getD i default).2 = none) qs.length
+
+/-- Every original query occurs at most once in each actual chunk. -/
+theorem actual_queries_chunk {m n g p : ℕ} (hn : 0 < n) (values : ℕ → ℤ)
+    {initial a : Data 64} (h : Instances.Output n (D m) g p values initial a)
+    (hD : 16 ≤ D m) (hDn : D m ≤ n) (hp : p ≠ 0) (idx : InstanceIndex p)
+    (hidx : idx ∈ instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) (D m) g p) :
+    let qs := RecordProduct.decodedQueries hn a.mem (RecordProduct.recordQueries n (D m) p idx)
+      (RecordProduct.recordQueryCount n (D m) p values idx)
+    qs.Nodup ∧ qs.toFinset = chunkOf
+      (fun u v : Fin n => values (pairIndex (u, v))) (D m) p idx.1 idx.2.1 := by
+  let wAB := fun u v : Fin n => values (pairIndex (u, v))
+  have hc := QuerySpec.card_residueClass wAB hp
+    (fun q => (values q % (p : ℤ)).toNat) (by intro pair; rfl) idx.1
+  obtain ⟨-, hnodup, hset⟩ := RecordProduct.decodedQueries_chunkOf values wAB hn hp
+    (by intro u v; rfl) (by omega) hDn h idx.1 idx.2.1
+    ((mem_instanceIndices wAB idx).mp hidx).1
+  rw [hc] at hnodup hset
+  exact ⟨hnodup, hset⟩
+
+/-- Add distinct actual records before applying the global bound; no per-record false-positive
+allowance is duplicated. The real product's detection theorem supplies answer correctness. -/
+theorem sum_recordFailures_le {m n g p : ℕ} (hn : 0 < n) (values : ℕ → ℤ)
+    {initial a : Data 64} (h : Instances.Output n (D m) g p values initial a)
+    (hD : 16 ≤ D m) (hDn : D m ≤ n) (hg : 1 ≤ g)
+    (hp : p ∈ Nat.sqrtPrimeWindow (D m))
+    (I : Finset (InstanceIndex p))
+    (hI : I ⊆ instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) (D m) g p) :
+    (∑ idx ∈ I, recordFailures (m := m) (g := g) hn values a.mem idx) ≤
+      falsePositiveCount (fun u v : Fin n => values (pairIndex (u, v)))
+        (fun b c => values (n * n + pairIndex (b, c)))
+        (fun u c => values (2 * (n * n) + pairIndex (u, c))) p := by
+  classical
+  let wAB := fun u v : Fin n => values (pairIndex (u, v))
+  let wBC := fun b c : Fin n => values (n * n + pairIndex (b, c))
+  let wAC := fun u c : Fin n => values (2 * (n * n) + pairIndex (u, c))
+  let queries := fun idx => RecordProduct.decodedQueries hn a.mem
+    (RecordProduct.recordQueries n (D m) p idx)
+    (RecordProduct.recordQueryCount n (D m) p values idx)
+  let ans := fun (idx : InstanceIndex p) (q : Fin n × Fin n) => decide
+    ((RecordProduct.leftMatrix m n g p values idx *
+      RecordProduct.rightMatrix m n g p values idx) q.1 q.2 ≠ 0)
+  have hp0 := (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.ne_zero
+  have hans : AnswersCorrect wAB wBC wAC (D m) g p ans :=
+    RecordProduct.product_answers_correct values wAB wBC wAC hD hg hp
+      (by intro b c; rfl) (by intro u c; rfl)
+  have hquery (idx) (hi : idx ∈ I) :=
+    actual_queries_chunk hn values h hD hDn hp0 idx (hI hi)
+  have hbound := sum_failed_occurrences_le wAB wBC wAC hp0 ans hans I hI queries
+    (⟨0, hn⟩, ⟨0, hn⟩) (fun idx hi => (hquery idx hi).1) (by
+      intro idx hi q hq
+      change q ∈ chunkOf wAB (D m) p idx.1 idx.2.1
+      rw [← (hquery idx hi).2, List.mem_toFinset]
+      exact hq)
+  simpa only [recordFailures, queries, ans, decide_eq_true_eq] using hbound
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime