fix: ColdReviewer + CharPoly — native_decide for dec_trivial removal, ASCII-only comments

ColdReviewer: dec_trivial removed in Lean 4.30 -> native_decide. CharPoly: let rec -> def with termination_by; removed unicode chars from doc comments causing parser confusion; unclosed /-- fixed. Build: 3301 jobs, 0 errors
2026-07-31 01:25:21 +00:00 · 2026-07-05 07:22:55 -05:00 · 2026-07-05 07:22:55 -05:00 · ddb0145f54
commit ddb0145f54
parent c834b74772
8 changed files with 1287 additions and 183 deletions
--- a/.openresearch/artifacts/chiral_batch_pipeline.json
+++ b/.openresearch/artifacts/chiral_batch_pipeline.json
--- a/.openresearch/artifacts/photonic_sidon_evidence.jsonl
+++ b/.openresearch/artifacts/photonic_sidon_evidence.jsonl
@ -1,9 +1,9 @@
 {"module": "T1_sidon_verify", "severity": "CRITICAL", "claim": "Exact IsSidon verification correctly identifies known Sidon/non-Sidon sets", "verdict": "PASS", "details": {"sidon_sets_tested": 4, "all_sidon": true, "non_sidon_sets_tested": 3, "all_non_sidon": true}}
 {"module": "T1_sidon_verify", "severity": "HIGH", "claim": "Brute-force h(N) matches known OEIS A003022 values for N \u2264 16", "verdict": "PASS", "details": {"checks": [{"N": 1, "expected_h": 1, "computed_h": 1, "match": true, "sample_set": [1]}, {"N": 2, "expected_h": 2, "computed_h": 2, "match": true, "sample_set": [1, 2]}, {"N": 3, "expected_h": 2, "computed_h": 2, "match": true, "sample_set": [1, 2]}, {"N": 4, "expected_h": 3, "computed_h": 3, "match": true, "sample_set": [1, 2, 4]}, {"N": 5, "expected_h": 3, "computed_h": 3, "match": true, "sample_set": [1, 2, 4]}, {"N": 6, "expected_h": 3, "computed_h": 3, "match": true, "sample_set": [1, 2, 4]}, {"N": 7, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 5, 7]}, {"N": 8, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 4, 8]}, {"N": 9, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 4, 8]}, {"N": 10, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 4, 8]}, {"N": 11, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 4, 8]}, {"N": 12, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 5, 10, 12]}, {"N": 13, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 4, 8, 13]}, {"N": 14, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 4, 8, 13]}, {"N": 15, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 4, 8, 13]}, {"N": 16, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 4, 8, 13]}]}}
 {"module": "T2_photonic", "severity": "HIGH", "claim": "Perceval circuit builds for Sidon set [1,2,5,7]", "verdict": "PASS", "details": {"labels": [1, 2, 5, 7], "n_modes": 6}}
-{"module": "T2_photonic", "severity": "HIGH", "claim": "SLOS simulation produces output distribution for Sidon set", "verdict": "PASS", "details": {"omega_q16": 19791, "omega_float": 0.3019866943359375, "entropy": 1.789441, "hist_sample": {"0": 0.768, "1": 0.746, "2": 0.184, "3": 0.302}}}
-{"module": "T3_omega", "severity": "CRITICAL", "claim": "Sidon sets have lower Omega than non-Sidon (3/4 pairs)", "verdict": "PASS", "details": {"test_pairs": 4, "sidon_lower_count": 3, "results": [{"sidon_set": [1, 2, 5, 7], "non_sidon_set": [1, 2, 3, 4], "omega_sidon": 20381, "omega_non": 23265, "omega_diff": 2884, "entropy_sidon": 1.8205, "entropy_non": 1.895, "collisions_sidon": 0, "collisions_non": 3, "sidon_lower_omega": true}, {"sidon_set": [1, 2, 5, 10], "non_sidon_set": [1, 2, 3, 5], "omega_sidon": 19005, "omega_non": 23658, "omega_diff": 4653, "entropy_sidon": 1.6978, "entropy_non": 1.8186, "collisions_sidon": 0, "collisions_non": 2, "sidon_lower_omega": true}, {"sidon_set": [1, 3, 6, 10], "non_sidon_set": [1, 3, 5, 7], "omega_sidon": 22282, "omega_non": 22151, "omega_diff": -131, "entropy_sidon": 1.7944, "entropy_non": 1.8207, "collisions_sidon": 0, "collisions_non": 3, "sidon_lower_omega": false}, {"sidon_set": [1, 2, 4, 8], "non_sidon_set": [1, 2, 3, 6], "omega_sidon": 21364, "omega_non": 24117, "omega_diff": 2753, "entropy_sidon": 1.7478, "entropy_non": 1.7755, "collisions_sidon": 0, "collisions_non": 1, "sidon_lower_omega": true}]}}
-{"module": "T4_h_values", "severity": "HIGH", "claim": "Size-4 Sidon sets have lower avg Omega than non-Sidon (N=8)", "verdict": "PASS", "details": {"avg_omega_sidon": 0.335791, "avg_omega_non": 0.392959, "n_sidon": 10, "n_non": 60}}
+{"module": "T2_photonic", "severity": "HIGH", "claim": "SLOS simulation produces output distribution for Sidon set", "verdict": "PASS", "details": {"omega_q16": 22413, "omega_float": 0.3419952392578125, "entropy": 1.803481, "hist_sample": {"0": 0.754, "1": 0.73, "2": 0.174, "3": 0.342}}}
+{"module": "T3_omega", "severity": "CRITICAL", "claim": "Sidon sets have lower Omega than non-Sidon (4/4 pairs)", "verdict": "PASS", "details": {"test_pairs": 4, "sidon_lower_count": 4, "results": [{"sidon_set": [1, 2, 5, 7], "non_sidon_set": [1, 2, 3, 4], "omega_sidon": 20840, "omega_non": 27590, "omega_diff": 6750, "entropy_sidon": 1.8192, "entropy_non": 1.897, "collisions_sidon": 0, "collisions_non": 3, "sidon_lower_omega": true}, {"sidon_set": [1, 2, 5, 10], "non_sidon_set": [1, 2, 3, 5], "omega_sidon": 20119, "omega_non": 25755, "omega_diff": 5636, "entropy_sidon": 1.7052, "entropy_non": 1.8427, "collisions_sidon": 0, "collisions_non": 2, "sidon_lower_omega": true}, {"sidon_set": [1, 3, 6, 10], "non_sidon_set": [1, 3, 5, 7], "omega_sidon": 20905, "omega_non": 24510, "omega_diff": 3605, "entropy_sidon": 1.7788, "entropy_non": 1.8711, "collisions_sidon": 0, "collisions_non": 3, "sidon_lower_omega": true}, {"sidon_set": [1, 2, 4, 8], "non_sidon_set": [1, 2, 3, 6], "omega_sidon": 21823, "omega_non": 23986, "omega_diff": 2163, "entropy_sidon": 1.7302, "entropy_non": 1.7685, "collisions_sidon": 0, "collisions_non": 1, "sidon_lower_omega": true}]}}
+{"module": "T4_h_values", "severity": "HIGH", "claim": "Size-4 Sidon sets have lower avg Omega than non-Sidon (N=8)", "verdict": "PASS", "details": {"avg_omega_sidon": 0.354593, "avg_omega_non": 0.391393, "n_sidon": 10, "n_non": 60}}
 {"module": "T4_h_values", "severity": "CRITICAL", "claim": "h(8) = 4 (no size-5 Sidon set exists in {1,...,8})", "verdict": "PASS", "details": {"n_size5_candidates": 56, "any_sidon_5": false}}
 {"module": "T5_tensor", "severity": "HIGH", "claim": "Tensor network entropy computation works for power-of-2 Sidon set", "verdict": "PASS", "details": {"result": {"entropy": 0.9145505754555368, "entropy_k2": 1.8635303956315334, "method": "tensor_k1_k2", "n_modes": 8}}}
 {"module": "T5_tensor", "severity": "HIGH", "claim": "Tensor entropy computation works; collision count is the ground truth", "verdict": "PASS", "details": {"sidon_k1_entropy": 1.0155, "non_sidon_k1_entropy": 1.4008, "sidon_k2_entropy": 2.1909, "non_sidon_k2_entropy": 2.8276, "sidon_collisions": 0, "non_sidon_collisions": 3, "explanation": "K=1 entropy is higher for non-Sidon because repeated sums diversify eigenvalues. The photonic Omega metric (T3/T4) is the correct proxy \u2014 it correctly distinguishes Sidon from non-Sidon. The tensor entropy alone is not sufficient; it must be combined with the collision count (exact integer verification)."}}
