Skip to content

STATE.adoc

Latest commit

 

History

History
399 lines (371 loc) · 22 KB

STATE.adoc

File metadata and controls

399 lines (371 loc) · 22 KB
Raw

STATE — cross-session log

2026-10-27 — rung 3d: TropicalAdapterPath imported, unparaphrased

  • Upstream prerequisite: hyperpolymath/tropical-types#65 moves that package from Lean v4.13.0 to v4.35.0. No statement changes; seven proof edits for core-API drift (implicit arguments of List.not_mem_nil, List.mem_cons_self, List.mem_map_of_mem; Nat.max_def now unfolds to an if; new core add_max_add_*/add_min_add_* simp lemmas made four simp [.., helper] calls loop). There: lake build → 20 jobs green, and its own lean.yml axiom audit, run verbatim, passes; only hub_ceiling moved (propext → propext, Quot.sound, from core simp).

  • Here: lakefile.toml requires tropical-resource-typing at a full commit, pinned for now to #65’s head 226c9e1 so this PR’s CI exercises the real dependency. scripts/fetch-siblings.sh pins the same commit. Re-pin both to #65’s merge commit before merging this.

  • New Marches/TropicalAdapter.lean imports TropicalAdapterPath and re-states none of it. bottleneck (upstream’s min-max ⊗ as a marches Grade, by upstream’s laws); pathCost_eq_accum (upstream’s pathCost is Grade.accum); pathCost_append_via_accum; carried_floor (hub_ceiling read as provenance); bottleneck_carries_unit (a non-empty path carries 𝟙: no loop-freedom from this grade).

  • track-siblings.yml: a tropical-types re-pin now also moves lakefile.toml and lake-manifest.json, so the re-check builds marches against the new HEAD. A failed re-check restores the pins and files an issue (before, it exited red with no issue). Negative control run here: pointing the lake pin at e172f8a (v4.13-only) re-materialises that commit and fails the build (TropicalAdapterPath.lean:132:12, omega); restoring it builds green.

  • KC-13: the one LINK in the correspondence table (both sides Lean, imported). README rows PROVEN / PROVEN (finite).

  • Gates on v4.35.0, verbatim:

    $ lake build
Build completed successfully (19 jobs).
$ grep -rnw sorry Marches/ Marches.lean  # empty
$ lake env lean Marches/BadGadget.lean
[(false, false), (true, true), (false, false), (true, true)]
$ scripts/check-correspondence.sh
PASS: 28 Lean names and 22 sibling names exist at the pins; both negative controls refused

    #print axioms on the five new declarations: propext and/or Quot.sound, each exactly the footprint of the upstream lemma it consumes (pathCost_cons, hub_ceiling, tcMul_one_left). marches adds none. The 20 rung-3e declarations still report none.

  • actionlint 1.7.7 and shellcheck clean (workflow run block extracted and checked too); Asciidoctor warning counts unchanged from main.

  • ROADMAP 3d: met on the PR-head pin; the merge-commit re-pin closes it. Rung 3 then stays OPEN only on 3f: postern still not found (list_repos query postern: no match, 2026-10-27). No tag.

2026-10-27 — rung 3e: path provenance as graded accumulation (echo-types bridge)

  • New Marches/Provenance.lean, imported from Marches.lean. Cut.lean said where a well-typed trace may go; this says what it carries.

    • Grade (a ⊗-monoid: associativity and both units) and Grade.accum, the grade a word of labels accumulates. accum_append (a monoid homomorphism from label words) and accum_map (reads through a relabelling).

    • One region, TropicalGrade: run_eq_seq_carried, the end signature of a run is the start ⊗ the grade its word carried; carried_cons_ne_one, a non-empty word carries a non-unit grade; no_return_of_carried recovers tropical_no_return through the grade.

    • Across the interface: trace_cross_shape, a well-typed two-region trace that crosses is an A-word from an A-start, the crossing, a B-word (typing alone; no strictness used). Interface.fibre is the preimage fibre of τ; Interface.carried is the A-signature at the crossing as a point of it; trace_cross_lands.

    • Region DAG: DiscSys.carried_in_cut and carried_to_cross_in_past, the grade reaching a point inside a cut, or a crossing out of ↓r, is accumulated by a trace of the cut prefix alone (conditional on Acyclic, as every compose theorem is).

    • Exhibits: id_carries (the identity crossing carries the grade intact); zero_forgets, zero_fibre_distinguishes, collapse₀, collapse₁ (a collapsing crossing forgets the A-grade, and the fibre still tells the two traces apart); trace₀ of Cut.lean graded to 4.

  • echo-types read at 1073d60 (its HEAD on 2026-10-27, shallow clone). Its Echo f y := Σ x, f x ≡ y is "the standard preimage fiber" by its own README; EchoProvenance.agda gives the collapse and distinguish theorems. Pinned in scripts/fetch-siblings.sh (ECHO_TYPES_COMMIT); check-correspondence.sh now greps echo-types: refs too (a fabricated echo-types name was run through it and refused); track-siblings.yml re-pins it weekly. Nothing Agda is imported or re-declared.

  • docs/kcut-correspondence.adoc: KC-9 (fibre ↔ Echo, echo-intro), KC-10 (the collapse exhibit ↔ provenance-collapses-at, echoes-distinguish-tag), KC-11 (graded cut-locality, KC-4 again), KC-12 (accumulation needs the ⊗-monoid; K-4’s two laws supply neither associativity nor the right unit). All ASSUMED. F6 row updated.

  • Gates on v4.35.0, verbatim:

    $ lake build
