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
Draft
DrMurphyIsIn wants to merge 13 commits into
DrMurphyIsIn wants to merge 13 commits into
Conversation
…ime-free boundary: L = 2/5, 9/20, 1/2, hypothesis-free, no Arb seam weil_positivity_window_half: every Weil test with support in [-L, L], 2L <= 1, has Re weilForm (autocorr g) >= 0; weil_window_floor_half : WindowFloor (1/2) (7/20000000). The n = 2 prime-comb term is present (2L = 1 > log 2) and accounted exactly. Pole terms KEPT (goal-node test class). Build 8955 jobs, all guard lines standard; skeptic not refuted; lead re-probed axioms. Finite window, NOT RH. conjecture1_proved = False. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6
…t compiles against MMDefs; no grant before #607 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6
…buildable) instead of window_half (KWin2_BridgeHeavy needs 17-19 GB, above the 16 GB hosted runner, so CI cannot verify it) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6
# Conflicts: # telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean
…r bound, not BraggDefect.expLo) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6
# Conflicts: # telperion/missions/mirrormere/lean/Statements.lean
…venance (honest labels) + rvm_bridge judge bundle merge cl/kwin (#615 grant) + main; read-back written in the author's session, recorded independence = "unverified"; granted via `mission grant` ([grant] digests, gate 2026-09-23.1; owner ruling 2026-09-24); rvm_bridge judge bundle regenerated (--check OK, 54 challenges). window_half (KWin2_BridgeHeavy) stays unregistered (outside CI). conjecture1_proved = False. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6
…l-only) `MM_weil_positivity_window_two_fifths` declares `heavy_certificates = true`, so the Comparator judge writes its config with `enable_nanoda = false`: the Lean kernel replay and the export axiom whitelist still run, the second (nanoda) kernel does not. The L = 1/2 window certificates are the heaviest in the registry (~1100 s and ~16 GB per decide in the local rebuild), well past what a 16 GB runner survives with two kernels. Merged cl/kwin in, which carries main (#632's flag, swap step and dispatch filter, #625's `ulimit -s unlimited`) and the same flag on the prime-free-window node. The two heavy nodes land in different shards -- prime-free in rvm_bridge 2/4, two-fifths in 3/4 -- so each shard has at most one heavy node and gets the swap step only where it is needed. Judge bundle regenerated; `judge --island rvm_bridge --check` matches the registry (54 challenges) and both heavy nodes' config rows read `lean-kernel-only`. `mission verify` is OK on all four campaigns. The records follow once the shards pass, as `comparator-record --lean-kernel-only`. No Lean source changes; no status change; conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
`judge rvm_bridge 3/4` of run 36170028959 (job 108205123231) passed 13/13. The
line for this node is
COMPARATOR PASS island=rvm_bridge node=MM_weil_positivity_window_two_fifths
theorem=weil_positivity_window_two_fifths run=36170028959
kernel=lean-kernel-only
and the other twelve nodes of that shard print `kernel=nanoda`, so the flag took
the second kernel off this node alone. All four rvm_bridge shards of the run
passed, so the other heavy node (prime-free window, shard 2/4 here) passed on
this branch too.
The recorded artifact sha256 (f868b415...) equals the one in `[grant]`: the judge
checked the artifact the grant pinned. `provenance-report` now prints "Lean
kernel only (heavy_certificates: nanoda not run)" for both heavy nodes.
Also merged cl/kwin, which carries the prime-free-window record, so this branch
states both verdicts.
This record additionally pins `job_id`, `job_url` and the observed `kernel_mode`.
The run's own conclusion is not a usable anchor: pushing a record onto the same
pull request supersedes the run that validated the artifact (missions-comparator
cancels in-progress runs on pull_request), so cl/kwin's run 36169770951 now reads
"cancelled" although the job that judged the node succeeded. The job plus the
artifact hash are what a verifier can check. Those three fields come from a
schema addition that is not on main yet (PR pending); code without it ignores
them, which I checked by loading this node with the branch's own registry
loader.
`mission verify` OK on all four campaigns; `judge --island rvm_bridge --check`
matches the registry (54 challenges). No status change, no Lean source change;
conjecture1_proved = False.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR is stacked on #615.
conjecture1_proved = False: it is positivity on a finite window, not RH.It extends the kernel-native Weil window from the prime-free boundary (2L = log 2, #615) to L = 2/5, 9/20 and 1/2. At these widths the prime-2 term is present in the Weil form, since 2L = 1 > log 2.
weil_positivity_window_half. For every Weil test g with support in [-L, L] and 2L <= 1,Re weilForm (autocorr g) >= 0. The quantitative form isWindowFloor (1/2) (7/20000000). It is hypothesis-free, with no Arb seam.decide +kernel, and a projection tail. The finite prime-comb term is bounded pointwise by a certified polynomial (degree-95 Taylor of cos,comb_le_combPoly; margin loss ~1e-11, valid because |F|^2 >= 0), and a rounded checker closes the thin margin at L = 1/2.Verification
weil_positivity_window_half,weil_window_floor_halfand..._nine_twentiethsmyself.mission verifyis OK for all four campaigns.Registry
The registered node is
MM.weil_positivity_window_two_fifths(DRAFT). Its artifact,KWin2_Bridge, is in CI's default build and the main axiom guard, with a 12.2 GB peak. The L = 9/20 and L = 1/2 results inKWin2_BridgeHeavyare proved and verified locally, but they peak at 17-19 GB, above the 16 GB hosted runner. They are therefore NOT registered until CI can build them. It will not be granted before #607; after #607 it gets an independent audit and then the Comparator judge.🤖 Generated with Claude Code
https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6
Update (independent skeptic, peer session): the L = 1/2 chain is sound end to end. A separate Rayleigh-Ritz on the true form puts the even-sector minima 2.5 to 5x above the certified floors. Its three flagged diff defects were stale-base drift, not edits: cl/kwin had gained the regenerated statement header, the #616
|| true, and the ZHU provenance lines after this branch forked. They are fixed by merging cl/kwin (8f37304). The mirrormere Statements package builds, and the rvm_bridge guard elaborates with 0 errors and standard axioms only. The registered node is 2/5 only; window_half stays out of CI and ungranted.