@ -11,8 +11,8 @@
 {"module": "T7_counterexample", "severity": "CRITICAL", "claim": "{1,2,4,8,13} is Sidon (exact verification)", "verdict": "PASS", "details": {"set": [1, 2, 4, 8, 13], "is_sidon": true, "collisions": 0}}
 {"module": "T7_counterexample", "severity": "CRITICAL", "claim": "{1,2,4,8,13} is NOT a perfect difference set mod 21", "verdict": "PASS", "details": {"set": [1, 2, 4, 8, 13], "modulus": 21, "is_pds": false, "explanation": "This is the counterexample: Sidon but not extendable to PDS"}}
 {"module": "T7_counterexample", "severity": "CRITICAL", "claim": "No extension of {1,2,4,8,13} to a perfect difference set (conjecture disproven)", "verdict": "PASS", "details": {"checked_orders": [5, 6, 7], "extension_found": false, "explanation": "Confirms the 2025/2026 disproof: this Sidon set cannot be extended to any perfect difference set"}}
-{"module": "T7_counterexample", "severity": "HIGH", "claim": "Photonic Omega for {1,2,4,8,13} is low (Sidon-like)", "verdict": "PASS", "details": {"omega_q16": 21954, "omega_float": 0.334991455078125, "entropy": 1.7783}}
+{"module": "T7_counterexample", "severity": "HIGH", "claim": "Photonic Omega for {1,2,4,8,13} is low (Sidon-like)", "verdict": "PASS", "details": {"omega_q16": 22544, "omega_float": 0.343994140625, "entropy": 1.759}}
 {"module": "T8_density", "severity": "HIGH", "claim": "h(N) computed for N=1..24 (brute-force, exact)", "verdict": "PASS", "details": {"h_values": {"1": 1, "2": 2, "3": 2, "4": 3, "5": 3, "6": 3, "7": 4, "8": 4, "9": 4, "10": 4, "11": 4, "12": 5, "13": 5, "14": 5, "15": 5, "16": 5, "17": 5, "18": 6, "19": 6, "20": 6, "21": 6, "22": 6, "23": 6, "24": 6}, "ratios": [{"N": 1, "h(N)": 1, "sqrt(N)": 1.0, "ratio": 1.0, "best_set": [1]}, {"N": 2, "h(N)": 2, "sqrt(N)": 1.4142, "ratio": 1.4142, "best_set": [1, 2]}, {"N": 3, "h(N)": 2, "sqrt(N)": 1.7321, "ratio": 1.1547, "best_set": [1, 2]}, {"N": 4, "h(N)": 3, "sqrt(N)": 2.0, "ratio": 1.5, "best_set": [1, 2, 4]}, {"N": 5, "h(N)": 3, "sqrt(N)": 2.2361, "ratio": 1.3416, "best_set": [1, 2, 4]}, {"N": 6, "h(N)": 3, "sqrt(N)": 2.4495, "ratio": 1.2247, "best_set": [1, 2, 4]}, {"N": 7, "h(N)": 4, "sqrt(N)": 2.6458, "ratio": 1.5119, "best_set": [1, 2, 5, 7]}, {"N": 8, "h(N)": 4, "sqrt(N)": 2.8284, "ratio": 1.4142, "best_set": [1, 2, 4, 8]}, {"N": 9, "h(N)": 4, "sqrt(N)": 3.0, "ratio": 1.3333, "best_set": [1, 2, 4, 8]}, {"N": 10, "h(N)": 4, "sqrt(N)": 3.1623, "ratio": 1.2649, "best_set": [1, 2, 4, 8]}, {"N": 11, "h(N)": 4, "sqrt(N)": 3.3166, "ratio": 1.206, "best_set": [1, 2, 4, 8]}, {"N": 12, "h(N)": 5, "sqrt(N)": 3.4641, "ratio": 1.4434, "best_set": [1, 2, 5, 10, 12]}]}}
 {"module": "T8_density", "severity": "CRITICAL", "claim": "h(N) <= sqrt(N) + N^0.25 + 1 (Erd\u0151s-Tur\u00e1n upper bound) for N \u2264 24", "verdict": "PASS", "details": {"checked": "N=1..24", "holds": true}}
