Skip to content

STATE.adoc

Latest commit

 

History

History
491 lines (458 loc) · 27.3 KB

STATE.adoc

File metadata and controls

491 lines (458 loc) · 27.3 KB
Raw

STATE — cross-session log

2026-11-09 — proof status under the estate proof policy (not a rung)

  • New PROOF-STATUS.adoc, as standards 3-practice/PROOF-POLICY.adoc §8.5 asks. marches is theory (§1), so Agda is the source of truth; its Lean files are target-only evidence (§3). Every theorem: Agda OPEN, Rocq OPEN, ungraded. Owner decision: record now, port to Agda next (new ROADMAP section, ahead of rung 4).

  • Lean leg receipt on abe636a, v4.35.0: lake build 19 jobs; no sorry, admit, axiom, native_decide, extern. Lean.collectAxioms over all 446 Marches declarations: 402 none, 41 propext, 3 propext, Quot.sound; none on sorryAx or Classical.choice. The propext cases are generated injEq lemmas, the Gao–Rexford gext match, and the tropical-types lemmas the adapter consumes. Groups that rest on them are recorded PROVEN-WITH-AXIOMS, naming them (the policy does not yet rule on Lean’s built-ins).

  • CLAUDE.md said "Lean 4 for proofs"; it now defers to the estate policy. README.adoc’s status table now says its `PROVEN means Lean-kernel accepted, not graded.

  • Every theorem name in PROOF-STATUS.adoc was checked with #check (all resolve). Issues #54 and #55 closed as false alarms (the stale tropical-types pin, fixed by #57).

  • secret-scanner.yml had failed at startup, zero jobs, on every run since #33 (a job-level call to a remote reusable). Replaced by the template’s inline scanner (rsr-template-repo 2be7b88, its #295): three jobs, scan / gitleaks, scan / rust-secrets, scan / shell-secrets, job bodies unchanged; checkout pinned by marches' tag (v7.0.1, which the lock resolves to the template’s commit 3d3c42e). Lock entry added by hand in the generator’s shape (no new dependency; the relock bot needs AUTOMATION_TOKEN). Run locally first: gitleaks 8.18.4 (checksum OK) with the estate baseline at standards e064539, working tree and full 68-commit history: no leaks; shell job: none detected; rust job: skips (no Cargo.toml). actionlint clean.

  • Review round (CodeRabbit on #59), each checked against PROOF-POLICY §8.2–§8.4 at standards d036da3:

    • The grade census uses 211 theorems as the denominator; the 235 definitions are not obligations. By kind: 171 theorems and 231 definitions use no axioms, 37 and 4 use propext, 3 and 0 use propext, Quot.sound.

    • The Lean receipt now gives the full commit and the Marches/ tree digest. It is re-run at 6db6c0a (Lean inputs unchanged) and scoped as historical, not a §8.4 current receipt. A CI receipt job is OPEN.

    • PWG-2i and PWG-2ii now also require each Lean or Rocq axiom to be admissible under disposition (c).

    • In the README, the Gao–Rexford table, valley_free_iff_gwalk and both tropical-adapter rows are PROVEN-WITH-AXIOMS, naming their axioms; this is per-name #print axioms, and only GR. and TropicalAdapter. headline names use any. The README’s "no dependencies" claims were stale (tropical-types) and are corrected.

    • The next action below is the Agda port; 3f is deferred.

2026-11-04 — rung 3d closed: tropical-types re-pinned to the #65 merge commit

  • #52 merged before hyperpolymath/tropical-types#65, so main kept the PR-head pin 226c9e1. #65 squash-merged as 168f09d and its branch was deleted; 226c9e1 is then on no branch, and a fresh clone’s git fetch origin never brings it in. Reproduced: TROPICAL_TYPES_COMMIT=226c9e1… scripts/fetch-siblings.sh on an empty _build/dependencies → fatal: reference is not a tree: 226c9e1….

  • That is why the 2026-11-02 track-siblings run filed #54 (choreographic-types) and #55 (resource-algebra): both checks died on the tropical-types fetch, not on a lost name. With the fixed pin, both siblings at their current HEADs (8751c7d, e25d35d) give PASS. The next weekly run re-pins them.

  • The same run had already committed the right re-pins on ci/track-siblings (tropical-types → 168f09d, echo-types → b0982c4) and failed only at gh pr create (Actions may not open PRs without AUTOMATION_TOKEN). Those two commits are cherry-picked here with -x, authorship kept. 168f09d and 226c9e1 have identical Lean trees (git diff --stat over *.lean, lean-toolchain, lakefile.lean is empty).

  • F6, echo-types 1073d60..b0982c4: one commit, and it touches neither proofs/agda/Echo.agda nor proofs/agda/EchoProvenance.agda.

  • #52’s squash also carries CodeRabbit’s autofix of track-siblings.yml (its Major finding: build candidate pins without the write token). Read after the fact: a read-only check job builds and passes patches and JSON as data; publish holds the token, applies only patches touching the four pin files, and still exits red on broken names. shellcheck on both extracted run blocks: clean except SC2153 (info, BASE comes from env:), which actionlint 1.7.7 also reports.

  • Gates on v4.35.0 at 168f09d, from an empty _build/dependencies:

    $ 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

  • ROADMAP 3d: met. Rung 3 stays OPEN on 3f only (postern: list_repos query postern empty). No tag.

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/proven-cicd-and-workflows#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/proven-cicd-and-workflows#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/proven-cicd-and-workflows#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

The Agda port (ROADMAP.adoc, "Agda source of truth"; owner decision 2026-11-09), group by group, each recorded in PROOF-STATUS.adoc. It takes precedence over rung 4.

Deferred, not the next action: rung 3f, the postern cross-issue. It waits on hyperpolymath/postern existing (not found 2026-11-09); 3d and 3e are met. Obtain the real files; never reconstruct from memory. One rung only.