allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(infra): parallel Gremlin edge loader; graph load complete

Browse source 
- 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
This commit is contained in:
allaun 2026-06-20 19:57:29 -05:00
parent e3521925a4
commit 8245ee633f
8 changed files with 477 additions and 151 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -282,3 +282,4 @@ result
# Recovery secrets backup - DO NOT COMMIT
4-Infrastructure/infra/secrets/
typescript

4
0-Core-Formalism/lean/Semantics/AGENTS.md
View file

@ -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`.

60
0-Core-Formalism/lean/Semantics/ExtensionScaffold/Physics/NBody.lean
View file

@ -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 :

356
0-Core-Formalism/lean/Semantics/Semantics/ErdosRenyiPipeline.lean
View file

@ -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<b,a,b∈S have distinct differences b-a ∈ {1,...,n-1},
-- so |S|(|S|-1)/2 ≤ n-1, giving |S|²-|S| ≤ 2(n-1).
-- Combined with |S| > 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<b vs b<a are mutually exclusive)
have h_disj : Disjoint sp sp' := by
rw [Finset.disjoint_filter]
intro ⟨a, b⟩ _ h1 h2
exact Nat.lt_asymm h1 h2
-- Step 5: sp ∪ sp' = S.offDiag (every off-diagonal pair satisfies a<b or b<a)
have h_union : sp ∪ sp' = S.offDiag := by
ext ⟨a, b⟩
simp only [hsp, hsp', Finset.mem_union, Finset.mem_filter, Finset.mem_offDiag]
constructor
· rintro (⟨h, _⟩ | ⟨h, _⟩) <;> 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<b, c<d in S, then a+d = b+c,
-- and Sidon with ordering gives a=c, b=d.
have h_inj : Set.InjOn (fun p : ℕ × ℕ => 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 and c<d so no underflow)
have haS : a ∈ S := ha.1.1
have hbS : b ∈ S := ha.1.2.1
have hcS : c ∈ S := hc.1.1
have hdS : d ∈ S := hc.1.2.1
have hab : a < b := ha.2
have hcd : c < d := hc.2
-- Beta-reduce heq and convert ℕ subtraction equality to addition equality
simp only at heq
-- b - a = d - c in ℕ with a<b and c<d gives a+d = b+c
have hsum : a + d = b + c := by omega
-- Apply Sidon: a+d = b+c, use ordering case split
-- IsSidonSet: ∀ a∈S b∈S c∈S d∈S, a≤b → c≤d → a+b=c+d → a=c ∧ b=d
-- We need a+d=b+c rewritten as a+d=c+b with a≤d and c≤b (or handle the other case)
by_cases had : a ≤ d
· by_cases hcb : c ≤ b
· -- a+d=b+c, a≤d, c≤b → Sidon: a,d ∈S, c,b ∈S, a+d=c+b → a=c ∧ d=b
have hsum' : a + d = c + b := by linarith
have h := hSidon a haS d hdS c hcS b hbS had hcb hsum'
simp only [Prod.mk.injEq]
exact ⟨h.1, h.2.symm⟩
· -- c > b: a+d = b+c > b+b ≥ a+b (wait, a<b so a≤b-1 so a+b≤2b-1)
-- more directly: c>b and c<d so b<c<d; and a+d=b+c means d-b=c-a>0
-- but also a<b so a+d=b+c and d=b+c-a>b. Combined with c>b and a<b:
-- d = b + c - a ≥ b + (b+1) - (b-1) = b+2 (this is getting complicated)
-- Just: from a+d=b+c with c>b: a+d > a+b so d>b; and d<n,c<n both < n fine.
-- From c>b≥0 and a+d=b+c: d = b+c-a. With a<b: d = b+c-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 b<c i.e. b≤c-1. Use Sidon with b≤c and a≤d:
-- hSidon b hbS c hcS a haS d hdS (b≤c by c>b → c.succ≤ but b<c gives b≤c-1≤c) had
push_neg at hcb
-- hcb : b < c
have hbc_le : b ≤ c := Nat.le_of_lt hcb
-- hsum : a + d = b + c → b + c = a + d and b≤c, a≤d
have hsum2 : b + c = a + d := hsum.symm
have h := hSidon b hbS c hcS a haS d hdS hbc_le had hsum2
-- h : b = a ∧ c = d, 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<a and c<d<a<b: a+d < a+a ≤ 2a < a+b
-- and b+c ≥ b+1 > b. Hmm. d<a so d≤a-1. b+c = a+d ≤ a+(a-1) = 2a-1.
-- but c<d<a and b>a, so b+c > a + c ≥ a+0, and also b+c > a+d? No: b+c=a+d.
-- d<a and c<d: so c<a. b+c = a+d with b>a and d<a and c<a.
-- b > 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<d<a<b: we have a≤d? No: d<a. hSidon needs ordering.
-- Use Sidon on (d,a) and (c,b)? d<a and c<b: d+a = c+b? No: a+d = b+c means d+a=c+b.
-- d ≤ a-1 < a. c < d < a. b > a > d > c. So d ≤ a, c ≤ b? d<a→d≤a; c<b→c≤b.
-- hSidon d hdS a haS c hcS b hbS (d≤a) (c≤b) (d+a=c+b)
-- d+a = a+d = b+c = c+b. ✓
have hda_le : d ≤ a := Nat.le_of_lt had
have hcd_lt_b : c < b := Nat.lt_trans hcd had |>.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

3
0-Core-Formalism/lean/Semantics/Semantics/HachimojiManifoldAxiom.lean
View file

@ -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)

100
0-Core-Formalism/lean/Semantics/Semantics/ImaginarySemanticTime.lean
View file

@ -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)

25
AGENTS.md
View file

@ -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:

79
scripts/load_dependency_graph.py
View file

@ -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).")