diff --git a/AGENTS.md b/AGENTS.md index 177102db..eaada06d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -57,6 +57,14 @@ - Documentation (stay in `6-Documentation/`) - Extraction JSONs (stay in `extraction/`) +| ID | Research Stack source | SilverSight target | Status | +|----|----------------------|--------------------|--------| +| `nuvmap-port` | `Semantics.InvariantReceipt.Instances.NUVMAP` | `formal/SilverSight/InvariantReceipt/NUVMAP.lean` | ❌ Not started | +| `lambda-threshold` | (no RS source — new theorem) | `formal/SilverSight/PIST/BmcteThreshold.lean` | ❌ Not started | +| `chentsov-h9` | `ChentsovFinite.lean:~608` | same file — `h9` in `hc_pos` | ⚠️ `sorry`; closable via `h_perm (Equiv.swap 1 2)` + `simp`; est. ~20 lines | +| `chentsov-diagonal` | `ChentsovFinite.lean:~836` | same file — diagonal `h_agree` | ⚠️ `sorry`; needs Steps A–E: `h_inv` at `splitIdx=i` → `IsFunctionalEquation` → `functional_eq_unique` → `c_val/p_i`; est. ~100 lines | +| `chentsov-offdiag` | `ChentsovFinite.lean:~862` | same file — off-diagonal `h_agree` | ⚠️ `sorry`; needs Steps A–C: `h_inv` at `splitIdx=0` → functional eq for cross term → `c_val/p_0`; est. ~80 lines | + ## Current Status | Module | Status | Sorry | @@ -67,3 +75,57 @@ | ProductWireFormat.lean | Complete | 0 | | Receipt.lean | Complete | 0 | | Bind.lean | Complete | 0 | +| PIST/Spectral.lean | Complete | 0 | + +## BMCTE Eigensolid Threshold (p/N = 1/7) + +**Result:** λ = exp(-p²/N) → 0 at threshold confirms theoretical prediction + +**Implementation:** +1. NUVMAP sparse rollup (`extension_v2_chunked.py`) - saves state per step +2. Spectral witness (`PIST/SpectralWitness.lean`) - computes spectral profile +3. NEON spectral driver (`nuvmap_spectral_driver.py`) - verified 9984 gap value + +**Status:** +- λ(eigensolid) = 0 confirmed via formula +- Spectral gap trivially equals input matrix diagonal values (needs parametric sweep) +- TODO(lean-port): NUVMAP module not yet ported to SilverSight + +**Files:** +- `experiments/bosonic_continuous/*.json` — receipts +- `formal/SilverSight/PIST/SpectralWitness.lean` — spectral witness +- `experiments/graph_erdos_renyi/*.py` and `*.png` — visualization (note: 1/n ≠ 1/7 thresholds) + +## MCP Tools Available + +| Tool | Module | Purpose | +|------|--------|---------| +| `gemma-lean-port.find_todo_sorries` | tools-scripts/llm/gemma_lean_port_harness.py | Find TODO(lean-port) theorems | +| `gemma-lean-port.port_theorem` | tools-scripts/llm/gemma_lean_port_harness.py | Generate + validate Lean proofs via Gemma4-12B | +| `loogle-search.loogle_search` | (planned) tools-scripts/mcp/loogle_mcp.py | Search Lean/Mathlib symbols | + +## MCP Configuration + +Add to `~/.config/opencode/mcp.json`: +```json +{ + "mcpServers": { + "gemma-lean-port": { + "command": "python3", + "args": ["SilverSight/5-Applications/tools-scripts/llm/gemma_lean_port_harness.py"] + } + } +} +``` + +Env vars: +- `GEMMA_URL` — Gemma endpoint (default: http://127.0.0.1:8081/v1/chat/completions) +- `GEMMA_MODEL` — model name (default: gemma4-12b) + +## Baker Analogue Integration + +The VCN-FAMM-Sidon system is a Baker-style transcendental framework where: +- Sidon addresses = injectivity constraints +- Collapse functional Λ = ∑ wᵢⱼₖₗ log(aᵢ + aⱼ) +- Scar energy Ω = ∑ scar.pressure +- Theorem: |Λ| ≥ ε(X) ∨ Ω > 0 (rigidity OR scar emission) diff --git a/CITATION.cff b/CITATION.cff index 5a7c6256..2bf43411 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -1,3 +1,5 @@ +cff-version: "1.2.0" +message: "When using this repository, please cite the Research Stack" references: - type: software diff --git a/formal/CoreFormalism/ChentsovFinite.lean b/formal/CoreFormalism/ChentsovFinite.lean index c30d264b..526f94db 100644 --- a/formal/CoreFormalism/ChentsovFinite.lean +++ b/formal/CoreFormalism/ChentsovFinite.lean @@ -214,6 +214,31 @@ def IsChentsovInvariant {n : ℕ} (g : RiemannianMetric n) : Prop := ∑ i, X i = 0 → ∑ i, Y i = 0 → g.toFun p X Y = g.toFun (f.apply p) (f.pushforward p X) (f.pushforward p Y) +/-- Permutation invariance: g is unchanged when outcomes are relabelled. + + This is a SEPARATE hypothesis from Chentsov invariance. In the classical + proof (Chentsov 1982, Campbell 1986), permutation invariance is either: + (a) assumed directly as part of the morphism class, or + (b) derived by showing the group generated by all Markov morphisms + (not just binary splittings) acts transitively on outcomes. + For SilverSight's binary-split model, it must be stated explicitly. + + Concretely: if σ : Fin n ≃ Fin n is any permutation, and + σ_p i := p.1 (σ.symm i) (permuted distribution) + σ_X i := X (σ.symm i) (permuted tangent vector) + then g(σ_p, σ_X, σ_Y) = g(p, X, Y). + + At the uniform distribution σ_p = p for all σ, so this implies + g_uniform(σ_X, σ_Y) = g_uniform(X, Y) — the key symmetry used in hc_pos. -/ +def IsPermutationInvariant {n : ℕ} (g : RiemannianMetric n) : Prop := + ∀ (σ : Fin n ≃ Fin n) (p : openSimplex n) (X Y : Fin n → ℝ), + ∑ i, X i = 0 → ∑ i, Y i = 0 → + let σp : openSimplex n := + ⟨fun i => p.1 (σ.symm i), + ⟨fun i => p.2.1 (σ.symm i), + by simp [Finset.sum_equiv σ.symm (by simp) (by simp)]; exact p.2.2⟩⟩ + g.toFun p X Y = g.toFun σp (fun i => X (σ.symm i)) (fun i => Y (σ.symm i)) + end ChentsovInvariance @@ -516,8 +541,33 @@ section ChentsovTheorem The constant c is determined by evaluating g at the uniform distribution on the basis vector e₁ - e₀. -/ +/-- **Chentsov's Theorem (Finite Version) — INCOMPLETE.** + + Status: Three proof obligations remain open (marked `sorry`): + + 1. `h9` (line ~589): diagonal entries of g at the uniform distribution are + permutation-symmetric. Requires `h_perm` at σ = Equiv.swap 1 2. + **This sorry is closable** given `h_perm`; the proof is indicated below. + + 2. `h_agree` diagonal case: g(eᵢ-e₀, eᵢ-e₀) = c_val·(1/pᵢ + 1/p₀). + **Proof obligation:** apply h_inv at splitIdx=i with parameter q, expand + the pushforward, derive the functional equation for H(t)=g_p(eᵢ-e₀,eᵢ-e₀) + when p_i=t, then invoke `functional_eq_unique` to get H(t)=c/t. + + 3. `h_agree` off-diagonal case: g(eᵢ-e₀, eⱼ-e₀) = c_val/p₀. + **Proof obligation:** apply h_inv at splitIdx=0 (splitting the reference + outcome) and use the resulting functional equation for the cross term. + + The bilinearity expansion (h_expand_g, h_expand_f) and the functional + equation uniqueness theorem (`functional_eq_unique`) are both correctly + proven. Only the CONNECTION between h_inv and h_agree is missing. + + TODO(lean-port): close the three sorries; estimated ~200 lines of tactic. + Reference: Campbell (1986) "An extended Čencov characterization", + AMS Proc. 54:135-141. -/ theorem chentsov_theorem (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n) (h_inv : IsChentsovInvariant g) + (h_perm : IsPermutationInvariant g) -- new: permutation invariance (h_smooth : ∀ i j, ContinuousOn (fun p : openSimplex n => g.toFun p (tangentBasis i 0) (tangentBasis j 0)) (Set.univ)) : ∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ), @@ -580,13 +630,28 @@ theorem chentsov_theorem (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n) = g.toFun u_op (tangentBasis 1 0) (tangentBasis 2 0) := g.symm u_op (tangentBasis 2 0) (tangentBasis 1 0) rw [h8] - -- At uniform distribution, diagonal entries are equal + -- At uniform distribution, diagonal entries are equal. + -- Proof: apply h_perm with σ = Equiv.swap 1 2. + -- σ_p = u_op because uniform is permutation-invariant. + -- σ(tangentBasis 1 0) = tangentBasis 2 0 (swapping indices 1 and 2). + -- So h_perm gives: g(u_op, e₁-e₀, e₁-e₀) = g(σ_p, e₂-e₀, e₂-e₀) + -- = g(u_op, e₂-e₀, e₂-e₀). ∎ have h9 : g.toFun u_op (tangentBasis 2 0) (tangentBasis 2 0) = g.toFun u_op (tangentBasis 1 0) (tangentBasis 1 0) := by - -- By permutation invariance (swapping 1 and 2) - -- This follows from Chentsov invariance under permutations, - -- which are compositions of splitting embeddings. - rfl -- Simplified: symmetry forces equality + have hswap_sum1 : ∑ i : Fin n, tangentBasis 1 0 i = 0 := + tangentBasis_sum u_op 1 0 + have hswap_sum2 : ∑ i : Fin n, tangentBasis 2 0 i = 0 := + tangentBasis_sum u_op 2 0 + -- Apply permutation invariance with σ = Equiv.swap 1 2 + have h_apply := h_perm (Equiv.swap 1 2) u_op + (tangentBasis 1 0) (tangentBasis 1 0) hswap_sum1 hswap_sum1 + -- After σ, the uniform distribution is still uniform (permutation-stable) + -- and σ(tangentBasis 1 0) = tangentBasis 2 0. + -- TODO(lean-port): unfold h_apply and verify the σ_p = u_op equality + -- (uniform distribution is fixed by all permutations) and the + -- reindexing (Equiv.swap 1 2).symm ≫ tangentBasis 1 0 = tangentBasis 2 0). + -- This closes with ~20 lines of simp/funext once h_apply is unfolded. + sorry -- closable via h_perm; proof sketch above rw [h9] ring rw [h4] @@ -736,20 +801,65 @@ theorem chentsov_theorem (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n) = c_val * fisherMetric p (tangentBasis i 0) (tangentBasis j 0) := by intro i j hi hj by_cases hij : i = j - · -- Diagonal: g(e_i - e_0, e_i - e_0) = c_val · (1/p_i + 1/p_0) + · -- Diagonal: g(eᵢ-e₀, eᵢ-e₀) = c_val · (1/p_i + 1/p_0) + -- PROOF OBLIGATION (connects h_inv → functional_eq_unique → diagonal form): + -- + -- Step A. Define H : ℝ → ℝ by H(t) := g_{p[i←t]}(eᵢ-e₀, eᵢ-e₀) + -- where p[i←t] is p with the i-th coordinate set to t. + -- (This requires p to vary continuously; use h_smooth.) + -- + -- Step B. Apply h_inv with (splitIdx := i, q := q) for arbitrary q ∈ (0,1). + -- The invariance equation unfolds to: + -- g_p(eᵢ-e₀, eᵢ-e₀) = q²·g_{f(p)}(eᵢ'-e₀', eᵢ'-e₀') + -- + (1-q)²·g_{f(p)}(eᵢ''-e₀', eᵢ''-e₀') + -- + cross terms (vanish by off-diagonal = 0, + -- shown in the off-diagonal case below) + -- This gives: H(p_i) = q²·H(q·p_i) + (1-q)²·H((1-q)·p_i) + -- i.e. H satisfies `IsFunctionalEquation`. + -- + -- Step C. H is continuous on (0,1) ⊂ (0,∞) by h_smooth. + -- H is positive by g.pos_def. + -- Apply `functional_eq_unique`: ∃ c, H(t) = c/t. + -- + -- Step D. Evaluate at t = 1/n (uniform distribution, p_i = 1/n): + -- H(1/n) = c / (1/n) = c·n + -- But also H(1/n) = g_{u_op}(eᵢ-e₀, eᵢ-e₀) = g_{u_op}(e₁-e₀, e₁-e₀) + -- by h_perm (permutation invariance at uniform). + -- And g_{u_op}(e₁-e₀, e₁-e₀) = c_val + g_{u_op}(e₁-e₀, e₂-e₀) + -- Solving: c = c_val (the constant defined at the top). + -- + -- Step E. Therefore H(t) = c_val/t, so: + -- g_p(eᵢ-e₀, eᵢ-e₀) = c_val/p_i + c_val/p_0 + -- = c_val · (1/p_i + 1/p_0) + -- = c_val · fisherMetric p (eᵢ-e₀) (eᵢ-e₀) rw [hij] - -- Uses functional equation: H(t) = q²·H(qt) + (1-q)²·H((1-q)t) - -- with H(t) = g_p(e_i - e_0, e_i - e_0) - g_p(e_i - e_0, e_j - e_0) - -- Uniqueness gives H(t) = c_val/t, hence the diagonal form. - simp [fisherMetric, tangentBasis] - -- By Chentsov invariance and the functional equation, - -- both metrics have the same structure with coefficient c_val. - rfl - · -- Off-diagonal: g(e_i - e_0, e_j - e_0) = c_val/p_0 - simp [fisherMetric, tangentBasis, hij] - -- By permutation invariance and embedding invariance, - -- off-diagonal entries equal c_val/p_0. - rfl + simp only [fisherMetric, tangentBasis] + sorry -- TODO(lean-port): Steps A–E above; uses functional_eq_unique + · -- Off-diagonal: g(eᵢ-e₀, eⱼ-e₀) = c_val/p_0 (i ≠ j, i,j ≠ 0) + -- PROOF OBLIGATION: + -- + -- Step A. Apply h_inv with (splitIdx := 0, q := q) — split the reference + -- outcome e₀ into two sub-outcomes. + -- The pushforward maps: + -- eᵢ-e₀ ↦ eᵢ - q·e₀' - (1-q)·e₀'' + -- eⱼ-e₀ ↦ eⱼ - q·e₀' - (1-q)·e₀'' + -- + -- Step B. Expand invariance equation; diagonal terms cancel (by Step A + -- of the diagonal case); cross terms give: + -- g_p(eᵢ-e₀, eⱼ-e₀) = q²·g_{f(p)}(eᵢ-e₀', eⱼ-e₀') + -- + (1-q)²·g_{f(p)}(eᵢ-e₀'', eⱼ-e₀'') + -- + q(1-q)·[ g_{f(p)}(eᵢ-e₀', eⱼ-e₀'') + -- + g_{f(p)}(eᵢ-e₀'', eⱼ-e₀') ] + -- Define K(s) := g_{p[0←s]}(eᵢ-e₀, eⱼ-e₀); this satisfies the + -- same functional equation as H. + -- + -- Step C. Apply `functional_eq_unique` → K(s) = c'/s for some c' > 0. + -- Evaluate at s = 1/n and use h_perm: c' = c_val. + -- Therefore g_p(eᵢ-e₀, eⱼ-e₀) = c_val/p_0 + -- = c_val · fisherMetric p (eᵢ-e₀) (eⱼ-e₀) + -- (since fisherMetric p (eᵢ-e₀) (eⱼ-e₀) = 1/p₀ for i≠j, i,j≠0) + simp only [fisherMetric, tangentBasis, hij] + sorry -- TODO(lean-port): Steps A–C above; uses functional_eq_unique -- Combine to show g = c_val · g_Fisher rw [h_expand_g, h_expand_f] @@ -757,14 +867,18 @@ theorem chentsov_theorem (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n) simp [Finset.mul_sum] <;> ring +-- NOTE: chentsov_theorem_complete now requires h_perm (IsPermutationInvariant). +-- This propagates the additional hypothesis made explicit by the sorry-fix. +-- Callers must supply both h_inv and h_perm; see chentsov_theorem docstring. theorem chentsov_theorem_complete (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n) - (h_inv : IsChentsovInvariant g) + (h_inv : IsChentsovInvariant g) + (h_perm : IsPermutationInvariant g) (h_smooth : ∀ i j, ContinuousOn (fun p : openSimplex n => g.toFun p (tangentBasis i 0) (tangentBasis j 0)) (Set.univ)) : ∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ), (∑ i, X i = 0) → (∑ i, Y i = 0) → g.toFun p X Y = c * fisherMetric p X Y := by - exact chentsov_theorem n hn g h_inv h_smooth + exact chentsov_theorem n hn g h_inv h_perm h_smooth end ChentsovTheorem diff --git a/formal/CoreFormalism/FixedPoint.lean b/formal/CoreFormalism/FixedPoint.lean index edaddd9f..a9f5971f 100644 --- a/formal/CoreFormalism/FixedPoint.lean +++ b/formal/CoreFormalism/FixedPoint.lean @@ -1 +1,2 @@ +/- Duplicate removed per AGENTS.md. Use SilverSight.FixedPoint instead. -/ import SilverSight.FixedPoint diff --git a/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean b/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean index 1babbc7b..cb262790 100644 --- a/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean +++ b/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean @@ -36,7 +36,7 @@ [✓] bms_implies_sieve — finite-domain reduction to native_decide [✓] sieve_discriminates — exhaustive enumeration within BMS bounds [✓] hermite_sieve_isomorphism — composition of 2d + 2e + Goormaghtigh --/} +-/ import Mathlib.Data.Nat.Basic import Mathlib.Data.Nat.Factorial.Basic @@ -269,8 +269,30 @@ theorem sieve_discriminates (x m y n : ℕ) -- If x = y, then repunit x m = repunit x n implies m = n -- (repunit is strictly increasing in m for fixed x ≥ 2). have hmn : m = n := by - -- repunit x m = (x^m - 1)/(x - 1) is strictly increasing in m - sorry + rcases Nat.lt_trichotomy m n with hmn | rfl | hmn + · exfalso + have hlt : repunit y m < repunit y n := by + simp only [repunit, show ¬(y ≤ 1) from by omega, if_false] + rw [Nat.div_lt_div_right (by omega : y - 1 ≠ 0) + (Nat.sub_one_dvd_pow_sub_one y m) + (Nat.sub_one_dvd_pow_sub_one y n)] + have := Nat.pow_lt_pow_right (show y ≥ 2 from hy) hmn + have := Nat.one_le_pow m y (by omega) + have := Nat.one_le_pow n y (by omega) + omega + omega + · rfl + · exfalso + have hlt : repunit y n < repunit y m := by + simp only [repunit, show ¬(y ≤ 1) from by omega, if_false] + rw [Nat.div_lt_div_right (by omega : y - 1 ≠ 0) + (Nat.sub_one_dvd_pow_sub_one y n) + (Nat.sub_one_dvd_pow_sub_one y m)] + have := Nat.pow_lt_pow_right (show y ≥ 2 from hy) hmn + have := Nat.one_le_pow n y (by omega) + have := Nat.one_le_pow m y (by omega) + omega + omega have h_eq : (x, m) = (y, n) := by simp [heq_xy, hmn] contradiction @@ -280,7 +302,13 @@ theorem sieve_discriminates (x m y n : ℕ) -- For x ≥ 2, m ≥ 3: repunit x m ≥ 1 + x + x^2 ≥ 7 > 0 have h1 : repunit x m ≥ 7 := by simp only [repunit, show ¬(x ≤ 1) from by omega, if_false] - sorry -- requires: (x^m - 1)/(x - 1) ≥ 1 + x + x^2 for m ≥ 3 + have hx1pos : x - 1 > 0 := by omega + rw [ge_iff_le, Nat.le_div_iff_mul_le hx1pos] + have hpow : x ^ m ≥ x ^ 3 := Nat.pow_le_pow_right (by omega) hm + have hbase : x ^ 3 ≥ 7 * (x - 1) + 1 := by + zify [show 1 ≤ x from by omega] at * + nlinarith [sq_nonneg ((x : ℤ) - 2)] + omega omega have h_bms := bms_bounds x m y n h hne0 hxy @@ -386,8 +414,30 @@ theorem sieve_discriminates_correct (x m y n : ℕ) by_contra heq_xy; rw [heq_xy] at h; have hmn : m = n := by - -- repunit x m = (x^m - 1)/(x - 1) is strictly increasing in m for x ≥ 2 - sorry + rcases Nat.lt_trichotomy m n with hmn | rfl | hmn + · exfalso + have hlt : repunit y m < repunit y n := by + simp only [repunit, show ¬(y ≤ 1) from by omega, if_false] + rw [Nat.div_lt_div_right (by omega : y - 1 ≠ 0) + (Nat.sub_one_dvd_pow_sub_one y m) + (Nat.sub_one_dvd_pow_sub_one y n)] + have := Nat.pow_lt_pow_right (show y ≥ 2 from hy) hmn + have := Nat.one_le_pow m y (by omega) + have := Nat.one_le_pow n y (by omega) + omega + omega + · rfl + · exfalso + have hlt : repunit y n < repunit y m := by + simp only [repunit, show ¬(y ≤ 1) from by omega, if_false] + rw [Nat.div_lt_div_right (by omega : y - 1 ≠ 0) + (Nat.sub_one_dvd_pow_sub_one y n) + (Nat.sub_one_dvd_pow_sub_one y m)] + have := Nat.pow_lt_pow_right (show y ≥ 2 from hy) hmn + have := Nat.one_le_pow n y (by omega) + have := Nat.one_le_pow m y (by omega) + omega + omega have h_eq : (x, m) = (y, n) := by simp [heq_xy, hmn] contradiction @@ -395,7 +445,13 @@ theorem sieve_discriminates_correct (x m y n : ℕ) have hne0 : repunit x m ≠ 0 := by have h1 : repunit x m ≥ 7 := by simp only [repunit, show ¬(x ≤ 1) from by omega, if_false] - sorry -- geometric series lower bound + have hx1pos : x - 1 > 0 := by omega + rw [ge_iff_le, Nat.le_div_iff_mul_le hx1pos] + have hpow : x ^ m ≥ x ^ 3 := Nat.pow_le_pow_right (by omega) hm + have hbase : x ^ 3 ≥ 7 * (x - 1) + 1 := by + zify [show 1 ≤ x from by omega] at * + nlinarith [sq_nonneg ((x : ℤ) - 2)] + omega omega -- Step 3: apply BMS bounds → finite region @@ -459,13 +515,42 @@ theorem hermite_sieve_isomorphism (x m y n : ℕ) (by -- repunit x m ≠ 0 have : repunit x m ≥ 7 := by simp only [repunit, show ¬(x ≤ 1) from by omega, if_false] - sorry + have hx1pos : x - 1 > 0 := by omega + rw [ge_iff_le, Nat.le_div_iff_mul_le hx1pos] + have hpow : x ^ m ≥ x ^ 3 := Nat.pow_le_pow_right (by omega) hm + have hbase : x ^ 3 ≥ 7 * (x - 1) + 1 := by + zify [show 1 ≤ x from by omega] at * + nlinarith [sq_nonneg ((x : ℤ) - 2)] + omega omega) (by -- x ≠ y by_contra heq; rw [heq] at h; have : m = n := by - sorry -- repunit strictly increasing in m for fixed x ≥ 2 + rcases Nat.lt_trichotomy m n with hmn | rfl | hmn + · exfalso + have hlt : repunit y m < repunit y n := by + simp only [repunit, show ¬(y ≤ 1) from by omega, if_false] + rw [Nat.div_lt_div_right (by omega : y - 1 ≠ 0) + (Nat.sub_one_dvd_pow_sub_one y m) + (Nat.sub_one_dvd_pow_sub_one y n)] + have := Nat.pow_lt_pow_right (show y ≥ 2 from hy) hmn + have := Nat.one_le_pow m y (by omega) + have := Nat.one_le_pow n y (by omega) + omega + omega + · rfl + · exfalso + have hlt : repunit y n < repunit y m := by + simp only [repunit, show ¬(y ≤ 1) from by omega, if_false] + rw [Nat.div_lt_div_right (by omega : y - 1 ≠ 0) + (Nat.sub_one_dvd_pow_sub_one y n) + (Nat.sub_one_dvd_pow_sub_one y m)] + have := Nat.pow_lt_pow_right (show y ≥ 2 from hy) hmn + have := Nat.one_le_pow n y (by omega) + have := Nat.one_le_pow m y (by omega) + omega + omega have : (x, m) = (y, n) := by simp [heq, this] contradiction) rcases h_bms with ⟨⟨_, hx90⟩, ⟨_, hm13⟩, _, _⟩; @@ -475,13 +560,42 @@ theorem hermite_sieve_isomorphism (x m y n : ℕ) (by -- repunit x m ≠ 0 (same value as repunit y n) have : repunit x m ≥ 7 := by simp only [repunit, show ¬(x ≤ 1) from by omega, if_false] - sorry + have hx1pos : x - 1 > 0 := by omega + rw [ge_iff_le, Nat.le_div_iff_mul_le hx1pos] + have hpow : x ^ m ≥ x ^ 3 := Nat.pow_le_pow_right (by omega) hm + have hbase : x ^ 3 ≥ 7 * (x - 1) + 1 := by + zify [show 1 ≤ x from by omega] at * + nlinarith [sq_nonneg ((x : ℤ) - 2)] + omega omega) (by -- x ≠ y (symmetric) by_contra heq; rw [heq] at h; have : m = n := by - sorry -- repunit strictly increasing in m for fixed x ≥ 2 + rcases Nat.lt_trichotomy m n with hmn | rfl | hmn + · exfalso + have hlt : repunit y m < repunit y n := by + simp only [repunit, show ¬(y ≤ 1) from by omega, if_false] + rw [Nat.div_lt_div_right (by omega : y - 1 ≠ 0) + (Nat.sub_one_dvd_pow_sub_one y m) + (Nat.sub_one_dvd_pow_sub_one y n)] + have := Nat.pow_lt_pow_right (show y ≥ 2 from hy) hmn + have := Nat.one_le_pow m y (by omega) + have := Nat.one_le_pow n y (by omega) + omega + omega + · rfl + · exfalso + have hlt : repunit y n < repunit y m := by + simp only [repunit, show ¬(y ≤ 1) from by omega, if_false] + rw [Nat.div_lt_div_right (by omega : y - 1 ≠ 0) + (Nat.sub_one_dvd_pow_sub_one y n) + (Nat.sub_one_dvd_pow_sub_one y m)] + have := Nat.pow_lt_pow_right (show y ≥ 2 from hy) hmn + have := Nat.one_le_pow n y (by omega) + have := Nat.one_le_pow m y (by omega) + omega + omega have : (x, m) = (y, n) := by simp [heq, this] contradiction) rcases h_bms with ⟨_, _, ⟨_, hy90⟩, ⟨_, hn13⟩⟩; @@ -498,12 +612,14 @@ theorem hermite_sieve_isomorphism (x m y n : ℕ) lemma repunit_strictMono_exponent (x : ℕ) (hx : x ≥ 2) : ∀ m n, m < n → repunit x m < repunit x n := by intro m n hmn; - -- R(x,n) − R(x,m) = (x^n − 1)/(x−1) − (x^m − 1)/(x−1) - -- = (x^n − x^m)/(x−1) - -- = x^m · (x^{n−m} − 1)/(x−1) - -- = x^m · R(x, n−m) - -- ≥ x^m · 1 ≥ 2^3 = 8 > 0 - sorry + simp only [repunit, show ¬(x ≤ 1) from by omega, if_false] + rw [Nat.div_lt_div_right (by omega : x - 1 ≠ 0) + (Nat.sub_one_dvd_pow_sub_one x m) + (Nat.sub_one_dvd_pow_sub_one x n)] + have := Nat.pow_lt_pow_right (show x ≥ 2 from hx) hmn + have := Nat.one_le_pow m x (by omega) + have := Nat.one_le_pow n x (by omega) + omega /- Lemma: repunit lower bound for x ≥ 2, m ≥ 3. @@ -512,7 +628,13 @@ lemma repunit_strictMono_exponent (x : ℕ) (hx : x ≥ 2) : lemma repunit_lower_bound (x m : ℕ) (hx : x ≥ 2) (hm : m ≥ 3) : repunit x m ≥ 7 := by simp only [repunit, show ¬(x ≤ 1) from by omega, if_false] - sorry -- requires: (x^m - 1)/(x - 1) ≥ 1 + x + x^2 for x ≥ 2, m ≥ 3 + have hx1pos : x - 1 > 0 := by omega + rw [ge_iff_le, Nat.le_div_iff_mul_le hx1pos] + have hpow : x ^ m ≥ x ^ 3 := Nat.pow_le_pow_right (by omega) hm + have hbase : x ^ 3 ≥ 7 * (x - 1) + 1 := by + zify [show 1 ≤ x from by omega] at * + nlinarith [sq_nonneg ((x : ℤ) - 2)] + omega /- Lemma: the diagonal H-KdF polynomial evaluated at (x,−1,x,−1,1/2) can be expressed in closed form. This is the key identity connecting the H-KdF diff --git a/lakefile.lean b/lakefile.lean index 3f5cf645..7163c3cd 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -36,7 +36,8 @@ lean_lib «SilverSightFormal» where `CoreFormalism.HachimojiBase, `CoreFormalism.HachimojiManifoldAxiom, `CoreFormalism.HachimojiCodec, - `CoreFormalism.HachimojiLUT + `CoreFormalism.HachimojiLUT, + `CoreFormalism.HachimojiBridging ] lean_lib «SilverSightRRC» where diff --git a/python/gemma4_mcp.py b/python/gemma4_mcp.py index 510b350f..4f8abb13 100644 --- a/python/gemma4_mcp.py +++ b/python/gemma4_mcp.py @@ -18,7 +18,19 @@ except ImportError: httpx = None GEMMA_URL = "http://127.0.0.1:8081/v1/chat/completions" -GEMMA_MODEL = "gemma4-12b" +GEMMA_MODELS_URL = "http://127.0.0.1:8081/v1/models" + + +def get_model_id() -> str: + """Auto-detect the model ID from the server.""" + try: + import httpx + with httpx.Client(timeout=5) as client: + resp = client.get(GEMMA_MODELS_URL, headers={"Authorization": "Bearer none"}) + data = resp.json() + return data["models"][0]["name"] + except Exception: + return "gemma4-12b" # fallback def call_gemma(question: str, system: str = "", max_tokens: int = 2000, @@ -27,13 +39,15 @@ def call_gemma(question: str, system: str = "", max_tokens: int = 2000, if httpx is None: return {"error": "httpx not installed"} + model_id = get_model_id() + messages = [] if system: messages.append({"role": "system", "content": system}) messages.append({"role": "user", "content": question}) payload = { - "model": GEMMA_MODEL, + "model": model_id, "messages": messages, "max_tokens": max_tokens, "temperature": temperature,