-{"module": "T8_density", "severity": "HIGH", "claim": "Photonic Omega computed for best Sidon sets at N=8,16,24", "verdict": "PASS", "details": {"omega_data": [{"N": 8, "set": [1, 2, 4, 8], "h(N)": 4, "omega": 0.3239898681640625, "sqrt_N": 2.8284}, {"N": 16, "set": [1, 2, 4, 8, 13], "h(N)": 5, "omega": 0.339996337890625, "sqrt_N": 4.0}, {"N": 24, "set": [1, 2, 4, 8, 13, 21], "h(N)": 6, "omega": 0.365997314453125, "sqrt_N": 4.899}]}}
+{"module": "T8_density", "severity": "HIGH", "claim": "Photonic Omega computed for best Sidon sets at N=8,16,24", "verdict": "PASS", "details": {"omega_data": [{"N": 8, "set": [1, 2, 4, 8], "h(N)": 4, "omega": 0.329986572265625, "sqrt_N": 2.8284}, {"N": 16, "set": [1, 2, 4, 8, 13], "h(N)": 5, "omega": 0.3639984130859375, "sqrt_N": 4.0}, {"N": 24, "set": [1, 2, 4, 8, 13, 21], "h(N)": 6, "omega": 0.3339996337890625, "sqrt_N": 4.899}]}}
 {"module": "T8_density", "severity": "HIGH", "claim": "Tensor network entropy for power-of-2 Sidon sets at N=32,64,128", "verdict": "PASS", "details": {"tensor_data": [{"N": 32, "set_size": 6, "set": [1, 2, 4, 8, 16, 32], "entropy": 0.9163, "entropy_k2": 1.9013, "sqrt_N": 5.6569}, {"N": 64, "set_size": 6, "set": [1, 2, 4, 8, 16, 32], "entropy": 0.9163, "entropy_k2": 1.9013, "sqrt_N": 8.0}, {"N": 128, "set_size": 6, "set": [1, 2, 4, 8, 16, 32], "entropy": 0.9163, "entropy_k2": 1.9013, "sqrt_N": 11.3137}], "explanation": "Entropy scales with set size, not N. Larger Sidon sets = more modes = higher entropy."}}
--- a/.openresearch/artifacts/pipeline_result.json
+++ b/.openresearch/artifacts/pipeline_result.json
@ -0,0 +1,80 @@
+{
+  "experiment": "pipeline_core",
+  "timestamp": "2026-07-05T03:54:18Z",
+  "stages": [
+    "BraidStorm(k=8)",
+    "TreeBraid",
+    "AngrySphinx(budget=128)",
+    "MultisurfacePacker(max=64)",
+    "COUCH(threshold=49152)",
+    "QuaternionSidonFilter"
+  ],
+  "labels": [
+    1,
+    2,
+    4,
+    8,
+    16,
+    32,
+    64,
+    128
+  ],
+  "S": 128,
+  "moduli": [
+    7,
+    3,
+    5,
+    11,
+    13,
+    17,
+    19,
+    23,
+    29
+  ],
+  "phases": [
+    0,
+    45,
+    90,
+    135,
+    180,
+    225,
+    270,
+    315
+  ],
+  "stage_timings": {
+    "BraidStorm(k=8)": {
+      "input": 1,
+      "output": 256,
+      "time_s": 0.0004
+    },
+    "TreeBraid": {
+      "input": 256,
+      "output": 256,
+      "time_s": 0.0
+    },
+    "AngrySphinx(budget=128)": {
+      "input": 256,
+      "output": 256,
+      "time_s": 0.0001
+    },
+    "MultisurfacePacker(max=64)": {
+      "input": 256,
+      "output": 64,
+      "time_s": 0.0
+    },
+    "COUCH(threshold=49152)": {
+      "input": 64,
+      "output": 64,
+      "time_s": 0.0
+    },
+    "QuaternionSidonFilter": {
+      "input": 64,
+      "output": 0,
+      "time_s": 0.0011
+    }
+  },
+  "total_output": 0,
+  "elapsed_s": 0.0016,
+  "final_configs": [],
+  "sha256": "f922489a57b79546e7bedfd8b77ac09e3ec01f4b3fd082f44e6c50b51a2a47fd"
+}
--- a/formal/SilverSight/AngrySphinx.lean
+++ b/formal/SilverSight/AngrySphinx.lean
@ -254,33 +254,70 @@ equation returns `none`. The infinity is converted to a closed system.
 theorem frustration_bounded (pressure : AttackPressure) :
    frustrationUnderPressure pressure = { value := Q16_16.one } ∨
    frustrationUnderPressure pressure ≠ { value := Q16_16.one } := by
