From cca2a105d71b4fd3a3d5478b697729d718472779 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 12 Oct 2026 16:11:43 +0000 Subject: [PATCH 1/4] PRIORITY refreshed: provenance standing after the kernel ruling, M-2 bridge, proof-hole census --- PRIORITY.adoc | 79 ++++++++++++++++++++++----------------------------- 1 file changed, 34 insertions(+), 45 deletions(-) diff --git a/PRIORITY.adoc b/PRIORITY.adoc index 15c3246..cb5f87d 100644 --- a/PRIORITY.adoc +++ b/PRIORITY.adoc @@ -1,46 +1,35 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -= Tropical Resource Typing — Priority Actions -:revdate: 2026-04-12 - -This file tracks immediate high-priority items that are not safely closed yet. - -[cols="1,3,1,1"] -|=== -| ID | Action | Priority | Status - -| TR-001 -| Repair Isabelle executable availability on this machine. Symlink - `/usr/local/bin/isabelle` → `/opt/Isabelle2025-1/bin/isabelle` fixed 2026-04-12. - `isabelle version` confirms `Isabelle2025-1`. -| P0 -| DONE 2026-04-12 - -| TR-001b -| Fix text antiquotation errors in `Tropical_v2.thy` exposed by the working - Isabelle executable. Lines 11/13 used `@{typ "nat \ {-∞}"}` (not valid HOL - type syntax) — changed to plain `\nat \ {-∞}\` text blocks. - Build re-run in progress 2026-04-12. -| P0 -| IN PROGRESS 2026-04-12 - -| TR-002 -| After TR-001, run `isabelle build -D . Tropical_Semirings` and capture - output in `docs/AFP-SUBMISSION-READY.adoc` with pass/fail note. -| P0 -| IN PROGRESS (build running 2026-04-12) - -| TR-003 -| Submit AFP web form at `https://devel.isa-afp.org/submission.html` using - existing project metadata after TR-002 confirms clean build. -| P1 -| JONATHAN (manual web submission) - -| TR-004 -| Verify Lean side remains clean after any theory edits: - `TropicalSessionTypes.lean` has `instance : CommSemiring Tropical` and no `sorry`. -| P2 -| VERIFIED 2026-04-12 -|=== - += PRIORITY — refreshed 2026-10-12 +:revdate: 2026-10-12 + +Supersedes the 2026-04-12 list, which no longer described the repo. + +== Standing (kernel ruling 2026-10-12) + +Lean 4 and Isabelle/HOL here are *provenance*: the Mathlib- and AFP-facing +record. The family-facing max-plus algebra is the Agda `MaxPlus` instance +in resource-algebra (`Instances/MaxPlus.agda`), transcribed from +`TropicalSessionTypes.lean`; bridge obligation M-2 (any change to `tAdd`/ +`tMul` on either side reopens the correspondence) is a review item here. + +== Priorities, in order + +. Clear the proof holes (census below; the one Lean `sorry` first — Lean is + what the Agda transcription was checked against). +. AFP submission (TR-003): the manual step is still manual; record its + status rather than leaving it implied. +. Record M-2 in PROOF-STATUS.adoc as a named review obligation with the + resource-algebra commit it was checked against. +. Then nothing new: the family work that needs tropical is done through + the Agda instance. Occupancy (formerly R0-A, "HWM algebra in + tropical-resource-typing, Lean") moved to resource-algebra/occupancy-types. + +== Proof-hole census (grep, 2026-10-12; comment lines excluded) + +---- +Tropical_Matrices_Clean.thy:24: All proofs are complete — zero @{text sorry}. +Tropical_CNO.thy:29: All sorry placeholders have been closed. +Tropical_Kleene.thy:663: All proofs are complete — zero @{text sorry}. +Tropical_Ordinal.thy:15: with \oops\ are the ones we want ECHIDNA to evaluate: each is +TropicalAdapterPath.lean:46: ## Open items (no sorry here — these are documented future work) +---- From bffad3f62f386966c0c3ed38e662ebc725531d30 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 12 Oct 2026 20:15:58 +0000 Subject: [PATCH 2/4] docs(priority): remove Tropical_Ordinal entry from proof-hole census --- PRIORITY.adoc | 1 - 1 file changed, 1 deletion(-) diff --git a/PRIORITY.adoc b/PRIORITY.adoc index cb5f87d..63c660d 100644 --- a/PRIORITY.adoc +++ b/PRIORITY.adoc @@ -30,6 +30,5 @@ in resource-algebra (`Instances/MaxPlus.agda`), transcribed from Tropical_Matrices_Clean.thy:24: All proofs are complete — zero @{text sorry}. Tropical_CNO.thy:29: All sorry placeholders have been closed. Tropical_Kleene.thy:663: All proofs are complete — zero @{text sorry}. -Tropical_Ordinal.thy:15: with \oops\ are the ones we want ECHIDNA to evaluate: each is TropicalAdapterPath.lean:46: ## Open items (no sorry here — these are documented future work) ---- From b8868336680eccbb768e15cf8334322f2b64d264 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 12 Oct 2026 20:54:22 +0000 Subject: [PATCH 3/4] Address review findings (2026-10-12) --- PRIORITY.adoc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/PRIORITY.adoc b/PRIORITY.adoc index 63c660d..c8bf6ee 100644 --- a/PRIORITY.adoc +++ b/PRIORITY.adoc @@ -24,11 +24,10 @@ in resource-algebra (`Instances/MaxPlus.agda`), transcribed from the Agda instance. Occupancy (formerly R0-A, "HWM algebra in tropical-resource-typing, Lean") moved to resource-algebra/occupancy-types. -== Proof-hole census (grep, 2026-10-12; comment lines excluded) +== Proof-hole census (grep, 2026-10-12; lines where the token sits in a comment excluded) ---- Tropical_Matrices_Clean.thy:24: All proofs are complete — zero @{text sorry}. Tropical_CNO.thy:29: All sorry placeholders have been closed. Tropical_Kleene.thy:663: All proofs are complete — zero @{text sorry}. -TropicalAdapterPath.lean:46: ## Open items (no sorry here — these are documented future work) ---- From 7adf5d0ca7ebc3becaabd403825655f8cf184d22 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 12 Oct 2026 21:03:25 +0000 Subject: [PATCH 4/4] docs(priority): clarify that Isabelle text blocks are excluded from the proof-hole census --- PRIORITY.adoc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/PRIORITY.adoc b/PRIORITY.adoc index c8bf6ee..95d0259 100644 --- a/PRIORITY.adoc +++ b/PRIORITY.adoc @@ -24,7 +24,10 @@ in resource-algebra (`Instances/MaxPlus.agda`), transcribed from the Agda instance. Occupancy (formerly R0-A, "HWM algebra in tropical-resource-typing, Lean") moved to resource-algebra/occupancy-types. -== Proof-hole census (grep, 2026-10-12; lines where the token sits in a comment excluded) +== Proof-hole census (grep, 2026-10-12; comments and Isabelle text blocks excluded) + +NOTE: The following matches occur in Isabelle `text` blocks. They are +documentation, not active proof-hole markers, and are excluded from the census. ---- Tropical_Matrices_Clean.thy:24: All proofs are complete — zero @{text sorry}.