Build completed successfully (16 jobs).
$ grep -rnw sorry Marches/ Marches.lean  # empty
$ lake env lean Marches/BadGadget.lean
[(false, false), (true, true), (false, false), (true, true)]
$ lake env lean Axioms.lean   # #print axioms, the 20 new declarations
'Marches.Grade.accum_append' does not depend on any axioms
  (all 20 lines read "does not depend on any axioms")
$ scripts/check-correspondence.sh
PASS: 24 Lean names and 21 sibling names exist at the pins; both negative controls refused

    A first proof of no_return_of_carried through Nat.add_left_cancel picked up propext; it was reproved from a < a + carried and is axiom-free.

  • actionlint 1.7.7 clean on track-siblings.yml; shellcheck clean on both scripts; Asciidoctor renders the edited .adoc files without warnings. grep -ni converg Marches/Provenance.lean hits only the delimitation.

  • ROADMAP 3e: met 2026-10-27. Rung 3 stays OPEN: 3d and 3f are not done. No tag.

2026-10-19 — CI: estate audit pinned to cicd-suite b17ec1a (not a rung)

  • hyperpolymath/cicd-suite#55 merged as b17ec1a; the caller’s pin moves from 376898b. One line changed in main-estate-audit.yml.

  • What the move brings: cicd-suite’s manifest-check ignore-list inputs (manifest-deed-paths-ignore, manifest-k9-paths-ignore), which default to empty, so marches' behaviour is unchanged; the composite pins inside the reusable now serve current cicd-suite code; and #55 cures cicd-suite main’s red lock-transitive-closure. marches passes neither new input.

  • Still de-onboarded from actions.lock (checked with yq). b17ec1a is an ancestor of cicd-suite origin/main.

  • Gates: actionlint 1.7.7 clean on the caller. No Lean file changed.

2026-10-19 — toolchain v4.34.1 → v4.35.0 (weekly track-lean bot)

  • Gates on v4.35.0, verbatim:

    $ lake build
Build completed successfully (15 jobs).
$ grep -rnw sorry Marches/ Marches.lean  # empty
$ lake env lean Marches/BadGadget.lean
[(false, false), (true, true), (false, false), (true, true)]

2026-10-14 — CI: estate audit pinned to cicd-suite main (not a rung)

  • hyperpolymath/cicd-suite#50 merged as 376898b. Its tree is identical to afa28ff, the PR head marches has called since #44 (git diff --stat afa28ff 376898b is empty). So this changes only the pin, from a PR-branch commit to a commit on cicd-suite’s main.

  • track-estate-audit.yml now has a main commit to compare against, and will move the pin forward weekly by PR.

  • Gates: actionlint 1.7.7 clean on the caller. No Lean file changed.

2026-10-14 — CI: the estate audit becomes a thin caller of cicd-suite (not a rung)

  • Central Estate CI/CD Audit / estate-audit failed after 8s for three reasons:

    • The 26-step copy of cicd-suite’s workflow held here was frozen by actions.lock at cicd-suite@5a10b72. That commit predates cicd-suite #32, which fixed the Required Files Gate.

    • All 26 gates ran in one job, so the first failure hid the rest.

    • Two of the steps (prat, semantic-audit) were stubs that could not fail.

  • The fix is in hyperpolymath/cicd-suite#50 and here:

    • .github/workflows/main-estate-audit.yml is now a ten-line caller of cicd-suite’s reusable audit, pinned at a full SHA. The reusable reports five checks (governance, hygiene, manifests, languages, advisory), and each runs every gate even after one fails. It no longer runs the stubs.

    • cicd-suite’s scripts/deonboard-estate-audit.sh removed the caller from actions.lock, a pure removal of its entry and of the three dependencies only it reached (cicd-suite@main, deed-ecosystem, k9-ecosystem). Onboarded, a cross-repo reusable call startup-fails under sha_pinning_required. The relock workflow from #41 scopes itself to tracked workflows plus those with no uses:, so it leaves the caller out.

    • .github/workflows/track-estate-audit.yml (no uses:) opens a PR each week that moves the pin to cicd-suite HEAD. That PR’s own audit run is the check. It needs AUTOMATION_TOKEN.

  • The workflow and lock changes reached main through #41, which carried a byte-identical port of them. This PR (#44) adds this record.

  • Pin: afa28ff, the head of cicd-suite#50, so that this PR’s pull_request run exercises the cross-repo call for real. Merge cicd-suite#50 first, then re-pin here to its merge commit.

  • Gates: actionlint 1.7.7 clean on both workflows. lake build → Build completed successfully (15 jobs).; grep -rnw sorry empty; #eval orbit unchanged. No Lean file changed.

  • Local harness: cicd-suite’s 24 composite gates at 1aa6bfb were run as composite steps (bash -e -o pipefail) against this commit. All 24 exit

    1. Negative control: with the gates at 5a10b72, the same harness fails required-files, which reproduces the original failure. The pull_request run of the caller is the authoritative check.

2026-10-14 — CI: actions.lock relocked remotely (not a rung)

  • One root cause behind both red checks: .github/workflows/actions.lock drifted.

    • Dependabot (#34) bumped lean-action → v1.6.1 and codeql-action → v4.38.2 but left the lock on v1.6.0 / v4.38.0, so CI ends in startup_failure. dependabot-core still gates lock rewriting behind its github_actions_lockfile experiment.

    • The lock held cicd-suite@main at 5a10b72, before cicd-suite #32 fixed the Required Files Gate (grep -v | wc -l under -e -o pipefail on a comment-only CODEOWNERS). That is why estate-audit fails. The bug is already fixed upstream, so nothing needs filing.

  • .github/workflows/actions-lock.yml (new, no uses:) runs github/gh-actions-lock v0.2.0 --relock remotely. It triggers on pushes to main that change a workflow, weekly, and on dispatch. It is scoped to the workflows the lock already tracks plus every workflow with no uses:, and opens a PR only when actions.lock alone changes.

  • Track latest (maintainer preference: everything updated and checked against latest). Two weekly workflows, neither with uses:; Lean comes from elan’s installer.

    • track-lean.yml: tries the latest stable Lean and runs the three gates. Green → a PR (toolchain, README, STATE entry); red → an issue. Dry run here on v4.35.0: Build completed successfully (15 jobs)., sorry grep empty, #eval orbit unchanged, so the first run opens a v4.35.0 PR.

    • track-siblings.yml: runs check-correspondence.sh against each sibling’s HEAD. Green → one re-pin commit per sibling in one PR; a missing name → an issue, pin unchanged. Dry run here: choreographic-types edb784a→ec08c7a PASS, resource-algebra cf9235c→638dd3e PASS, tropical-types current. Names only; F6 still needs the diff read.

    • Lean headers now point at scripts/fetch-siblings.sh instead of naming a pin, so a re-pin leaves no stale SHA in prose.

  • 3d decided: depend on tropical-types, tracking latest (ROADMAP).

  • Gates: actionlint 1.7.7 (with shellcheck) clean. The run itself can only be exercised on GitHub, because this sandbox cannot reach the GitHub API.

2026-10-14 — toolchain v4.34.0 → v4.34.1 (patch; review finding on #36)

  • CodeRabbit flagged #36 (Major, security): v4.34.1 is the patched release of the 4.34 line. Verified against leanprover/lean4 rather than the bot’s summary: v4.34.0..v4.34.1 adds three runtime reference-count fixes (leanprover/lean4 #15241 sticky counts in deletion cascades, #15288 children of overflowed objects, #15307 panic instead of wrapping in sharecommon_quick_fn), a BitVec.ofNatClamp backport and release preparation. marches checks only its own proofs, so the practical risk was low. Taking the patch keeps the soundness floor on the patched build at no cost.

  • Gates on v4.34.1: lake build → Build completed successfully (15 jobs).; grep -rnw sorry Marches/ Marches.lean empty; #eval orbit unchanged ([(false, false), (true, true), (false, false), (true, true)]). The v4.34.0 results below are now historical.

2026-10-14 — rung 3, items 3a–3c: a region crossing is a cut (Claude Code session, MRC-01)

  • Marches/Cut.lean (3a). A cut is a predecessor-closed set of regions.

    • Cut.edge_crosses_past: in an acyclic graph every edge leaves the principal cut of its source.

    • Cut.path_back_crosses_no_cut: an edge on a cycle crosses no cut, so Acyclic is load-bearing.

    • DiscSys.trace_cross_crosses_cut: every crossing in a well-typed trace crosses a cut holding the start, not the end.

    • DiscSys.trace_mem_back, trace_inside, no_reentry: no re-entry, i.e. no_back_cross lifted to every cut.

    • DiscSys.composeCut: prefix-closure. Its traces are exactly the composite’s traces that end in the prefix (composeCut_trace_embed / _reflect).

    • The two-region Interface versions are trace_cross_crosses_cut and trace_stays_in_B. CutExhibit holds a concrete trace and a negative control.

  • Marches/Tropical.lean TropicalGrade (3b). K-4’s two laws over TropicalNat (seq_unitl, alt_idem). S-3 inside marches: better_reverses_altLe, altLe_one (𝟙 on top, as Loss), s3_witness.

  • docs/kcut-correspondence.adoc + scripts/check-correspondence.sh (3c). Lean ↔ Agda names, each pairing ASSUMED (M-2 idiom). The script fetches siblings at pins (scripts/fetch-siblings.sh, _build/dependencies) and checks names only. Pins: choreographic-types edb784a, resource-algebra cf9235c, tropical-types e172f8a.

  • F6 added (FALSIFIERS.adoc), and it FIRED on reading. MRC-01’s proposed Acyclic ↔ Consistent pairing is withdrawn: Agda’s Consistent p c is a party-indexed merge condition, and marches has no parties. F6 stays open (narrowed).

  • Citation corrections found while reading the pins:

    • T-2’s receiver-knows / sender-knows are in Instances.agda, not Transport.agda.

    • TropicalAdapterPath.lean is in hyperpolymath/tropical-types, whose lake package is tropical-resource-typing, on Lean v4.13.0.

    • marches' TropicalNat is min-plus, so it is not one of M-2’s two (max-plus) objects.

  • Gates:

    • lake build → Build completed successfully (15 jobs).

    • grep -rnw sorry Marches/ Marches.lean is empty.

    • #eval orbit is unchanged ([(false, false), (true, true), (false, false), (true, true)]).

    • #print axioms: every declaration added in 3a/3b depends on no axioms.

    • scripts/check-correspondence.sh → PASS: 15 Lean names and 16 sibling names exist at the pins; both negative controls refused. A mutation test (one bad Lean name, one bad Agda name, one wrong pin) → FAIL, as it should.

  • CI anomalies, pre-existing on main, not caused by this rung:

    • CI has ended in startup_failure since #34. Dependabot moved lean-action to v1.6.1 and codeql-action to v4.38.2 without relocking actions.lock. Fix: gh actions-lock, as in #25.

    • estate-audit fails at cicd-suite’s Required Files Gate. Under -e -o pipefail, a comment-only CODEOWNERS makes grep -v | wc -l exit 1 silently. The fix belongs in cicd-suite.

  • postern was not reachable (add_repo: not found or no access; no list_repos match). No cross-issue was filed. The import plan is kept in the correspondence doc.

  • Status rows moved:

    • New PROVEN rows (README) for 3a/3b.

    • One ASSUMED row for the K-CUT correspondence.

    • No convergence claim (grep -ni converg on new files hits only the disclaimers).

  • Rung 3 stays OPEN: 3d (TropicalAdapterPath import), 3e (echo-types bridge) and 3f (postern) are not done. No tag.

2026-10-14 — toolchain moved to v4.34.0 before rung 3 (Claude Code session)

  • Maintainer decision (MRC-01 open question): move lean-toolchain from v4.15.0 to the estate’s v4.34.0 floor (F-11) before any rung-3 module is added, as its own change.

  • No source change was needed: the tree at ea1920a was built on both toolchains first, and both gave Build completed successfully with no warnings and the same #eval orbit.

  • Gates on v4.34.0: lake build → Build completed successfully (14 jobs).; grep -rnw sorry Marches/ Marches.lean empty; #eval orbit unchanged ([(false, false), (true, true), (false, false), (true, true)]).

  • Rung 3 still OPEN; nothing else moved.

2026-07-07 — rung 2 built and verified (Claude Code session)

  • Digraph foundation lifted: Marches/Digraph.lean — RPath, RPath.snoc/trans/flip, and Acyclic moved out of the GR namespace into Marches. GRHierarchy.lean refactored to consume them, so the customer→provider hierarchy (rung 1) and the region DAG (rung 2) are the SAME Marches.Acyclic. GR proofs unchanged in substance.

  • Reassembly by composition: Marches/Reassembly.lean —

    • Discipline abstracts the shared invariant (strict order + typed step judgment whose every step worsens); Discipline.no_loop proves loop-freedom ONCE, generically.

    • PathAlgebra.toDiscipline — the rung-0 kernel is an instance; toDiscipline_no_loop recovers no_return.

    • DiscSys.compose (HEADLINE): a finite acyclic DAG of disciplines is itself a Discipline. Composite btrans needs only RPath.trans; composite birrefl needs EXACTLY Acyclic S.E (the honest n-region home of the assumption); cstep_worsens is discharged from the componentwise obligations + DAG stratification, no global re-proof — the by-construction counterpart of Kirigami cut soundness. Because compose returns a Discipline, composites NEST: Reassembly.nestedComposed composes a composite as a region.

    • Negatives: no_foreign_local (a region’s label can’t fire from another region), no_self_cross (acyclicity ⇒ self-edge unconstructible).

    • Crossing maps τ are UNCONSTRAINED — worsening is by DAG position.

  • Interface.strict RETIRED (roadmap-sanctioned): rung 2 confirmed order-preservation of crossing maps is never load-bearing, so the field was deleted from Compose.Interface (and its provider in Freewheel.lean) rather than kept as a proven-unused wart.

  • Gates: lake build → Build completed successfully. (14 modules, zero deps); grep -rnw sorry empty; #eval orbit unchanged ([(false, false), (true, true), (false, false), (true, true)]).

  • Claim discipline held: loop-freedom of the typed judgment is NOT protocol convergence (agda-routing’s ground); no convergence claim added anywhere.

2026-07-07 — rung 1 built and verified (Claude Code session)

  • GR wired into Trace: Marches/GRTrace.lean — the five legal (relationship, signature) moves are the constructors of GStep; ill-typed moves (valley, second peer hop, any move from ⊥) are unconstructible. Derivations from c are EXACTLY the valley-free words (gtrace_iff_valley_free), and coincide with non-⊥ evaluation of the rung-0 table (valley_free_iff_gwalk).

  • Acyclicity explicit: Marches/GRHierarchy.lean — Acyclic T.custOf is a named hypothesis; gr_loop_free derives (node, signature) state-level loop-freedom UNDER it. Never silently discharged (F5). Convergence remains agda-routing’s ground; not claimed anywhere.

  • F2 discharged: Marches/Freewheel.lean — identity-extension algebra, inflationary but not strict; f2_discharged exhibits a well-typed non-empty returning trace. hA/hB are load-bearing; stratification alone is not enough. FALSIFIERS F2 → held.

  • Gates re-run: lake build → Build completed successfully.; grep -rnw sorry empty; #eval orbit unchanged ([(false, false), (true, true), (false, false), (true, true)]).

  • Deferred to rung 2 (unchanged): n-region DAG composition; Interface.strict becomes load-bearing or is deleted.

2026-07-07 — rung 0 built and verified (claude.ai session)

  • Repo scaffolded; six modules + root compile clean under Lean 4 v4.15.0, zero dependencies, zero sorry.

  • #eval orbit output (machine-evaluated): [(false, false), (true, true), (false, false), (true, true)].

  • Prior-art first sweep done; agda-routing and Kirigami found and written into LIMITATIONS; claim narrowed accordingly before first commit — no retraction debt.

  • Known deferred items: F2 counterexample (rung 1); GR↔Trace wiring (rung 1); Interface.strict currently unused (rung 2 or delete); LICENSE text TODO (copy from palimpsest-license, do not improvise).

Next action

Rung 3 (see ROADMAP.adoc), the remaining items. 3d: once hyperpolymath/tropical-types#65 merges, re-pin lakefile.toml, lake-manifest.json, scripts/fetch-siblings.sh and the correspondence pin table to its merge commit (one sed of the SHA; then lake build and scripts/check-correspondence.sh). 3e: met 2026-10-27 (Marches/Provenance.lean). 3f: file the postern cross-issue once that repository exists. Obtain the real files; never reconstruct from memory. One rung only.