-  cases pressure with | mk j =>
-    simp [frustrationUnderPressure]
-    split_ifs with h
-    · left; rfl
-    · right; intro heq; simpa [h] using heq
+  unfold frustrationUnderPressure
+  by_cases h : pressure.joules = 0
+  · left; simp [h]
+  · right; intro h_eq
+    have : Q16_16.ofRatio 1 (pressure.joules + 1) = Q16_16.one := by
+      simpa [h] using h_eq
+    -- ofRatio 1 (j+1) with j ≠ 0 means 65536/(j+1) < 65536 = one.toInt
+    have h_gt1 : 1 < pressure.joules + 1 := by omega
+    have h_div : 65536 / (pressure.joules + 1) < 65536 :=
+      Nat.div_lt_self (by omega) h_gt1
+    have h_val_lt : (Q16_16.ofRatio 1 (pressure.joules + 1)).toInt < Q16_16.one.toInt := by
+      unfold Q16_16.ofRatio Q16_16.scale Q16_16.toInt
+      have h_ne_zero : pressure.joules + 1 ≠ 0 := by omega
+      simp [h_ne_zero]
+      have h_one_val : (↑Q16_16.one : ℤ) = 65536 := rfl
+      rw [h_one_val]
+      have h_nonneg : 0 ≤ (65536 : Int) / (↑(pressure.joules) + 1) := by positivity
+      have h_le_self : (65536 : Int) / (↑(pressure.joules) + 1) ≤ 65536 := by
+        apply Int.ediv_le_self; omega
+      have h_id : q16Clamp ((65536 : Int) / (↑(pressure.joules) + 1)) = (65536 : Int) / (↑(pressure.joules) + 1) :=
+        q16Clamp_id_of_inRange _ (by
+          have : q16MinRaw = (-2147483648 : ℤ) := rfl
+          omega)
+          (by
+            have h_max : (65536 : ℕ) ≤ q16MaxRaw := by unfold q16MaxRaw; norm_num
+            omega)
+      rw [h_id]
+      have h_nat : (65536 : ℕ) / (pressure.joules + 1) < 65536 :=
+        Nat.div_lt_self (by norm_num) h_gt1
+      exact_mod_cast h_nat
+    have h_val_eq : (Q16_16.ofRatio 1 (pressure.joules + 1)).toInt = Q16_16.one.toInt := by
+      simpa using congrArg Q16_16.toInt this
+    exact h_val_lt.ne h_val_eq

 /-- For any pressure p ≥ 1, frustration F(p) < 1 (strictly decreasing).
    The defense is weakening but hasn't collapsed yet. -/
 theorem frustration_decreases (p : Nat) (hp : p ≥ 1) :
    (frustrationUnderPressure { joules := p }).value < Q16_16.one := by
  unfold frustrationUnderPressure
-  split_ifs with h
+  by_cases h : p = 0
  · omega
-  · -- F = Q16_16.ofRatio 1 (p+1) where p ≥ 1, so p+1 ≥ 2
-    -- ofRatio 1 n = Q16_SCALE / n when n ≥ 1
-    -- Q16_SCALE / (p+1) < Q16_SCALE when p+1 > 1 (i.e., p ≥ 1)
-    have h_denom_ne_zero : p + 1 ≠ 0 := by omega
-    have h_denom_pos : 0 < p + 1 := by omega
-    have h_div_nat : 65536 / (p + 1) < 65536 :=
-      Nat.div_lt_self (by norm_num : 1 ≤ 65536) h_denom_pos
-    have h_div_int : (Int.ofNat (65536 / (p + 1))) < (65536 : ℤ) := by
-      exact_mod_cast h_div_nat
-    -- Unfold Q16_16 <, which is toInt a < toInt b
-    -- ofRatio 1 (p+1) when p+1 ≠ 0 = ofRawInt (Int.ofNat (65536 / (p+1)))
-    -- toInt extracts the value, giving Int.ofNat (65536 / (p+1))
-    -- one = ⟨65536, ...⟩, toInt gives 65536
-    simpa [Q16_16.ofRatio, Q16_16.one, Q16_16.toInt, h_denom_ne_zero, Q16_16.scale] using h_div_int
+  · have h_one_lt : 1 < p + 1 := by omega
+    have h_val_lt : (Q16_16.ofRatio 1 (p + 1)).toInt < (Q16_16.one).toInt := by
+      unfold Q16_16.ofRatio Q16_16.scale Q16_16.toInt
+      have h_ne_zero : p + 1 ≠ 0 := by omega
+      simp [h_ne_zero]
+      have h_one_val : (↑Q16_16.one : ℤ) = 65536 := rfl
+      rw [h_one_val]
+      have h_nonneg : 0 ≤ (65536 : Int) / (↑(p : ℤ) + 1) := by positivity
+      have h_le_self : (65536 : Int) / (↑(p : ℤ) + 1) ≤ 65536 := by
+        apply Int.ediv_le_self; omega
+      have h_id : q16Clamp ((65536 : Int) / (↑(p : ℤ) + 1)) = (65536 : Int) / (↑(p : ℤ) + 1) :=
+        q16Clamp_id_of_inRange _ (by
+          have : q16MinRaw = (-2147483648 : ℤ) := rfl
+          omega)
+          (by
+            have h_max : (65536 : ℕ) ≤ q16MaxRaw := by unfold q16MaxRaw; norm_num
+            omega)
+      rw [h_id]
+      have h_nat : (65536 : ℕ) / (p + 1) < 65536 :=
+        Nat.div_lt_self (by norm_num) h_one_lt
+      exact_mod_cast h_nat
+    simp [h]
+    simpa using h_val_lt

 /-! §7 Evaluation Witnesses -/

--- a/formal/SilverSight/ColdReviewer.lean
+++ b/formal/SilverSight/ColdReviewer.lean
@ -4,8 +4,10 @@

 import CoreFormalism.FixedPoint
 import SilverSight.AdjugateMatrix
+import Mathlib.Tactic

 set_option linter.dupNamespace false
+set_option maxRecDepth 200000

 namespace SilverSight.ColdReviewer

@ -44,7 +46,8 @@ def psiInversion (M adjM : Matrix8) (detM : Q16_16) : Q16_16 :=
  maxAbsEntry residual

 theorem psiInversion_identity : psiInversion identity8 identity8 one = zero := by
-  dec_trivial
+  -- `dec_trivial` removed in Lean 4.30; concrete 8×8 Q16_16 computation
+  native_decide

 -- ═══════════════════════════════════════════════════════════════════════════
 -- §2  Ψ_gap
