Repository navigation
feat(provenance): rung 3e, path provenance as graded accumulation - #51
Conversation
Marches/Provenance.lean answers what a well-typed trace carries, as Cut.lean answered where it may go. Words accumulate a grade in a ⊗-monoid (accum_append: a monoid homomorphism). In one tropical region the end signature of a run is the start ⊗ the carried grade (run_eq_seq_carried), and a non-empty word carries a non-unit grade. A two-region trace that crosses is an A-word, the crossing, a B-word (trace_cross_shape, typing alone); what crosses is the A-signature at the crossing, which B sees only through τ, so Interface.fibre (the preimage fibre of τ) is what was carried and cannot be seen. In the region DAG the grade reaching a cut, or a crossing out of ↓r, is accumulated by a trace of the prefix alone. Exhibits: an identity crossing carries the grade intact; a collapsing one forgets it while the fibre still distinguishes. echo-types is pinned at 1073d60 as a fourth sibling (fetch-siblings.sh, check-correspondence.sh, track-siblings.yml); KC-9 to KC-12 pair the fibre and the law set, all ASSUMED under F6. Nothing Agda is imported. Gates: lake build green (16 jobs); grep -rnw sorry empty; #eval orbit unchanged; #print axioms none on all 20 new declarations; check-correspondence.sh PASS (24 Lean, 21 sibling names). Rung 3 stays open on 3d and 3f; no tag. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX
|
No actionable comments were generated in the recent review.
 |
| Layer / File(s) | Summary |
|---|---|
Grade accumulation and tropical results Marches/Provenance.lean, README.adoc, docs/kcut-correspondence.adoc, FALSIFIERS.adoc |
Adds a grade monoid and list accumulation laws. Proves tropical run and non-return results, and records the accumulation correspondence and its stated limitations. |
Crossing traces and interface fibres Marches/Provenance.lean, README.adoc, docs/kcut-correspondence.adoc |
Characterises traces containing a crossing and defines the carried A-signature in the landing-point fibre. Adds identity and collapsing examples and records the KC-9 and KC-10 comparisons. |
Grade results for cut prefixes Marches/Provenance.lean, README.adoc, docs/kcut-correspondence.adoc |
Adds theorems relating grades of traces to prefixes in cuts and principal past cuts. Documents the cut-locality correspondence in KC-11. |
Echo-types checks and milestone records Marches.lean, .github/workflows/track-siblings.yml, scripts/*, docs/kcut-correspondence.adoc, README.adoc, ROADMAP.adoc, STATE.adoc |
Adds the echo-types commit pin and sibling checks. Adds the KC-9 to KC-12 correspondence records and updates the rung 3e status and validation records. |
Priority:
Estimated code review effort: 4 (Complex) | ~45 minutes
Change: Feature
Merge Risk: 
d4d0c
-
No actionable issue remains from this review. The change is mergeable after normal project checks.
Pre-merge checks: 
-
Check name Status Explanation Title check The title names the change accurately: it adds the rung 3e provenance module, Marches/Provenance.lean, which models path provenance as graded accumulation. It is specific and follows the conventional-… Docstring Coverage No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Documentation-only edits and deletions within survi… Linked Issues check Check skipped because no linked issues were found for this pull request. Out of Scope Changes check Check skipped because no linked issues were found for this pull request. Description check The pull request description directly matches the changeset. It describes the new provenance module, graded accumulation, crossing interfaces, echo-types bridge, documentation updates, and validation … Full details: Title check
-
Explanation
The title names the change accurately: it adds the rung 3e provenance module, Marches/Provenance.lean, which models path provenance as graded accumulation. It is specific and follows the conventional-commit form. The title does not mention the echo-types bridge or the pin and CI changes, which is acceptable because it names the primary change.
Full details: Docstring Coverage
-
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 2 files. (8 skipped: 8 unsupported.)
Full details: Description check
-
Explanation
The pull request description directly matches the changeset. It describes the new provenance module, graded accumulation, crossing interfaces, echo-types bridge, documentation updates, and validation gates.
-
Finishing Touches
-
📝 Generate docstrings
-
- Commit to this branch
- Create a new PR
-
- Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.
Comment @coderabbitai help to get the list of available commands.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Rung 3e: what a trace carries (echo-types bridge)
Cut.leananswered where a well-typed trace may go.Marches/Provenance.leananswers what it carries.Theorems (all PROVEN by
lake build, all axiom-free)⊗-assoc + both units)Grade.accum_append,accum_mapstart ⊗ carried(word)TropicalGrade.run_eq_seq_carriedno_returnfalls outcarried_cons_ne_one,no_return_of_carriedtrace_cross_shapeτ; its fibre isInterface.fibreInterface.fibre,Interface.carried,trace_cross_lands↓r, is accumulated by a trace of the prefix alone (conditional onAcyclic)DiscSys.carried_in_cut,carried_to_cross_in_pastid_carries,zero_forgets,zero_fibre_distinguishes,collapse₀,collapse₁The bridge
echo-types'
Echo f y := Σ x, f x ≡ yis, by its own README, "the standard preimage fiber".Interface.fibreis that fibre for the crossing map, in marches' own terms; nothing Agda is imported or re-declared. echo-types is pinned at1073d60as a fourth sibling (fetch-siblings.sh,check-correspondence.shregex,track-siblings.yml), anddocs/kcut-correspondence.adocgains KC-9 to KC-12, all ASSUMED under F6. KC-12 records a finding: accumulation needs the⊗-monoid, which K-4's two laws do not supply.Gates (verbatim in
STATE.adoc)lake build→Build completed successfully (16 jobs).grep -rnw sorry Marches/ Marches.lean→ empty#eval orbit→[(false, false), (true, true), (false, false), (true, true)]#print axiomson the 20 new declarations → none (one first proof picked uppropextviaNat.add_left_canceland was reproved)scripts/check-correspondence.sh→PASS: 24 Lean names and 21 sibling names exist at the pins; both negative controls refused; a fabricated echo-types name was also run through it and refusedCI on the head: all 11 checks green, including
build(the Lean CI, now that #50 movedci.ymlandactions.locktolean-action@v1.6.2together) and CodeRabbit with no actionable comments.Rung 3 stays OPEN on 3d and 3f; no tag.
🤖 Generated with Claude Code
https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX