missions: judge li_positivity (24) and quasicrystal (7 of 8) islands

.github/workflows/missions-comparator.yml

@@ -17,17 +17,16 @@ 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).
 #
 # Not a required check yet. To make a node's record reflect a pass:
 #   PYTHONPATH=src python -m telperion.cli mission comparator-record <Slug> --run-id <run> \
 #       --theorem <name> --run-url <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 }})"

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

telperion/missions/judge/README.md

@@ -7,6 +7,9 @@ and holds one bridge module per proved node:
 ```lean
 import <artifact module>            -- the solution
 import <island AxiomGuard modules>  -- 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)
 <the artifact's own `open` lines>
 namespace <the artifact's namespace at the declaration>
 theorem _root_.MissionJudge.<Slug> :