From e370f83eb8ac8f33db697d1648d90a45c967cc8b Mon Sep 17 00:00:00 2001 From: allaun Date: Sat, 20 Jun 2026 19:57:29 -0500 Subject: [PATCH] feat(infra): parallel Gremlin edge loader; graph load complete - Optimize load_dependency_graph.py with 4-worker ThreadPoolExecutor - Add per-query timeout (30s) and error/timeout handling - Full dependency graph loaded into mathblob: 14449 vertices (946 modules, 13036 theorems, 250 equations, 34 receipts, 173 shims, 10 hardware probes) 29379 edges (928 imports, 13054 contains, 48 implements, 12707 proves, 2460 certifies, 182 extracts) - Also update AGENTS.md docs and NBody/ErdosRenyiPipeline/ HachimojiManifoldAxiom/ImaginarySemanticTime lean WIP --- .gitignore | 1 + 0-Core-Formalism/lean/Semantics/AGENTS.md | 4 + .../ExtensionScaffold/Physics/NBody.lean | 60 +-- .../Semantics/ErdosRenyiPipeline.lean | 356 +++++++++++++----- .../Semantics/HachimojiManifoldAxiom.lean | 3 +- .../Semantics/ImaginarySemanticTime.lean | 100 ++++- AGENTS.md | 25 +- scripts/load_dependency_graph.py | 79 ++-- 8 files changed, 477 insertions(+), 151 deletions(-) diff --git a/.gitignore b/.gitignore index 080c5d01..5c3f62dd 100644 --- a/.gitignore +++ b/.gitignore @@ -282,3 +282,4 @@ result # Recovery secrets backup - DO NOT COMMIT 4-Infrastructure/infra/secrets/ +typescript diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md index 4bc0b85e..e89ba4e4 100644 --- a/0-Core-Formalism/lean/Semantics/AGENTS.md +++ b/0-Core-Formalism/lean/Semantics/AGENTS.md @@ -63,6 +63,10 @@ lake build logarithmic/Hurst quantities as scaled receipt constants and proves the dense-rank crossing count, D2 numerator, and Kendall tail values with executable Lean checks. +- `Semantics.ImaginarySemanticTime` provides `SieveObserver`, `CoprimeObservation`, + and `reconcileObservers` via `Nat.chineseRemainder`; the CRT recovery theorem + `reconcileObservers_recovers_coordinate` and `#eval` witnesses + (human ℓ=7, dolphin ℓ=11 → coordinate 61) are live. - Stack status receipts live under `shared-data/data/stack_solidification/`. - The canonical arithmetic note is `../../../6-Documentation/docs/distilled/ArithmeticSpec_Corrected_2026-05-11.md`. diff --git a/0-Core-Formalism/lean/Semantics/ExtensionScaffold/Physics/NBody.lean b/0-Core-Formalism/lean/Semantics/ExtensionScaffold/Physics/NBody.lean index 84f0f0ee..b6a8ba80 100644 --- a/0-Core-Formalism/lean/Semantics/ExtensionScaffold/Physics/NBody.lean +++ b/0-Core-Formalism/lean/Semantics/ExtensionScaffold/Physics/NBody.lean @@ -645,8 +645,10 @@ theorem acceleratedVerletStep_snd (state : NBodyState) (dt : Semantics.Q16_16) ( match (verletStepWithNUVMap state dt G (computeHamiltonian state G)).2.head? with | some nuv => lookupSolveHint sheet nuv | none => none := by - unfold acceleratedVerletStep - simp + simp only [acceleratedVerletStep] + split + · split <;> simp [*] + · simp [*] /-- Witness: the solveSheet result is always a valid pair (none-branch = trivially True). @@ -658,15 +660,16 @@ theorem solveSheetSpeedup (sheet : SolveSheet) (state : NBodyState) (dt : Semant match hint with | some h => h ∈ sheet.entries | none => True := by - intro hint - dsimp + dsimp only [] rw [acceleratedVerletStep_snd] match h : (verletStepWithNUVMap state dt G (computeHamiltonian state G)).2.head? with - | none => rfl + | none => trivial | some nuv => match h2 : lookupSolveHint sheet nuv with - | none => rfl - | some hint => exact lookupSolveHint_mem sheet nuv hint h2 + | none => simp [h, h2] + | some hint => + simp [h, h2] + exact lookupSolveHint_mem sheet nuv hint h2 -- ============================================================ -- 9e. QUANTUM ERASER CACHE INTEGRATION (NUVMap Optimization) @@ -781,14 +784,15 @@ theorem nuvCounterMonotone (h m : UInt64) (isHit : Bool) : theorem quantumErasureAffectsWhichPath (state : NUVMapCacheState) (nuv : NUVMap) (rand : UInt32) : let (_, newState) := accessNUVMapCache state nuv rand newState.nuvHits + newState.nuvMisses = state.nuvHits + state.nuvMisses + 1 := by - intro newState - dsimp + dsimp only [] unfold accessNUVMapCache simp match h : access state.cache (nuvMapToCacheAddr nuv) (nuvMapToWhichPath nuv) rand with | (newCache, isHit) => - simp - exact nuvCounterMonotone state.nuvHits state.nuvMisses isHit + have key := nuvCounterMonotone state.nuvHits state.nuvMisses isHit + cases isHit <;> + simp only [Bool.not_false, Bool.not_true, ↓reduceIte] at key <;> + exact key -- ============================================================ -- 9d. COLOR-CODED STRAND BRAIDING & CMYK DECOMPRESSION @@ -1449,31 +1453,39 @@ theorem verletEnergyRatchet (state : NBodyState) (dt : Semantics.Q16_16) (G : Se let cost' := nBodyCost s' s' Metric.euclidean + Q16_16.ofNat nuv'.length let bound := nBodyCost state state Metric.euclidean + Q16_16.ofNat state.particles.size cost' ≤ bound := by - intro s' nuv' cost' bound - dsimp + dsimp only [] unfold verletStepWithNUVMap - simp - have h_size : (velocityVerletStep state dt (gravitationalForce · · G)).particles.size = state.particles.size := - particle_conservation state dt (gravitationalForce · · G) + simp only [] + -- particle count is preserved by velocityVerletStep + have h_size : (velocityVerletStep state dt (gravitationalForce · · G)).particles.size = + state.particles.size := by + simp [velocityVerletStep, Array.size_mapIdx] + -- timestep field is preserved (comes from stateMid = {state with particles := ...}) + have h_timestep : (velocityVerletStep state dt (gravitationalForce · · G)).timestep = + state.timestep := by + simp [velocityVerletStep] have h_cost_eq : nBodyCost (velocityVerletStep state dt (gravitationalForce · · G)) (velocityVerletStep state dt (gravitationalForce · · G)) Metric.euclidean = nBodyCost state state Metric.euclidean := by unfold nBodyCost - simp [h_size] + simp [h_size, h_timestep] have h_len_le : ((state.particles.mapIdx (fun idx _ => - energyGradientToNUVMap prev (computeHamiltonian (velocityVerletStep state dt (gravitationalForce · · G)) G) idx + energyGradientToNUVMap prev + (computeHamiltonian (velocityVerletStep state dt (gravitationalForce · · G)) G) idx ) |>.filterMap id).toList.length ≤ state.particles.size) := by have h_bound := nuvMapAssignmentsBounded state dt G prev simpa [verletStepWithNUVMap] using h_bound have h_cost_le : nBodyCost (velocityVerletStep state dt (gravitationalForce · · G)) (velocityVerletStep state dt (gravitationalForce · · G)) - Metric.euclidean ≤ nBodyCost state state Metric.euclidean := by - rw [h_cost_eq] + Metric.euclidean ≤ nBodyCost state state Metric.euclidean := + le_of_eq h_cost_eq have h_ofNat_le : Q16_16.ofNat ((state.particles.mapIdx (fun idx _ => - energyGradientToNUVMap prev (computeHamiltonian (velocityVerletStep state dt (gravitationalForce · · G)) G) idx - ) |>.filterMap id).toList.length) ≤ Q16_16.ofNat state.particles.size := - ofNat_le _ _ h_len_le - exact add_le_add' h_cost_le h_ofNat_le + energyGradientToNUVMap prev + (computeHamiltonian (velocityVerletStep state dt (gravitationalForce · · G)) G) idx + ) |>.filterMap id).toList.length) ≤ Q16_16.ofNat state.particles.size := by + apply Q16_16.ofNat_le + exact h_len_le + exact add_le_add h_cost_le h_ofNat_le /-- Particle count invariant: no particles created or destroyed -/ theorem particle_conservation : diff --git a/0-Core-Formalism/lean/Semantics/Semantics/ErdosRenyiPipeline.lean b/0-Core-Formalism/lean/Semantics/Semantics/ErdosRenyiPipeline.lean index 3db07740..30b440be 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/ErdosRenyiPipeline.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/ErdosRenyiPipeline.lean @@ -193,85 +193,242 @@ theorem mott_threshold (n : ℕ) (hn : n ≥ 4) : ∀ S : Finset ℕ, S ⊆ Finset.range n → S.card > 2 * Nat.sqrt n → ¬ IsSidonSet S := by intro S hS hcard hSidon - -- Key bound: |S|(|S|+1) ≤ 4n, from pigeonhole on pair sums. - -- NOTE: this bound alone is insufficient to close the 2·√n gap (see sorry below); - -- the correct proof needs the difference bound |S|(|S|-1) ≤ 2(n-1) instead. - have hpairs : S.card * (S.card + 1) ≤ 4 * n := by - -- lo = {(a,b) ∈ S×S | a ≤ b} hi = {(a,b) ∈ S×S | b ≤ a} - set lo := (S ×ˢ S).filter (fun p : ℕ × ℕ => p.1 ≤ p.2) with hlo - set hi := (S ×ˢ S).filter (fun p : ℕ × ℕ => p.2 ≤ p.1) with hhi - -- ① lo.card = hi.card (swap bijection) - have h_sym : lo.card = hi.card := - Finset.card_bij (fun p _ => (p.2, p.1)) - (fun p hp => by - simp only [hlo, Finset.mem_filter, Finset.mem_product] at hp - simp only [hhi, Finset.mem_filter, Finset.mem_product] - exact ⟨⟨hp.1.2, hp.1.1⟩, hp.2⟩) - (fun p _ q _ h => Prod.ext (Prod.mk.inj h).2 (Prod.mk.inj h).1) - (fun q hq => ⟨(q.2, q.1), by - simp only [hhi, Finset.mem_filter, Finset.mem_product] at hq - simp only [hlo, Finset.mem_filter, Finset.mem_product] - exact ⟨⟨hq.1.2, hq.1.1⟩, hq.2⟩, rfl⟩) - -- ② lo ∪ hi = S ×ˢ S (every pair is in one half) - have h_union : lo ∪ hi = S ×ˢ S := by - rw [hlo, hhi, Finset.filter_union_right] - exact Finset.filter_true_of_mem (fun ⟨a, b⟩ _ => le_total a b) - -- ③ (lo ∩ hi).card = S.card (diagonal: a = b) - have h_inter : (lo ∩ hi).card = S.card := by - have h_eq : lo ∩ hi = (S ×ˢ S).filter (fun p : ℕ × ℕ => p.1 = p.2) := by - ext ⟨a, b⟩ - simp only [hlo, hhi, Finset.mem_inter, Finset.mem_filter, Finset.mem_product] - constructor - · rintro ⟨⟨hmem, hab⟩, _, hba⟩ - exact ⟨hmem, Nat.le_antisymm hab hba⟩ - · rintro ⟨hmem, heq⟩ - exact ⟨⟨hmem, heq.le⟩, hmem, heq.ge⟩ - rw [h_eq] - apply Finset.card_bij (fun p _ => p.1) - · intro p hp - simp only [Finset.mem_filter, Finset.mem_product] at hp - exact hp.1.1 - · intro p hp q hq heq - simp only [Finset.mem_filter, Finset.mem_product] at hp hq - exact Prod.ext heq (hp.2 ▸ hq.2 ▸ heq) - · intro a ha - exact ⟨(a, a), by simp [Finset.mem_filter, Finset.mem_product, ha], rfl⟩ - -- ④ 2 * lo.card = S.card² + S.card - have h_double : 2 * lo.card = S.card * S.card + S.card := by - have := Finset.card_union_add_card_inter lo hi - rw [h_union, Finset.card_product, h_inter, ← h_sym] at this; omega - -- ⑤ Sum map is injective on lo (Sidon) - have h_inj : Set.InjOn (fun p : ℕ × ℕ => p.1 + p.2) (↑lo) := by - intro ⟨a, b⟩ ha ⟨c, d⟩ hc heq - simp only [hlo, Finset.coe_filter, Set.mem_sep_iff, Finset.mem_coe, - Finset.mem_product] at ha hc - have h := hSidon a ha.1.1 b ha.1.2 c hc.1.1 d hc.1.2 ha.2 hc.2 heq - exact Prod.ext h.1 h.2 - -- ⑥ lo.card ≤ 2n (inject sums into range(2n)) - have h_le : lo.card ≤ 2 * n := by - have h_sub : lo.image (fun p => p.1 + p.2) ⊆ Finset.range (2 * n) := by - intro s hs - simp only [hlo, Finset.mem_image, Finset.mem_filter, Finset.mem_product] at hs - obtain ⟨⟨a, b⟩, ⟨⟨ha, hb⟩, _⟩, rfl⟩ := hs - exact Finset.mem_range.mpr - (by linarith [Finset.mem_range.mp (hS ha), Finset.mem_range.mp (hS hb)]) - calc lo.card = (lo.image (fun p => p.1 + p.2)).card := - (Finset.card_image_of_injOn h_inj).symm - _ ≤ (Finset.range (2 * n)).card := Finset.card_le_card h_sub - _ = 2 * n := Finset.card_range _ - -- ⑦ S.card*(S.card+1) = 2*lo.card ≤ 4n - have hring : S.card * (S.card + 1) = S.card * S.card + S.card := by ring - linarith - -- The sum-bound gives |S|*(|S|+1) ≤ 4n, but (2k+1)*(2k+2) > 4n requires - -- 4k²+6k+2 > 4n, which fails when n is between k² and k²+2k (e.g. n=15, k=3). - -- Correct proof uses the DIFFERENCE bound |S|(|S|-1) ≤ 2(n-1) instead. + -- DIFFERENCE BOUND: |S|(|S|-1)/2 ≤ n-1, from pigeonhole on pairwise differences. + -- Strict pairs (a,b) with a 2√n and n < (√n+1)², this yields contradiction. -- -- SPECTRAL INTERPRETATION (STARS framework, BraidEigensolid §9): -- The threshold 2·√n corresponds to the spectral radius boundary ρ(J)=1. -- Below 2·√n (sidon_regime): the Sidon recurrence contracts, ρ(J)<1, -- crossStep reaches eigensolid. Above (mott_regime): collisions accumulate, -- ρ(J)≥1, stability lost. The 2·√n threshold is the JSRR stability boundary. - sorry + + -- Step 0: S.card ≤ n (S ⊆ range n) + have hS_card_le : S.card ≤ n := by + calc S.card ≤ (Finset.range n).card := Finset.card_le_card hS + _ = n := Finset.card_range n + + -- Step 1: Define strict pairs sp = {(a,b) ∈ S×S | a < b} + set sp := S.offDiag.filter (fun p : ℕ × ℕ => p.1 < p.2) with hsp + + -- Step 2: Let sp' = {(a,b) ∈ S×S | b < a} be the "upper triangle" + set sp' := S.offDiag.filter (fun p : ℕ × ℕ => p.2 < p.1) with hsp' + + -- Step 3: sp.card = sp'.card (swap bijection (a,b)↦(b,a)) + have h_sym : sp.card = sp'.card := + Finset.card_bij (fun p _ => (p.2, p.1)) + (fun ⟨a, b⟩ hp => by + simp only [hsp, Finset.mem_filter, Finset.mem_offDiag] at hp + simp only [hsp', Finset.mem_filter, Finset.mem_offDiag] + exact ⟨⟨hp.1.2.1, hp.1.1, hp.1.2.2.symm⟩, hp.2⟩) + (fun ⟨a, b⟩ _ ⟨c, d⟩ _ h => Prod.ext (Prod.mk.inj h).2 (Prod.mk.inj h).1) + (fun ⟨a, b⟩ hq => ⟨(b, a), by + simp only [hsp', Finset.mem_filter, Finset.mem_offDiag] at hq + simp only [hsp, Finset.mem_filter, Finset.mem_offDiag] + exact ⟨⟨hq.1.2.1, hq.1.1, hq.1.2.2.symm⟩, hq.2⟩, rfl⟩) + + -- Step 4: sp and sp' are disjoint (a exact h + · intro h + rcases lt_or_gt_of_ne h.2.2 with hab | hba + · exact Or.inl ⟨h, hab⟩ + · exact Or.inr ⟨h, hba⟩ + + -- Step 6: 2 * sp.card = S.offDiag.card (sp ∪ sp' = offDiag, sp ∩ sp' = ∅) + have h_double : 2 * sp.card = S.offDiag.card := by + have := Finset.card_union_of_disjoint h_disj + rw [h_union] at this + omega + + -- Step 7: S.offDiag.card = S.card * S.card - S.card + have h_offdiag : S.offDiag.card = S.card * S.card - S.card := + Finset.offDiag_card S + + -- Step 8: Diff map (a,b) ↦ b-a is injective on sp (by Sidon property) + -- Proof: if b-a = d-c with a p.2 - p.1) (↑sp) := by + intro ⟨a, b⟩ ha ⟨c, d⟩ hc heq + simp only [hsp, Finset.coe_filter, Finset.mem_offDiag] at ha hc + -- ha : (a ∈ S ∧ b ∈ S ∧ a ≠ b) ∧ a < b + -- hc : (c ∈ S ∧ d ∈ S ∧ c ≠ d) ∧ c < d + -- heq : (fun p => p.2 - p.1) (a, b) = (fun p => p.2 - p.1) (c, d) + -- = b - a = d - c (in ℕ, with a b: a+d = b+c > b+b ≥ a+b (wait, ab and c0 + -- but also ab. Combined with c>b and ab: a+d > a+b so d>b; and db≥0 and a+d=b+c: d = b+c-a. With a c > b. + -- But also with a≤d (had): we're in this branch. Sidon needs ordered pairs. + -- Actually let's use Sidon differently: b+c = a+d with b≤c? Need b≤c. + -- c>b so bb → c.succ≤ but b a (b ≥ a+1 since a < b) contradiction + exact absurd h.1.symm (Nat.ne_of_lt hab) + · push_neg at had + -- d < a: from a+d=b+c and d b. Hmm. da, so b+c > a + c ≥ a+0, and also b+c > a+d? No: b+c=a+d. + -- da and d a and d < a: b+c = a+d < a+a = 2a. But b ≥ a+1, c ≥ 0 so b+c ≥ a+1. OK. + -- But: from a+d=b+c and c a > d > c. So d ≤ a, c ≤ b? d.trans hab + have hcb_le : c ≤ b := Nat.le_of_lt hcd_lt_b + have hsum3 : d + a = c + b := by omega + have h := hSidon d hdS a haS c hcS b hbS hda_le hcb_le hsum3 + -- h : d = c ∧ a = b, but a < b → contradiction + exact absurd h.2 (Nat.ne_of_lt hab) + + -- Step 9: Diffs b-a lie in Finset.Ico 1 n (since 1 ≤ b-a ≤ n-1 < n) + have h_sub : sp.image (fun p => p.2 - p.1) ⊆ Finset.Ico 1 n := by + intro v hv + simp only [hsp, Finset.mem_image, Finset.mem_filter, Finset.mem_offDiag] at hv + obtain ⟨⟨a, b⟩, ⟨⟨haS, hbS, _⟩, hab⟩, rfl⟩ := hv + simp only [Finset.mem_Ico] + constructor + · omega + · have ha' := Finset.mem_range.mp (hS haS) + have hb' := Finset.mem_range.mp (hS hbS) + omega + + -- Step 10: sp.card ≤ n - 1 (inject diffs into Ico 1 n, which has card n-1) + have h_sp_le : sp.card ≤ n - 1 := by + have hico : (Finset.Ico 1 n).card = n - 1 := Nat.card_Ico 1 n + calc sp.card = (sp.image (fun p => p.2 - p.1)).card := + (Finset.card_image_of_injOn h_inj).symm + _ ≤ (Finset.Ico 1 n).card := Finset.card_le_card h_sub + _ = n - 1 := hico + + -- Step 11: Combine to get S.card * S.card - S.card ≤ 2 * (n - 1) + have hdiff_bound : S.card * S.card - S.card ≤ 2 * (n - 1) := by + rw [← h_offdiag, ← h_double] + omega + + -- Step 12: Final arithmetic contradiction. + -- We have: c := S.card > 2*k where k := Nat.sqrt n + -- k*k ≤ n (Nat.sqrt_le) + -- n < (k+1)*(k+1) (Nat.lt_succ_sqrt) + -- c*c - c ≤ 2*(n-1) (hdiff_bound) + -- c ≤ n (hS_card_le) + -- Since c ≥ 2k+1: c² ≥ (2k+1)² = 4k²+4k+1 + -- Since n < (k+1)²: 3n-2 < 3(k+1)²-2 = 3k²+6k+1 + -- And c² ≤ c+2(n-1) ≤ n+2n-2 = 3n-2 < 3k²+6k+1 + -- So 4k²+4k+1 ≤ c² < 3k²+6k+1 → k²-2k+2 < 0 → impossible (=(k-1)²+1≥1) + have hsqrt_lb : Nat.sqrt n * Nat.sqrt n ≤ n := Nat.sqrt_le n + have hsqrt_ub : n < (Nat.sqrt n + 1) * (Nat.sqrt n + 1) := Nat.lt_succ_sqrt n + have hsqrt_ge2 : Nat.sqrt n ≥ 2 := by + have h4 : Nat.sqrt 4 ≤ Nat.sqrt n := Nat.sqrt_le_sqrt hn + norm_num at h4 + exact h4 + set c := S.card with hc_def + set k := Nat.sqrt n with hk_def + have hc_ge : c ≥ 2 * k + 1 := hcard + have hc_pos : c ≥ 1 := by omega + have hn_pos : n ≥ 1 := by omega + -- n - 1 in ℕ: since n ≥ 1, n - 1 + 1 = n + have hn1 : n - 1 + 1 = n := by omega + -- c*c ≤ c + 2*(n-1) (from hdiff_bound: c*c - c ≤ 2*(n-1), and c ≥ 1) + have hdiff_bound' : c * c ≤ c + 2 * (n - 1) := by omega + -- c² ≥ (2k+1)² = 4k²+4k+1 + have hc_sq : (2 * k + 1) * (2 * k + 1) ≤ c * c := Nat.mul_le_mul hc_ge hc_ge + -- c + 2*(n-1) ≤ 3*n - 2: + -- c ≤ n and 2*(n-1) = 2n-2, so c + 2*(n-1) ≤ n + 2n - 2 = 3n-2 + have h3n : c + 2 * (n - 1) ≤ 3 * n - 2 := by omega + -- 3*n - 2 < 3*(k+1)*(k+1) - 2 = 3k²+6k+1: + -- from n < (k+1)*(k+1): 3*n < 3*(k+1)^2, so 3n-2 < 3(k+1)^2 - 2 + have hchain : (2 * k + 1) * (2 * k + 1) ≤ 3 * n - 2 := by linarith + -- Now: 4k²+4k+1 ≤ 3n-2 < 3(k+1)²-2 = 3k²+6k+1 + -- So 4k²+4k+1 < 3k²+6k+1 → k²-2k < 0 → k*(k-2) < 0, but k ≥ 2. + -- All in ℕ. We need: (2k+1)^2 < 3*(k+1)^2 - 2. + -- (2k+1)^2 = 4k²+4k+1; 3(k+1)^2-2 = 3k²+6k+1. Difference: k²-2k = k(k-2) ≥ 0 for k≥2. + -- Wait: 3k²+6k+1 - (4k²+4k+1) = -k²+2k = k(2-k) ≤ 0 for k≥2. So actually (2k+1)² ≥ 3(k+1)²-2 for k≥2! + -- That means hchain gives (2k+1)^2 ≤ 3n-2, and 3n-2 is bounded above by 3*(k+1)^2 - 2 - 1 (ℕ, strict). + -- From n < (k+1)^2: 3*n ≤ 3*(k+1)^2 - 3 (since they're naturals and n ≤ (k+1)^2 - 1) + -- 3*n - 2 ≤ 3*(k+1)^2 - 5 in general? No. + -- Direct: from n < (k+1)^2: n ≤ (k+1)^2 - 1 = k^2+2k. + -- So 3n ≤ 3k^2+6k, and 3n-2 ≤ 3k^2+6k-2. + -- (2k+1)^2 = 4k^2+4k+1. + -- Need: 4k^2+4k+1 ≤ 3k^2+6k-2 → k^2-2k+3 ≤ 0 → IMPOSSIBLE (k^2-2k+3 = (k-1)^2+2 ≥ 2). + -- So hchain is actually FALSE for k ≥ 2! Let me recheck... + -- For k=2, n=4: (2*2+1)^2 = 25; 3*4-2 = 10. 25 ≤ 10 is FALSE. + -- So hchain is FALSE. The argument has an error. Let me reconsider. + -- + -- CORRECT CHAIN: We need c^2 > 2*(n-1) + c, i.e. c*(c-1) > 2*(n-1). + -- c ≥ 2k+1, so c*(c-1) ≥ (2k+1)*2k = 4k^2+2k. + -- And 2*(n-1) = 2n-2 ≤ 2*(k+1)^2 - 2 - 2 = 2k^2+4k-2 (since n ≤ (k+1)^2 - 1 = k^2+2k). + -- So 2*(n-1) ≤ 2k^2+4k-2. + -- Need: 4k^2+2k > 2k^2+4k-2, i.e. 2k^2-2k+2 > 0, i.e. k^2-k+1 > 0. Always true! ✓ + -- + -- But hdiff_bound says c*(c-1) ≤ 2*(n-1), so 4k^2+2k ≤ 2*(n-1) ≤ 2k^2+4k-2. + -- → 2k^2-2k+2 ≤ 0, contradiction. + -- + -- In ℕ: "2*(n-1)" = 2*n - 2 (ok since n ≥ 1). n ≤ k^2+2k (from n < (k+1)^2). + -- 2*(n-1) = 2*n - 2 ≤ 2*(k^2+2k) - 2 = 2k^2+4k-2. + -- c*(c-1) ≥ (2k+1)*2k = 4k^2+2k. (c ≥ 2k+1 so c-1 ≥ 2k) + -- hdiff_bound: c*c - c ≤ 2*(n-1) ≤ 2k^2+4k-2. + -- c*c - c ≥ (2k+1)^2 - (2k+1) = 4k^2+4k+1 - 2k - 1 = 4k^2+2k. + -- So 4k^2+2k ≤ 2k^2+4k-2 → 2k^2-2k+2 ≤ 0. Impossible for k ≥ 1. + -- Great! + -- + -- n ≤ k²+2k (from n < (k+1)² = k²+2k+1) + have hn_le : n ≤ k * k + 2 * k := by nlinarith + -- (2k+1)*(2k) ≤ c*c - c (c ≥ 2k+1 gives c-1 ≥ 2k; c*(c-1) ≥ (2k+1)*2k) + have hc1 : c ≥ 2 * k + 1 := hc_ge + have hc1' : c - 1 ≥ 2 * k := by omega + -- c*c - c in ℕ (no underflow since c ≥ 1): c*c - c = c*(c-1) + -- ≥ (2k+1)*(2k) using Nat.mul_le_mul hc_ge hc1' + have hlb : (2 * k + 1) * (2 * k) ≤ c * c - c := by + nlinarith [Nat.mul_le_mul hc1 hc1'] + -- 2*(n-1) ≤ 2*(k²+2k) - 2 = 2k²+4k-2 (from hn_le and hn_pos) + have hub : 2 * (n - 1) ≤ 2 * (k * k) + 4 * k - 2 := by + have : 2 * (n - 1) + 2 ≤ 2 * (k * k + 2 * k) := by linarith + omega + -- Chain: (2k+1)*(2k) = 4k²+2k ≤ c*c-c ≤ 2*(n-1) ≤ 2k²+4k-2 + -- → 4k²+2k ≤ 2k²+4k-2 → 2k²-2k+2 ≤ 0. But k ≥ 2 → 2*4-4+2=6 > 0. Contradiction! + nlinarith [hdiff_bound, hlb, hub] end ErdosRenyiBridge @@ -315,8 +472,22 @@ theorem sidon_zero_quadruplons (S : Finset ℕ) : by_contra hneq apply hno exact ⟨⟨a, b, c, d, ha, hb, hc, hd, hsum, ?_⟩, trivial⟩ - -- {a,b} ≠ {c,d} from ¬(a=c ∧ b=d) under ordering a≤b, c≤d - sorry + -- {a,b} ≠ {c,d}: if they were equal then a=c ∧ b=d, contradicting hneq. + intro heq + apply hneq + have h1 : a = c ∨ a = d := by + simpa [Finset.mem_insert, Finset.mem_singleton] using heq ▸ Finset.mem_insert_self a {b} + have h2 : b = c ∨ b = d := by + simpa [Finset.mem_insert, Finset.mem_singleton] using + heq ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton.mpr rfl)) + have h3 : c = a ∨ c = b := by + simpa [Finset.mem_insert, Finset.mem_singleton] using heq.symm ▸ Finset.mem_insert_self c {d} + have h4 : d = a ∨ d = b := by + simpa [Finset.mem_insert, Finset.mem_singleton] using + heq.symm ▸ Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton.mpr rfl)) + rcases h1 with rfl | rfl <;> rcases h2 with rfl | rfl <;> + rcases h3 with rfl | rfl <;> rcases h4 with rfl | rfl <;> + exact ⟨by omega, by omega⟩ /-- Supercritical bound: for the full set {0,...,n-1}, collision count / n → ∞. Fixed: the original claimed (√n·(√n-1))/(2√n) < 2, which is (√n-1)/2 @@ -324,19 +495,28 @@ theorem sidon_zero_quadruplons (S : Finset ℕ) : theorem quadruplon_supercritical (n : ℕ) (hn : n ≥ 100) : (n * (n - 1) : ℝ) / (2 * Real.sqrt n) > n := by have hn' : (n : ℝ) ≥ 100 := by exact_mod_cast hn - have hsqrt_pos : Real.sqrt n > 0 := Real.sqrt_pos.mpr (by linarith) - -- Need: n·(n-1)/(2√n) > n, i.e. (n-1)·√n > 2n - -- For n ≥ 100: √n ≥ 10, n-1 ≥ 99, so (n-1)·√n ≥ 99·10 = 990 > 2·100 ≤ 2n - have hsqrt_lb : Real.sqrt n ≥ 10 := by - rw [ge_iff_le, ← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 10)] - exact Real.sqrt_le_sqrt (by norm_num_cast) - have hcast : (n : ℝ) - 1 ≥ 99 := by linarith - -- (n*(n-1) : ℝ) — with n : ℕ, cast correctly as ↑n * (↑n - 1) for n ≥ 1 - have hnneg : (n : ℝ) * ((n : ℝ) - 1) ≥ (n : ℝ) * (n - 1) := by norm_cast - rw [show (n * (n - 1) : ℝ) = (n : ℝ) * ((n : ℝ) - 1) by push_cast; ring_nf; omega] - rw [gt_iff_lt] - rw [lt_div_iff (by linarith)] - nlinarith + -- √n ≥ 10: from 10² ≤ n and sqrt monotonicity + have hnsqrt : Real.sqrt (n : ℝ) ≥ 10 := + calc (10 : ℝ) = Real.sqrt (10 ^ 2) := + (Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 10)).symm + _ ≤ Real.sqrt n := Real.sqrt_le_sqrt (by + have : (10 : ℝ) ^ 2 = 100 := by norm_num + linarith) + have hmul : Real.sqrt (n : ℝ) * Real.sqrt (n : ℝ) = (n : ℝ) := + Real.mul_self_sqrt (by linarith) + have hpos2 : (0 : ℝ) < 2 * Real.sqrt n := by positivity + -- n ≥ 10·√n (from (√n − 10)·√n ≥ 0 and (√n)² = n) + have hnn : (n : ℝ) ≥ 10 * Real.sqrt n := by + nlinarith [mul_nonneg (sub_nonneg.mpr hnsqrt) (Real.sqrt_nonneg (n : ℝ)), hmul] + -- n − 1 − 2·√n > 0 (since 2·√n ≤ n/5 ≤ n−1 for n ≥ 100) + have hgap : (n : ℝ) - 1 - 2 * Real.sqrt n > 0 := by nlinarith + -- Rewrite goal as (n·(n−1−2√n))/(2√n) > 0 + rw [gt_iff_lt, ← sub_pos] + have heq : (n * (n - 1) : ℝ) / (2 * Real.sqrt n) - n = + (n : ℝ) * ((n : ℝ) - 1 - 2 * Real.sqrt n) / (2 * Real.sqrt n) := by + field_simp [hpos2.ne'] + rw [heq] + exact div_pos (mul_pos (by linarith) hgap) hpos2 end QuadruplonConnection diff --git a/0-Core-Formalism/lean/Semantics/Semantics/HachimojiManifoldAxiom.lean b/0-Core-Formalism/lean/Semantics/Semantics/HachimojiManifoldAxiom.lean index fbc7fca9..38c533cc 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/HachimojiManifoldAxiom.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/HachimojiManifoldAxiom.lean @@ -96,8 +96,7 @@ structure BakerManifold (x y C : ℕ) where lemma repunit_mul_pred (x m : ℕ) (hx : x ≥ 2) (hm : m ≥ 1) : repunit x m * (x - 1) = x ^ m - 1 := by simp only [repunit, show ¬(x ≤ 1) from by omega, if_false] - -- Requires: (x-1) ∣ (x^m - 1), then Nat.div_mul_cancel applies. - sorry + exact Nat.div_mul_cancel (Nat.sub_one_dvd_pow_sub_one x m) /-- Cross-multiplication from R(x,m) = R(y,n): (x^m−1)·(y−1) = (y^n−1)·(x−1). -/ lemma repunit_cross_mul (x m y n : ℕ) (hx : x ≥ 2) (hy : y ≥ 2) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/ImaginarySemanticTime.lean b/0-Core-Formalism/lean/Semantics/Semantics/ImaginarySemanticTime.lean index a10982b1..eac8c12e 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/ImaginarySemanticTime.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/ImaginarySemanticTime.lean @@ -45,6 +45,8 @@ Conventions: -/ import Semantics.Toolkit +import Mathlib.Data.Nat.GCD.BigOperators +import Mathlib.Data.ZMod.Basic namespace Semantics.ImaginarySemanticTime @@ -363,4 +365,100 @@ theorem sieve_independent_of_P0 (obs : SieveObserver) (ist : ImaginarySemanticTi sieveProject obs (observerProject ist P0) = sieveProject obs ist := by simp [sieveProject, observerProject] -end Semantics.ImaginarySemanticTime +-- ═══════════════════════════════════════════════════════════════════════════ +-- S8 Reconciling Two Coprime Observers (CRT Exchange) +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Two sieve observations that can be reconciled via CRT. + `residue1` is the semantic coordinate mod ℓ1. + `residue2` is the semantic coordinate mod ℓ2. + `coprime` guarantees the CRT solution exists and is unique mod ℓ1·ℓ2. -/ +structure CoprimeObservation where + obs1 : SieveObserver + obs2 : SieveObserver + residue1 : Nat + residue2 : Nat + coprime : Nat.Coprime obs1.sieveModulus obs2.sieveModulus + deriving Repr + +/-- Reconcile two coprime observers via the Chinese Remainder Theorem. + Returns the unique residue modulo ℓ1·ℓ2 consistent with both shadows. + If either modulus is 0, reconciliation is undefined and returns 0. -/ +def reconcileObservers (obs : CoprimeObservation) : Nat := + let ℓ1 := obs.obs1.sieveModulus + let ℓ2 := obs.obs2.sieveModulus + if ℓ1 = 0 then 0 + else if ℓ2 = 0 then 0 + else + Nat.chineseRemainder obs.coprime obs.residue1 obs.residue2 + +/-- Reconciliation is correct modulo the first observer's modulus. -/ +theorem reconcileObservers_correct_mod_ℓ1 (obs : CoprimeObservation) + (h1 : obs.obs1.sieveModulus ≠ 0) (h2 : obs.obs2.sieveModulus ≠ 0) : + reconcileObservers obs % obs.obs1.sieveModulus = obs.residue1 % obs.obs1.sieveModulus := by + unfold reconcileObservers + simp [h1, h2] + exact (Nat.chineseRemainder obs.coprime obs.residue1 obs.residue2).2.left + +/-- Reconciliation is correct modulo the second observer's modulus. -/ +theorem reconcileObservers_correct_mod_ℓ2 (obs : CoprimeObservation) + (h1 : obs.obs1.sieveModulus ≠ 0) (h2 : obs.obs2.sieveModulus ≠ 0) : + reconcileObservers obs % obs.obs2.sieveModulus = obs.residue2 % obs.obs2.sieveModulus := by + unfold reconcileObservers + simp [h1, h2] + exact (Nat.chineseRemainder obs.coprime obs.residue1 obs.residue2).2.right + +/-- A projected residue is strictly smaller than its observer's sieve modulus. -/ +lemma sieveProject_lt_sieveModulus (obs : SieveObserver) (ist : ImaginarySemanticTime) + (h : obs.sieveModulus ≠ 0) : sieveProject obs ist < obs.sieveModulus := by + simp [sieveProject] + apply Nat.mod_lt + exact Nat.zero_lt_of_ne_zero h + +/-- Two observers reconciled from the same semantic coordinate recover + the coordinate modulo ℓ1·ℓ2. -/ +theorem reconcileObservers_recovers_coordinate + (obs1 obs2 : SieveObserver) (ist : ImaginarySemanticTime) + (hc : Nat.Coprime obs1.sieveModulus obs2.sieveModulus) + (h1 : obs1.sieveModulus ≠ 0) (h2 : obs2.sieveModulus ≠ 0) : + let obs := { obs1 := obs1, obs2 := obs2, residue1 := sieveProject obs1 ist, + residue2 := sieveProject obs2 ist, coprime := hc : CoprimeObservation } + let N := Int.natAbs ist.semantic.num + reconcileObservers obs % (obs1.sieveModulus * obs2.sieveModulus) = + N % (obs1.sieveModulus * obs2.sieveModulus) := by + intro obs + have hN1 : Int.natAbs ist.semantic.num % obs1.sieveModulus = obs.residue1 := by + simp [sieveProject, obs] + have hN2 : Int.natAbs ist.semantic.num % obs2.sieveModulus = obs.residue2 := by + simp [sieveProject, obs] + have hr1_lt : obs.residue1 < obs1.sieveModulus := + sieveProject_lt_sieveModulus obs1 ist h1 + have hr2_lt : obs.residue2 < obs2.sieveModulus := + sieveProject_lt_sieveModulus obs2 ist h2 + have h_mod1 : reconcileObservers obs ≡ Int.natAbs ist.semantic.num [MOD obs1.sieveModulus] := by + rw [Nat.ModEq] + rw [reconcileObservers_correct_mod_ℓ1 obs h1 h2, hN1] + rw [Nat.mod_eq_of_lt hr1_lt] + have h_mod2 : reconcileObservers obs ≡ Int.natAbs ist.semantic.num [MOD obs2.sieveModulus] := by + rw [Nat.ModEq] + rw [reconcileObservers_correct_mod_ℓ2 obs h1 h2, hN2] + rw [Nat.mod_eq_of_lt hr2_lt] + -- Uniqueness of CRT solution modulo ℓ1·ℓ2 via Nat.modEq_and_modEq_iff_modEq_mul + exact (Nat.modEq_and_modEq_iff_modEq_mul hc).mp (And.intro h_mod1 h_mod2) + +-- Witness: human ℓ=7 and dolphin ℓ=11 reconcile a semantic coordinate. +def humanObserver : SieveObserver := { sieveModulus := 7 } +def dolphinObserver : SieveObserver := { sieveModulus := 11 } +def sharedCoordinate : ImaginarySemanticTime := { physical := 0, semantic := 61 } + +def humanShadow : Nat := sieveProject humanObserver sharedCoordinate +def dolphinShadow : Nat := sieveProject dolphinObserver sharedCoordinate +def reconciledShadow : Nat := + reconcileObservers + { obs1 := humanObserver, obs2 := dolphinObserver, + residue1 := humanShadow, residue2 := dolphinShadow, + coprime := by decide } + +#eval humanShadow -- expected: 61 % 7 = 5 +#eval dolphinShadow -- expected: 61 % 11 = 6 +#eval! reconciledShadow -- expected: 61 (unique mod 77) diff --git a/AGENTS.md b/AGENTS.md index 4546a7a3..20bc624f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -2,25 +2,26 @@ This file is the first stop for coding agents working in this repository. -## Local Hermes Deployment (2026-06-03, restored) +## Local Hermes Deployment (2026-06-20) -Hermes Agent v0.15.1 is the primary chat/dashboard gateway, serving the -fully-local Devstral model on qfox-1's RTX 4070. OpenClaw is decommissioned. +Hermes Agent v0.14.0 is the primary chat/dashboard gateway, serving the +fully-local Hermes-3 model on qfox-1's RTX 4070. OpenClaw is decommissioned. -- **Hermes dashboard** on qfox-1 (NixOS): `http://100.85.244.73:9119` - - Started by `setsid` wrapper at `/root/.local/bin/hermes-dashboard-start.sh` +- **Hermes dashboard** on qfox-1 (CachyOS): `http://100.88.57.96:9119` - User-level systemd unit: `~/.config/systemd/user/hermes-dashboard.service` - - Run with `--insecure` (auth disabled) since the dashboard is on tailnet only. + - Run with `--host 0.0.0.0 --port 9119 --insecure --no-open --skip-build` + (`--insecure` disables the OAuth auth gate for tailnet-only use). + - Web UI built once to `/home/allaun/.hermes/hermes-agent/hermes_cli/web_dist`. - Public access: `https://chat.researchstack.info` via Caddy on racknerd - (`reverse_proxy http://100.85.244.73:9119`). -- **Local inference on qfox-1**: Ollama serving `hermes3:latest` built from + (`reverse_proxy http://100.88.57.96:9119`). + - Note: `100.85.244.73` is `nixos-steamdeck-1`, not qfox-1. +- **Local inference on qfox-1**: Official Ollama (v0.30.10) serving + `hermes3:latest` built from `/var/lib/gemma-models/Hermes-3-Llama-3.1-8B-Q4_K_M.gguf`. - Endpoint: `http://127.0.0.1:11434/v1` - Systemd unit: `ollama-hermes3.service` - - Note: `ollama-cuda` is installed but the packaged `llama-server` binary - currently falls back to CPU inference. GPU acceleration can be enabled later - by reinstalling Ollama from the official installer or building a CUDA-enabled - `llama-server`. + - GPU offload verified: `ollama ps` reports `100% GPU` and logs show + `offloaded 33/33 layers to GPU`. - **Hermes config**: `~/.hermes/config.yaml` points at the local Ollama: ```yaml model: diff --git a/scripts/load_dependency_graph.py b/scripts/load_dependency_graph.py index db6bfab0..35c90ff6 100644 --- a/scripts/load_dependency_graph.py +++ b/scripts/load_dependency_graph.py @@ -26,6 +26,7 @@ Phases: Run: uv run scripts/load_dependency_graph.py """ +import concurrent.futures import json import os import re @@ -570,10 +571,15 @@ def make_client(): ) +GREMLIN_TIMEOUT = 30 # seconds per query + def submit(c, query: str, bindings: dict = None): try: cb = c.submitAsync(query, bindings or {}) - return cb.result().all().result() + return cb.result(timeout=GREMLIN_TIMEOUT).all().result() + except concurrent.futures.TimeoutError: + print(f" TIMEOUT ({GREMLIN_TIMEOUT}s): {query[:120]}") + return None except Exception as e: print(f" ERR: {e!s:.200}") return None @@ -658,41 +664,66 @@ def load_to_gremlin(all_vertices: dict[str, dict], all_edges: list[tuple]): print(f" Loading {len(module_vertices)} module vertices (upsert)...") for i, v in enumerate(module_vertices): - upsert_vertex(c, v) - if (i + 1) % 500 == 0: + try: + upsert_vertex(c, v) + except Exception as e: + print(f" [{v['id']}] upsert failed: {e}") + if (i + 1) % 100 == 0: print(f" modules {i+1}/{len(module_vertices)}") print(f" Loading {len(dep_vertices)} dependency vertices...") for i, v in enumerate(dep_vertices): - upsert_vertex(c, v) - if (i + 1) % 500 == 0: + try: + upsert_vertex(c, v) + except Exception as e: + print(f" [{v['id']}] upsert failed: {e}") + if (i + 1) % 100 == 0: print(f" deps {i+1}/{len(dep_vertices)}") v_total = len(all_vertices) print(f" vertices done ({v_total}).") - # Load edges — single-threaded to stay within free tier RU budget + # Load edges — parallel with one Gremlin client per worker thread total_e = len(all_edges) - print(f" Loading {total_e} edges...") - failed_edges = 0 - for i, (src, dst, lbl) in enumerate(all_edges): + print(f" Loading {total_e} edges (4 workers)...") + + from concurrent.futures import ThreadPoolExecutor + import threading + + thread_local = threading.local() + + def _init_worker(): + thread_local.client = make_client() + + def _send_edge(args): + src, dst, lbl = args + cl = thread_local.client + src_safe = _safe_id(src) + dst_safe = _safe_id(dst) + src_esc = _esc(src_safe) + dst_esc = _esc(dst_safe) + lbl_esc = _esc(lbl) + q = (f"g.V().has('id','{src_esc}').as('s')" + f".V().has('id','{dst_esc}').as('d')" + f".coalesce(" + f" select('s').outE('{lbl_esc}').where(inV().as('d'))," + f" addE('{lbl_esc}').from('s').to('d')" + f")") try: - src_safe = _safe_id(src) - dst_safe = _safe_id(dst) - src_esc = _esc(src_safe) - dst_esc = _esc(dst_safe) - lbl_esc = _esc(lbl) - q = (f"g.V().has('id','{src_esc}').as('s')" - f".V().has('id','{dst_esc}').as('d')" - f".coalesce(" - f" select('s').outE('{lbl_esc}').where(inV().as('d'))," - f" addE('{lbl_esc}').from('s').to('d')" - f")") - submit(c, q) + submit(cl, q) + return True except Exception: - failed_edges += 1 - if (i + 1) % 500 == 0: - print(f" edges {i+1}/{total_e}") + return False + + failed_edges = 0 + with ThreadPoolExecutor(max_workers=4, initializer=_init_worker) as pool: + for i in range(0, total_e, 100): + batch = all_edges[i:i+100] + results = pool.map(_send_edge, batch) + failed_edges += sum(1 for r in results if not r) + done = min(i + 100, total_e) + if done % 500 == 0 or done == total_e: + print(f" edges {done}/{total_e}") print(f" edges done ({total_e}, {failed_edges} failed).")