missions: judge li_positivity (24) and quasicrystal (7 of 8) islands - #627
Draft
DrMurphyIsIn wants to merge 1 commit into
Draft
DrMurphyIsIn wants to merge 1 commit into
DrMurphyIsIn wants to merge 1 commit into
Conversation
…7 of 8) li_positivity: its two AxiomGuard libs cannot be imported together (`ZeroFreeBridge.zeta_sphere_bound` is declared in DlvpZetaDisk, in AxiomGuardLiPositivity's closure, and in ZeroFreeElementary, in AxiomGuardZeroFree's), so a per-island policy imports only the first guard whose island-local import closure contains the artifact (22 bridges use AxiomGuardLiPositivity, 2 AxiomGuardZeroFree) and the root module carries no imports; CI builds the bridge modules by name. All 24 elaborate locally against the island build; RH_zero_free_polylog, RH_li_rungs_lt_five and MM_bragg_bridge pass the v4.34.0-rc1 Comparator under both kernels. quasicrystal: 7 of 8 (MM_leakage_composite_zero declares four local defs before its theorem; the bridge imports the artifact, so re-declaring them is a duplicate declaration -- reported, not skipped; judging it needs the statement re-registered against the island's own definitions, an owner decision). The island has no AxiomGuard lean_lib, so its bridges import only the artifact (documented: no shadowing guard there). All 7 elaborate; MM_twofreq_realrooted_iff and MM_nt_brick_conditional pass the v4.32.0 Comparator. Also carries the judge-step `ulimit -s` raise from #625 (nanoda main-thread stack overflow on KWin certificates). Matrix: li_positivity 0/2, 1/2; quasicrystal 0/1; bundles-in-sync checks all five islands. 27 judge tests. Co-Authored-By: Claude Fable 5.1 <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.
Extends the independent judge (
missions-comparator.yml, see #607) to two more islands. No registry status change, no grant.conjecture1_proved = False.RH_zero_free_polylog,RH_li_rungs_lt_five,MM_bragg_bridgepass under Lean kernel + nanoda (2.7-3.6 min each)MM_twofreq_realrooted_iff(76 s),MM_nt_brick_conditional(22 s) passli_positivity guard policy. Its two AxiomGuard libs cannot be imported into one module:
ZeroFreeBridge.zeta_sphere_boundis declared inDlvpZetaDisk(inAxiomGuardLiPositivity's closure) and inZeroFreeElementary(inAxiomGuardZeroFree's).judge.pynow has a per-island policy (GUARD_POLICY_ONE_CONTAINING = {"li_positivity"}): each bridge imports only the first guard whose island-local import closure contains its artifact (22 useAxiomGuardLiPositivity, 2 useAxiomGuardZeroFree), and the bundle's root module carries no imports (CI builds bridge modules by name). The shadowing check therefore covers that guard's closure rather than the whole island; documented in the README and AUDIT_INDEPENDENCE section 4.quasicrystal.
MM_leakage_composite_zerois not consumable as registered: its statement declares four localdefs before the theorem, and the bridge imports the artifact, so re-declaring them is a duplicate declaration. Judging it needs the statement re-registered against the island's own definitions (an owner decision on a proved node's statement); it is reported by the generator, not silently skipped. The island has noAxiomGuard*lean_lib, so its bridges import only the artifact (no shadowing guard there;AxiomGuardQC.leanruns vialake env leanin the satake job).Also carries the judge-step
ulimit -sraise from #625.bundles-in-syncnow checks all five islands. Judge tests: 27.Shard times from this PR's run will be added here. Once green, the passes get recorded on the nodes with
mission comparator-recordin a follow-up to #624.🤖 Generated with Claude Code
https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU