From 77406f85199ccd730a66a3a5da07557341743208 Mon Sep 17 00:00:00 2001 From: "Dr. Murphy" Date: Thu, 24 Sep 2026 20:26:35 -0400 Subject: [PATCH] missions: judge li_positivity (24 nodes, 2 shards) and quasicrystal (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 Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU --- .github/workflows/missions-comparator.yml | 31 +- .../docs/AUDIT_INDEPENDENCE_2026-09-23.md | 19 +- telperion/missions/judge/README.md | 3 + .../judge/li_positivity/MANIFEST.json | 273 ++++++++++++++++++ .../MM_bragg_bridge.comparator.json | 13 + .../MM_rect_trace_reading.comparator.json | 13 + ...MM_spectral_cooked_control.comparator.json | 13 + .../li_positivity/MissionChallenges.lean | 3 + .../MissionChallenges/MM_bragg_bridge.lean | 37 +++ .../MM_rect_trace_reading.lean | 38 +++ .../MM_spectral_cooked_control.lean | 17 ++ .../MissionChallenges/RH_backlund_s_log.lean | 24 ++ .../RH_bl_finite_multiset.lean | 22 ++ .../RH_borel_caratheodory_deriv.lean | 25 ++ .../RH_companion_bragg_reduction.lean | 30 ++ .../RH_dlvp_region_effective.lean | 24 ++ .../RH_li_ladder_height.lean | 26 ++ .../RH_li_ladder_height_sharp.lean | 26 ++ .../RH_li_ladder_reduction.lean | 23 ++ .../RH_li_neg_refutes_rh.lean | 23 ++ .../MissionChallenges/RH_li_rung0_kernel.lean | 20 ++ .../RH_li_rung_certificates.lean | 22 ++ .../RH_li_rungs_lt_five.lean | 22 ++ .../RH_li_rungs_of_height_4000.lean | 24 ++ .../RH_li_rungs_of_height_4000_sharp.lean | 24 ++ .../MissionChallenges/RH_strip_repr.lean | 20 ++ .../RH_zero_free_gamma5.lean | 23 ++ .../RH_zero_free_polylog.lean | 24 ++ .../MissionChallenges/RH_zeta_log_bound.lean | 22 ++ .../MissionChallenges/RH_zeta_repr_R1.lean | 22 ++ .../RH_zeta_zero_confined.lean | 23 ++ .../MissionChallenges/RH_zeta_zero_im_ge.lean | 23 ++ .../RH_backlund_s_log.comparator.json | 13 + .../RH_bl_finite_multiset.comparator.json | 13 + ...H_borel_caratheodory_deriv.comparator.json | 13 + ..._companion_bragg_reduction.comparator.json | 13 + .../RH_dlvp_region_effective.comparator.json | 13 + .../RH_li_ladder_height.comparator.json | 13 + .../RH_li_ladder_height_sharp.comparator.json | 13 + .../RH_li_ladder_reduction.comparator.json | 13 + .../RH_li_neg_refutes_rh.comparator.json | 13 + .../RH_li_rung0_kernel.comparator.json | 13 + .../RH_li_rung_certificates.comparator.json | 13 + .../RH_li_rungs_lt_five.comparator.json | 13 + ...RH_li_rungs_of_height_4000.comparator.json | 13 + ...rungs_of_height_4000_sharp.comparator.json | 13 + .../RH_strip_repr.comparator.json | 13 + .../RH_zero_free_gamma5.comparator.json | 13 + .../RH_zero_free_polylog.comparator.json | 13 + .../RH_zeta_log_bound.comparator.json | 13 + .../RH_zeta_repr_R1.comparator.json | 13 + .../RH_zeta_zero_confined.comparator.json | 13 + .../RH_zeta_zero_im_ge.comparator.json | 13 + .../judge/li_positivity/lakefile.toml | 12 + .../judge/li_positivity/lean-toolchain | 1 + .../missions/judge/quasicrystal/MANIFEST.json | 88 ++++++ ...ler_factor_section_offline.comparator.json | 13 + .../MM_nt_brick_conditional.comparator.json | 13 + .../MM_offline_disjoint_discs.comparator.json | 13 + ...MM_primelog_spectrum_dense.comparator.json | 13 + ...finversive_iff_hardyz_real.comparator.json | 13 + ..._torus_section_n2_rigidity.comparator.json | 13 + .../MM_twofreq_realrooted_iff.comparator.json | 13 + .../judge/quasicrystal/MissionChallenges.lean | 7 + .../MM_euler_factor_section_offline.lean | 22 ++ .../MM_nt_brick_conditional.lean | 21 ++ .../MM_offline_disjoint_discs.lean | 22 ++ .../MM_primelog_spectrum_dense.lean | 21 ++ .../MM_selfinversive_iff_hardyz_real.lean | 25 ++ .../MM_torus_section_n2_rigidity.lean | 23 ++ .../MM_twofreq_realrooted_iff.lean | 22 ++ .../missions/judge/quasicrystal/lakefile.toml | 12 + .../judge/quasicrystal/lean-toolchain | 1 + telperion/src/telperion/missions/judge.py | 57 +++- telperion/tests/test_missions_judge.py | 39 ++- 75 files changed, 1667 insertions(+), 22 deletions(-) create mode 100644 telperion/missions/judge/li_positivity/MANIFEST.json create mode 100644 telperion/missions/judge/li_positivity/MM_bragg_bridge.comparator.json create mode 100644 telperion/missions/judge/li_positivity/MM_rect_trace_reading.comparator.json create mode 100644 telperion/missions/judge/li_positivity/MM_spectral_cooked_control.comparator.json create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/MM_bragg_bridge.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/MM_rect_trace_reading.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/MM_spectral_cooked_control.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_backlund_s_log.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_bl_finite_multiset.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_borel_caratheodory_deriv.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_companion_bragg_reduction.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_dlvp_region_effective.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_height.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_height_sharp.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_reduction.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_li_neg_refutes_rh.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rung0_kernel.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rung_certificates.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_lt_five.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_of_height_4000.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_of_height_4000_sharp.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_strip_repr.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_zero_free_gamma5.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_zero_free_polylog.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_log_bound.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_repr_R1.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_zero_confined.lean create mode 100644 telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_zero_im_ge.lean create mode 100644 telperion/missions/judge/li_positivity/RH_backlund_s_log.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_bl_finite_multiset.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_borel_caratheodory_deriv.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_companion_bragg_reduction.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_dlvp_region_effective.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_li_ladder_height.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_li_ladder_height_sharp.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_li_ladder_reduction.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_li_neg_refutes_rh.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_li_rung0_kernel.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_li_rung_certificates.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_li_rungs_lt_five.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_li_rungs_of_height_4000.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_li_rungs_of_height_4000_sharp.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_strip_repr.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_zero_free_gamma5.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_zero_free_polylog.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_zeta_log_bound.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_zeta_repr_R1.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_zeta_zero_confined.comparator.json create mode 100644 telperion/missions/judge/li_positivity/RH_zeta_zero_im_ge.comparator.json create mode 100644 telperion/missions/judge/li_positivity/lakefile.toml create mode 100644 telperion/missions/judge/li_positivity/lean-toolchain create mode 100644 telperion/missions/judge/quasicrystal/MANIFEST.json create mode 100644 telperion/missions/judge/quasicrystal/MM_euler_factor_section_offline.comparator.json create mode 100644 telperion/missions/judge/quasicrystal/MM_nt_brick_conditional.comparator.json create mode 100644 telperion/missions/judge/quasicrystal/MM_offline_disjoint_discs.comparator.json create mode 100644 telperion/missions/judge/quasicrystal/MM_primelog_spectrum_dense.comparator.json create mode 100644 telperion/missions/judge/quasicrystal/MM_selfinversive_iff_hardyz_real.comparator.json create mode 100644 telperion/missions/judge/quasicrystal/MM_torus_section_n2_rigidity.comparator.json create mode 100644 telperion/missions/judge/quasicrystal/MM_twofreq_realrooted_iff.comparator.json create mode 100644 telperion/missions/judge/quasicrystal/MissionChallenges.lean create mode 100644 telperion/missions/judge/quasicrystal/MissionChallenges/MM_euler_factor_section_offline.lean create mode 100644 telperion/missions/judge/quasicrystal/MissionChallenges/MM_nt_brick_conditional.lean create mode 100644 telperion/missions/judge/quasicrystal/MissionChallenges/MM_offline_disjoint_discs.lean create mode 100644 telperion/missions/judge/quasicrystal/MissionChallenges/MM_primelog_spectrum_dense.lean create mode 100644 telperion/missions/judge/quasicrystal/MissionChallenges/MM_selfinversive_iff_hardyz_real.lean create mode 100644 telperion/missions/judge/quasicrystal/MissionChallenges/MM_torus_section_n2_rigidity.lean create mode 100644 telperion/missions/judge/quasicrystal/MissionChallenges/MM_twofreq_realrooted_iff.lean create mode 100644 telperion/missions/judge/quasicrystal/lakefile.toml create mode 100644 telperion/missions/judge/quasicrystal/lean-toolchain diff --git a/.github/workflows/missions-comparator.yml b/.github/workflows/missions-comparator.yml index 6a305e2ba..e423fe2ce 100644 --- a/.github/workflows/missions-comparator.yml +++ b/.github/workflows/missions-comparator.yml @@ -17,8 +17,8 @@ name: missions-comparator # written by the proof's author, which is the point. # # Sharded per island (`--shard I/N` over slug order; every node lands in exactly one shard). -# The Comparator tag FOLLOWS THE ISLAND TOOLCHAIN (dbn v4.34.0-rc1, rvm_bridge v4.33.0-rc2, -# zeta_reflection v4.32.0): +# The Comparator tag FOLLOWS THE ISLAND TOOLCHAIN (dbn / li_positivity v4.34.0-rc1, +# rvm_bridge v4.33.0-rc2, zeta_reflection / quasicrystal v4.32.0): # the comparator + lean4export must be built with the toolchain whose .olean they export, so # the v4.32.0 pin of the BG bridge does not apply here. Landrun (urfave/cli) strips the `--` # separator lean4export needs, hence the shim (same as proof-comparator.yml). @@ -26,8 +26,7 @@ name: missions-comparator # Not a required check yet. To make a node's record reflect a pass: # PYTHONPATH=src python -m telperion.cli mission comparator-record --run-id \ # --theorem --run-url -# Islands not yet wired: li_positivity (24 nodes, renders; the island build alone is ~1 h), -# quasicrystal / zero_free_bridge (v4.32.0; their lakefiles path-require other islands), and +# Islands not yet wired: zero_free_bridge (1 node, v4.32.0; shared-packages wiring) and # zeta_zero_localization (monolith lakefile, cannot be path-required: ARG_MAX). BG's nine # nodes are judged by proof-comparator.yml in self-check mode. conjecture1_proved = False. @@ -38,6 +37,10 @@ on: - "telperion/examples/dbn/**" - "telperion/examples/rvm_bridge/**" - "telperion/examples/zeta_reflection/**" + - "telperion/examples/li_positivity/**" + - "telperion/examples/quasicrystal/**" + - "telperion/examples/li_positivity/**" + - "telperion/examples/quasicrystal/**" - "telperion/src/telperion/missions/judge.py" - "telperion/src/telperion/comparator.py" - "telperion/scripts/guard_anchors.py" @@ -73,14 +76,14 @@ jobs: working-directory: telperion run: | set -euo pipefail - for isl in dbn rvm_bridge zeta_reflection; do + for isl in dbn rvm_bridge zeta_reflection li_positivity quasicrystal; do PYTHONPATH=src python -m telperion.missions.judge --island "$isl" --check done - - name: Every wired island still renders (li_positivity is listed, not judged, yet) + - name: Every wired island still renders working-directory: telperion run: | set -euo pipefail - for isl in dbn rvm_bridge zeta_reflection li_positivity; do + for isl in dbn rvm_bridge zeta_reflection li_positivity quasicrystal; do PYTHONPATH=src python -m telperion.missions.judge --island "$isl" --list | tail -1 done @@ -104,6 +107,12 @@ jobs: shard: "3/4" - island: zeta_reflection shard: "0/1" + - island: li_positivity + shard: "0/2" + - island: li_positivity + shard: "1/2" + - island: quasicrystal + shard: "0/1" name: judge ${{ matrix.island }} ${{ matrix.shard }} env: BUNDLE: telperion/missions/judge/${{ matrix.island }} @@ -206,6 +215,14 @@ jobs: run: | set -uo pipefail echo "lean4export = $COMPARATOR_LEAN4EXPORT ; nanoda = $COMPARATOR_NANODA" + # Stack (2026-09-24, #615 run 36055910789): nanoda's kernel is recursive and the KWin + # artifacts carry large `decide +kernel` LDL^T certificates; replaying them overflowed + # the 8 MB MAIN-thread stack ("thread 'main' has overflowed its stack", exit 134). + # RUST_MIN_STACK only sizes spawned threads, so raise the process limit here; the + # comparator's children (lean4export, nanoda) inherit it. Fall back to 4 GB if the + # runner's hard limit refuses unlimited; never let the fallback itself fail the job. + ulimit -s unlimited 2>/dev/null || ulimit -s 4194304 2>/dev/null || echo "::warning::could not raise the stack limit (ulimit -s); large certificates may overflow nanoda" + echo "stack limit (KB): $(ulimit -s)" fail=0; pass=0 { echo "## missions-comparator: ${{ matrix.island }} shard ${{ matrix.shard }} (run ${{ github.run_id }})" diff --git a/telperion/docs/AUDIT_INDEPENDENCE_2026-09-23.md b/telperion/docs/AUDIT_INDEPENDENCE_2026-09-23.md index 747f45846..6d00ffcf8 100644 --- a/telperion/docs/AUDIT_INDEPENDENCE_2026-09-23.md +++ b/telperion/docs/AUDIT_INDEPENDENCE_2026-09-23.md @@ -95,13 +95,18 @@ islands' `generate.py --check` jobs. Whether the island's `DBN.H` is the de Brui `H` is the read-back's job. The judge closes the gap between the two: given the vocabulary, the artifact proves this proposition and nothing weaker. -Coverage on 2026-09-23: the `dbn` island (3 nodes), the `rvm_bridge` island (52 nodes, -four shards) and the `zeta_reflection` island (9 of 10 nodes: `AND_g2_reflected_band` -declares a namespace inside its statement, which the bridge cannot reproduce beside the -artifact; it is reported, not skipped) are wired; `li_positivity` (24 nodes) renders and is -listed but not yet run; `quasicrystal` (7 of 8: `MM_leakage_composite_zero` carries local -`def`s), `zero_free_bridge` (1) and `zeta_zero_localization` (3; monolith lakefile, cannot be -path-required) are not wired. BG's nine nodes are judged by `proof-comparator.yml` in +Coverage on 2026-09-24: `dbn` (3 nodes), `rvm_bridge` (52, four shards), `zeta_reflection` +(9 of 10: `AND_g2_reflected_band` declares a namespace inside its statement, which the bridge +cannot reproduce beside the artifact; reported, not skipped), `li_positivity` (24, two shards) +and `quasicrystal` (7 of 8: `MM_leakage_composite_zero` declares four local `def`s before its +theorem, and the bridge module imports the artifact, so re-declaring them would be a duplicate +declaration; judging it needs the statement re-registered against the island's own +definitions, an owner decision on a proved node) are wired. `quasicrystal` has no +`AxiomGuard*` lean_lib, so its bridge modules import only the artifact: the duplicate- +declaration shadowing guard described above does not apply there (`AxiomGuardQC.lean` is run +by `lake env lean` in the satake job, which imports the whole island for the `#print axioms` +check). Not wired: `zero_free_bridge` (1) and `zeta_zero_localization` (3; monolith lakefile, +cannot be path-required). BG's nine nodes are judged by `proof-comparator.yml` in self-check mode (no independent statement; statement identity there is by human review). ## 5. What a session should do now diff --git a/telperion/missions/judge/README.md b/telperion/missions/judge/README.md index e433e3bd5..84d85c085 100644 --- a/telperion/missions/judge/README.md +++ b/telperion/missions/judge/README.md @@ -7,6 +7,9 @@ and holds one bridge module per proved node: ```lean import -- the solution import -- the whole island: a shadowed constant is a build error + -- (li_positivity: only the guard whose closure holds the + -- artifact; its two guards cannot co-import. quasicrystal: + -- none; the island has no AxiomGuard lean_lib) namespace theorem _root_.MissionJudge. : diff --git a/telperion/missions/judge/li_positivity/MANIFEST.json b/telperion/missions/judge/li_positivity/MANIFEST.json new file mode 100644 index 000000000..64707c93e --- /dev/null +++ b/telperion/missions/judge/li_positivity/MANIFEST.json @@ -0,0 +1,273 @@ +{ + "island": "li_positivity", + "package": "LiPositivity", + "toolchain": "leanprover/lean4:v4.34.0-rc1", + "comparator_tag": "v4.34.0-rc1", + "not_consumable": [], + "nodes": [ + { + "slug": "MM_bragg_bridge", + "campaign": "mirrormere", + "theorem": "DiffractionCore.rect_explicit_formula_bragg", + "solution_module": "RvMBraggBridge", + "challenge_module": "MissionChallenges.MM_bragg_bridge", + "bridge_theorem": "MissionJudge.MM_bragg_bridge", + "config": "MM_bragg_bridge.comparator.json", + "artifact_sha256": "119ae3d24773634211a277a6100dcf864d430becebb49c686336585782c93f74", + "statement_sha256": "710d4a1920aaac2dc670cf7a5e0672a2d230ce68567347bf9fb0b3c77a043be8" + }, + { + "slug": "MM_rect_trace_reading", + "campaign": "mirrormere", + "theorem": "DiffractionCore.rect_trace_reading", + "solution_module": "RvMTraceReading", + "challenge_module": "MissionChallenges.MM_rect_trace_reading", + "bridge_theorem": "MissionJudge.MM_rect_trace_reading", + "config": "MM_rect_trace_reading.comparator.json", + "artifact_sha256": "144f1b7c20eac9e317e2971484fa5909a713384476494cd470d72386e8072fd7", + "statement_sha256": "b5168609cd272526bbf0eb831a83bf862f99d074e825dcd27862f5151fd96451" + }, + { + "slug": "MM_spectral_cooked_control", + "campaign": "mirrormere", + "theorem": "spectral_cooked_control", + "solution_module": "RvMSpectralCookedControl", + "challenge_module": "MissionChallenges.MM_spectral_cooked_control", + "bridge_theorem": "MissionJudge.MM_spectral_cooked_control", + "config": "MM_spectral_cooked_control.comparator.json", + "artifact_sha256": "42d09183dadd1f860f37292e2d392182cf90b22a702626182ab7806c903ef34d", + "statement_sha256": "ea1041e357afd946621840b04665906cf208979e16c06951bf1ba9abd2d43f23" + }, + { + "slug": "RH_backlund_s_log", + "campaign": "rh", + "theorem": "Backlund.riemannS_abs_le_log_of_ne_zero", + "solution_module": "RvMBacklundLogCont", + "challenge_module": "MissionChallenges.RH_backlund_s_log", + "bridge_theorem": "MissionJudge.RH_backlund_s_log", + "config": "RH_backlund_s_log.comparator.json", + "artifact_sha256": "1eb43fc74ba25fe45777dc6de0521e566fa0195e951df62cf6ede13e9ec8106a", + "statement_sha256": "5bbeb021e755b3dc618c6c38911ffc358db1acf27c362b01cb985c1fa023195a" + }, + { + "slug": "RH_bl_finite_multiset", + "campaign": "rh", + "theorem": "bl_finite_multiset", + "solution_module": "RvMBlFiniteMultiset", + "challenge_module": "MissionChallenges.RH_bl_finite_multiset", + "bridge_theorem": "MissionJudge.RH_bl_finite_multiset", + "config": "RH_bl_finite_multiset.comparator.json", + "artifact_sha256": "50da48fdf7fb0327da549f96a3d0cefd3f030642777e87df544d4655b1c86c2c", + "statement_sha256": "b22036d8b4a724816c9fc7df2be67aabc6664ec219eb2bfa03795b0e30b248b7" + }, + { + "slug": "RH_borel_caratheodory_deriv", + "campaign": "rh", + "theorem": "ZeroFreeBridge.norm_deriv_le_of_re_le", + "solution_module": "DlvpBCDeriv", + "challenge_module": "MissionChallenges.RH_borel_caratheodory_deriv", + "bridge_theorem": "MissionJudge.RH_borel_caratheodory_deriv", + "config": "RH_borel_caratheodory_deriv.comparator.json", + "artifact_sha256": "4dc8f213e2592a7deb22958635dfc477dd9a481da3d4ad01ad420da97eabb705", + "statement_sha256": "60ef97ef2228012158983410abd5ce07c5d65424352b4b1910474503b9c666eb" + }, + { + "slug": "RH_companion_bragg_reduction", + "campaign": "rh", + "theorem": "RvMWeierstrass.taylorCoeff_companion_bragg_of_exhaustion_limits", + "solution_module": "RvMCompanionBraggLimit", + "challenge_module": "MissionChallenges.RH_companion_bragg_reduction", + "bridge_theorem": "MissionJudge.RH_companion_bragg_reduction", + "config": "RH_companion_bragg_reduction.comparator.json", + "artifact_sha256": "3ff0bc086401d936059dde249c9ec888ce58ef07feedc28fcc59ecc1f3162e8e", + "statement_sha256": "3af9842160ed496a7711db145586fdcc5277b734843e065abf5412a4d0588a7a" + }, + { + "slug": "RH_dlvp_region_effective", + "campaign": "rh", + "theorem": "ZeroFreeBridge.dlvp_zeta_region_rate_effective", + "solution_module": "DlvpZetaRateEffective", + "challenge_module": "MissionChallenges.RH_dlvp_region_effective", + "bridge_theorem": "MissionJudge.RH_dlvp_region_effective", + "config": "RH_dlvp_region_effective.comparator.json", + "artifact_sha256": "b9b791fefcef87f70abca02438f50feff2468cbb5bf5d87e23eeec769ac1f696", + "statement_sha256": "70926b5c4081e2579e2af17309943a0d9842f02c3c03bdbaff1791986afda1e0" + }, + { + "slug": "RH_li_ladder_height", + "campaign": "rh", + "theorem": "LiLadderHeight.li_rung_of_zeros_on_line_below", + "solution_module": "LiLadderHeight", + "challenge_module": "MissionChallenges.RH_li_ladder_height", + "bridge_theorem": "MissionJudge.RH_li_ladder_height", + "config": "RH_li_ladder_height.comparator.json", + "artifact_sha256": "b87f01ed8f29013b0c8cd6ead9d77ccb8686ea38dea4a03acf344a6cd90909e1", + "statement_sha256": "d42f2257a65a0c15480e07dcb6aeab0f7a1718f9109b8cf4a548207ecde7ff50" + }, + { + "slug": "RH_li_ladder_height_sharp", + "campaign": "rh", + "theorem": "LiLadderHeight.li_rung_of_zeros_on_line_below_sharp", + "solution_module": "LiLadderSharp", + "challenge_module": "MissionChallenges.RH_li_ladder_height_sharp", + "bridge_theorem": "MissionJudge.RH_li_ladder_height_sharp", + "config": "RH_li_ladder_height_sharp.comparator.json", + "artifact_sha256": "356115f9f2c3da563b4afc0e35abf7b6dedcc987b4acc7ecf6c89fc27ee75e03", + "statement_sha256": "c556d6f6445f35591ab9de253a251fcaadeec6f74480316a54c5a877f042b819" + }, + { + "slug": "RH_li_ladder_reduction", + "campaign": "rh", + "theorem": "LiPositivity.li_rh_iff_tail", + "solution_module": "LiLadder", + "challenge_module": "MissionChallenges.RH_li_ladder_reduction", + "bridge_theorem": "MissionJudge.RH_li_ladder_reduction", + "config": "RH_li_ladder_reduction.comparator.json", + "artifact_sha256": "8148230536417e52f0a7042c8e8c6d5bff9018ff42095c6ae281e60703e2e8a8", + "statement_sha256": "8873878ead92a881dcc2d244eafae1e8f41980bdd061c0b7f0f46195d2f9aa94" + }, + { + "slug": "RH_li_neg_refutes_rh", + "campaign": "rh", + "theorem": "LiPositivity.li_neg_refutes_rh", + "solution_module": "LiPositivity", + "challenge_module": "MissionChallenges.RH_li_neg_refutes_rh", + "bridge_theorem": "MissionJudge.RH_li_neg_refutes_rh", + "config": "RH_li_neg_refutes_rh.comparator.json", + "artifact_sha256": "c55d21299fdebbf3c7133e0d81ade237c39f6992a500f8ebff01607ac7c1e8ce", + "statement_sha256": "d7a1f9f166c7e2a5b5acbd7b7a34c663b7623c29a6ece7ead2ccd64c3549e7e7" + }, + { + "slug": "RH_li_rung0_kernel", + "campaign": "rh", + "theorem": "li_rung0_kernel", + "solution_module": "LiLadderHeight", + "challenge_module": "MissionChallenges.RH_li_rung0_kernel", + "bridge_theorem": "MissionJudge.RH_li_rung0_kernel", + "config": "RH_li_rung0_kernel.comparator.json", + "artifact_sha256": "b87f01ed8f29013b0c8cd6ead9d77ccb8686ea38dea4a03acf344a6cd90909e1", + "statement_sha256": "1a8eff7cf1bb6fa34019330b675842f7dd261dbba9b4337f259a5ecd1f7220e3" + }, + { + "slug": "RH_li_rung_certificates", + "campaign": "rh", + "theorem": "LiPositivity.li_rung_19", + "solution_module": "LiPositivity", + "challenge_module": "MissionChallenges.RH_li_rung_certificates", + "bridge_theorem": "MissionJudge.RH_li_rung_certificates", + "config": "RH_li_rung_certificates.comparator.json", + "artifact_sha256": "c55d21299fdebbf3c7133e0d81ade237c39f6992a500f8ebff01607ac7c1e8ce", + "statement_sha256": "8c14404d9969e90dc6f316b7d5afe081e1d8201e328c5e814b4848138d8ca665" + }, + { + "slug": "RH_li_rungs_lt_five", + "campaign": "rh", + "theorem": "LowHeightBox.li_rungs_lt_five", + "solution_module": "LiBoxRungs", + "challenge_module": "MissionChallenges.RH_li_rungs_lt_five", + "bridge_theorem": "MissionJudge.RH_li_rungs_lt_five", + "config": "RH_li_rungs_lt_five.comparator.json", + "artifact_sha256": "e2f64b7c4a120b60e1eca46f9c88e18af65d742345ad854f7e7b3b6443085bb0", + "statement_sha256": "87f1a579fbc0223ebddc261ebc587b567b7220b5185189c3df90f83ef7adc27f" + }, + { + "slug": "RH_li_rungs_of_height_4000", + "campaign": "rh", + "theorem": "LiLadderHeight.li_rungs_of_bands_4000_upto", + "solution_module": "LiLadderHeight", + "challenge_module": "MissionChallenges.RH_li_rungs_of_height_4000", + "bridge_theorem": "MissionJudge.RH_li_rungs_of_height_4000", + "config": "RH_li_rungs_of_height_4000.comparator.json", + "artifact_sha256": "b87f01ed8f29013b0c8cd6ead9d77ccb8686ea38dea4a03acf344a6cd90909e1", + "statement_sha256": "915f92e9ae958c1a0654283c7686052291a975a3453320fbc6ffaf41ab588334" + }, + { + "slug": "RH_li_rungs_of_height_4000_sharp", + "campaign": "rh", + "theorem": "LiLadderHeight.li_rungs_of_bands_4000_upto_sharp", + "solution_module": "LiLadderSharp", + "challenge_module": "MissionChallenges.RH_li_rungs_of_height_4000_sharp", + "bridge_theorem": "MissionJudge.RH_li_rungs_of_height_4000_sharp", + "config": "RH_li_rungs_of_height_4000_sharp.comparator.json", + "artifact_sha256": "356115f9f2c3da563b4afc0e35abf7b6dedcc987b4acc7ecf6c89fc27ee75e03", + "statement_sha256": "192da17382d65133d4caf527deecc77e44a66c5e12b73e4e29be8766284fc4f4" + }, + { + "slug": "RH_strip_repr", + "campaign": "rh", + "theorem": "ZeroFreeBridge.zeta_fract_repr", + "solution_module": "StripReprAssembled", + "challenge_module": "MissionChallenges.RH_strip_repr", + "bridge_theorem": "MissionJudge.RH_strip_repr", + "config": "RH_strip_repr.comparator.json", + "artifact_sha256": "57347940ba4dc5acdf4b442c6400eaffc5c67dc5d2e5f0a7b6569a0d54d524fa", + "statement_sha256": "cc08404b957d2543a9c05b4b07cef2ed44b1d8f0b600f3e135dbac5dbe02bcc1" + }, + { + "slug": "RH_zero_free_gamma5", + "campaign": "rh", + "theorem": "ZeroFreeBridge.riemannZeta_zero_free_poly", + "solution_module": "ZeroFreeElementary", + "challenge_module": "MissionChallenges.RH_zero_free_gamma5", + "bridge_theorem": "MissionJudge.RH_zero_free_gamma5", + "config": "RH_zero_free_gamma5.comparator.json", + "artifact_sha256": "a9e2b823293aca063fc977c08294037e836c5183fd93d8294642b0cfbb1ba58e", + "statement_sha256": "6f7294447765d7e470eadcaf90de39056e7e29274f3f8ca8054969bbafe39fbd" + }, + { + "slug": "RH_zero_free_polylog", + "campaign": "rh", + "theorem": "ZeroFreeBridge.riemannZeta_zero_free_polylog", + "solution_module": "ZeroFreePolylog", + "challenge_module": "MissionChallenges.RH_zero_free_polylog", + "bridge_theorem": "MissionJudge.RH_zero_free_polylog", + "config": "RH_zero_free_polylog.comparator.json", + "artifact_sha256": "8c163fb78beddd71215b29b01b9f807ac91af9821118d40dbbb584350abd75e1", + "statement_sha256": "4c6dc5e44c304e8b47ce25e6542a11cae6908352ccdff07c072ef2aabdd9f1fb" + }, + { + "slug": "RH_zeta_log_bound", + "campaign": "rh", + "theorem": "ZeroFreeBridge.zeta_log_bound", + "solution_module": "ZetaLogBound", + "challenge_module": "MissionChallenges.RH_zeta_log_bound", + "bridge_theorem": "MissionJudge.RH_zeta_log_bound", + "config": "RH_zeta_log_bound.comparator.json", + "artifact_sha256": "d76e727e8d57be281309f9606f17a8e03e9b2c9549f25800ff8bee39dec545de", + "statement_sha256": "8ae719eb0c17662b908bfcd6c700f7cd46eeffa3ef41e10c29fc52ac62027bd5" + }, + { + "slug": "RH_zeta_repr_R1", + "campaign": "rh", + "theorem": "ZeroFreeBridge.zeta_repr_R1", + "solution_module": "StripReprR1", + "challenge_module": "MissionChallenges.RH_zeta_repr_R1", + "bridge_theorem": "MissionJudge.RH_zeta_repr_R1", + "config": "RH_zeta_repr_R1.comparator.json", + "artifact_sha256": "14ffee54e74eefd9f0d5334d21ad23655df49614c82f617b03579ccc8e857c77", + "statement_sha256": "506da57caf351cfa3f2664114351fcdec7408c34a8a7e7b5a76f7965dfd14cac" + }, + { + "slug": "RH_zeta_zero_confined", + "campaign": "rh", + "theorem": "LowHeightBox.zeta_zero_confined", + "solution_module": "LowHeightBox", + "challenge_module": "MissionChallenges.RH_zeta_zero_confined", + "bridge_theorem": "MissionJudge.RH_zeta_zero_confined", + "config": "RH_zeta_zero_confined.comparator.json", + "artifact_sha256": "6410f9321d22a20ed02957fc14b189d58e00ead106344a10d6236f4adde4d057", + "statement_sha256": "5c05f145266a10d9cc1fc9565b6804bd0fbb7d545413a9e580feff52545f6669" + }, + { + "slug": "RH_zeta_zero_im_ge", + "campaign": "rh", + "theorem": "LowHeightBox.zeta_zero_im_ge", + "solution_module": "LowHeightBox", + "challenge_module": "MissionChallenges.RH_zeta_zero_im_ge", + "bridge_theorem": "MissionJudge.RH_zeta_zero_im_ge", + "config": "RH_zeta_zero_im_ge.comparator.json", + "artifact_sha256": "6410f9321d22a20ed02957fc14b189d58e00ead106344a10d6236f4adde4d057", + "statement_sha256": "0ee478c2500e8a28c37be1ad20344963217cd62939d2f614ef52be03cb1a3462" + } + ] +} diff --git a/telperion/missions/judge/li_positivity/MM_bragg_bridge.comparator.json b/telperion/missions/judge/li_positivity/MM_bragg_bridge.comparator.json new file mode 100644 index 000000000..772a60fec --- /dev/null +++ b/telperion/missions/judge/li_positivity/MM_bragg_bridge.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_bragg_bridge", + "solution_module": "MissionChallenges.MM_bragg_bridge", + "theorem_names": [ + "MissionJudge.MM_bragg_bridge" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/MM_rect_trace_reading.comparator.json b/telperion/missions/judge/li_positivity/MM_rect_trace_reading.comparator.json new file mode 100644 index 000000000..7b93ef733 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MM_rect_trace_reading.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_rect_trace_reading", + "solution_module": "MissionChallenges.MM_rect_trace_reading", + "theorem_names": [ + "MissionJudge.MM_rect_trace_reading" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/MM_spectral_cooked_control.comparator.json b/telperion/missions/judge/li_positivity/MM_spectral_cooked_control.comparator.json new file mode 100644 index 000000000..a6ffc7ea5 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MM_spectral_cooked_control.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_spectral_cooked_control", + "solution_module": "MissionChallenges.MM_spectral_cooked_control", + "theorem_names": [ + "MissionJudge.MM_spectral_cooked_control" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/MissionChallenges.lean b/telperion/missions/judge/li_positivity/MissionChallenges.lean new file mode 100644 index 000000000..1eba61d48 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges.lean @@ -0,0 +1,3 @@ +-- DO NOT EDIT BY HAND. No root imports on `li_positivity`: its AxiomGuard libs cannot +-- be imported together, so each bridge module imports one of them and is built by +-- name (`lake build MissionChallenges.`), never through this root. diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/MM_bragg_bridge.lean b/telperion/missions/judge/li_positivity/MissionChallenges/MM_bragg_bridge.lean new file mode 100644 index 000000000..e6acf75e1 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/MM_bragg_bridge.lean @@ -0,0 +1,37 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_bragg_bridge. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_bragg_bridge.lean (header sha256 a5d716d44923abc1), binders and conclusion verbatim; the + PROOF is the artifact constant `DiffractionCore.rect_explicit_formula_bragg` from RvMBraggBridge. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import RvMBraggBridge +import AxiomGuardLiPositivity + +namespace DiffractionCore + +open Complex MeasureTheory Real +open scoped Topology + +theorem _root_.MissionJudge.MM_bragg_bridge : + ∀ (sigma0 sigma1 T0 T1 : ℝ) (hsig : sigma0 ≤ sigma1) (hT : T0 ≤ T1) (hσ1 : 1 < sigma1) + (c : ℂ) (R : ℝ) + (hbox_ball : ∀ ρ : ℂ, (sigma0 ≤ ρ.re ∧ ρ.re ≤ sigma1) → (T0 ≤ ρ.im ∧ ρ.im ≤ T1) → + ρ ∈ Metric.ball c R) + (hs1 : (1 : ℂ) ∉ Metric.ball c R) + (hnzb : ∀ x ∈ Set.uIcc sigma0 sigma1, riemannZeta (↑x + (T0 : ℂ) * I) ≠ 0) + (hnzt : ∀ x ∈ Set.uIcc sigma0 sigma1, riemannZeta (↑x + (T1 : ℂ) * I) ≠ 0) + (hnzl : ∀ y ∈ Set.uIcc T0 T1, riemannZeta ((sigma0 : ℂ) + ↑y * I) ≠ 0) + (hins : ∀ ρ ∈ RHInBoxAnalytic.zeroFinset c R hs1, + sigma0 < ρ.re ∧ ρ.re < sigma1 ∧ T0 < ρ.im ∧ ρ.im < T1), 2 * ↑π * I * ∑ ρ ∈ RHInBoxAnalytic.zeroFinset c R hs1, + ((MeromorphicOn.divisor riemannZeta (Metric.ball c R) : ℂ → ℤ) ρ : ℂ) + = (∫ x in sigma0..sigma1, logDeriv riemannZeta (↑x + (T0 : ℂ) * I)) + - (∫ x in sigma0..sigma1, logDeriv riemannZeta (↑x + (T1 : ℂ) * I)) + - I • (∑' n : ℕ, braggTerm sigma1 T0 T1 n) + - I • (∫ y in T0..T1, logDeriv riemannZeta ((sigma0 : ℂ) + ↑y * I)) := + DiffractionCore.rect_explicit_formula_bragg + +end DiffractionCore diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/MM_rect_trace_reading.lean b/telperion/missions/judge/li_positivity/MissionChallenges/MM_rect_trace_reading.lean new file mode 100644 index 000000000..b034fe05f --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/MM_rect_trace_reading.lean @@ -0,0 +1,38 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_rect_trace_reading. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_rect_trace_reading.lean (header sha256 d5dbc8be7b69e78e), binders and conclusion verbatim; the + PROOF is the artifact constant `DiffractionCore.rect_trace_reading` from RvMTraceReading. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import RvMTraceReading +import AxiomGuardLiPositivity + +namespace DiffractionCore + +open Complex MeasureTheory Real DiffractionCore +open scoped Topology + +theorem _root_.MissionJudge.MM_rect_trace_reading : + ∀ (sigma0 sigma1 T0 T1 : ℝ) (hsig : sigma0 ≤ sigma1) (hT : T0 ≤ T1) (hσ1 : 1 < sigma1) + (c : ℂ) (R : ℝ) + (hbox_ball : ∀ ρ : ℂ, (sigma0 ≤ ρ.re ∧ ρ.re ≤ sigma1) → (T0 ≤ ρ.im ∧ ρ.im ≤ T1) → + ρ ∈ Metric.ball c R) + (hs1 : (1 : ℂ) ∉ Metric.ball c R) + (hnzb : ∀ x ∈ Set.uIcc sigma0 sigma1, riemannZeta (↑x + (T0 : ℂ) * I) ≠ 0) + (hnzt : ∀ x ∈ Set.uIcc sigma0 sigma1, riemannZeta (↑x + (T1 : ℂ) * I) ≠ 0) + (hnzl : ∀ y ∈ Set.uIcc T0 T1, riemannZeta ((sigma0 : ℂ) + ↑y * I) ≠ 0) + (hins : ∀ ρ ∈ RHInBoxAnalytic.zeroFinset c R hs1, + sigma0 < ρ.re ∧ ρ.re < sigma1 ∧ T0 < ρ.im ∧ ρ.im < T1), ∑ ρ ∈ RHInBoxAnalytic.zeroFinset c R hs1, + ((MeromorphicOn.divisor riemannZeta (Metric.ball c R) : ℂ → ℤ) ρ : ℂ) + = (1 / (2 * ↑π * I)) * + ((∫ x in sigma0..sigma1, logDeriv riemannZeta (↑x + (T0 : ℂ) * I)) + - (∫ x in sigma0..sigma1, logDeriv riemannZeta (↑x + (T1 : ℂ) * I)) + - I • (∑' n : ℕ, braggTerm sigma1 T0 T1 n) + - I • (∫ y in T0..T1, logDeriv riemannZeta ((sigma0 : ℂ) + ↑y * I))) := + DiffractionCore.rect_trace_reading + +end DiffractionCore diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/MM_spectral_cooked_control.lean b/telperion/missions/judge/li_positivity/MissionChallenges/MM_spectral_cooked_control.lean new file mode 100644 index 000000000..7750cc194 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/MM_spectral_cooked_control.lean @@ -0,0 +1,17 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_spectral_cooked_control. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_spectral_cooked_control.lean (header sha256 bdfe0af62cef535b), binders and conclusion verbatim; the + PROOF is the artifact constant `spectral_cooked_control` from RvMSpectralCookedControl. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import RvMSpectralCookedControl +import AxiomGuardLiPositivity + +theorem MissionJudge.MM_spectral_cooked_control : + ∀ (n : ℕ) (γ : Fin n → ℝ), ∃ A : Matrix (Fin n) (Fin n) ℂ, A.IsHermitian ∧ + A.charpoly = ∏ i, (Polynomial.X - Polynomial.C ((γ i : ℝ) : ℂ)) := + spectral_cooked_control diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_backlund_s_log.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_backlund_s_log.lean new file mode 100644 index 000000000..537ad9d01 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_backlund_s_log.lean @@ -0,0 +1,24 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_backlund_s_log. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_backlund_s_log.lean (header sha256 ec00ae361e114283), binders and conclusion verbatim; the + PROOF is the artifact constant `Backlund.riemannS_abs_le_log_of_ne_zero` from RvMBacklundLogCont. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import RvMBacklundLogCont +import AxiomGuardLiPositivity + +namespace Backlund + +open Complex MeasureTheory + +theorem _root_.MissionJudge.RH_backlund_s_log : + ∀ {T : ℝ} (hT : 4 ≤ T) + (hζne : ∀ x ∈ Set.Icc (1 / 2 : ℝ) 2, riemannZeta ((x : ℂ) + (T : ℂ) * I) ≠ 0), |DiffractionCore.riemannS T| + ≤ Real.log ((4 * T + 19) / ‖backlundAux T ((2 : ℝ) : ℂ)‖) / Real.log (7 / 4 / (3 / 2)) + 2 := + Backlund.riemannS_abs_le_log_of_ne_zero + +end Backlund diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_bl_finite_multiset.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_bl_finite_multiset.lean new file mode 100644 index 000000000..54a95878e --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_bl_finite_multiset.lean @@ -0,0 +1,22 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_bl_finite_multiset. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_bl_finite_multiset.lean (header sha256 68298a4747241b82), binders and conclusion verbatim; the + PROOF is the artifact constant `bl_finite_multiset` from RvMBlFiniteMultiset. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import RvMBlFiniteMultiset +import AxiomGuardLiPositivity + +open Complex Finset Filter Topology + +theorem MissionJudge.RH_bl_finite_multiset : + ∀ (S : Finset ℂ) + (h0 : (0 : ℂ) ∉ S) (h1 : (1 : ℂ) ∉ S) + (hsym : ∀ ρ ∈ S, 1 - (starRingEnd ℂ) ρ ∈ S), (∀ n : ℕ, 0 < n → + 0 ≤ (∑ ρ ∈ S, (1 - ((1 - 1 / ρ)⁻¹) ^ n)).re) + ↔ ∀ ρ ∈ S, ρ.re = 1 / 2 := + bl_finite_multiset diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_borel_caratheodory_deriv.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_borel_caratheodory_deriv.lean new file mode 100644 index 000000000..60e69eb87 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_borel_caratheodory_deriv.lean @@ -0,0 +1,25 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_borel_caratheodory_deriv. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_borel_caratheodory_deriv.lean (header sha256 a77a39437b93c621), binders and conclusion verbatim; the + PROOF is the artifact constant `ZeroFreeBridge.norm_deriv_le_of_re_le` from DlvpBCDeriv. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import DlvpBCDeriv +import AxiomGuardLiPositivity + +namespace ZeroFreeBridge + +open Complex Metric + +theorem _root_.MissionJudge.RH_borel_caratheodory_deriv : + ∀ {h : ℂ → ℂ} {c : ℂ} {R r M' : ℝ} + (hr : 0 < r) (hrR : r < R) + (hana : DifferentiableOn ℂ h (ball c R)) (hM' : 0 < M') + (hbound : ∀ z ∈ ball c R, (h z).re - (h c).re ≤ M'), ‖deriv h c‖ ≤ 2 * M' / (R - r) := + ZeroFreeBridge.norm_deriv_le_of_re_le + +end ZeroFreeBridge diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_companion_bragg_reduction.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_companion_bragg_reduction.lean new file mode 100644 index 000000000..6bbc1bc8c --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_companion_bragg_reduction.lean @@ -0,0 +1,30 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_companion_bragg_reduction. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_companion_bragg_reduction.lean (header sha256 179e8131187f63bb), binders and conclusion verbatim; the + PROOF is the artifact constant `RvMWeierstrass.taylorCoeff_companion_bragg_of_exhaustion_limits` from RvMCompanionBraggLimit. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import RvMCompanionBraggLimit +import AxiomGuardLiPositivity + +namespace RvMWeierstrass + +open Complex Filter Topology + +theorem _root_.MissionJudge.RH_companion_bragg_reduction : + ∀ (n : ℕ) + (zeroSum boundary bragg : ℕ → ℂ) (boundaryLim braggLim : ℂ) + (hformula : ∀ k, 2 * (Real.pi : ℂ) * I * zeroSum k = boundary k - bragg k) + (hzero : Tendsto (fun k => 2 * (Real.pi : ℂ) * I * zeroSum k) atTop + (𝓝 (2 * (Real.pi : ℂ) * I * LiCriterion.taylorCoeff LiCriterion.riemannXi n))) + (hboundary : Tendsto boundary atTop (𝓝 boundaryLim)) + (hbragg : Tendsto bragg atTop (𝓝 braggLim)), LiCriterion.taylorCoeff DiffractionCore.zetaPoleCompanion n + = (boundaryLim - braggLim) / (2 * (Real.pi : ℂ) * I) + - 1 - LiCriterion.taylorCoeff Complex.Gammaℝ n := + RvMWeierstrass.taylorCoeff_companion_bragg_of_exhaustion_limits + +end RvMWeierstrass diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_dlvp_region_effective.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_dlvp_region_effective.lean new file mode 100644 index 000000000..c7fa0e9e5 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_dlvp_region_effective.lean @@ -0,0 +1,24 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_dlvp_region_effective. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_dlvp_region_effective.lean (header sha256 ee5a8607789a7959), binders and conclusion verbatim; the + PROOF is the artifact constant `ZeroFreeBridge.dlvp_zeta_region_rate_effective` from DlvpZetaRateEffective. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import DlvpZetaRateEffective +import AxiomGuardLiPositivity + +namespace ZeroFreeBridge + +open Complex MeromorphicOn Metric + +theorem _root_.MissionJudge.RH_dlvp_region_effective : + ∀ (β γ : ℝ) (k : ℤ) + (h34 : 3/4 ≤ β) (hβ1 : β < 1) (hΓ : 55/16 ≤ |γ|) (hk : 1 ≤ k) + (hmρ₀ : divisor riemannZeta (ball ((2 : ℂ) + (γ : ℂ) * I) (11/8)) ((β : ℂ) + (γ : ℂ) * I) = k), β ≤ 1 - dlvpRateC / Real.log |γ| := + ZeroFreeBridge.dlvp_zeta_region_rate_effective + +end ZeroFreeBridge diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_height.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_height.lean new file mode 100644 index 000000000..d95ecce5d --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_height.lean @@ -0,0 +1,26 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_li_ladder_height. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_li_ladder_height.lean (header sha256 f0c5b46cd97556e9), binders and conclusion verbatim; the + PROOF is the artifact constant `LiLadderHeight.li_rung_of_zeros_on_line_below` from LiLadderHeight. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LiLadderHeight +import AxiomGuardLiPositivity + +namespace LiLadderHeight + +open scoped Real +open LiCriterion +open LiFacePrelude + +theorem _root_.MissionJudge.RH_li_ladder_height : + ∀ (T : ℝ) (hT : 1 ≤ T) + (hline : ∀ ρ : ℂ, riemannZeta ρ = 0 → 0 < ρ.re → ρ.re < 1 → |ρ.im| ≤ T → ρ.re = 1 / 2) + (n : ℕ) (hn : (n + 1 : ℝ) ≤ 3 * π * T / 2), 0 ≤ (taylorCoeff riemannXi n).re := + LiLadderHeight.li_rung_of_zeros_on_line_below + +end LiLadderHeight diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_height_sharp.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_height_sharp.lean new file mode 100644 index 000000000..6ed92773c --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_height_sharp.lean @@ -0,0 +1,26 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_li_ladder_height_sharp. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_li_ladder_height_sharp.lean (header sha256 d5ada182fa53be39), binders and conclusion verbatim; the + PROOF is the artifact constant `LiLadderHeight.li_rung_of_zeros_on_line_below_sharp` from LiLadderSharp. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LiLadderSharp +import AxiomGuardLiPositivity + +namespace LiLadderHeight + +open scoped Real +open LiCriterion +open LiFacePrelude + +theorem _root_.MissionJudge.RH_li_ladder_height_sharp : + ∀ (T : ℝ) (hT : 1 ≤ T) + (hline : ∀ ρ : ℂ, riemannZeta ρ = 0 → 0 < ρ.re → ρ.re < 1 → |ρ.im| ≤ T → ρ.re = 1 / 2) + (n : ℕ) (hn : (n + 1 : ℝ) ≤ 2 * π * (T - 1 / 2)), 0 ≤ (taylorCoeff riemannXi n).re := + LiLadderHeight.li_rung_of_zeros_on_line_below_sharp + +end LiLadderHeight diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_reduction.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_reduction.lean new file mode 100644 index 000000000..e61ff3a05 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_ladder_reduction.lean @@ -0,0 +1,23 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_li_ladder_reduction. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_li_ladder_reduction.lean (header sha256 c9d72d2c8009b0a2), binders and conclusion verbatim; the + PROOF is the artifact constant `LiPositivity.li_rh_iff_tail` from LiLadder. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LiLadder +import AxiomGuardLiPositivity + +namespace LiPositivity + +open LiCriterion + +theorem _root_.MissionJudge.RH_li_ladder_reduction : + ∀ (N : ℕ) + (hpre : ∀ n, n < N → 0 ≤ (taylorCoeff riemannXi n).re), RiemannHypothesis ↔ ∀ n, N ≤ n → 0 ≤ (taylorCoeff riemannXi n).re := + LiPositivity.li_rh_iff_tail + +end LiPositivity diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_neg_refutes_rh.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_neg_refutes_rh.lean new file mode 100644 index 000000000..e237007bf --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_neg_refutes_rh.lean @@ -0,0 +1,23 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_li_neg_refutes_rh. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_li_neg_refutes_rh.lean (header sha256 8b3d06edc541908e), binders and conclusion verbatim; the + PROOF is the artifact constant `LiPositivity.li_neg_refutes_rh` from LiPositivity. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LiPositivity +import AxiomGuardLiPositivity + +namespace LiPositivity + +open LiCriterion + +theorem _root_.MissionJudge.RH_li_neg_refutes_rh : + ∀ (n : ℕ) (hi : ℝ) + (hhi : (taylorCoeff riemannXi n).re ≤ hi) (hneg : hi < 0), ¬RiemannHypothesis := + LiPositivity.li_neg_refutes_rh + +end LiPositivity diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rung0_kernel.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rung0_kernel.lean new file mode 100644 index 000000000..df3f8e0cf --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rung0_kernel.lean @@ -0,0 +1,20 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_li_rung0_kernel. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_li_rung0_kernel.lean (header sha256 337db1dc44959b04), binders and conclusion verbatim; the + PROOF is the artifact constant `li_rung0_kernel` from LiLadderHeight. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LiLadderHeight +import AxiomGuardLiPositivity + +open scoped Real +open LiCriterion +open LiFacePrelude + +theorem MissionJudge.RH_li_rung0_kernel : + 0 ≤ (LiCriterion.taylorCoeff LiCriterion.riemannXi 0).re := + li_rung0_kernel diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rung_certificates.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rung_certificates.lean new file mode 100644 index 000000000..d76b78d22 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rung_certificates.lean @@ -0,0 +1,22 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_li_rung_certificates. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_li_rung_certificates.lean (header sha256 f9ae82bf6c156682), binders and conclusion verbatim; the + PROOF is the artifact constant `LiPositivity.li_rung_19` from LiPositivity. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LiPositivity +import AxiomGuardLiPositivity + +namespace LiPositivity + +open LiCriterion + +theorem _root_.MissionJudge.RH_li_rung_certificates : + ∀ (hlo : ((876927687209 / 100000000000) : ℝ) ≤ (taylorCoeff riemannXi 19).re), 0 ≤ (taylorCoeff riemannXi 19).re := + LiPositivity.li_rung_19 + +end LiPositivity diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_lt_five.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_lt_five.lean new file mode 100644 index 000000000..dbd29e13b --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_lt_five.lean @@ -0,0 +1,22 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_li_rungs_lt_five. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_li_rungs_lt_five.lean (header sha256 6743e10ff3813519), binders and conclusion verbatim; the + PROOF is the artifact constant `LowHeightBox.li_rungs_lt_five` from LiBoxRungs. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LiBoxRungs +import AxiomGuardLiPositivity + +namespace LowHeightBox + +open Complex LiCriterion + +theorem _root_.MissionJudge.RH_li_rungs_lt_five : + ∀ n : ℕ, n < 5 → 0 ≤ (taylorCoeff riemannXi n).re := + LowHeightBox.li_rungs_lt_five + +end LowHeightBox diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_of_height_4000.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_of_height_4000.lean new file mode 100644 index 000000000..03fada1a0 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_of_height_4000.lean @@ -0,0 +1,24 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_li_rungs_of_height_4000. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_li_rungs_of_height_4000.lean (header sha256 f4977db040200582), binders and conclusion verbatim; the + PROOF is the artifact constant `LiLadderHeight.li_rungs_of_bands_4000_upto` from LiLadderHeight. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LiLadderHeight +import AxiomGuardLiPositivity + +namespace LiLadderHeight + +open scoped Real +open LiCriterion +open LiFacePrelude + +theorem _root_.MissionJudge.RH_li_rungs_of_height_4000 : + ∀ (hall : ∀ ρ : ℂ, riemannZeta ρ = 0 → 0 < ρ.im → ρ.im ≤ 4000 → ρ.re = 1 / 2), ∀ n : ℕ, n ≤ 18848 → 0 ≤ (taylorCoeff riemannXi n).re := + LiLadderHeight.li_rungs_of_bands_4000_upto + +end LiLadderHeight diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_of_height_4000_sharp.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_of_height_4000_sharp.lean new file mode 100644 index 000000000..8224e9693 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_li_rungs_of_height_4000_sharp.lean @@ -0,0 +1,24 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_li_rungs_of_height_4000_sharp. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_li_rungs_of_height_4000_sharp.lean (header sha256 f07141b4e612cf3e), binders and conclusion verbatim; the + PROOF is the artifact constant `LiLadderHeight.li_rungs_of_bands_4000_upto_sharp` from LiLadderSharp. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LiLadderSharp +import AxiomGuardLiPositivity + +namespace LiLadderHeight + +open scoped Real +open LiCriterion +open LiFacePrelude + +theorem _root_.MissionJudge.RH_li_rungs_of_height_4000_sharp : + ∀ (hall : ∀ ρ : ℂ, riemannZeta ρ = 0 → 0 < ρ.im → ρ.im ≤ 4000 → ρ.re = 1 / 2), ∀ n : ℕ, n ≤ 25128 → 0 ≤ (taylorCoeff riemannXi n).re := + LiLadderHeight.li_rungs_of_bands_4000_upto_sharp + +end LiLadderHeight diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_strip_repr.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_strip_repr.lean new file mode 100644 index 000000000..fee7abf88 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_strip_repr.lean @@ -0,0 +1,20 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_strip_repr. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_strip_repr.lean (header sha256 137b516045890e6e), binders and conclusion verbatim; the + PROOF is the artifact constant `ZeroFreeBridge.zeta_fract_repr` from StripReprAssembled. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import StripReprAssembled +import AxiomGuardLiPositivity + +namespace ZeroFreeBridge + +theorem _root_.MissionJudge.RH_strip_repr : + ∀ {s : ℂ} (hs : s ∈ stripDomain), riemannZeta s = stripRHS s := + ZeroFreeBridge.zeta_fract_repr + +end ZeroFreeBridge diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_zero_free_gamma5.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zero_free_gamma5.lean new file mode 100644 index 000000000..fa407b34f --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zero_free_gamma5.lean @@ -0,0 +1,23 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_zero_free_gamma5. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_zero_free_gamma5.lean (header sha256 7de16fa2b95d4ab4), binders and conclusion verbatim; the + PROOF is the artifact constant `ZeroFreeBridge.riemannZeta_zero_free_poly` from ZeroFreeElementary. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import ZeroFreeElementary +import AxiomGuardZeroFree + +namespace ZeroFreeBridge + +open Filter Topology + +theorem _root_.MissionJudge.RH_zero_free_gamma5 : + ∃ c > (0 : ℝ), ∀ β γ : ℝ, + riemannZeta ((β : ℂ) + γ * Complex.I) = 0 → 2 ≤ γ → β ≤ 1 - c / γ ^ 5 := + ZeroFreeBridge.riemannZeta_zero_free_poly + +end ZeroFreeBridge diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_zero_free_polylog.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zero_free_polylog.lean new file mode 100644 index 000000000..b8366ee0b --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zero_free_polylog.lean @@ -0,0 +1,24 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_zero_free_polylog. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_zero_free_polylog.lean (header sha256 02299e57afc7c2b7), binders and conclusion verbatim; the + PROOF is the artifact constant `ZeroFreeBridge.riemannZeta_zero_free_polylog` from ZeroFreePolylog. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import ZeroFreePolylog +import AxiomGuardZeroFree + +namespace ZeroFreeBridge + +open Filter Topology + +theorem _root_.MissionJudge.RH_zero_free_polylog : + ∃ c > (0 : ℝ), ∀ β γ : ℝ, + riemannZeta ((β : ℂ) + γ * Complex.I) = 0 → 2 ≤ γ → + β ≤ 1 - c / (γ ^ 4 * (1 + Real.log (2 * γ))) := + ZeroFreeBridge.riemannZeta_zero_free_polylog + +end ZeroFreeBridge diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_log_bound.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_log_bound.lean new file mode 100644 index 000000000..be6141719 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_log_bound.lean @@ -0,0 +1,22 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_zeta_log_bound. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_zeta_log_bound.lean (header sha256 9482553b398bc972), binders and conclusion verbatim; the + PROOF is the artifact constant `ZeroFreeBridge.zeta_log_bound` from ZetaLogBound. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import ZetaLogBound +import AxiomGuardLiPositivity + +namespace ZeroFreeBridge + +open MeasureTheory Filter Topology Set + +theorem _root_.MissionJudge.RH_zeta_log_bound : + ∀ {σ t : ℝ} (hσ1 : 1 ≤ σ) (hσ2 : σ ≤ 2) (ht : 2 ≤ |t|), ‖riemannZeta ((σ : ℂ) + t * Complex.I)‖ ≤ 6 * (1 + Real.log |t|) := + ZeroFreeBridge.zeta_log_bound + +end ZeroFreeBridge diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_repr_R1.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_repr_R1.lean new file mode 100644 index 000000000..e5b4d5669 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_repr_R1.lean @@ -0,0 +1,22 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_zeta_repr_R1. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_zeta_repr_R1.lean (header sha256 687097f4aacfc9e9), binders and conclusion verbatim; the + PROOF is the artifact constant `ZeroFreeBridge.zeta_repr_R1` from StripReprR1. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import StripReprR1 +import AxiomGuardLiPositivity + +namespace ZeroFreeBridge + +open MeasureTheory Filter Topology Set + +theorem _root_.MissionJudge.RH_zeta_repr_R1 : + ∀ {s : ℂ} (hs : 1 < s.re), riemannZeta s = stripRHS s := + ZeroFreeBridge.zeta_repr_R1 + +end ZeroFreeBridge diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_zero_confined.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_zero_confined.lean new file mode 100644 index 000000000..6f84b2985 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_zero_confined.lean @@ -0,0 +1,23 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_zeta_zero_confined. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_zeta_zero_confined.lean (header sha256 04037e4296785265), binders and conclusion verbatim; the + PROOF is the artifact constant `LowHeightBox.zeta_zero_confined` from LowHeightBox. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LowHeightBox +import AxiomGuardLiPositivity + +namespace LowHeightBox + +open Complex MeasureTheory Set Filter Topology +open scoped Real + +theorem _root_.MissionJudge.RH_zeta_zero_confined : + ∀ (s : ℂ) (h0 : riemannZeta s = 0) (hre : 0 < s.re ∧ s.re < 1), (s.re - 1 / 2) ^ 2 ≤ s.im ^ 2 / 3 - 1 / 4 := + LowHeightBox.zeta_zero_confined + +end LowHeightBox diff --git a/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_zero_im_ge.lean b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_zero_im_ge.lean new file mode 100644 index 000000000..8acb98673 --- /dev/null +++ b/telperion/missions/judge/li_positivity/MissionChallenges/RH_zeta_zero_im_ge.lean @@ -0,0 +1,23 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node rh/RH_zeta_zero_im_ge. + The TYPE below is the registered statement, missions/rh/lean/Statements/ + RH_zeta_zero_im_ge.lean (header sha256 3c9b90ff94c7956e), binders and conclusion verbatim; the + PROOF is the artifact constant `LowHeightBox.zeta_zero_im_ge` from LowHeightBox. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import LowHeightBox +import AxiomGuardLiPositivity + +namespace LowHeightBox + +open Complex MeasureTheory Set Filter Topology +open scoped Real + +theorem _root_.MissionJudge.RH_zeta_zero_im_ge : + ∀ (s : ℂ) (h0 : riemannZeta s = 0) (hre : 0 < s.re ∧ s.re < 1), Real.sqrt 3 / 2 ≤ |s.im| := + LowHeightBox.zeta_zero_im_ge + +end LowHeightBox diff --git a/telperion/missions/judge/li_positivity/RH_backlund_s_log.comparator.json b/telperion/missions/judge/li_positivity/RH_backlund_s_log.comparator.json new file mode 100644 index 000000000..52c84bcd5 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_backlund_s_log.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_backlund_s_log", + "solution_module": "MissionChallenges.RH_backlund_s_log", + "theorem_names": [ + "MissionJudge.RH_backlund_s_log" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_bl_finite_multiset.comparator.json b/telperion/missions/judge/li_positivity/RH_bl_finite_multiset.comparator.json new file mode 100644 index 000000000..82031572c --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_bl_finite_multiset.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_bl_finite_multiset", + "solution_module": "MissionChallenges.RH_bl_finite_multiset", + "theorem_names": [ + "MissionJudge.RH_bl_finite_multiset" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_borel_caratheodory_deriv.comparator.json b/telperion/missions/judge/li_positivity/RH_borel_caratheodory_deriv.comparator.json new file mode 100644 index 000000000..51cb19565 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_borel_caratheodory_deriv.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_borel_caratheodory_deriv", + "solution_module": "MissionChallenges.RH_borel_caratheodory_deriv", + "theorem_names": [ + "MissionJudge.RH_borel_caratheodory_deriv" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_companion_bragg_reduction.comparator.json b/telperion/missions/judge/li_positivity/RH_companion_bragg_reduction.comparator.json new file mode 100644 index 000000000..d0fe386e5 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_companion_bragg_reduction.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_companion_bragg_reduction", + "solution_module": "MissionChallenges.RH_companion_bragg_reduction", + "theorem_names": [ + "MissionJudge.RH_companion_bragg_reduction" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_dlvp_region_effective.comparator.json b/telperion/missions/judge/li_positivity/RH_dlvp_region_effective.comparator.json new file mode 100644 index 000000000..1285199b8 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_dlvp_region_effective.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_dlvp_region_effective", + "solution_module": "MissionChallenges.RH_dlvp_region_effective", + "theorem_names": [ + "MissionJudge.RH_dlvp_region_effective" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_li_ladder_height.comparator.json b/telperion/missions/judge/li_positivity/RH_li_ladder_height.comparator.json new file mode 100644 index 000000000..01b1501aa --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_li_ladder_height.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_li_ladder_height", + "solution_module": "MissionChallenges.RH_li_ladder_height", + "theorem_names": [ + "MissionJudge.RH_li_ladder_height" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_li_ladder_height_sharp.comparator.json b/telperion/missions/judge/li_positivity/RH_li_ladder_height_sharp.comparator.json new file mode 100644 index 000000000..f8e615fee --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_li_ladder_height_sharp.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_li_ladder_height_sharp", + "solution_module": "MissionChallenges.RH_li_ladder_height_sharp", + "theorem_names": [ + "MissionJudge.RH_li_ladder_height_sharp" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_li_ladder_reduction.comparator.json b/telperion/missions/judge/li_positivity/RH_li_ladder_reduction.comparator.json new file mode 100644 index 000000000..58cd116d5 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_li_ladder_reduction.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_li_ladder_reduction", + "solution_module": "MissionChallenges.RH_li_ladder_reduction", + "theorem_names": [ + "MissionJudge.RH_li_ladder_reduction" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_li_neg_refutes_rh.comparator.json b/telperion/missions/judge/li_positivity/RH_li_neg_refutes_rh.comparator.json new file mode 100644 index 000000000..d6e89bb78 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_li_neg_refutes_rh.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_li_neg_refutes_rh", + "solution_module": "MissionChallenges.RH_li_neg_refutes_rh", + "theorem_names": [ + "MissionJudge.RH_li_neg_refutes_rh" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_li_rung0_kernel.comparator.json b/telperion/missions/judge/li_positivity/RH_li_rung0_kernel.comparator.json new file mode 100644 index 000000000..eadcd7a5a --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_li_rung0_kernel.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_li_rung0_kernel", + "solution_module": "MissionChallenges.RH_li_rung0_kernel", + "theorem_names": [ + "MissionJudge.RH_li_rung0_kernel" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_li_rung_certificates.comparator.json b/telperion/missions/judge/li_positivity/RH_li_rung_certificates.comparator.json new file mode 100644 index 000000000..83029abcf --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_li_rung_certificates.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_li_rung_certificates", + "solution_module": "MissionChallenges.RH_li_rung_certificates", + "theorem_names": [ + "MissionJudge.RH_li_rung_certificates" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_li_rungs_lt_five.comparator.json b/telperion/missions/judge/li_positivity/RH_li_rungs_lt_five.comparator.json new file mode 100644 index 000000000..768d8afc9 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_li_rungs_lt_five.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_li_rungs_lt_five", + "solution_module": "MissionChallenges.RH_li_rungs_lt_five", + "theorem_names": [ + "MissionJudge.RH_li_rungs_lt_five" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_li_rungs_of_height_4000.comparator.json b/telperion/missions/judge/li_positivity/RH_li_rungs_of_height_4000.comparator.json new file mode 100644 index 000000000..7997464b7 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_li_rungs_of_height_4000.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_li_rungs_of_height_4000", + "solution_module": "MissionChallenges.RH_li_rungs_of_height_4000", + "theorem_names": [ + "MissionJudge.RH_li_rungs_of_height_4000" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_li_rungs_of_height_4000_sharp.comparator.json b/telperion/missions/judge/li_positivity/RH_li_rungs_of_height_4000_sharp.comparator.json new file mode 100644 index 000000000..cae6610e5 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_li_rungs_of_height_4000_sharp.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_li_rungs_of_height_4000_sharp", + "solution_module": "MissionChallenges.RH_li_rungs_of_height_4000_sharp", + "theorem_names": [ + "MissionJudge.RH_li_rungs_of_height_4000_sharp" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_strip_repr.comparator.json b/telperion/missions/judge/li_positivity/RH_strip_repr.comparator.json new file mode 100644 index 000000000..957b8201e --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_strip_repr.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_strip_repr", + "solution_module": "MissionChallenges.RH_strip_repr", + "theorem_names": [ + "MissionJudge.RH_strip_repr" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_zero_free_gamma5.comparator.json b/telperion/missions/judge/li_positivity/RH_zero_free_gamma5.comparator.json new file mode 100644 index 000000000..15cbbd243 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_zero_free_gamma5.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_zero_free_gamma5", + "solution_module": "MissionChallenges.RH_zero_free_gamma5", + "theorem_names": [ + "MissionJudge.RH_zero_free_gamma5" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_zero_free_polylog.comparator.json b/telperion/missions/judge/li_positivity/RH_zero_free_polylog.comparator.json new file mode 100644 index 000000000..65913b778 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_zero_free_polylog.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_zero_free_polylog", + "solution_module": "MissionChallenges.RH_zero_free_polylog", + "theorem_names": [ + "MissionJudge.RH_zero_free_polylog" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_zeta_log_bound.comparator.json b/telperion/missions/judge/li_positivity/RH_zeta_log_bound.comparator.json new file mode 100644 index 000000000..6794f75d7 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_zeta_log_bound.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_zeta_log_bound", + "solution_module": "MissionChallenges.RH_zeta_log_bound", + "theorem_names": [ + "MissionJudge.RH_zeta_log_bound" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_zeta_repr_R1.comparator.json b/telperion/missions/judge/li_positivity/RH_zeta_repr_R1.comparator.json new file mode 100644 index 000000000..032eee534 --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_zeta_repr_R1.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_zeta_repr_R1", + "solution_module": "MissionChallenges.RH_zeta_repr_R1", + "theorem_names": [ + "MissionJudge.RH_zeta_repr_R1" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_zeta_zero_confined.comparator.json b/telperion/missions/judge/li_positivity/RH_zeta_zero_confined.comparator.json new file mode 100644 index 000000000..8113160fb --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_zeta_zero_confined.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_zeta_zero_confined", + "solution_module": "MissionChallenges.RH_zeta_zero_confined", + "theorem_names": [ + "MissionJudge.RH_zeta_zero_confined" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/RH_zeta_zero_im_ge.comparator.json b/telperion/missions/judge/li_positivity/RH_zeta_zero_im_ge.comparator.json new file mode 100644 index 000000000..2396ad42a --- /dev/null +++ b/telperion/missions/judge/li_positivity/RH_zeta_zero_im_ge.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.RH_zeta_zero_im_ge", + "solution_module": "MissionChallenges.RH_zeta_zero_im_ge", + "theorem_names": [ + "MissionJudge.RH_zeta_zero_im_ge" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/li_positivity/lakefile.toml b/telperion/missions/judge/li_positivity/lakefile.toml new file mode 100644 index 000000000..3b728a8e4 --- /dev/null +++ b/telperion/missions/judge/li_positivity/lakefile.toml @@ -0,0 +1,12 @@ +name = "MissionJudge_li_positivity" +# Generated by telperion.missions.judge -- DO NOT EDIT BY HAND. +# Path-requires the li_positivity island so its artifact modules and these +# challenge modules share one workspace for `lake env comparator`. +defaultTargets = ["MissionChallenges"] + +[[require]] +name = "LiPositivity" +path = "../../../examples/li_positivity/lean" + +[[lean_lib]] +name = "MissionChallenges" diff --git a/telperion/missions/judge/li_positivity/lean-toolchain b/telperion/missions/judge/li_positivity/lean-toolchain new file mode 100644 index 000000000..75def6093 --- /dev/null +++ b/telperion/missions/judge/li_positivity/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.0-rc1 diff --git a/telperion/missions/judge/quasicrystal/MANIFEST.json b/telperion/missions/judge/quasicrystal/MANIFEST.json new file mode 100644 index 000000000..6079a5578 --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MANIFEST.json @@ -0,0 +1,88 @@ +{ + "island": "quasicrystal", + "package": "Quasicrystal", + "toolchain": "leanprover/lean4:v4.32.0", + "comparator_tag": "v4.32.0", + "not_consumable": [ + "mirrormere/MM_leakage_composite_zero: statement declares `def` besides its theorem; only a single theorem/lemma can be judged (local definitions would collide with the artifact)" + ], + "nodes": [ + { + "slug": "MM_euler_factor_section_offline", + "campaign": "mirrormere", + "theorem": "EulerFactorSectionOffline.euler_factor_section_offline", + "solution_module": "EulerFactorSectionOffline", + "challenge_module": "MissionChallenges.MM_euler_factor_section_offline", + "bridge_theorem": "MissionJudge.MM_euler_factor_section_offline", + "config": "MM_euler_factor_section_offline.comparator.json", + "artifact_sha256": "f7de3a5ef79bef910bbf2e049f8bf14888560cd9eb44e3b557149c4e9e05e492", + "statement_sha256": "5c5a3e23db9076331f26ca4800b72a2561bf7ac003d87c8c79c6df9f19b27733" + }, + { + "slug": "MM_nt_brick_conditional", + "campaign": "mirrormere", + "theorem": "Quasicrystal.zeta_ordinates_not_uniformlyDiscrete_of_unbounded_density", + "solution_module": "BoundaryLemmas", + "challenge_module": "MissionChallenges.MM_nt_brick_conditional", + "bridge_theorem": "MissionJudge.MM_nt_brick_conditional", + "config": "MM_nt_brick_conditional.comparator.json", + "artifact_sha256": "bb6f0d04dbd6c9d1d103cb08e45866b2162781218e9fef13fb69835b78c7e747", + "statement_sha256": "2553bc64cf6d65a87b4877e4ccd3d3ff4e98109dc082857c01e93730f4dc274f" + }, + { + "slug": "MM_offline_disjoint_discs", + "campaign": "mirrormere", + "theorem": "Quasicrystal.offline_disjoint_discs", + "solution_module": "OfflineDiscs", + "challenge_module": "MissionChallenges.MM_offline_disjoint_discs", + "bridge_theorem": "MissionJudge.MM_offline_disjoint_discs", + "config": "MM_offline_disjoint_discs.comparator.json", + "artifact_sha256": "9c4b6dbf394e0fa2eb385d255bcdd42b42eee72fd598909d4d0094d0872a910c", + "statement_sha256": "466a87f6b8bd7afb44a7b5077433e05f65a3aa9257bcc518ed6c19c28113da25" + }, + { + "slug": "MM_primelog_spectrum_dense", + "campaign": "mirrormere", + "theorem": "Quasicrystal.primeLogSpectrum_dense", + "solution_module": "BoundaryLemmas", + "challenge_module": "MissionChallenges.MM_primelog_spectrum_dense", + "bridge_theorem": "MissionJudge.MM_primelog_spectrum_dense", + "config": "MM_primelog_spectrum_dense.comparator.json", + "artifact_sha256": "bb6f0d04dbd6c9d1d103cb08e45866b2162781218e9fef13fb69835b78c7e747", + "statement_sha256": "72fbb2b2835c3660f2cf38ea85712c3b985bc1c6698e03c03d61aecfbbfe2824" + }, + { + "slug": "MM_selfinversive_iff_hardyz_real", + "campaign": "mirrormere", + "theorem": "Quasicrystal.selfInversive_iff_hardyZ_real", + "solution_module": "InvolutionDictionary", + "challenge_module": "MissionChallenges.MM_selfinversive_iff_hardyz_real", + "bridge_theorem": "MissionJudge.MM_selfinversive_iff_hardyz_real", + "config": "MM_selfinversive_iff_hardyz_real.comparator.json", + "artifact_sha256": "7cbddf365565a23bdb02c9bee84be1e19704b46f28605a7c36e3e939983c7a98", + "statement_sha256": "685f95d8ed2ad597264d8d480406db2c8e39531415deccb36a6f26169505a3ea" + }, + { + "slug": "MM_torus_section_n2_rigidity", + "campaign": "mirrormere", + "theorem": "Quasicrystal.torus_section_n2_rigidity", + "solution_module": "TorusSectionLadder", + "challenge_module": "MissionChallenges.MM_torus_section_n2_rigidity", + "bridge_theorem": "MissionJudge.MM_torus_section_n2_rigidity", + "config": "MM_torus_section_n2_rigidity.comparator.json", + "artifact_sha256": "f36228c7c216b18e2fb15e708135df51d9f7b343082b50ee8e862204f36e56b8", + "statement_sha256": "f5ddf09d460e5f3ea5587b4c413b121d341f966817ba7264bd053c12d08141f3" + }, + { + "slug": "MM_twofreq_realrooted_iff", + "campaign": "mirrormere", + "theorem": "Quasicrystal.twoFreq_realRooted_iff", + "solution_module": "TwoFreqRigidity", + "challenge_module": "MissionChallenges.MM_twofreq_realrooted_iff", + "bridge_theorem": "MissionJudge.MM_twofreq_realrooted_iff", + "config": "MM_twofreq_realrooted_iff.comparator.json", + "artifact_sha256": "5bd27f2c7303e5d5d447b90b41b2a1a3dd931f368ff65bae55c9e33d4e24cf91", + "statement_sha256": "c5aeb410defc350df9ec27eec073971bf09894a71d678366359daf45c4c16e02" + } + ] +} diff --git a/telperion/missions/judge/quasicrystal/MM_euler_factor_section_offline.comparator.json b/telperion/missions/judge/quasicrystal/MM_euler_factor_section_offline.comparator.json new file mode 100644 index 000000000..a8147307d --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MM_euler_factor_section_offline.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_euler_factor_section_offline", + "solution_module": "MissionChallenges.MM_euler_factor_section_offline", + "theorem_names": [ + "MissionJudge.MM_euler_factor_section_offline" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/quasicrystal/MM_nt_brick_conditional.comparator.json b/telperion/missions/judge/quasicrystal/MM_nt_brick_conditional.comparator.json new file mode 100644 index 000000000..dd0bf9d1d --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MM_nt_brick_conditional.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_nt_brick_conditional", + "solution_module": "MissionChallenges.MM_nt_brick_conditional", + "theorem_names": [ + "MissionJudge.MM_nt_brick_conditional" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/quasicrystal/MM_offline_disjoint_discs.comparator.json b/telperion/missions/judge/quasicrystal/MM_offline_disjoint_discs.comparator.json new file mode 100644 index 000000000..b9e8924bf --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MM_offline_disjoint_discs.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_offline_disjoint_discs", + "solution_module": "MissionChallenges.MM_offline_disjoint_discs", + "theorem_names": [ + "MissionJudge.MM_offline_disjoint_discs" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/quasicrystal/MM_primelog_spectrum_dense.comparator.json b/telperion/missions/judge/quasicrystal/MM_primelog_spectrum_dense.comparator.json new file mode 100644 index 000000000..18dc183c2 --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MM_primelog_spectrum_dense.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_primelog_spectrum_dense", + "solution_module": "MissionChallenges.MM_primelog_spectrum_dense", + "theorem_names": [ + "MissionJudge.MM_primelog_spectrum_dense" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/quasicrystal/MM_selfinversive_iff_hardyz_real.comparator.json b/telperion/missions/judge/quasicrystal/MM_selfinversive_iff_hardyz_real.comparator.json new file mode 100644 index 000000000..ddd86d2f9 --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MM_selfinversive_iff_hardyz_real.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_selfinversive_iff_hardyz_real", + "solution_module": "MissionChallenges.MM_selfinversive_iff_hardyz_real", + "theorem_names": [ + "MissionJudge.MM_selfinversive_iff_hardyz_real" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/quasicrystal/MM_torus_section_n2_rigidity.comparator.json b/telperion/missions/judge/quasicrystal/MM_torus_section_n2_rigidity.comparator.json new file mode 100644 index 000000000..85b04facb --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MM_torus_section_n2_rigidity.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_torus_section_n2_rigidity", + "solution_module": "MissionChallenges.MM_torus_section_n2_rigidity", + "theorem_names": [ + "MissionJudge.MM_torus_section_n2_rigidity" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/quasicrystal/MM_twofreq_realrooted_iff.comparator.json b/telperion/missions/judge/quasicrystal/MM_twofreq_realrooted_iff.comparator.json new file mode 100644 index 000000000..61eb8a1df --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MM_twofreq_realrooted_iff.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_twofreq_realrooted_iff", + "solution_module": "MissionChallenges.MM_twofreq_realrooted_iff", + "theorem_names": [ + "MissionJudge.MM_twofreq_realrooted_iff" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/quasicrystal/MissionChallenges.lean b/telperion/missions/judge/quasicrystal/MissionChallenges.lean new file mode 100644 index 000000000..4c6be8ae9 --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MissionChallenges.lean @@ -0,0 +1,7 @@ +import MissionChallenges.MM_euler_factor_section_offline +import MissionChallenges.MM_nt_brick_conditional +import MissionChallenges.MM_offline_disjoint_discs +import MissionChallenges.MM_primelog_spectrum_dense +import MissionChallenges.MM_selfinversive_iff_hardyz_real +import MissionChallenges.MM_torus_section_n2_rigidity +import MissionChallenges.MM_twofreq_realrooted_iff diff --git a/telperion/missions/judge/quasicrystal/MissionChallenges/MM_euler_factor_section_offline.lean b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_euler_factor_section_offline.lean new file mode 100644 index 000000000..c7052f9c1 --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_euler_factor_section_offline.lean @@ -0,0 +1,22 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_euler_factor_section_offline. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_euler_factor_section_offline.lean (header sha256 fa3c783e7bc1b9d7), binders and conclusion verbatim; the + PROOF is the artifact constant `EulerFactorSectionOffline.euler_factor_section_offline` from EulerFactorSectionOffline. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import EulerFactorSectionOffline + +namespace EulerFactorSectionOffline + +open Quasicrystal + +theorem _root_.MissionJudge.MM_euler_factor_section_offline : + ¬ (∀ x : ℂ, + twoFreq 1 ((-(1 / Real.sqrt 2) : ℝ) : ℂ) 0 (-(Real.log 2)) x = 0 → x.im = 0) := + EulerFactorSectionOffline.euler_factor_section_offline + +end EulerFactorSectionOffline diff --git a/telperion/missions/judge/quasicrystal/MissionChallenges/MM_nt_brick_conditional.lean b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_nt_brick_conditional.lean new file mode 100644 index 000000000..faabdc76e --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_nt_brick_conditional.lean @@ -0,0 +1,21 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_nt_brick_conditional. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_nt_brick_conditional.lean (header sha256 9921b9185d246847), binders and conclusion verbatim; the + PROOF is the artifact constant `Quasicrystal.zeta_ordinates_not_uniformlyDiscrete_of_unbounded_density` from BoundaryLemmas. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import BoundaryLemmas + +namespace Quasicrystal + +open Real + +theorem _root_.MissionJudge.MM_nt_brick_conditional : + ∀ {Ordinates : Set ℝ} (hRvM : RvMUnboundedMeanDensity Ordinates), ¬ IsUniformlyDiscrete Ordinates := + Quasicrystal.zeta_ordinates_not_uniformlyDiscrete_of_unbounded_density + +end Quasicrystal diff --git a/telperion/missions/judge/quasicrystal/MissionChallenges/MM_offline_disjoint_discs.lean b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_offline_disjoint_discs.lean new file mode 100644 index 000000000..5273e3bd3 --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_offline_disjoint_discs.lean @@ -0,0 +1,22 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_offline_disjoint_discs. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_offline_disjoint_discs.lean (header sha256 bac57ccef7c3f828), binders and conclusion verbatim; the + PROOF is the artifact constant `Quasicrystal.offline_disjoint_discs` from OfflineDiscs. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import OfflineDiscs + +namespace Quasicrystal + +theorem _root_.MissionJudge.MM_offline_disjoint_discs : + ∀ (S : Finset ℂ) + (hstrip : ∀ z ∈ S, 0 < z.re ∧ z.re < 1), ∃ r : ℝ, 0 < r ∧ + (∀ z ∈ S, ∀ w ∈ S, z ≠ w → Disjoint (Metric.closedBall z r) (Metric.closedBall w r)) ∧ + (∀ z ∈ S, Metric.closedBall z r ⊆ {s : ℂ | 0 < s.re ∧ s.re < 1}) := + Quasicrystal.offline_disjoint_discs + +end Quasicrystal diff --git a/telperion/missions/judge/quasicrystal/MissionChallenges/MM_primelog_spectrum_dense.lean b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_primelog_spectrum_dense.lean new file mode 100644 index 000000000..96015a46d --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_primelog_spectrum_dense.lean @@ -0,0 +1,21 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_primelog_spectrum_dense. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_primelog_spectrum_dense.lean (header sha256 642789c568ecf42c), binders and conclusion verbatim; the + PROOF is the artifact constant `Quasicrystal.primeLogSpectrum_dense` from BoundaryLemmas. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import BoundaryLemmas + +namespace Quasicrystal + +open Real + +theorem _root_.MissionJudge.MM_primelog_spectrum_dense : + Dense (↑(AddSubgroup.closure ({Real.log 2, Real.log 3} : Set ℝ)) : Set ℝ) := + Quasicrystal.primeLogSpectrum_dense + +end Quasicrystal diff --git a/telperion/missions/judge/quasicrystal/MissionChallenges/MM_selfinversive_iff_hardyz_real.lean b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_selfinversive_iff_hardyz_real.lean new file mode 100644 index 000000000..c17687abb --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_selfinversive_iff_hardyz_real.lean @@ -0,0 +1,25 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_selfinversive_iff_hardyz_real. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_selfinversive_iff_hardyz_real.lean (header sha256 8cfa120c735a6388), binders and conclusion verbatim; the + PROOF is the artifact constant `Quasicrystal.selfInversive_iff_hardyZ_real` from InvolutionDictionary. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import InvolutionDictionary + +namespace Quasicrystal + +open Polynomial Complex + +theorem _root_.MissionJudge.MM_selfinversive_iff_hardyz_real : + ∀ {p : ℂ[X]} {phase u : ℂ} + (hid : ∀ z : ℂ, z ≠ 0 → + z ^ p.natDegree * (starRingEnd ℂ) (p.eval (1 / (starRingEnd ℂ) z)) + = phase * p.eval z) + (hu_norm : ‖u‖ = 1) (hu_sq : u ^ 2 = phase) (ω : ℝ) (x : ℝ), (hardyZ p u ω x).im = 0 := + Quasicrystal.selfInversive_iff_hardyZ_real + +end Quasicrystal diff --git a/telperion/missions/judge/quasicrystal/MissionChallenges/MM_torus_section_n2_rigidity.lean b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_torus_section_n2_rigidity.lean new file mode 100644 index 000000000..ed0beba55 --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_torus_section_n2_rigidity.lean @@ -0,0 +1,23 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_torus_section_n2_rigidity. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_torus_section_n2_rigidity.lean (header sha256 ae6668c61cff9908), binders and conclusion verbatim; the + PROOF is the artifact constant `Quasicrystal.torus_section_n2_rigidity` from TorusSectionLadder. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import TorusSectionLadder + +namespace Quasicrystal + +open Complex + +theorem _root_.MissionJudge.MM_torus_section_n2_rigidity : + ∀ (c₁ c₂ : ℂ) (lam₁ lam₂ : ℝ) + (hc₁ : c₁ ≠ 0) (hc₂ : c₂ ≠ 0) (hlam : lam₁ ≠ lam₂), (∀ x : ℂ, linearTorusForm 2 ![c₁, c₂] (torusOrbit 2 ![lam₁, lam₂] x) = 0 → x.im = 0) + ↔ ‖c₁‖ = ‖c₂‖ := + Quasicrystal.torus_section_n2_rigidity + +end Quasicrystal diff --git a/telperion/missions/judge/quasicrystal/MissionChallenges/MM_twofreq_realrooted_iff.lean b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_twofreq_realrooted_iff.lean new file mode 100644 index 000000000..8f49e5198 --- /dev/null +++ b/telperion/missions/judge/quasicrystal/MissionChallenges/MM_twofreq_realrooted_iff.lean @@ -0,0 +1,22 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_twofreq_realrooted_iff. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_twofreq_realrooted_iff.lean (header sha256 17b7c24b90f05018), binders and conclusion verbatim; the + PROOF is the artifact constant `Quasicrystal.twoFreq_realRooted_iff` from TwoFreqRigidity. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import TwoFreqRigidity + +namespace Quasicrystal + +open Complex + +theorem _root_.MissionJudge.MM_twofreq_realrooted_iff : + ∀ (c₁ c₂ : ℂ) (lam₁ lam₂ : ℝ) + (hc₁ : c₁ ≠ 0) (hc₂ : c₂ ≠ 0) (hlam : lam₁ ≠ lam₂), (∀ x : ℂ, twoFreq c₁ c₂ lam₁ lam₂ x = 0 → x.im = 0) ↔ ‖c₁‖ = ‖c₂‖ := + Quasicrystal.twoFreq_realRooted_iff + +end Quasicrystal diff --git a/telperion/missions/judge/quasicrystal/lakefile.toml b/telperion/missions/judge/quasicrystal/lakefile.toml new file mode 100644 index 000000000..50ea87cb5 --- /dev/null +++ b/telperion/missions/judge/quasicrystal/lakefile.toml @@ -0,0 +1,12 @@ +name = "MissionJudge_quasicrystal" +# Generated by telperion.missions.judge -- DO NOT EDIT BY HAND. +# Path-requires the quasicrystal island so its artifact modules and these +# challenge modules share one workspace for `lake env comparator`. +defaultTargets = ["MissionChallenges"] + +[[require]] +name = "Quasicrystal" +path = "../../../examples/quasicrystal/lean" + +[[lean_lib]] +name = "MissionChallenges" diff --git a/telperion/missions/judge/quasicrystal/lean-toolchain b/telperion/missions/judge/quasicrystal/lean-toolchain new file mode 100644 index 000000000..94b9f495b --- /dev/null +++ b/telperion/missions/judge/quasicrystal/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.32.0 diff --git a/telperion/src/telperion/missions/judge.py b/telperion/src/telperion/missions/judge.py index 946e5709a..628939a82 100644 --- a/telperion/src/telperion/missions/judge.py +++ b/telperion/src/telperion/missions/judge.py @@ -156,6 +156,16 @@ def module_name_of(lean_dir: Path, artifact: Path) -> str: _LIB_RE = re.compile(r'(?ms)^\[\[lean_lib\]\]\s*\nname\s*=\s*"([^"]+)"') +#: Islands whose AxiomGuard libs cannot all be imported into one module. li_positivity: +#: `ZeroFreeBridge.zeta_sphere_bound` is declared in both DlvpZetaDisk (in +#: AxiomGuardLiPositivity's closure) and ZeroFreeElementary (in AxiomGuardZeroFree's), so a +#: bridge that imports both fails with "environment already contains". For these islands the +#: bridge imports only the FIRST guard (sorted) whose import closure contains the artifact, +#: so the shadowing check covers that guard's closure rather than the whole island. Every +#: other island imports all of its guards (they co-import; zeta_reflection has ten). +GUARD_POLICY_ONE_CONTAINING = frozenset({"li_positivity"}) + + def island_guard_modules(lean_dir: Path) -> List[str]: """The island's `AxiomGuard*` lean_libs, which by convention import every island module. Importing them into a challenge makes a shadowed vocabulary constant a build error.""" @@ -163,6 +173,36 @@ def island_guard_modules(lean_dir: Path) -> List[str]: return sorted(m.group(1) for m in _LIB_RE.finditer(text) if m.group(1).startswith("AxiomGuard")) +def artifact_imports(text: str) -> List[str]: + """The `import` lines of a Lean source (comments stripped).""" + ga = _guard_anchors() + return [m.group(1) for m in _IMPORT_RE.finditer(ga.strip_lean_comments(text))] + + +def import_closure(lean_dir: Path, module: str, _seen: Optional[set] = None) -> set: + """Island-local import closure of `module` (modules whose source is under `lean_dir`; + external packages are not followed). Includes `module` itself.""" + seen = _seen if _seen is not None else set() + if module in seen: + return seen + seen.add(module) + src = Path(lean_dir) / (module.replace(".", "/") + ".lean") + if src.is_file(): + for dep in artifact_imports(src.read_text()): + import_closure(lean_dir, dep, seen) + return seen + + +def guards_for(lean_dir: Path, island: str, guards: Sequence[str], solution_module: str) -> List[str]: + """Which guard libs a bridge for `solution_module` imports (see GUARD_POLICY_ONE_CONTAINING).""" + if island not in GUARD_POLICY_ONE_CONTAINING: + return list(guards) + for g in guards: + if solution_module in import_closure(lean_dir, g): + return [g] + return [] + + # --------------------------------------------------------------------------- # The challenge (bridge) module # --------------------------------------------------------------------------- @@ -387,8 +427,17 @@ def files(self) -> "OrderedDict[str, str]": "[[lean_lib]]\n" 'name = "MissionChallenges"\n' ) - files["MissionChallenges.lean"] = "".join( - f"import {c.challenge_module}\n" for c in self.challenges) + if self.island in GUARD_POLICY_ONE_CONTAINING: + # A root that imports every bridge would co-import the guards that cannot coexist + # (li_positivity: zeta_sphere_bound). CI builds the bridge modules by name, never + # the root, so the root is a comment here rather than a build failure. + files["MissionChallenges.lean"] = ( + f"-- {_SENTINEL}. No root imports on `{self.island}`: its AxiomGuard libs cannot\n" + "-- be imported together, so each bridge module imports one of them and is built by\n" + "-- name (`lake build MissionChallenges.`), never through this root.\n") + else: + files["MissionChallenges.lean"] = "".join( + f"import {c.challenge_module}\n" for c in self.challenges) for c in self.challenges: files[f"MissionChallenges/{c.slug}.lean"] = c.challenge_text files[f"{c.slug}.comparator.json"] = json.dumps(c.config, indent=2) + "\n" @@ -438,8 +487,8 @@ def build_bundle(telperion_root: Path, island: str, *, enable_nanoda: bool = Tru try: text = render_challenge( slug=a.node, campaign=a.campaign, theorem=a.theorem, solution_module=sol, - guard_modules=guards, statement_text=statement_text, - artifact_text=a.artifact.read_text()) + guard_modules=guards_for(lean_dir, island, guards, sol), + statement_text=statement_text, artifact_text=a.artifact.read_text()) except JudgeError as e: problems.append(f"{a.campaign}/{a.node}: {e}") continue diff --git a/telperion/tests/test_missions_judge.py b/telperion/tests/test_missions_judge.py index db7df74c7..02abf6371 100644 --- a/telperion/tests/test_missions_judge.py +++ b/telperion/tests/test_missions_judge.py @@ -240,6 +240,36 @@ def test_artifact_context_collects_namespace_and_opens(): judge.artifact_context("import Mathlib\ntheorem other : True := trivial\n", stmt) +def test_guard_policy_one_containing(tmp_path, monkeypatch): + """On islands whose guards cannot co-import, the bridge imports only the first guard whose + island-local import closure contains the artifact (li_positivity's zeta_sphere_bound clash).""" + art = "import Mathlib\n\ntheorem g : (1 : ℕ) = 1 := rfl\n" + stmt = "import Statements.Defs\n\ntheorem g : (1 : ℕ) = 1 := by sorry\n" + tel = _island(tmp_path, artifact=art, statement=stmt) + lean = tel / "examples" / "isl" / "lean" + (lean / "lakefile.toml").write_text(LAKEFILE + '\n[[lean_lib]]\nname = "AxiomGuardOther"\n') + (lean / "AxiomGuardIsl.lean").write_text("import Vocab\n") # does NOT reach Art + (lean / "Vocab.lean").write_text("import Mathlib\n") + (lean / "AxiomGuardOther.lean").write_text("import Mid\n") + (lean / "Mid.lean").write_text("import Art\n") # reaches Art transitively + assert judge.import_closure(lean, "AxiomGuardOther") >= {"AxiomGuardOther", "Mid", "Art"} + assert "Art" not in judge.import_closure(lean, "AxiomGuardIsl") + # default policy: all guards + [c] = judge.build_bundle(tel, "isl").challenges + assert "import AxiomGuardIsl\nimport AxiomGuardOther\n" in c.challenge_text + # one-containing policy: only the guard that reaches the artifact + monkeypatch.setattr(judge, "GUARD_POLICY_ONE_CONTAINING", frozenset({"isl"})) + [c] = judge.build_bundle(tel, "isl").challenges + assert "import Art\nimport AxiomGuardOther\n" in c.challenge_text and "AxiomGuardIsl" not in c.challenge_text + # the root module carries no imports under this policy (it would co-import the guards) + root = judge.build_bundle(tel, "isl").files()["MissionChallenges.lean"] + assert not [ln for ln in root.splitlines() if ln.startswith("import ")] and "DO NOT EDIT" in root + # and no guard at all when none reaches it + (lean / "Mid.lean").write_text("import Mathlib\n") + [c] = judge.build_bundle(tel, "isl").challenges + assert "AxiomGuard" not in c.challenge_text.split("-/", 1)[1] + + def test_unknown_toolchain_is_refused(): with pytest.raises(judge.JudgeError, match="no known Comparator tag"): judge.comparator_tag("leanprover/lean4:v4.99.0") @@ -324,18 +354,19 @@ def _live() -> bool: return (TELPERION / "missions" / "rh" / "mission.toml").exists() -@pytest.mark.parametrize("island", ["dbn", "rvm_bridge", "zeta_reflection"]) +@pytest.mark.parametrize("island", ["dbn", "rvm_bridge", "zeta_reflection", "li_positivity", "quasicrystal"]) def test_live_committed_bundle_is_in_sync(island): """The committed challenges ARE the registry statements; CI runs the same check.""" if not _live(): pytest.skip("live registry not present") b = judge.build_bundle(TELPERION, island) - # zeta_reflection: AND_g2_reflected_band declares a namespace in its statement (reported) - assert len(b.skipped) == (1 if island == "zeta_reflection" else 0) + # zeta_reflection: AND_g2_reflected_band declares a namespace in its statement; + # quasicrystal: MM_leakage_composite_zero declares local defs (both reported, not skipped) + assert len(b.skipped) == (1 if island in ("zeta_reflection", "quasicrystal") else 0) assert judge.check_bundle(b, judge.default_out(TELPERION, island)) == [] -@pytest.mark.parametrize("island,expected", [("dbn", 3), ("rvm_bridge", 52), ("zeta_reflection", 5), ("li_positivity", 24)]) +@pytest.mark.parametrize("island,expected", [("dbn", 3), ("rvm_bridge", 52), ("zeta_reflection", 9), ("li_positivity", 24), ("quasicrystal", 7)]) def test_live_islands_render(island, expected): if not _live(): pytest.skip("live registry not present")