diff --git a/AGENTS.md b/AGENTS.md index bd20e062..399ccb39 100644 --- a/AGENTS.md +++ b/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) | — | diff --git a/formal/SilverSight/BlockCoprimeDensity.lean b/formal/SilverSight/BlockCoprimeDensity.lean new file mode 100644 index 00000000..d35f0d29 --- /dev/null +++ b/formal/SilverSight/BlockCoprimeDensity.lean @@ -0,0 +1,224 @@ +/- +BlockCoprimeDensity.lean — C(n) block-coprime density + +Formalizes the Euler product for the natural density of pairs (r, M) ∈ ℕ² +satisfying the block-coprime condition gcd(r, M+j) = 1 for all j = 0..n. + +C(n) = ζ(2) · ∏_{p prime} (1 − min(n+1, p) / p²) + +Structure: + §1 Local factor and saturation partition + §2 Finite Euler product D_G(n) = ∏_{p ≤ G} (1 − min(n+1, p) / p²) + §3 Boundary values at n=0, n=1 and the ζ(2) connection + §4 Asymptotic D(n) ∼ e^{-γ} / log(n+1) (Mertens) + §5 Bridge to SieveLemmas coprime-sieve reconstruction + §6 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)) + - SilverSight.SieveLemmas (CRT coprime-sieve reconstruction) + - SilverSight.CRTSidon (CRT torus preserves Sidon property) +-/ + +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 Euler product D(n). -/ +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 their ζ(2) factor (1 − 1/p²) instead of + the active factor (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)) + +/-- For a saturated prime (p ≤ n+1), the local factor simplifies to 1 − 1/p. + Since min(n+1, p) = p, the factor 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². -/ +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 ℕ. -/ +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 of the raw block-coprime density D(n). -/ +def D_finite (n G : ℕ) : ℚ := + Finset.prod (primesUpTo G) (fun p => localFactor n p) + +/-- C_G(n) = ζ(2) · D_G(n). + Uses the Euler product identity ζ(2) = ∏_p (1 − 1/p²)^{-1}: + + C_G(n) = (∏_{p ≤ G} (1-1/p²)^{-1}) · (∏_{p ≤ G} (1 − min(n+1, p)/p²)) + + For finite G this is rational; the infinite limit C(n) is real. -/ +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) connection +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- 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_finite(0, G) = ∏_{p ≤ G} (1 − 1/p²) — the 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: at n=0, each factor (1 − 1/p²) cancels its own inverse + from the ζ(2) expansion. -/ +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 is 1 − 2/p² for all primes. -/ +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] + +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_finite(1, G) = ∏_{p ≤ G} (1 − 2/p²) — the Feller-Tornier Euler product. -/ +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 Asymptotic (Mertens theorem) +-- ═══════════════════════════════════════════════════════════════════════════ + +/- +Mertens' third theorem: ∏_{p ≤ x} (1 − 1/p) ∼ e^{-γ} / log x. + +This implies: D(n) = C(n)/ζ(2) ∼ e^{-γ} / log(n+1). + +The analytic proof is beyond the scope of this finite formalization. +The constant is documented here as a reference. +-/ + +/-- Approximate Mertens constant e^{-γ} ≈ 0.561459483566885 as a ℚ fraction. -/ +def mertensConstant : ℚ := 561459483566885 / 1000000000000000 + +/-- Approximate asymptotic D(n) ∼ e^{-γ} / log(n+1). + The log(n+1) denominator is represented as the rational (n+1) for + the reciprocal scaling; the exact analytic formula is real-valued. -/ +def asymptoticBound (n : ℕ) : ℚ := + mertensConstant / ((n+1 : ℕ).succ : ℚ) + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §5 Bridge to SieveLemmas +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- +SilverSight.SieveLemmas.depth_token_coprime_intersect proves the existence +and uniqueness side: two coprime sieve observers reconstruct the coordinate +modulo ℓ₁·ℓ₂. This module provides the density side: C(n) gives the asymptotic +frequency of (r, M) pairs satisfying the block-coprime condition. + +SieveLemmas: coprime observers reconstruct the coordinate (quality) +This module: C(n) gives the density of coprime-block pairs (quantity) +-/ +def densityBridgeNote : String := + "C(n) is the density analogue of SieveLemmas.depth_token_coprime_intersect" + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §6 Eval witnesses +-- ═══════════════════════════════════════════════════════════════════════════ + +-- D_finite(0, 31) = ∏_{p ≤ 31} (1 − 1/p²) ≈ 0.607927 (as ℚ) +#eval D_finite 0 31 + +-- D_finite(1, 31) = ∏_{p ≤ 31} (1 − 2/p²) ≈ 0.322634 (Feller-Tornier) +#eval D_finite 1 31 + +-- C_finite(0, 31) = 1 exactly (ζ(2) cancels) +#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 diff --git a/lakefile.lean b/lakefile.lean index 29108441..ecffbbac 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -50,6 +50,7 @@ lean_lib «SilverSightFormal» where `CoreFormalism.CRTSidon, `CoreFormalism.CRTSidonN, `SilverSight.AngrySphinx, + `SilverSight.BlockCoprimeDensity, `SilverSight.CollatzBraid, `SilverSight.GoldenSpiral, `SilverSight.GCCL,