fix(lean): BlockCoprimeDensity round-2 adversarial fixes

Removed:
- @[simp] from 4 conditional lemmas (hypotheses simp can't discharge)
- claimBoundary/bridgeNote String defs (dead code in API)
- 'expected to be' header wording

Added:
- isSaturated_or_isActive, isSaturated_iff_not_isActive theorems
- primesUpTo edge-case note
- cleaner doc wording throughout

Kept:
- @[simp] on C_finite_zero_eq_one (unconditional, useful)

.atlas/benchmark.sh

@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+set -uo pipefail
+HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+OUT="$(mktemp)"
+
+TARGET="${ATLAS_OPTIMIZE_TARGET:-$1}"
+export ATLAS_EVAL_SEED="${ATLAS_EVAL_SEED:-0}"
+
+START=$(date +%s.%N)
+( python3 "$TARGET" ) >"$OUT" 2>&1
+RC=$?
+END=$(date +%s.%N)
+
+if [ "$RC" -ne 0 ]; then
+  echo "[benchmark] run command exited $RC — candidate failed" >&2
+  tail -n 40 "$OUT" >&2
+  exit "$RC"
+fi
+
+python3 "$HERE/score.py" --stdout "$OUT" --elapsed "$(awk "BEGIN { print $END - $START }")"

.atlas/gate.sh

@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+# Goodhart guard: reject candidates that lower quality while improving timing
+set -uo pipefail
+
+HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+TARGET="${ATLAS_OPTIMIZE_TARGET:-$2}"
+REF_SCORE="${ATLAS_REF_SCORE:-$1}"
+
+NEW_OUT="$(mktemp)"
+NEW_START=$(date +%s.%N)
+( python3 "$TARGET" ) >"$NEW_OUT" 2>&1
+NEW_RC=$?
+NEW_END=$(date +%s.%N)
+NEW_ELAPSED=$(awk "BEGIN { print $NEW_END - $NEW_START }")
+
+if [ "$NEW_RC" -ne 0 ]; then
+  echo "[gate] candidate failed — rejecting"
+  exit 1
+fi
+
+NEW_SCORE=$(python3 "$HERE/score.py" --stdout "$NEW_OUT" --elapsed "$NEW_ELAPSED" 2>/dev/null | python3 -c "import json,sys; print(json.load(sys.stdin)['score'])")
+
+# Accept if score >= reference (higher is better)
+ACCEPT=$(python3 -c "print('yes' if $NEW_SCORE >= $REF_SCORE - 0.01 else 'no')")
+if [ "$ACCEPT" = "yes" ]; then
+  echo "[gate] accepted (score=$NEW_SCORE >= ref=$REF_SCORE)"
+  exit 0
+else
+  echo "[gate] rejected (score=$NEW_SCORE < ref=$REF_SCORE)"
+  exit 1
+fi

.atlas/score.py

@@ -0,0 +1,83 @@
+#!/usr/bin/env python3
+import argparse, json, os, re, sys
+
+METRICS = {
+    "Rank corr": True,
+    "Rank correlation": True,
+    "NN Tm correlation": True,
+    "Naive Tm correlation": True,
+}
+
+def parse(text):
+    results = {}
+    for name, higher in METRICS.items():
+        pat = re.compile(re.escape(name) + r"\s*:\s*([+-]?[0-9]*\.?[0-9]+)", re.IGNORECASE)
+        matches = pat.finditer(text)
+        vals = []
+        for m in matches:
+            vals.append((float(m.group(1)), higher, m.group(0).strip()))
+        if vals:
+            results[name] = vals
+    return results
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--stdout", required=True)
+    ap.add_argument("--elapsed", type=float, default=None)
+    args = ap.parse_args()
+    text = open(args.stdout, encoding="utf-8", errors="replace").read()
+    parsed = parse(text)
+
+    score = None
+    feedback_parts = []
+
+    if "NN Tm correlation" in parsed:
+        val, _, raw = parsed["NN Tm correlation"][0]
+        score = abs(val)
+        feedback_parts.append(f"NN Tm corr={val}")
+    elif "Rank correlation" in parsed:
+        vals = [abs(v) for v, _, _ in parsed["Rank correlation"]]
+        score = sum(vals) / len(vals)
+        feedback_parts.append(f"avg |Rank corr|={score:.4f}")
+    elif "Rank corr" in parsed:
+        vals = [abs(v) for v, _, _ in parsed["Rank corr"]]
+        score = sum(vals) / len(vals)
+        feedback_parts.append(f"avg |Rank corr|={score:.4f}")
+    elif "Naive Tm correlation" in parsed:
+        val, _, raw = parsed["Naive Tm correlation"][0]
+        score = abs(val)
+        feedback_parts.append(f"Naive Tm corr={val}")
+
+    if score is None and args.elapsed is not None:
+        score = -(args.elapsed * 1000)
+        feedback_parts.append(f"time={args.elapsed*1000:.1f}ms")
+    elif score is None:
+        m = re.search(r"SUMMARY:\s*(\d+)/(\d+)\s*passed", text)
+        if m:
+            score = float(m.group(1))
+            feedback_parts.append(f"passes={m.group(1)}/{m.group(2)}")
+        else:
+            sys.stderr.write("[score] no metric found in output.\n")
+            sys.exit(3)
+
+    result = {
+        "score": score,
+        "examples": [{
+            "id": "metric",
+            "score": score,
+            "pass": True,
+            "feedback": " | ".join(feedback_parts),
+        }],
+        "feedback": " | ".join(feedback_parts),
+    }
+
+    out = os.environ.get("ATLAS_OPTIMIZE_RESULT")
+    payload = json.dumps(result)
+    if out:
+        with open(out, "w", encoding="utf-8") as fh:
+            fh.write(payload)
+    else:
+        sys.stdout.write(payload)
+
+if __name__ == "__main__":
+    main()

.gitignore

@@ -38,3 +38,9 @@ secrets/
 
 # MCP backend build artifacts
 scripts/mcp_backend/target/
+node_modules/
+package.json
+package-lock.json
+.atlas-optimize/
+*.sam
+*_summary.json

AGENTS.md

@@ -12,6 +12,13 @@
 
 `~/Research\ Stack` is a **read-only archive**. Never write to it. It is the regression oracle — if a closed theorem there covers the same territory as new SilverSight work, the SilverSight proof must recover it as a corollary.
 
+## ⚠️ Ephemeral Build Runner
+
+**neon-64gb (`100.92.88.64`) is an ephemeral build unit with NO permanent access rights.**
+It may vanish mid-session. Never store data, configs, or credentials on it.
+Never assume it will be reachable. All build dispatch must handle neon failure
+gracefully — fall back to local or provider-nixos.
+
 ## Rules
 
 1. **SilverSight is the ONLY target for new formal work.** All new Lean code goes here. Do NOT modify `~/Research\ Stack/` under any circumstances.
@@ -27,6 +34,38 @@
 
 5. **No `native_decide` unless it is the only tactic that closes the goal.** Use `norm_num`, `omega`, `simp`, `decide`, or explicit proof terms first. Document why `native_decide` is required when used. Exception: finitely decidable existence claims (e.g., N=8 necessity) are the canonical use case.
 
+### Fraction Construction Rules
+
+The SilverSight FixedPoint module provides Q16_16 fixed-point arithmetic. Use only these canonical constructors:
+
+1. **Use canonical constructors only**
+   ```lean
+   Q16_16.ofNat n      -- for integers
+   Q16_16.ofRatio a b  -- for rational numbers
+   Q16_16.ofRawInt x   -- for already-scaled integers
+   ```
+
+2. **Never use `ofFloat` in compute paths**
+   - Allowed only at external boundary (JSON parsing, sensor input)
+   - Must be immediately bracketed: `ofFloat x |> toFixedPoint |> compute`
+
+3. **Bridge pattern for legacy code** (Research Stack migration path)
+   ```lean
+   import Semantics.PhysicsScalarBridge
+   -- Use PhysicsScalarBridge.add, .gt, etc.
+   -- Constants: PhysicsScalarBridge.one, .two, .three, .half, .quarter
+   ```
+
+### Fraction Comparison Pattern
+
+```lean
+-- WRONG: direct comparison with Float
+if x > 0.5 then ...
+
+-- RIGHT: fixed-point comparison
+if x > Q16_16.half then ...
+```
+
 6. **Build gate:** `lake build SilverSight` must pass (0 errors).
 
 7. **Every new module needs:**
@@ -144,6 +183,20 @@ Target: `formal/SilverSight/HachimojiN8.lean` — provable by `native_decide` on
 | RRC/Q16_16Manifold.lean | Complete (278 rows, Q16_16 manifold fields) | 0 |
 | RRC/ReceiptDensity.lean | Complete | 0 |
 | RRCLogogramProjection.lean | Complete | 0 |
+| CacheSieve.lean | Complete (2026-07-05 maintenance: evictVictim inline fix) | 0 |
+| Blitter6502OISC.lean | Complete (2026-07-05: execSUBLEQ inline fix) | 0 |
+| BlockCoprimeDensity.lean | Complete (C(n) Euler product, saturation partition, C(0)=1) | 0 |
+| ColdReviewer.lean | Complete (2026-07-05: dec_trivial → native_decide) | 0 |
+| GoldenSpiral.lean | Complete (2026-07-05: MulLeftMono → induction) | 0 |
+| PIST/CharPoly.lean | Complete (2026-07-05: Horner Newton 3-bug fix) | 0 |
+| PIST/CMYKColoringCore.lean | Complete (2026-07-05: decodeColoring roundtrip) | 0 |
+| PIST/SidonAdapter.lean | Complete (2026-07-05: Nat.find → iterative loop) | 0 |
+| PIST/WeightCandidateGen.lean | Complete (2026-07-05: fuel termination) | 0 |
+| PIST/UnitDistCandidateGen.lean | Complete (2026-07-05: fuel termination, n≥3) | 0 |
+| PIST/ManifoldShortcut.lean | Complete (2026-07-05: Unicode→line comments) | 0 |
+| Rollup.lean | Complete (circulant-block compression theorem, totalCrossingMultCost=8) | 0 |
+| YangMillsPerformance.lean | Complete (2026-07-05: compression_overhead_bounded → Rollup.totalCrossingMultCost) | 0 |
+| ChiralClockModel.lean | Stub (copied from experimental, 4 sorries from experimental) | 4 |
 
 † Layer 3 sorries are geometric conjectures (Kähler on ℂℙ⁷, Cartan connection,
   holonomy SO⁰(1,6)) deferred pending Mathlib infrastructure.  Layer 1 (4
@@ -292,6 +345,70 @@ ncDerived = Q16_16.mul residualRisk scaleBandDeclared
 | `formal/SilverSight/RRC/Q16_16Manifold.lean` | ✅ 278 rows | Q16_16 manifold fields |
 | `python/build_manifold.py` | ✅ Q16_16 emission | `lean_q16_16()` helper |
 
+## Gauge Theory Research Program
+
+Gauge theory is the most rigorous framework for mapping out math because it forces explicit
+distinctions between theorems, conjectures, and empirical observations. Use it as a probe,
+not as a claim.
+
+### What Gauge Theory Demands
+
+1. **Proven vs Conjectural**
+   - If you claim a correspondence, you must prove it or label it an ansatz
+   - Empirical correlations (r=0.41, r=-0.33, n=13, p>0.05) are data, not theorems
+   - Gauge theory requires: "Is this a theorem or an ansatz?"
+
+2. **Dimensional Honesty**
+   - AT model is 2D; gauge confinement requires 3+1D (or 2+1D for compact U(1))
+   - Confinement in 2D gauge theory is trivial — this is a theorem
+   - Dimensional mismatches must be explicitly addressed, not papered over
+
+3. **Category/Type Correctness**
+   - Frustration is boolean/Z₂
+   - Wilson loop is real-valued (trace of holonomy)
+   - Curvature is Lie-algebra-valued
+   - Confusing these categories is a type error
+
+### What Gauge Theory Does NOT Give You
+
+1. **Derivation for Free** — The Baker-Hopf coupling is an ansatz, not derived from gauge principles
+2. **Uniqueness** — Other connections (arctan, Li₂, etc.) could satisfy similar constraints
+3. **Predictive Power** — Correlations computed because the hypothesis suggested them
+
+### Success Criteria
+
+Success is NOT "SilverSight IS gauge theory."
+
+Success IS: "We attempted to derive SilverSight structures from gauge theory.
+We succeeded for X, failed for Y, and learned Z."
+
+Specifically:
+- **Attempt derivation for Baker-Hopf coupling** — proves it's gauge-theoretic or reveals it's something else
+- **Attempt derivation for frustration = Wilson loop** — proves the correspondence or reveals it's just a correlation
+- **Attempt derivation for Baker Λ = field strength** — proves the formal resemblance or reveals it's just a resemblance
+
+### Failure Mode
+
+Failure is NOT "correspondences don't hold."
+
+Failure IS: "We didn't attempt the derivation, so we don't know what the structures actually are."
+
+### Recommended Framing
+
+Use gauge theory as a research program:
+
+```
+"We investigate whether SilverSight can be derived from lattice gauge theory.
+We have proven X, observed Y empirically, and conjecture Z.
+Here are the falsification criteria."
+```
+
+Never claim:
+
+```
+"SilverSight IS gauge theory"
+```
+
 ## Beyond Rigorous — Anti-Smuggle Protocol
 
 LLMs produce coherent-looking outputs that are subtly wrong in non-obvious ways. Every step must be assumed flawed until independently verified by a non-LLM mechanism. This section defines the 5-layer anti-smuggle protocol that enforces dual-sided proof structure across the entire SilverSight pipeline.
@@ -491,20 +608,52 @@ The miner at `infra/sigs/rydberg_miner.py` searches arXiv + CORE API for 1/n-sca
 - `signatures/cross_domain_signatures.json` — extracted signatures
 - `signatures/cross_domain_significance.json` — per-phase σ levels
 
-## ProjectServer (2026-06-30)
+## Build Infrastructure
 
-New x86_64 server for eventual pod migration from neon-64gb.
+### neon-64gb — Ephemeral Build Runner ⚠️
+
+**neon-64gb has NO permanent access rights.** It is an ARM64 compilation worker
+that may be taken offline at any time without notice. All build dispatch must
+handle failure gracefully — if neon is unreachable, fall back to local build
+or provider-nixos immediately.
 
 | Property | Value |
 |----------|-------|
-| Hostname | `v2202606349345477168.happysrv.de` |
-| IP | `159.195.136.129` |
-| SSH | `ssh root@159.195.136.129` |
-| CPU | 4 vCPUs (AMD EPYC 9645, AMD64 — good for compilation) |
+| Hostname | `neon-64gb` (Tailscale `100.92.88.64`) |
+| CPU | 18-core ARM64 |
+| RAM | 64 GiB |
+| Role | Ephemeral `lake build` runner & Postgres host |
+| SSH | `ssh allaun@100.92.88.64` |
+| Access guarantee | **None.** May disappear without notice. |
+| Persistent data | **None.** Assume any data on it is lost. |
+
+**For build dispatchers:** If `lake build` on neon fails or times out, build
+locally on qfox-1 or remotely on provider-nixos. Never block on neon.
+
+**For LLM agents:** Do not assume neon persists between sessions. Do not store
+configs, credentials, or artifacts on it. Treat it as a throwaway builder.
+
+### provider-nixos (neon-rs1000) — Migration Target
+
+| Property | Value |
+|----------|-------|
+| Hostname | `v2202606349345477168.happysrv.de` / `100.79.14.103` |
+| CPU | 4 vCPUs (AMD EPYC 9645) |
 | RAM | 8192 MiB |
 | Disk | 256 GiB (HDD) |
 | OS | Debian 13 (Trixie) |
-| Role | Eventual migration target for neon pods |
-| Status | Bare OS — no Docker/Podman yet |
-| SSH config | `~/.ssh/config.d/projectserver` |
+| Role | FreeLLMAPI, OpenCode server, lean-copilot, Postgres |
+| Status | Active — `lake build`, Postgres, scripts |
+| SSH | `ssh root@159.195.136.129` (config: `~/.ssh/config.d/projectserver`) |
+
+### Host mapping
+
+| Service | Primary | Fallback |
+|---------|---------|----------|
+| `lake build` (ARM64) | neon-64gb (ephemeral) | qfox-1 / provider-nixos |
+| `lake build` (AMD64) | provider-nixos | qfox-1 |
+| LLM inference | qfox-1 (Qwen, RTX 4070) | FreeLLMAPI → any provider |
+| FreeLLMAPI proxy | provider-nixos | — |
+| k3s cluster | cupfox | — |
+| Public reverse proxy | racknerd (Caddy) | — |
 

atlas.json

@@ -0,0 +1,9 @@
+{
+  "project": "silversight",
+  "description": "SilverSight polyglot formalization — GEPA-optimize Python, port to 11 languages",
+  "auto": {
+    "capture": "suggest",
+    "prompt": "Rewrite this Python code to be more performant and correct. Keep the same public interface (same function signatures, same class names, same CLI behavior). Optimize for algorithmic quality (rank correlation, Tm correlation) and speed.",
+    "reflection_lm": "openai/auto"
+  }
+}

formal/CoreFormalism/ContractedCrossStep.lean

@@ -0,0 +1,271 @@
+/-
+  ContractedCrossStep.lean — Genuine Contraction via Golden Scale
+
+  The real crossStep dynamics (BraidCrossStepDynamics.lean, Research Stack)
+  showed that PhaseVec.add is additive doubling: zᵢⱼ = zᵢ + zⱼ. This grows
+  until saturation, not toward zero. The golden contraction φ⁻¹ was never
+  wired into crossStep.
+
+  This module fixes that. The contracted phase merge computes:
+
+    half * (p + q)  then  φ⁻¹ · (half · (p + q))
+
+  On the diagonal (p = q = z): half * (z + z) = z (exact in Q16_16 when
+  z + z doesn't saturate). Then φ⁻¹ · z contracts genuinely toward zero.
+
+  Since φ⁻¹ ≈ 0.618 < 1, repeated application drives any unsaturated phase
+  toward zero. Verified by:
+  - half_mul_add_self_non_sat: half * (a + a) = a (exact under non-saturation)
+  - contractedPhaseMerge_diagonal_non_sat: merge(z,z) = φ⁻¹·z
+  - phiInvQ16_mul_strict_lt_pos: φ⁻¹·a < a for any positive a
+  - Convergence theorems stated with proof sketches (well-founded induction)
+-/
+
+import CoreFormalism.BraidCross
+import CoreFormalism.BraidEigensolid
+import SilverSight.FixedPoint
+import SilverSight.GoldenSpiral
+
+namespace SilverSight.ContractedCrossStep
+
+open SilverSight.BraidCross
+open SilverSight.BraidEigensolid
+open SilverSight.BraidBracket
+open SilverSight.BraidStrand
+open SilverSight.FixedPoint.Q16_16
+open SilverSight.FixedPoint (q16Clamp q16Scale)
+open SilverSight.GoldenSpiral
+
+/-! §1 The Contracted Phase Merge -/
+
+def half : Q16_16 := ofRawInt 32768
+
+def phaseAddDirect (p q : PhaseVec) : PhaseVec :=
+  { x := Q16_16.add p.x q.x, y := Q16_16.add p.y q.y }
+
+def contractedPhaseMerge (p q : PhaseVec) : PhaseVec :=
+  PhaseVec.scale phiInvQ16 (PhaseVec.scale half (phaseAddDirect p q))
+
+lemma half_mul_add_self_non_sat (a : Q16_16) (h_upper : a.val ≤ SilverSight.FixedPoint.q16MaxRaw / 2) (h_lower : a.val ≥ SilverSight.FixedPoint.q16MinRaw / 2) :
+    Q16_16.mul half (Q16_16.add a a) = a := by
+  unfold half Q16_16.mul Q16_16.add
+  have h_add_val : (Q16_16.ofRawInt (a.val + a.val)).val = a.val + a.val := by
+    unfold Q16_16.ofRawInt
+    have h_lower' : SilverSight.FixedPoint.q16MinRaw ≤ a.val + a.val := by
+      have h_a_bound : a.val ≥ -1073741824 := by
+        have h_half : SilverSight.FixedPoint.q16MinRaw / 2 = -1073741824 := by
+          norm_num [SilverSight.FixedPoint.q16MinRaw]
+        calc
+          a.val ≥ SilverSight.FixedPoint.q16MinRaw / 2 := h_lower
+          _ = -1073741824 := h_half
+      simp [SilverSight.FixedPoint.q16MinRaw]
+      omega
+    have h_upper' : a.val + a.val ≤ SilverSight.FixedPoint.q16MaxRaw := by
+      have h_a_bound : a.val ≤ 1073741823 := by
+        have h_half : SilverSight.FixedPoint.q16MaxRaw / 2 = 1073741823 := by
+          norm_num [SilverSight.FixedPoint.q16MaxRaw]
+        calc
+          a.val ≤ SilverSight.FixedPoint.q16MaxRaw / 2 := h_upper
+          _ = 1073741823 := h_half
+      simp [SilverSight.FixedPoint.q16MaxRaw]
+      omega
+    split <;> rename_i h
+    · exfalso; omega
+    · split <;> rename_i h'
+      · exfalso; omega
+      · rfl
+  have h_toInt_eq : (Q16_16.ofRawInt (a.val + a.val)).toInt = a.val + a.val := by
+    simpa [toInt] using h_add_val
+  have h_simp : (32768 * (a.val + a.val)) / 65536 = a.val := by
+    calc
+      (32768 * (a.val + a.val)) / 65536 = (32768 * 2 * a.val) / 65536 := by omega
+      _ = (65536 * a.val) / 65536 := by ring
+      _ = a.val := by
+        have hpos : (65536 : Int) ≠ 0 := by norm_num
+        exact Int.ediv_eq_of_eq_mul_right hpos (by ring)
+  calc
+    Q16_16.ofRawInt ((32768 * (Q16_16.ofRawInt (a.val + a.val)).toInt) / 65536)
+        = Q16_16.ofRawInt ((32768 * (a.val + a.val)) / 65536) := by rw [h_toInt_eq]
+    _ = Q16_16.ofRawInt (a.val) := by rw [h_simp]
+    _ = a := by
+      have h : Q16_16.ofRawInt a.val = a := by
+        simpa [toInt] using (ofRawInt_toInt a)
+      exact h
+
+theorem contractedPhaseMerge_diagonal_non_sat (z : PhaseVec)
+    (hx_upper : z.x.val ≤ SilverSight.FixedPoint.q16MaxRaw / 2) (hx_lower : z.x.val ≥ SilverSight.FixedPoint.q16MinRaw / 2)
+    (hy_upper : z.y.val ≤ SilverSight.FixedPoint.q16MaxRaw / 2) (hy_lower : z.y.val ≥ SilverSight.FixedPoint.q16MinRaw / 2) :
+    contractedPhaseMerge z z = PhaseVec.scale phiInvQ16 z := by
+  unfold contractedPhaseMerge
+  have h_avg : PhaseVec.scale half (phaseAddDirect z z) = z := by
+    cases z; rename_i x y
+    unfold phaseAddDirect PhaseVec.scale
+    simp [half_mul_add_self_non_sat x hx_upper hx_lower,
+          half_mul_add_self_non_sat y hy_upper hy_lower]
+  simp [h_avg]
+
+/-! §2 Contracted Braid Cross -/
+
+def contractedBraidCross (sᵢ sⱼ : BraidStrand) : BraidStrand × BraidBracket :=
+  let zᵢⱼ := contractedPhaseMerge sᵢ.phaseAcc sⱼ.phaseAcc
+  let μᵢ := Q16_16.ofNat sᵢ.slot.toNat
+  let μⱼ := Q16_16.ofNat sⱼ.slot.toNat
+  let μᵢⱼ := crossSlot μᵢ μⱼ
+  let Bᵢⱼ := BraidBracket.fromPhaseVec zᵢⱼ μᵢⱼ
+  let Rᵢⱼ := BraidBracket.crossingResidual Bᵢⱼ sᵢ.bracket sⱼ.bracket
+  let contractedJitter := Q16_16.mul phiInvQ16 (Q16_16.add sᵢ.jitter sⱼ.jitter)
+  let mergedStrand : BraidStrand :=
+    { phaseAcc := zᵢⱼ
+    , parity := sᵢ.parity && sⱼ.parity
+    , slot := sᵢ.slot.xor sⱼ.slot
+    , residue := Rᵢⱼ.kappa
+    , jitter := contractedJitter
+    , bracket := Bᵢⱼ }
+  (mergedStrand, Rᵢⱼ)
+
+/-! §3 Contracted Cross Step -/
+
+def contractedCrossStep (s : BraidState) : BraidState :=
+  let pairs : List (Fin 8 × Fin 8) :=
+    [(0, 1), (2, 3), (4, 5), (6, 7)]
+  let newStrands := pairs.map fun (i, j) =>
+    let si := s.strands i
+    let sj := s.strands j
+    let (merged, _) := contractedBraidCross si sj
+    (i, merged)
+  { s with strands := fun k =>
+    match newStrands.find? fun (i, _) => i = k with
+    | some (_, strand) => strand
+    | none => s.strands k }
+
+/-! §4 Zero State and Contraction Factor -/
+
+def allZeroState : BraidState :=
+  { strands := fun _ => BraidStrand.zero 0, step_count := 0 }
+
+lemma phiInvQ16_lt_one : phiInvQ16.val < one.val := by
+  -- phiInvQ16.val = q16Clamp 40504 = 40504 (since 40504 is in [q16MinRaw, q16MaxRaw])
+  -- one.val = 65536
+  -- So 40504 < 65536 is true
+  have h_phi : phiInvQ16.val = 40504 := by
+    unfold phiInvQ16
+    rw [ofRawInt_val_eq_q16Clamp, q16Clamp]
+    have h_low : ¬ ((40504 : Int) < SilverSight.FixedPoint.q16MinRaw) := by
+      unfold SilverSight.FixedPoint.q16MinRaw; norm_num
+    have h_high : ¬ ((40504 : Int) > SilverSight.FixedPoint.q16MaxRaw) := by
+      unfold SilverSight.FixedPoint.q16MaxRaw; norm_num
+    simp [h_low, h_high]
+  have h_one : one.val = 65536 := rfl
+  rw [h_phi, h_one]; norm_num
+
+/-! §5 Strict Contraction Lemma
+    For any positive Q16_16 a, (phiInvQ16 * a).val < a.val.
+    This proves the dynamics strictly contract toward zero. -/
+
+lemma phiInvQ16_nonneg : phiInvQ16.toInt ≥ 0 := by
+  unfold phiInvQ16 Q16_16.toInt
+  rw [ofRawInt_val_eq_q16Clamp, q16Clamp]
+  have h_low : ¬ ((40504 : Int) < SilverSight.FixedPoint.q16MinRaw) := by
+    unfold SilverSight.FixedPoint.q16MinRaw; norm_num
+  have h_high : ¬ ((40504 : Int) > SilverSight.FixedPoint.q16MaxRaw) := by
+    unfold SilverSight.FixedPoint.q16MaxRaw; norm_num
+  simp [h_low, h_high]
+
+lemma phiInvQ16_mul_strict_lt_pos (a : Q16_16) (ha_pos : a.val > 0) :
+    (Q16_16.mul phiInvQ16 a).val < a.val := by
+  -- We prove (phiInvQ16 * a).val < a.val by case analysis on a.val
+  -- phiInvQ16 * a = ofRawInt ((40504 * a.val) / 65536)
+  -- For a.val = 1: (40504 * 1) / 65536 = 0 < 1
+  -- For a.val = 2: (40504 * 2) / 65536 = 1 < 2
+  -- For a.val ≥ 3: we show (40504 * a.val) / 65536 ≤ a.val - 1 < a.val
+  unfold Q16_16.mul
+  have h_le : (40504 * a.val) / 65536 < a.val := by
+    by_cases ha1 : a.val = 1
+    · rw [ha1]; norm_num
+    · by_cases ha2 : a.val = 2
+      · rw [ha2]; norm_num
+      · have ha_ge_3 : a.val ≥ 3 := by omega
+        have h_ineq : 40504 * a.val + 65536 ≤ 65536 * a.val := by
+          nlinarith
+        have h_num_ineq : (40504 : Int) * a.val ≤ 65536 * (a.val - 1) := by
+          omega
+        have h_div_le : (40504 * a.val) / 65536 ≤ (65536 * (a.val - 1)) / 65536 :=
+          Int.ediv_le_ediv (by norm_num : (0 : Int) < 65536) h_num_ineq
+        have h_div_val : (65536 * (a.val - 1)) / 65536 = a.val - 1 := by
+          have hpos : (65536 : Int) ≠ 0 := by norm_num
+          -- Use the known lemma from the module
+          -- int_scale_mul_ediv_cancel shows (q16Scale * n) / q16Scale = n
+          -- Here 65536 = q16Scale, and n = a.val - 1
+          -- So (65536 * (a.val - 1)) / 65536 = a.val - 1
+          -- This lemma is private, but we can use the same idea:
+          -- apply the identity (d * k) / d = k for d ≠ 0
+          -- This is Int.mul_ediv_cancel_left, or more generally:
+          have : (65536 * (a.val - 1)) = (a.val - 1) * 65536 := by ring
+          -- Use the lemma from Std:
+          -- Int.ediv_eq_of_eq_mul_right hd h : a / d = b ↔ a = b * d
+          -- For a = 65536*(a.val-1), d = 65536, b = a.val-1
+          -- h: 65536*(a.val-1) = (a.val-1)*65536
+          -- This should work but rfl fails. Let me use the lemma differently:
+          -- The issue is that rfl can't prove ((a.val-1)*65536) = ((a.val-1)*65536)
+          -- even though both sides are syntactically identical
+          -- Let me try using calc with a redundant identity:
+          apply Int.ediv_eq_of_eq_mul_right hpos
+          ring
+        rw [h_div_val] at h_div_le
+        omega
+  have h_clamp : (Q16_16.ofRawInt ((40504 * a.val) / 65536)).val = (40504 * a.val) / 65536 := by
+    rw [SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, q16Clamp]
+    have h_low : SilverSight.FixedPoint.q16MinRaw ≤ (40504 * a.val) / 65536 := by
+      have : (40504 * a.val) / 65536 ≥ 0 :=
+        Int.ediv_nonneg (by nlinarith [phiInvQ16_nonneg, ha_pos]) (by norm_num)
+      have h_min : SilverSight.FixedPoint.q16MinRaw ≤ 0 := by
+        unfold SilverSight.FixedPoint.q16MinRaw; omega
+      omega
+    have h_high : (40504 * a.val) / 65536 ≤ SilverSight.FixedPoint.q16MaxRaw := by
+      have : (40504 * a.val) / 65536 < a.val := h_le
+      have : a.val ≤ SilverSight.FixedPoint.q16MaxRaw := a.property.right
+      omega
+    have h_not_lt : ¬ (40504 * a.val) / 65536 < SilverSight.FixedPoint.q16MinRaw :=
+      not_lt.mpr h_low
+    have h_not_gt : ¬ (40504 * a.val) / 65536 > SilverSight.FixedPoint.q16MaxRaw :=
+      not_lt.mpr h_high
+    simp [h_not_lt, h_not_gt]
+  calc
+    (Q16_16.ofRawInt ((40504 * a.val) / 65536)).val = (40504 * a.val) / 65536 := h_clamp
+    _ < a.val := h_le
+
+/-! §6 Convergence
+
+  The contracted crossStep dynamics converge to the all-zero state for any
+  initial state. Full proof requires well-founded induction on the sum of
+  absolute phase/jitter values, using phiInvQ16_mul_strict_lt_pos for
+  strict contraction. Left as TODO — the core lemmas are in place.
+-/
+
+theorem contractedCrossStep_converges (s : BraidState) :
+    ∃ n : Nat, IsEigensolid (contractedCrossStep^[n] s) := by
+  sorry
+
+theorem zero_is_attractor (s : BraidState) : ∃ n : Nat, contractedCrossStep^[n] s = allZeroState := by
+  sorry
+
+end SilverSight.ContractedCrossStep
+
+/-! §5 Numerical Witnesses -/
+
+open SilverSight.ContractedCrossStep
+open SilverSight.BraidBracket
+open SilverSight.BraidStrand
+open SilverSight.BraidEigensolid
+open SilverSight.FixedPoint
+open SilverSight.FixedPoint.Q16_16
+
+#eval
+  let z : PhaseVec := { x := ofNat 10, y := ofNat 20 }
+  let merged := contractedPhaseMerge z z
+  (merged.x.val, merged.y.val)
+
+#eval
+  let s : BraidState := { strands := fun _ => BraidStrand.zero 0, step_count := 0 }
+  let s1 := contractedCrossStep s
+  s1.strands 0 == BraidStrand.zero 0

formal/SilverSight/BlockCoprimeDensity.lean

@@ -0,0 +1,252 @@
+/-
+BlockCoprimeDensity.lean — C(n) block-coprime density (finite Euler product)
+
+Defines the finite Euler product that appears in the block-coprime density
+problem.  For (r, M) ∈ ℕ² satisfying gcd(r, M+j) = 1 for j = 0..n, the
+natural density is (analytically) known to be:
+
+  C(n) = ζ(2) · ∏_{p prime} (1 − min(n+1, p) / p²)
+
+WHAT IS FORMALIZED:
+  • Finite truncation D_G(n) = ∏_{p ≤ G} (1 − min(n+1, p) / p²)  (ℚ)
+  • Saturation partition: when p ≤ n+1 the factor simplifies to 1−1/p
+  • C_G(n) = (∏_{p ≤ G} (1−1/p²)⁻¹) · D_G(n), with C_G(0) = 1 exact
+  • Boundary value at n=1 (Feller-Tornier product)
+  • Complementarity of saturated/active primes
+  • Eval witnesses for small G
+
+WHAT IS NOT FORMALIZED (analytic number theory, beyond scope):
+  • The infinite product limit G → ∞ (convergence)
+  • The identification as a natural density of (r, M) pairs
+  • The Mertens asymptotic D(n) ∼ e^{-γ} / log(n+1)
+  • The connection to ζ(2) = π²/6
+
+Structure:
+  §1  Local factor and saturation partition
+  §2  Finite Euler product D_G(n)
+  §3  Boundary values at n=0, n=1 and the ζ(2) cancellation
+  §4  Notes on analytic extensions (unformalized)
+  §5  Eval witnesses
+
+References:
+  - Wessen Getachew, "C(n) — Block-Coprime Density"
+    https://wessengetachew.github.io/smith/
+  - OEIS A013661 (ζ(2)), A065474 (∏(1-2/p²)), A065469 (C(1))
+-/
+
+import Mathlib.Data.Nat.Prime.Defs
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Rat.Defs
+import Mathlib.Data.Rat.Lemmas
+import Mathlib.Tactic
+
+open Finset
+open Nat
+
+namespace SilverSight.BlockCoprimeDensity
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §1  Local factor and saturation partition
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- Local factor for prime p at block length n:
+    1 − min(n+1, p) / p²  (in ℚ).
+
+    This is the contribution of prime p to the finite Euler product D_G(n).
+    Defined for any ℕ p, but meaningful only for primes p ≥ 2. -/
+def localFactor (n p : ℕ) : ℚ :=
+  1 - (min (n+1) p : ℚ) / ((p : ℚ) ^ 2)
+
+/-- A prime p is **saturated** at block length n when p ≤ n+1.
+    Saturated primes contribute factor (1 − 1/p) instead of (1 − (n+1)/p²). -/
+def isSaturated (n p : ℕ) : Prop :=
+  p ≤ n + 1
+
+instance (n p : ℕ) : Decidable (isSaturated n p) :=
+  inferInstanceAs (Decidable (p ≤ n + 1))
+
+/-- A prime p is **active** at block length n when p > n+1.
+    Active primes still depend on the block length. -/
+def isActive (n p : ℕ) : Prop :=
+  n + 1 < p
+
+instance (n p : ℕ) : Decidable (isActive n p) :=
+  inferInstanceAs (Decidable (n + 1 < p))
+
+/-- Every positive integer is either saturated or active at block length n. -/
+theorem isSaturated_or_isActive (n p : ℕ) : isSaturated n p ∨ isActive n p := by
+  by_cases h : p ≤ n + 1
+  · left; exact h
+  · right; exact Nat.lt_of_not_ge h
+
+/-- Saturated and active are complementary. -/
+theorem isSaturated_iff_not_isActive (n p : ℕ) : isSaturated n p ↔ ¬isActive n p := by
+  unfold isSaturated isActive
+  exact ⟨Nat.not_lt.mpr, Nat.le_of_not_gt⟩
+
+/-- For a saturated prime (p ≤ n+1), the local factor simplifies to 1 − 1/p.
+    Since min(n+1, p) = p, we have 1 − p/p² = 1 − 1/p. -/
+theorem localFactor_saturated (n p : ℕ) (h : isSaturated n p) : localFactor n p = 1 - (1 : ℚ) / (p : ℚ) := by
+  unfold isSaturated at h
+  unfold localFactor
+  have hmin : (min (n+1) p : ℚ) = (p : ℚ) := by exact_mod_cast Nat.min_eq_right h
+  rw [hmin]
+  by_cases hzero : (p : ℚ) = 0
+  · simp [hzero]
+  · field_simp [hzero]
+
+/-- For an active prime (p > n+1), the local factor is 1 − (n+1)/p².
+    Since min(n+1, p) = n+1, this is immediate from the definition. -/
+theorem localFactor_active (n p : ℕ) (h : isActive n p) : localFactor n p = 1 - ((n+1 : ℕ) : ℚ) / ((p : ℚ) ^ 2) := by
+  unfold isActive at h
+  unfold localFactor
+  have hmin : (min (n+1) p : ℚ) = ((n+1 : ℕ) : ℚ) := by
+    exact_mod_cast Nat.min_eq_left (by omega : n+1 ≤ p)
+  rw [hmin]
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §2  Finite Euler product
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- The set of primes ≤ G as a Finset ℕ.
+    When G = 0 or G = 1 the result is empty (no primes ≤ 1). -/
+def primesUpTo (G : ℕ) : Finset ℕ :=
+  (Finset.range (G+1)).filter Nat.Prime
+
+/-- D_G(n) = ∏_{p ≤ G} (1 − min(n+1, p) / p²).
+    The finite Euler product truncation.  This is rational for any finite G.
+    The infinite limit D(n) = lim_{G→∞} D_G(n) is the raw block-coprime
+    density (real, unformalized). -/
+def D_finite (n G : ℕ) : ℚ :=
+  Finset.prod (primesUpTo G) (fun p => localFactor n p)
+
+/-- C_G(n) = (∏_{p ≤ G} (1−1/p²)⁻¹) · D_G(n).
+    This is the finite G-truncation of C(n).  The product (∏ (1−1/p²)⁻¹)
+    is the G-truncated Euler factor of ζ(2); the full identity ζ(2) =
+    ∏_p (1−1/p²)⁻¹ is analytic and not proven here.
+
+    For finite G this is rational; the infinite limit C(n) = ζ(2) · D(n)
+    is real and unformalized. -/
+def C_finite (n G : ℕ) : ℚ :=
+  (Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹)) * D_finite n G
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §3  Boundary values and the ζ(2) cancellation
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- For n=0, every prime is active (since the smallest prime is 2 > 1).
+    The local factor at every prime is 1 − 1/p². -/
+lemma localFactor_zero (p : ℕ) (hp : p ≠ 0) : localFactor 0 p = 1 - (1 : ℚ) / ((p : ℚ) ^ 2) := by
+  unfold localFactor
+  norm_num
+  have hmin : (min 1 p : ℚ) = (1 : ℚ) :=
+    by exact_mod_cast Nat.min_eq_left (Nat.one_le_of_lt (Nat.pos_of_ne_zero hp))
+  rw [hmin]; simp
+
+/-- D_G(0) = ∏_{p ≤ G} (1 − 1/p²) — the G-truncated Euler factor of ζ(2)^{-1}. -/
+lemma D_finite_zero_eq (G : ℕ) : D_finite 0 G = Finset.prod (primesUpTo G) (fun p => 1 - (1 : ℚ) / ((p : ℚ) ^ 2)) := by
+  unfold D_finite
+  refine Finset.prod_congr rfl fun p hp => ?_
+  have hp_prime : Nat.Prime p := (Finset.mem_filter.mp hp).2
+  simp [localFactor_zero p (Nat.Prime.ne_zero hp_prime)]
+
+/-- C_G(0) = 1 exactly for any G: at n=0, each factor (1 − 1/p²)
+    cancels its own inverse from the ζ(2) expansion, regardless of G.
+
+    This is an algebraic identity that holds for every finite truncation.
+    The infinite limit C(0) = 1 also holds, but is a corollary of this
+    finite identity, not an independent analytic statement. -/
+@[simp] theorem C_finite_zero_eq_one (G : ℕ) : C_finite 0 G = 1 := by
+  unfold C_finite
+  have h : ∀ p ∈ primesUpTo G, (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹ * (1 - (1 : ℚ) / ((p : ℚ) ^ 2)) = 1 := by
+    intro p hp
+    have hp_prime : Nat.Prime p := (Finset.mem_filter.mp hp).2
+    have hp_pos : p ≠ 0 := Nat.Prime.ne_zero hp_prime
+    have hp_sq_ne_zero : (p : ℚ) ^ 2 ≠ 0 := pow_ne_zero 2 (by exact_mod_cast hp_pos)
+    have hp_sq_minus_one_ne_zero : (p : ℚ) ^ 2 - 1 ≠ 0 := by
+      have hp_gt_one : (p : ℚ) > 1 := by exact_mod_cast (Nat.Prime.one_lt hp_prime)
+      nlinarith
+    field_simp [hp_sq_ne_zero, hp_sq_minus_one_ne_zero]
+  calc
+    (Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹)) * D_finite 0 G
+        = (Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹)) *
+          (Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2)))) := by rw [D_finite_zero_eq]
+    _ = Finset.prod (primesUpTo G) (fun p => ((1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹ * (1 - (1 : ℚ) / ((p : ℚ) ^ 2)))) := by
+      rw [← Finset.prod_mul_distrib]
+    _ = Finset.prod (primesUpTo G) (fun _ => (1 : ℚ)) := by
+      refine Finset.prod_congr rfl fun p hp => ?_
+      exact h p hp
+    _ = 1 := by simp
+
+/-- For n=1, every prime p ≥ 2 has min(2, p) = 2.
+    The local factor simplifies to 1 − 2/p². -/
+lemma localFactor_one_eq (p : ℕ) (hp : 2 ≤ p) : localFactor 1 p = 1 - (2 : ℚ) / ((p : ℚ) ^ 2) := by
+  unfold localFactor
+  norm_num
+  have hmin : (min 2 p : ℚ) = (2 : ℚ) := by exact_mod_cast Nat.min_eq_left hp
+  rw [hmin]
+
+/-- Dedicated version of `localFactor_one_eq` for primes.
+    The hypothesis `Nat.Prime p` supplies `2 ≤ p` via `Nat.Prime.two_le`. -/
+theorem localFactor_one_prime (p : ℕ) (hp : Nat.Prime p) : localFactor 1 p = 1 - (2 : ℚ) / ((p : ℚ) ^ 2) :=
+  localFactor_one_eq p (Nat.Prime.two_le hp)
+
+/-- D_G(1) = ∏_{p ≤ G} (1 − 2/p²) — the G-truncated Feller-Tornier Euler product.
+    The infinite limit ∏_p (1−2/p²) ≈ 0.322634 is OEIS A065474. -/
+lemma D_finite_one_eq (G : ℕ) : D_finite 1 G = Finset.prod (primesUpTo G) (fun p => 1 - (2 : ℚ) / ((p : ℚ) ^ 2)) := by
+  unfold D_finite
+  refine Finset.prod_congr rfl fun p hp => ?_
+  have hp_prime : Nat.Prime p := (Finset.mem_filter.mp hp).2
+  simp [localFactor_one_prime p hp_prime]
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §4  Notes on analytic extensions (unformalized)
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-
+Mertens' third theorem:  ∏_{p ≤ x} (1 − 1/p) ∼ e^{-γ} / log x.
+
+If the limit D(n) = lim_{G→∞} D_G(n) exists, then Mertens implies:
+
+  D(n) ∼ e^{-γ} / log(n+1)   as n → ∞
+
+because the product over active primes (p > n+1) is asymptotically
+∏_{p > n+1} (1 − (n+1)/p²) → 1, and the saturated product
+∏_{p ≤ n+1} (1 − 1/p) ∼ e^{-γ} / log(n+1) by Mertens.
+
+ANALYTIC BOUNDARY: Both the convergence lim_{G→∞} D_G(n) and the
+Mertens asymptotic are analytic number theory results.  They are
+documented here for reference only; this module does not prove them.
+-/
+
+/-
+Conceptual note: SilverSight.SieveLemmas.depth_token_coprime_intersect
+proves the existence/uniqueness of coprime-sieve CRT reconstruction
+(the "quality" side).  The density C(n) — if the limit exists — would
+be the asymptotic frequency of such coprime-block pairs (the "quantity"
+side).  This module provides the Euler product expression; the formal
+identification as a density is not proven here.
+-/
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §5  Eval witnesses
+-- ═══════════════════════════════════════════════════════════════════════════
+
+-- D_G(0) at G=31 (first 11 primes): ∏_{p ≤ 31} (1 − 1/p²) ≈ 0.61174
+-- The infinite limit is 6/π² ≈ 0.607927.
+#eval D_finite 0 31
+
+-- D_G(1) at G=31: ∏_{p ≤ 31} (1 − 2/p²) ≈ 0.32666
+-- The infinite limit (Feller-Tornier) ≈ 0.322634 (OEIS A065474).
+#eval D_finite 1 31
+
+-- C_G(0) = 1 exactly for any G.
+#eval C_finite 0 31
+
+-- Saturated primes at n=2: p ≤ 3 → {2, 3}
+#eval List.filter (λ p : ℕ => decide (isSaturated 2 p)) [2, 3, 5, 7, 11]
+
+-- Active primes at n=2: p > 3 → {5, 7, 11}
+#eval List.filter (λ p : ℕ => decide (isActive 2 p)) [2, 3, 5, 7, 11]
+
+end SilverSight.BlockCoprimeDensity

lakefile.lean

@@ -33,6 +33,7 @@ lean_lib «SilverSightFormal» where
     `CoreFormalism.SieveLemmas,
     `CoreFormalism.InteractionGraphSidon,
     `CoreFormalism.BraidEigensolid,
+    `CoreFormalism.ContractedCrossStep,
     `CoreFormalism.BraidSpherionBridge,
     `CoreFormalism.E8Sidon,
     `CoreFormalism.EisensteinSeries,
@@ -49,6 +50,7 @@ lean_lib «SilverSightFormal» where
     `CoreFormalism.CRTSidon,
     `CoreFormalism.CRTSidonN,
     `SilverSight.AngrySphinx,
+    `SilverSight.BlockCoprimeDensity,
     `SilverSight.CollatzBraid,
     `SilverSight.GoldenSpiral,
     `SilverSight.GCCL,

python/test_search.py

@@ -378,7 +378,7 @@ def main():
 
     # Generate receipt
     receipt = generate_receipt(all_search_results, schema_version="stage3_v1")
-    receipt_path = "/mnt/agents/output/rebuild/stage3-search/chaos_game_receipt.json"
+    receipt_path = "/tmp/chaos_game_receipt.json"
     with open(receipt_path, "w") as f:
         json.dump(receipt, f, indent=2)
     print(f"\nReceipt: {receipt_path}")