@ -89,7 +92,7 @@ def psiSidon (s : Array Nat) : Nat :=
  if isSidonSet8 s then 0 else 1

 theorem psiSidon_canonical : psiSidon ((#[0,1,3,7,12,20,30,44] : Array Nat)) = 0 := by
-  dec_trivial
+  native_decide

 -- ═══════════════════════════════════════════════════════════════════════════
 -- §4  Unified Cold Reviewer Operator
@ -110,6 +113,7 @@ theorem canonical_scores_zero (h_gap : sigma.toInt ≥ (threshold_1_7).toInt) :
  have h_gap' : psiSpectral sigma = zero := psiSpectral_above sigma h_gap
  have h_sidon : psiSidon ((#[0,1,3,7,12,20,30,44] : Array Nat)) = 0 := psiSidon_canonical
  simp [h_inv, h_gap', h_sidon, mul_zero, one_mul]
-  dec_trivial
+  -- remaining: zero.add (zero.add (ofInt 0)) = zero
+  native_decide

 end SilverSight.ColdReviewer
--- a/formal/SilverSight/PIST/CharPoly.lean
+++ b/formal/SilverSight/PIST/CharPoly.lean
@ -2,10 +2,10 @@
 Copyright (c) 2026 SilverSight Contributors. All rights reserved.
 Released under Apache 2.0 license.

-Exact characteristic polynomial computation for n×n integer matrices.
-Uses the Faddeev–LeVerrier algorithm: all integer arithmetic, no floats.
+Exact characteristic polynomial computation for nxn integer matrices.
+Uses the Faddeev-LeVerrier algorithm: all integer arithmetic, no floats.

-The characteristic polynomial p(λ) = det(λI - A) has integer coefficients
+The characteristic polynomial p(lambda) = det(lambdaI - A) has integer coefficients
 when A has integer entries. This module computes them exactly.

 Key advantage over powerIteration: provably correct for all matrices,
@ -22,147 +22,87 @@ open SilverSight.FixedPoint
 open SilverSight.FixedPoint.Q16_16
 open SilverSight.PIST.MatrixN

-- ── Matrix trace ──────────────────────────────────────────────────────────
+-- -- Matrix trace ----------------------------------------------------------

-/-- Trace of an n×n integer matrix: sum of diagonal entries. -/
+/-- Trace of an nxn integer matrix: sum of diagonal entries. -/
 def matrixTrace (n : Nat) (mat : Array (Array Int)) : Int :=
  (List.range n).foldl (fun acc i => acc + getEntry mat i i) 0

-- ── Matrix multiplication (integer) ───────────────────────────────────────
+-- -- Matrix multiplication (integer) ---------------------------------------

-/-- Multiply two n×n integer matrices. All entries are exact integers. -/
+/-- Multiply two nxn integer matrices. All entries are exact integers. -/
 def matMulInt (n : Nat) (a b : Array (Array Int)) : Array (Array Int) :=
  Array.ofFn (n := n) fun i =>
    Array.ofFn (n := n) fun j =>
      (List.range n).foldl (fun acc k =>
        acc + getEntry a i.val k * getEntry b k j.val) 0

-- ── Matrix power (integer) ────────────────────────────────────────────────
+-- -- Matrix power (integer) ------------------------------------------------

 /-- Compute A^k for integer matrix A via repeated squaring.
    Returns (A^1, A^2, ..., A^k) as a list for trace extraction. -/
-def matPowers (n : Nat) (mat : Array (Array Int)) (k : Nat) : List (Array (Array Int)) :=
-  let rec loop (current : Array (Array Int)) (remaining : Nat) (acc : List (Array (Array Int))) : List (Array (Array Int)) :=
+def matPowersLoop (n : Nat) (mat : Array (Array Int)) (current : Array (Array Int))
+    (remaining : Nat) (acc : List (Array (Array Int))) : List (Array (Array Int)) :=
  match remaining with
  | 0 => acc.reverse
  | Nat.succ r =>
    let next := matMulInt n current mat
-        loop next r (current :: acc)
+    matPowersLoop n mat next r (current :: acc)
+
+def matPowers (n : Nat) (mat : Array (Array Int)) (k : Nat) : List (Array (Array Int)) :=
  if k = 0 then []
-  else loop mat (k - 1) [mat]
+  else matPowersLoop n mat mat (k - 1) [mat]

-- ── Faddeev–LeVerrier algorithm ───────────────────────────────────────────
+-- -- Faddeev-LeVerrier algorithm -----------------------------------------
+-- See comment block below for the math derivation.

-/-- Newton identity coefficients for the characteristic polynomial.
-
-    The Faddeev–LeVerrier recurrence:
-      c₀ = 1
-      cₖ = -(1/k) * (tr(A^k) + Σᵢ₌₁ᵏ⁻¹ cₖ₋ᵢ * tr(A^i))
-
-    Since we work in integers, we compute:
-      k! * cₖ = -(k-1)! * tr(A^k) - Σᵢ₌₁ᵏ⁻¹ (k-1)!/(i-1)! * cₖ₋ᵢ * tr(A^i) / ... 
-
-    Actually, the simplest integer approach: compute the Faddeev sequence
-    Bₖ = A·Bₖ₋₁ + cₖ₋₁·A  (with B₀ = I, c₀ = -tr(A))
-    and cₖ = -tr(Bₖ)/k
-
-    For integer matrices, Bₖ has integer entries but cₖ may be rational.
-    To avoid fractions, we scale: let D = lcm(1,2,...,n) and work in D·ℤ.
-
-    For n=8: D = lcm(1,2,3,4,5,6,7,8) = 840.
-
-    Alternative simpler approach: directly compute det(λI - A) via
-    cofactor expansion or Bareiss algorithm. For n=8 this is feasible.
-
-    We use the direct trace-based formula:
-      p(λ) = λⁿ - σ₁λⁿ⁻¹ + σ₂λⁿ⁻₂ - ... + (-1)ⁿσₙ
-
-    where σₖ = (1/k)(pₖ - σ₁pₖ₋₁ + σ₂pₖ₋₂ - ... + (-1)ᵏ⁻¹σₖ₋₁p₁)
-    and pₖ = tr(Aᵏ)
-
-    Working in scaled integers: let Sₖ = k!·σₖ. Then:
-      Sₖ = k!·σₖ = (k-1)!·pₖ - Σᵢ₌₁ᵏ⁻¹ (k-1)!·σₖ₋ᵢ·pᵢ·(-1)ⁱ⁻¹
-
-    Wait, this still has division. Let me use the simplest correct approach.
-
-    DIRECT COMPUTATION via the formula:
-      c₀ = 1
-      cₖ = -(1/k) * Σᵢ₌₀ᵏ⁻¹ cᵢ * tr(Aᵏ⁻ⁱ)
-
-    Scale by k! to get integers:
-      Cₖ = k!·cₖ
-      C₀ = 1
-      Cₖ = -(k-1)! * Σᵢ₌₀ᵏ⁻¹ Cᵢ/k! * tr(Aᵏ⁻ⁱ) ... still messy.
-
-    CLEANEST APPROACH: Use the fact that for integer matrices, the
-    characteristic polynomial has integer coefficients. Compute them
-    via the recursive formula with exact rational arithmetic.
-
-    Since Lean has Rat, we can use that. But for the integer-only
-    doctrine, we use the scaled version.
-
-    Actually, the simplest approach for n=8: compute the 8 traces
-    p₁,...,p₈, then apply Newton's identities with integer division
-    at each step. The division is exact (always produces integer).
-/ section FaddeevLeVerrier
-
-/-- Compute traces of A¹, A², ..., Aᵏ. -/
+/-- Compute traces of A1, A2, ..., Ak. -/
 def matrixTraces (n : Nat) (mat : Array (Array Int)) (k : Nat) : Array Int :=
  let powers := matPowers n mat k
  Array.ofFn (fun (i : Fin k) => matrixTrace n (powers.getD i.val mat))

-/-- Newton identity: compute σₖ from traces p₁,...,pₖ.
+-- Newton identity: compute sigma_k from traces p_1,...,p_k.
+-- The division by k is exact for integer matrices.

-    σ₀ = 1
-    σₖ = (1/k) * (pₖ - Σᵢ₌₁ᵏ⁻¹ σᵢ · pₖ₋ᵢ · (-1)ⁱ⁻¹)  ... no, the sign is:
-    σₖ = (1/k) * (pₖ·(-1)⁰ + σ₁·pₖ₋₁·(-1)¹ + ... + σₖ₋₁·p₁·(-1)ᵏ⁻¹)
+-- Algorithm details: Newton identities for characteristic polynomial.
+-- Standard recurrence: c_1 = -p_1, c_k = -(1/k) * sum_{i=1..k} c_{k-i} * p_i.

-    Wait, the standard Newton identities for characteristic polynomial
-    p(λ) = λⁿ + c₁λⁿ⁻¹ + ... + cₙ are:
-
-    c₁ = -p₁
-    c₂ = -(p₂ + c₁·p₁)/2
-    c₃ = -(p₃ + c₁·p₂ + c₂·p₁)/3
-    ...
-    cₖ = -(1/k) * Σᵢ₌₁ᵏ cₖ₋ᵢ · pᵢ   (with c₀ = 1)
-
-    Equivalently: k·cₖ = -Σᵢ₌₁ᵏ cₖ₋ᵢ · pᵢ
-
-    The division by k is always exact for integer matrices.
-/
+-- Algorithm details: Newton identities for characteristic polynomial.
+-- Standard recurrence: c_1 = -p_1, c_k = -(1/k) * sum_{i=1..k} c_{k-i} * p_i.
+-- The division by k is exact for integer matrices.

 /-- Characteristic polynomial coefficients via Newton identities.
-    Returns [c₁, c₂, ..., cₙ] where p(λ) = λⁿ + c₁λⁿ⁻¹ + ... + cₙ.
+    Returns [c_1, c_2, ..., c_n] where p(lambda) = lambda^n + c_1 lambda^{n-1} + ... + c_n.
    All coefficients are exact integers. -/
-def charPolyCoeffs (n : Nat) (mat : Array (Array Int)) : Array Int :=
-  if n = 0 then #[]
-  else
-    let traces := matrixTraces n mat n
-    -- Newton identity recurrence: k·cₖ = -Σᵢ₌₁ᵏ cₖ₋ᵢ · pᵢ
-    let rec loop (k : Nat) (cs : Array Int) : Array Int :=
+def charPolyLoop (n : Nat) (traces : Array Int) (k : Nat) (cs : Array Int) : Array Int :=
  if k > n then cs
  else
-        let p_k := traces.getD (k - 1) 0  -- p_k = tr(A^k), 1-indexed
-        -- Sum: Σᵢ₌₁ᵏ cₖ₋ᵢ · pᵢ  where c₀ = 1
+    let p_k := traces.getD (k - 1) 0
    let sum := (List.range k).foldl (fun acc i =>
-          let idx := i  -- 0-indexed, so i corresponds to i+1 in the formula
+      let idx := i
      let c_prev := if k - 1 - idx = 0 then 1 else cs.getD (k - 2 - idx) 0
      let p_i := traces.getD idx 0
      acc + c_prev * p_i) 0
    let c_k := -sum / (k : Int)
-        loop (k + 1) (cs.push c_k)
-    loop 1 #[]
+    charPolyLoop n traces (k + 1) (cs.push c_k)
+termination_by n.succ - k

-end FaddeevLeVerrier
+def charPolyCoeffs (n : Nat) (mat : Array (Array Int)) : Array Int :=
+  if n = 0 then #[]
+  else
+    let traces := matrixTraces n mat n
+    -- Newton identity recurrence: k*ck = -Sumi?1k ck?i * pi
+    charPolyLoop n traces 1 #[]

-- ── Spectral radius from characteristic polynomial ────────────────────────
+
+-- -- Spectral radius from characteristic polynomial ------------------------

 /-- Newton's method to find the largest real root of a polynomial.
-    Given coefficients [c₁, ..., cₙ] for p(λ) = λⁿ + c₁λⁿ⁻¹ + ... + cₙ,
+    Given coefficients [c1, ..., cn] for p(lambda) = lambdan + c1lambdan?1 + ... + cn,
    finds the root with largest absolute value.

    Uses Q16_16 arithmetic with a fixed number of iterations.
-    Starting guess: max(|cᵢ|)^(1/i) heuristic.
+    Starting guess: max(|ci|)^(1/i) heuristic.
 -/
 def newtonLargestRoot (coeffs : Array Int) (maxIter : Nat := 50) : Q16_16 :=
  if coeffs.size = 0 then zero
@ -170,14 +110,14 @@ def newtonLargestRoot (coeffs : Array Int) (maxIter : Nat := 50) : Q16_16 :=
    let n := coeffs.size
    -- Evaluate polynomial and its derivative at x (Q16_16)
    let evalPoly (x : Q16_16) : Q16_16 :=
-      -- Horner's method: p(x) = (...((x + c₁)x + c₂)x + ... + cₙ)
+      -- Horner's method: p(x) = (...((x + c1)x + c2)x + ... + cn)
      let result := (List.range n).foldl (fun acc i =>
        let c := coeffs.getD i 0
        add (mul acc x) (ofRawInt c)) x
      result
    let evalDeriv (x : Q16_16) : Q16_16 :=
-      -- p'(x) = n·xⁿ⁻¹ + (n-1)·c₁·xⁿ⁻² + ... + cₙ₋₁
-      let result := (List.range (n - 1)).foldl (fun acc i :=
+      -- p'(x) = n*xn?1 + (n-1)*c1*xn?2 + ... + cn?1
+      let result := (List.range (n - 1)).foldl (fun acc i =>
        let c := coeffs.getD i 0
        let coeff := ofRawInt ((n - i : Int) * c)
        add (mul acc x) coeff) (ofRawInt (n : Int))
@ -214,12 +154,12 @@ def spectralRadiusFromCharPoly (coeffs : Array Int) : Q16_16 :=
  else
    let root := newtonLargestRoot coeffs
    -- Return absolute value (spectral radius is non-negative)
-    if root.toInt ≥ 0 then root else ofRawInt (-root.toInt)
+    if root.toInt >= 0 then root else ofRawInt (-root.toInt)

-- ── Cayley-Hamilton theorem (statement) ───────────────────────────────────
+-- -- Cayley-Hamilton theorem (statement) -----------------------------------

 /-- The Cayley-Hamilton theorem: every matrix satisfies its own
-    characteristic polynomial. For A with charpoly p(λ), p(A) = 0.
+    characteristic polynomial. For A with charpoly p(lambda), p(A) = 0.

    This is stated as a Prop for future proof. The computational
    content is in charPolyCoeffs and the matrix evaluation.
@ -230,9 +170,9 @@ theorem cayley_hamilton_statement (n : Nat) (mat : Array (Array Int)) :
    -- matrix polynomial evaluation which is TODO.
    True := trivial

-- ── Integration: exact spectral profile ───────────────────────────────────
+-- -- Integration: exact spectral profile -----------------------------------

-/-- Exact spectral radius of an n×n integer matrix.
+/-- Exact spectral radius of an nxn integer matrix.
    Uses characteristic polynomial instead of power iteration.
    Provably correct for all matrices. -/
 def exactSpectralRadius (n : Nat) (mat : Array (Array Int)) : Q16_16 :=
@ -241,14 +181,13 @@ def exactSpectralRadius (n : Nat) (mat : Array (Array Int)) : Q16_16 :=
    let coeffs := charPolyCoeffs n mat
    spectralRadiusFromCharPoly coeffs

-/-- Test: characteristic polynomial of identity matrix is (λ-1)^8.
-    Coefficients: c₁=-8, c₂=28, c₃=-56, c₄=70, c₅=-56, c₆=28, c₇=-8, c₈=1. -/
-#eval charPolyCoeffs 2 #[#[1, 0], #[0, 1]]   -- expect: [-2, 1]  (λ² - 2λ + 1)
+-- Test: characteristic polynomial of identity matrix is (lambda-1)^8.
+#eval charPolyCoeffs 2 #[#[1, 0], #[0, 1]]

-/-- Test: trace of 2×2 identity is 2. -/
-#eval matrixTrace 2 #[#[1, 0], #[0, 1]]  -- expect: 2
+-- Test: trace of 2x2 identity is 2.
+#eval matrixTrace 2 #[#[1, 0], #[0, 1]]

-/-- Test: exact spectral radius of 2×2 identity is 1.0 (65536 in Q16_16). -/
-#eval (exactSpectralRadius 2 #[#[1, 0], #[0, 1]]).toInt  -- expect: 65536
+-- Test: exact spectral radius of 2x2 identity is 1.0 (65536 in Q16_16).
+#eval (exactSpectralRadius 2 #[#[1, 0], #[0, 1]]).toInt

 end SilverSight.PIST.CharPoly
--- a/formal/SilverSight/WorkloadTestbench.lean
+++ b/formal/SilverSight/WorkloadTestbench.lean
@ -120,7 +120,6 @@ theorem random_highest_self_loop :
    workloadSelfLoop .random ≥ workloadSelfLoop .stream ∧
    workloadSelfLoop .random ≥ workloadSelfLoop .strided := by
  simp [workloadSelfLoop, workloadToOp, HCMR.selfLoopProb]
-  omega

 /-- Stream workloads have the highest throughput. -/
 theorem stream_highest_throughput (baseRate : ℕ) :
@ -150,6 +149,5 @@ theorem random_causes_reset :
    CacheSieve.sieveTransition .unstable 10 (workloadSelfLoop .random) = (.reset, .demote) := by
  simp [workloadSelfLoop, workloadToOp, HCMR.selfLoopProb, CacheSieve.sieveTransition,
        CacheSieve.ContentionThreshold]
-  omega

 end SilverSight.WorkloadTestbench
--- a/formal/SilverSight/YangMillsPerformance.lean
+++ b/formal/SilverSight/YangMillsPerformance.lean
@ -85,7 +85,6 @@ def fullStackThroughput (baseRate : ℕ) : ℕ :=
 /-- Layer multiplier is non-negative (overhead ≤ 1). -/
 theorem multiplier_nonneg (layer : PerfLayer) : layerMultiplier layer ≥ 0 := by
  simp [layerMultiplier, overheadFactor]
-  omega

 /-- Cache layer has the highest overhead (most contention). -/
 theorem cache_highest_overhead :
@ -94,7 +93,6 @@ theorem cache_highest_overhead :
    overheadFactor .cache ≥ overheadFactor .compression ∧
    overheadFactor .cache ≥ overheadFactor .network := by
  simp [overheadFactor]
-  omega

 /-- Network layer has the second-highest overhead. -/
 theorem network_second_highest :
@ -102,51 +100,88 @@ theorem network_second_highest :
    overheadFactor .network > overheadFactor .sync ∧
    overheadFactor .network > overheadFactor .memory := by
  simp [overheadFactor]
-  omega
+
+/-- Key step: multiplying by a layer multiplier and dividing by 65536
+    never increases the accumulator (since `layerMultiplier ≤ 65536`). -/
+private lemma mul_div_le_self (acc : ℕ) (layer : PerfLayer) :
+    acc * layerMultiplier layer / 65536 ≤ acc := by
+  have hle : layerMultiplier layer ≤ 65536 := by
+    simp [layerMultiplier, overheadFactor]
+  have hpos : (0 : ℕ) < 65536 := by norm_num
+  -- acc * lm / 65536 ≤ acc * 65536 / 65536 (monotonic div) = acc (cancel after comm)
+  have h_step : acc * layerMultiplier layer / 65536 ≤ acc * 65536 / 65536 :=
+    Nat.div_le_div_right (Nat.mul_le_mul_left acc hle)
+  have h_cancel : acc * 65536 / 65536 = acc := by
+    rw [Nat.mul_comm]; exact Nat.mul_div_cancel_left acc hpos
+  rw [h_cancel] at h_step
+  exact h_step
+
+/-- Composed throughput never exceeds the starting accumulator:
+    each layer can only reduce throughput (since `layerMultiplier ≤ 65536`). -/
+private lemma composed_decreasing (acc : ℕ) (layers : List PerfLayer) :
+    composedThroughput acc layers ≤ acc := by
+  induction layers generalizing acc with
+  | nil => simp [composedThroughput]
+  | cons head tail ih =>
+    simp only [composedThroughput, List.foldl_cons]
+    refine Nat.le_trans (ih _) ?_
+    exact mul_div_le_self _ head

 /-- Composed throughput is monotonically decreasing with more layers. -/
 theorem more_layers_less_throughput (baseRate : ℕ) (layers : List PerfLayer)
    (hbase : baseRate > 0) (layer : PerfLayer) :
    composedThroughput baseRate (layers ++ [layer]) ≤
    composedThroughput baseRate layers := by
-  induction layers with
+  -- Prove by induction on layers, generalizing the accumulator.
+  -- `clear hbase` first so it isn't generalized into the IH (the IH would
+  -- then require a positivity proof for the new accumulator, which may be 0).
+  clear hbase
+  induction layers generalizing baseRate with
  | nil =>
-    simp [composedThroughput]
-    -- baseRate * (1 - overhead) ≤ baseRate when overhead ≥ 0
-    have h : layerMultiplier layer ≤ 65536 := by omega
-    nlinarith
-  | cons head tail IH =>
-    simp [composedThroughput]
-    have : (baseRate * layerMultiplier head / 65536) * layerMultiplier layer / 65536 ≤
-           baseRate * layerMultiplier head / 65536 := by
-      have h : layerMultiplier layer ≤ 65536 := by omega
-      nlinarith
-    omega
+    simp only [composedThroughput, List.nil_append, List.foldl_cons, List.foldl_nil]
+    exact mul_div_le_self baseRate layer
+  | cons head tail ih =>
+    simp only [composedThroughput, List.cons_append, List.foldl_cons]
+    exact ih (baseRate * layerMultiplier head / 65536)

 /-- HCMR connection: cache layer overhead = SUBLEQ self-loop probability. -/
 theorem cache_overhead_equals_subleq :
    overheadFactor .cache = HCMR.selfLoopProb .subleqWord := rfl

-/-- Full stack throughput is strictly less than base rate (overhead exists). -/
+/-- Full stack throughput is strictly less than base rate (overhead exists).
+
+    The cache layer alone (overhead 53908/65536 ≈ 0.823) reduces throughput
+    to `baseRate * 11628 / 65536 < baseRate` for any `baseRate > 0`.
+    The remaining 4 layers can only decrease throughput further. -/
 theorem full_stack_throughput_lt_base (baseRate : ℕ) (hbase : baseRate > 0) :
    fullStackThroughput baseRate < baseRate := by
-  simp [fullStackThroughput, composedThroughput, fullStack]
-  -- Each layer reduces throughput; with 5 layers of overhead, total < base
-  have h : layerMultiplier .cache < 65536 := by
-    simp [layerMultiplier, overheadFactor]; omega
-  -- After first layer: baseRate * (65536 - 53908) / 65536 < baseRate
-  nlinarith
+  -- Step 1: the first layer (cache) strictly decreases throughput.
+  have h_first : baseRate * layerMultiplier .cache / 65536 < baseRate := by
+    have hlm : layerMultiplier .cache = 11628 := by
+      unfold layerMultiplier overheadFactor; norm_num
+    rw [hlm]
+    have hpos : (0 : ℕ) < 65536 := by norm_num
+    rw [Nat.div_lt_iff_lt_mul hpos]
+    omega
+  -- Step 2: the remaining layers can only decrease throughput further.
+  have h_rest : fullStackThroughput baseRate ≤ baseRate * layerMultiplier .cache / 65536 := by
+    simp only [fullStackThroughput, composedThroughput, fullStack, List.foldl_cons, List.foldl_nil]
+    exact composed_decreasing _ [.memory, .sync, .compression, .network]
+  -- Combined: fullStackThroughput ≤ first_layer < baseRate.
+  omega

-/-- Conservation law connection: compression overhead is bounded below.
+/- Conservation law connection: compression overhead is bounded below.

-    The compression layer's overhead ≥ K(data) / data_size.
-    This is the conservation law from weird_machine_conservation_law.md. -/
-theorem compression_overhead_bounded (kData : ℕ) (dataSize : ℕ)
-    (h : dataSize > 0) :
-    overheadFactor .compression ≥ kData * 65536 / dataSize := by
-  -- This is a placeholder — the actual bound depends on the data
-  -- The conservation law states: program + residual ≥ K(data)
-  -- The compression overhead = residual / data_size ≥ K(data) / data_size
-  sorry
+   CONJECTURE (not proven): the compression layer's overhead ≥ K(data) / data_size.
+   This requires the conservation law from weird_machine_conservation_law.md:
+   program + residual ≥ K(data), so compression overhead = residual / data_size
+   ≥ K(data) / data_size. The bound depends on the Kolmogorov complexity K(data),
+   which is uncomputable in general — see PIST/ManifoldShortcut.lean's
+   `conservation_law` axiom for the formal statement.
+
+   Not stated as a theorem here because `overheadFactor .compression` is a fixed
+   constant (32768) while K(data) is unbounded — the inequality only holds under
+   the conservation-law hypothesis, not universally. -/
+-- theorem compression_overhead_bounded : omitted pending conservation law formalization

 end SilverSight.YangMillsPerformance