Skip to content

missions: record Comparator run 36054938938 on the 64 judged nodes; uncovered islands - #624

Draft
DrMurphyIsIn wants to merge 1 commit into
mainfrom
missions/comparator-backfill
Draft

DrMurphyIsIn wants to merge 1 commit into
mainfrom
missions/comparator-backfill

Conversation

@DrMurphyIsIn

Copy link
Copy Markdown
Owner

Backfill of [comparator] records from the first green missions-comparator run on main after #607 (run 36054938938, head a8bcca0): every proved node the judge covered now carries comparator = {run_id, date, artifact_sha256, theorem, run_url}, written with mission comparator-record. No status changed, no grant run, no read-back touched. conjecture1_proved = False.

What was recorded

island nodes recorded shard(s)
dbn 3 judge dbn 0/1
rvm_bridge 52 judge rvm_bridge 0..3/4
zeta_reflection 9 judge zeta_reflection 0/1

mission verify OK on all four campaigns. mission provenance-report after the backfill:

anduril: 10 proved, 1 without an independent read-back or a passing Comparator run
  (9 proved node(s) covered by a passing Comparator run)
bg: 9 proved, 9 without an independent read-back or a passing Comparator run
mirrormere: 38 proved, 14 without an independent read-back or a passing Comparator run
  (24 proved node(s) covered by a passing Comparator run)
rh: 53 proved, 22 without an independent read-back or a passing Comparator run
  (31 proved node(s) covered by a passing Comparator run)

A node with a [comparator] record leaves the provenance report only while the record's artifact_sha256 matches the artifact on disk; an edit to the artifact makes verify warn "independent verdict is stale" until the job passes again and the run is re-recorded.

Proved nodes still without judge coverage (48), and what each island needs

island proved nodes what it would take
li_positivity 24 (RH_backlund_s_log, RH_bl_finite_multiset, RH_borel_caratheodory_deriv, RH_companion_bragg_reduction, RH_dlvp_region_effective, RH_li_ladder_height, RH_li_ladder_height_sharp, RH_li_ladder_reduction, RH_li_neg_refutes_rh, RH_li_rung0_kernel, RH_li_rung_certificates, RH_li_rungs_lt_five, RH_li_rungs_of_height_4000, RH_li_rungs_of_height_4000_sharp, RH_strip_repr, RH_zero_free_gamma5, RH_zero_free_polylog, RH_zeta_log_bound, RH_zeta_repr_R1, RH_zeta_zero_confined, RH_zeta_zero_im_ge, MM_bragg_bridge, MM_rect_trace_reading, MM_spectral_cooked_control) Smallest step. The bundle already renders (24/24) and bundles-in-sync lists it. Add li_positivity to the judge matrix (toolchain v4.34.0-rc1, tag exists) and commit python -m telperion.missions.judge --island li_positivity. Cost: the island build alone is about an hour on the hosted runner (the li-positivity-compiles job), then ~2-3 min per node, so two shards of 12. One caveat to check on the first run: the island has TWO AxiomGuard libs (AxiomGuardLiPositivity, AxiomGuardZeroFree) and the closure-run audit noted AxiomGuardLiPositivity cannot import ZeroFreePolylog because of a zeta_sphere_bound clash; if the two guards do not co-import, the bridge module fails to build and the judge reports it. The fix is then to import only the guard(s) whose closure contains the artifact, or to resolve the clash on the island.
quasicrystal 8 (MM_euler_factor_section_offline, MM_leakage_composite_zero, MM_nt_brick_conditional, MM_offline_disjoint_discs, MM_primelog_spectrum_dense, MM_selfinversive_iff_hardyz_real, MM_torus_section_n2_rigidity, MM_twofreq_realrooted_iff) 7 of 8 render (v4.32.0, tag exists). MM_leakage_composite_zero is not consumable as registered: its statement declares four local defs before the theorem, which the bridge cannot re-declare beside the artifact's copies; judging it needs the statement re-registered to use the island's own definitions (an owner decision on a proved node's statement), or a judge mode that renames the local defs. The island path-requires the zeta_zero_localization sub-projects (same pattern the satake job builds), so a matrix entry + committed bundle should work; ~30-60 min.
zeta_zero_localization 3 (MM_bragg_defect_witness, MM_offline_pairs_le_defect, MM_recurrence_deficit_eq_excess) Cannot be path-required as is: the island's root lakefile is the 27k-lib monolith (Lake does not deduplicate LEAN_SRC_PATH, so lake env exceeds ARG_MAX, the same wall the zeta-reflection job hit). Needs the artifacts moved under, or a bundle that path-requires, the slim zzl_core / zzl_aux sub-projects, plus the shared-packages wiring the exp-enclosure job uses. zzl_aux/lakefile.toml also lists libs that are not monolith lean_libs (closure run 2026-09-22), so that drift must be fixed first.
zero_free_bridge 1 (RH_dlvp_zero_free_region) v4.32.0, tag exists; the island builds in CI via the zero-free-bridge-suite job. A one-node shard; needs a matrix entry + bundle, and the island's shared-packages wiring (it path-requires zeta_zero_localization's packages in the exp-enclosure job). ~45 min.
bg (proof/formalization) 9 (BG_cavity_recursion, BG_fractal_asymptote, BG_gstep_closure, BG_h1_bridge, BG_lb_classification, BG_merge_layer, BG_near_star_tail, BG_near_star_tie, BG_phi_le_one) Not an example island (artifacts under proof/formalization/R3Cert), so judge.py does not see it. proof-comparator.yml already judges three of the nine in self-check mode (no registry statement). To bring the nine under the registry judge: teach judge.py a second root (proof/formalization, package R3Cert) and let the bundle path-require it; the bridge form then works unchanged. Cost is the R3Cert build (the proof-lean job needs swap + staging to fit in 16 GB; ~1h45m), so this shard would want the same swap/stage steps or the warm build cache proof-lean keeps.
zeta_reflection (1 of 10) AND_g2_reflected_band Its statement declares a namespace block besides the theorem; same remedy as MM_leakage_composite_zero.

Nodes that land later (RH_dbn_debruijn_real_zeros from #609, AND_ladder_h1000_kernel from #613, AND_ladder_h8000_kernel from #620, MM_weil_positivity_prime_free_window from #615) become judge targets automatically once proved; each such PR must regenerate its island's bundle so bundles-in-sync stays green, and can then cite the judge run with mission comparator-record (and, for #620, mission ci-record for the kernel-ladder job it declares in requires_ci_job).

🤖 Generated with Claude Code

https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU

First green missions-comparator run on main after #607 (head a8bcca0):
judge dbn 0/1, rvm_bridge 0..3/4, zeta_reflection 0/1 all passed. Each
judged node now carries [comparator] {run_id, date, artifact_sha256,
theorem, run_url}, written with `mission comparator-record` from the
`COMPARATOR PASS` lines of the run's job logs (3 dbn + 52 rvm_bridge +
9 zeta_reflection). No status changed, no grant run, no read-back touched;
verify OK on all four campaigns. Provenance report now: anduril 1/10
flagged, bg 9/9, mirrormere 14/38, rh 22/53. conjecture1_proved = False.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant