mirrormere: the full prime-free window (2L <= log 2) proved kernel-native, hypothesis-free, no Arb seam (draft; includes #606; grant after #607) - #615

Open

DrMurphyIsIn wants to merge 12 commits into

mainfrom

Commits on Sep 24, 2026

rvm_bridge: KWin -- kernel-native (Arb-free) prime-free window: WindowFloor(log2/2, 9/10000) and the PrimeFreeWindowPositivity body at 2L = log 2, hypothesis-free

Dr. Murphy
and
claude
committed
c4d17bc
merge origin/main into cl/kwin; KWin_Bridge: RvMBridge31.PrimeFreeWindowPositivity (E6Bridge31, main) PROVED hypothesis-free; register MM_weil_positivity_prime_free_window (DRAFT)

Dr. Murphy
and
claude
committed
fbbcade
mirrormere: registry fixes from independent review -- [proof] link, name MM.weil_positivity_prime_free_window, window_tenth containment now a kernel corollary (weil_positivity_window_tenth_of_prime…

Dr. Murphy
and
claude
committed
3cd7a08
mirrormere: regenerate MM_weil_positivity_prime_free_window statement WITH imports (Mathlib + Statements.MMDefs) via the mission CLI

Dr. Murphy
and
claude
committed
b4191a0
Merge remote-tracking branch 'origin/main' into cl/kwin
Dr. Murphy
committed
77c6ad9
Merge remote-tracking branch 'origin/main' into cl/kwin
Dr. Murphy
committed
e099048
Merge remote-tracking branch 'origin/main' into cl/kwin
Dr. Murphy
committed
fc2d1ba
mirrormere: grant MM.weil_positivity_prime_free_window under #607 provenance (honest labels) + rvm_bridge judge bundle

Dr. Murphy
and
claude
committed
a772f5b

Commits on Sep 25, 2026

Merge remote-tracking branch 'origin/main' into cl/kwin
Dr. Murphy
committed
8f3fbd3
Merge remote-tracking branch 'origin/main' into HEAD
Dr. Murphy
committed
0c97ff7
missions: heavy_certificates on the KWin node (judge runs Lean-kernel-only)

Dr. Murphy
and
claude
committed
2d33e58
missions: record the Lean-kernel-only Comparator pass on the KWin node

Dr. Murphy
and
claude
committed
0a8f24d