TJC-1814: leanchecker per push, nanoda at release; brace README superscripts

.github/workflows/ci.yml

@@ -18,30 +18,20 @@ jobs:
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           build-args: --wfail
-      # lean-action's nanoda integration cannot detect this package's module
-      # name (it requires a [package] table in lakefile.toml, which Lake
-      # rejects, and it conflates the package name with the root module), so
-      # the same check runs here explicitly with the module name pinned, and
-      # with the checker sources pinned by commit rather than cloned at HEAD.
-      - name: nanoda external kernel check
+      # Kernel re-check of every Goemans module with leanchecker, the external
+      # checker that ships inside the Lean toolchain (lean4checker's
+      # successor). The independent-implementation nanoda re-check of the full
+      # export runs at release time in release.yml. lean-action's nanoda
+      # integration is unusable here: its module detection requires a
+      # [package] table that Lake's TOML schema rejects, and its pinned
+      # checker predates lean4export's NDJSON format.
+      - name: leanchecker external kernel re-check
         run: |
           set -euo pipefail
-          if ! command -v cargo >/dev/null; then
-            curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \
-              | sh -s -- -y --default-toolchain stable --profile minimal
-            . "$HOME/.cargo/env"
-          fi
-          git clone https://github.com/leanprover/lean4export.git _lean4export
-          git -C _lean4export checkout af5aa64bb914c3c2c781f378088dbd38acf4f804
-          cp lean-toolchain _lean4export/
-          (cd _lean4export && lake build)
-          git clone https://github.com/ammkrn/nanoda_lib.git _nanoda_lib
-          git -C _nanoda_lib checkout e5438ac0a85a036b6dfe093aa457bc3448498014
-          (cd _nanoda_lib && cargo build --release)
-          lake env _lean4export/.lake/build/bin/lean4export Goemans > _nanoda_export.txt
-          wc -c _nanoda_export.txt
-          printf '%s' '{"export_file_path":"_nanoda_export.txt","use_stdin":false,"permitted_axioms":["propext","Classical.choice","Quot.sound","Lean.trustCompiler"],"unpermitted_axiom_hard_error":false,"nat_extension":true,"string_extension":true,"print_success_message":true}' > _nanoda_config.json
-          _nanoda_lib/target/release/nanoda_bin _nanoda_config.json
+          for M in Goemans $(ls Goemans/*.lean | sed 's|Goemans/|Goemans.|; s|\.lean$||'); do
+            echo "leanchecker $M"
+            lake env leanchecker "$M"
+          done
 
   python:
     name: Python ${{ matrix.python }}

.github/workflows/release.yml

@@ -17,9 +17,22 @@ jobs:
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           build-args: --wfail
-      # Same explicit nanoda check as ci.yml (lean-action's integration cannot
-      # detect this package's module name); checker sources pinned by commit.
-      - name: nanoda external kernel check
+      # Same per-module leanchecker re-check as ci.yml.
+      - name: leanchecker external kernel re-check
+        run: |
+          set -euo pipefail
+          for M in Goemans $(ls Goemans/*.lean | sed 's|Goemans/|Goemans.|; s|\.lean$||'); do
+            echo "leanchecker $M"
+            lake env leanchecker "$M"
+          done
+      # Independent Rust kernel re-check (nanoda) of the complete NDJSON
+      # export: Goemans plus its full mathlib closure, ~300k declarations.
+      # Both checker sources are pinned by commit; the json_string branch is
+      # the one that parses lean4export's current NDJSON format.
+      # unpermitted_axiom_hard_error stays false because Lean core *declares*
+      # sorryAx in every environment (declaring is not depending); the
+      # axiom-dependency policy is enforced in-build by Goemans.TrustAudit.
+      - name: nanoda independent kernel re-check
         run: |
           set -euo pipefail
           if ! command -v cargo >/dev/null; then
@@ -32,11 +45,11 @@ jobs:
           cp lean-toolchain _lean4export/
           (cd _lean4export && lake build)
           git clone https://github.com/ammkrn/nanoda_lib.git _nanoda_lib
-          git -C _nanoda_lib checkout e5438ac0a85a036b6dfe093aa457bc3448498014
+          git -C _nanoda_lib checkout 9c3a447bb3fd3056c906a05978ae8e13f524cd21
           (cd _nanoda_lib && cargo build --release)
           lake env _lean4export/.lake/build/bin/lean4export Goemans > _nanoda_export.txt
           wc -c _nanoda_export.txt
-          printf '%s' '{"export_file_path":"_nanoda_export.txt","use_stdin":false,"permitted_axioms":["propext","Classical.choice","Quot.sound","Lean.trustCompiler"],"unpermitted_axiom_hard_error":false,"nat_extension":true,"string_extension":true,"print_success_message":true}' > _nanoda_config.json
+          printf '%s' '{"export_file_path":"_nanoda_export.txt","use_stdin":false,"permitted_axioms":["propext","Classical.choice","Quot.sound","Lean.trustCompiler"],"unpermitted_axiom_hard_error":false,"nat_extension":true,"string_extension":true,"print_success_message":true,"num_threads":4}' > _nanoda_config.json
           _nanoda_lib/target/release/nanoda_bin _nanoda_config.json
       - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9
         with:

README.md

@@ -6,16 +6,16 @@ Rybin Digraph, with Obstructions to
 Amplification_](paper/goemans_gap_paper.pdf).
 
 The main result determines the exact worst-case cost ratio on the
-seven-vertex Rybin digraph $H^*$:
+seven-vertex Rybin digraph $H^{\ast}$:
 
 $$
-\rho(H^*)=\rho^*=\frac{2}{2\sqrt 2-1}
+\rho(H^{\ast})=\rho^{\ast}=\frac{2}{2\sqrt 2-1}
                =\frac{4\sqrt 2+2}{7}
                \approx 1.0938363214.
 $$
 
-Here $\rho(H^*)$ is the supremum, over positive-fractional-cost instances on
-$H^*$, of the least admissible unsplittable cost divided by the fractional
+Here $\rho(H^{\ast})$ is the supremum, over positive-fractional-cost instances on
+$H^{\ast}$, of the least admissible unsplittable cost divided by the fractional
 cost. The supremum is not attained. The repository also checks D. Rybin's
 original counterexample exactly: fractional cost 58 versus minimum admissible
 unsplittable cost 60, a ratio of $30/29$.
@@ -33,11 +33,11 @@ exploratory computation.
 
 | Component | Method | Claim level |
 |---|---|---|
-| `Goemans/` | Lean 4 + mathlib, kernel checked | Exact upper bound, explicit integral Pell lower family, supremum equality, and strict non-attainment on $H^*$ — in parametrized and first-principles graph form, with path enumeration, flow decomposition, and literal model round trips proved; plus the Section 5 gate collapse, both conclusions of Proposition 5.1, Definition 6.1, Lemmas 6.2–6.4, Remark 6.5, and Definition 7.1/Lemma 7.2 with the one-stage unit-demand threshold and strict ratio bound |
+| `Goemans/` | Lean 4 + mathlib, kernel checked | Exact upper bound, explicit integral Pell lower family, supremum equality, and strict non-attainment on $H^{\ast}$ — in parametrized and first-principles graph form, with path enumeration, flow decomposition, and literal model round trips proved; plus the Section 5 gate collapse, both conclusions of Proposition 5.1, Definition 6.1, Lemmas 6.2–6.4, Remark 6.5, and Definition 7.1/Lemma 7.2 with the one-stage unit-demand threshold and strict ratio bound |
 | `verify-goemans` | Exhaustive integer enumeration | Exact 58-versus-60 counterexample and exact violation-budget thresholds |
 | `amplify-family` | `fractions.Fraction` | Exact checks for the displayed integral families |
 | `revision-checks` | Exhaustive rational enumeration | Exact checks for the general-family examples, gate collapse, and dummy-terminal embedding |
-| `certify-sweep` | Seeded NumPy floating-point vertex enumeration and local search | Numerical stress test on $H^*$ plus a sampled four-terminal side search; boundary points and cases with more than nine admissible routing vectors are skipped, so this is not a proof certificate |
+| `certify-sweep` | Seeded NumPy floating-point vertex enumeration and local search | Numerical stress test on $H^{\ast}$ plus a sampled four-terminal side search; boundary points and cases with more than nine admissible routing vectors are skipped, so this is not a proof certificate |
 | `interval-search` | Exhaustive finite structure enumeration plus truncated assignment enumeration and floating-point grid/refinement | Exploratory records in the stated chain subclass; at most the first 16 minimal-transit assignments per structure are examined |
 | `laned-search` | Seeded floating-point heuristic over every fifth canonical structure | Exploratory records in the stated laned subclass; a deterministic one-fifth structure subsample |
 

RELEASE_CHECKLIST.md

@@ -26,7 +26,7 @@ published.
   and the committed PDF reproduces byte-for-byte.
 - [ ] The supplement is built from the exact tagged commit, its embedded
   manifest verifies, and a second build produces the same archive checksum.
-- [ ] Release notes state the fixed-\(H^*\) scope, attribute the original
+- [ ] Release notes state the fixed-\(H^{\ast}\) scope, attribute the original
   counterexample to D. Rybin, say that global boundedness remains open, and
   retain the “not peer reviewed” label.
 - [ ] The draft GitHub release and all attached artifacts have received a final

RELEASE_NOTES.md

@@ -5,10 +5,10 @@ Research preprint and reproducibility artifact. **Not peer reviewed.**
 ## Result and scope
 
 This release proves the exact worst-case admissible unsplittable-to-fractional
-cost ratio on D. Rybin's fixed seven-vertex digraph \(H^*\):
+cost ratio on D. Rybin's fixed seven-vertex digraph \(H^{\ast}\):
 
 \[
-\rho(H^*)=\frac{2}{2\sqrt 2-1},
+\rho(H^{\ast})=\frac{2}{2\sqrt 2-1},
 \]
 
 as a supremum that is not attained. It does **not** prove a global, planar,