mirrormere: Weil window positivity past the prime-free boundary to L = 1/2, kernel-native, no Arb (draft; stacked on #615; grant after #607) - #619

Draft

DrMurphyIsIn wants to merge 13 commits into

Commits on Sep 24, 2026

rvm_bridge: KWin2 -- kernel-native Weil window positivity PAST the prime-free boundary: L = 2/5, 9/20, 1/2, hypothesis-free, no Arb seam

Dr. Murphy
and
claude
committed
fed5a61
mirrormere: register MM.weil_positivity_window_half (DRAFT); statement compiles against MMDefs; no grant before #607

Dr. Murphy
and
claude
committed
1e96a6a
mirrormere: register MM.weil_positivity_window_two_fifths (DRAFT, CI-buildable) instead of window_half (KWin2_BridgeHeavy needs 17-19 GB, above the 16 GB hosted runner, so CI cannot verify it)

Dr. Murphy
and
claude
committed
2bf7701
Merge remote-tracking branch 'origin/cl/kwin' into cl/kwin2
Dr. Murphy
committed
8f37304
missions: NOT_MIRRORS exemption for KWin2.expLo (rational Taylor lower bound, not BraggDefect.expLo)

Dr. Murphy
and
claude
committed
5c6d6d7
Merge remote-tracking branch 'origin/cl/kwin' into cl/kwin2
Dr. Murphy
committed
b1a7194
Merge remote-tracking branch 'origin/cl/kwin' into cl/kwin2
Dr. Murphy
committed
66f65e4
mirrormere: grant MM.weil_positivity_window_two_fifths under #607 provenance (honest labels) + rvm_bridge judge bundle

Dr. Murphy
and
claude
committed
3fa979b

Commits on Sep 25, 2026

Merge remote-tracking branch 'origin/cl/kwin' into cl/kwin2
Dr. Murphy
committed
b20081c
Merge remote-tracking branch 'origin/cl/kwin' into HEAD
Dr. Murphy
committed
9ae3bc5
missions: heavy_certificates on the KWin2 node (judge runs Lean-kernel-only)

Dr. Murphy
and
claude
committed
8e9b4cb
Merge remote-tracking branch 'origin/cl/kwin' into HEAD
Dr. Murphy
committed
c8dddd7
missions: record the Lean-kernel-only Comparator pass on the KWin2 node

Dr. Murphy
and
claude
committed
63d9e7b