diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e0b5ecb..a3d45b5 100644 --- a/.github/workflows/ci.yml +++ b/.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 }} diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 3fd63b3..c76d783 100644 --- a/.github/workflows/release.yml +++ b/.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: diff --git a/README.md b/README.md index b215fe2..f1eb61e 100644 --- a/README.md +++ b/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 | diff --git a/RELEASE_CHECKLIST.md b/RELEASE_CHECKLIST.md index 53e562c..3b24fed 100644 --- a/RELEASE_CHECKLIST.md +++ b/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 diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index ed3c014..8b04cc2 100644 --- a/RELEASE_NOTES.md +++ b/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,