examples: Example 5 — database provenance (K-provenance semiring)#81
Merged
Conversation
Adds proofs/agda/EchoExampleProvenance.agda — formal Agda counterpart
to Example 5 from docs/echo-types/examples.md (previously
informal-only). A two-element Row source with payload + boolean
K-provenance annotation, projecting to payload-only; the lost prov
bit is exactly what Echo carries.
Headlines pinned in Smoke.agda:
- provenance-collapses (Σ-witness, project non-injective)
- echo-prov-true / echo-prov-false (concrete echo witnesses)
- echoes-distinguish-provenance ("Echo remembers what projection
forgot" — distinct prov on the carriers at same projected value)
- echo-prov-true≢echo-prov-false (echoes themselves separated)
- collapse-via-residue (tie-in to EchoResidue layer)
The shape mirrors Example 1 (square9 / SignedNine); the semantic
load shifts from "sign of a numerical preimage" to "origin
annotation of a database row".
Cluster context: Example 5 is in the presentation-dependence
cluster identified by PR #76 (alongside Examples 9, 10). This
slice lands the Agda half for Example 5; Examples 9 and 10 stay
informal per the PR-#76 verdict.
Invariants honoured: --safe --without-K; no postulates, no funext,
no escape pragmas; clean-worktree builds green for the new module,
All.agda, and Smoke.agda.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
force-pushed
the
examples/db-provenance
branch
from
1f9a064 to
89d4159
Compare
6 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
…#86) ## Summary Gate **F1** of the earn-back plan — the MAKE-OR-BREAK retraction from [R-2026-05-18](../blob/main/docs/retractions.adoc) — now passes. The 2026-05-18 spike `EchoGradedComonadF1.agda` had two of three graded-comonad laws closed (`gc-counit-l`, `gc-counit-r`) and named the remaining obstruction precisely: an isolated proof-engineering type-mismatch at the inductive step of `gc-coassoc`, requiring an explicit δ-naturality lemma over the outer `R` layer rather than the ad-hoc `coe-cong-R ∘ sym` push. This PR discharges that obligation: ```agda δ-suc : ∀ m n {A} (x : D (m + n) A) (b : Bool) → δ (suc m) n {A} (x , b) ≡ (δ m n x , b) δ-suc m n {A} x b = coe-cong-R (D-+ m n A) x b ``` This factor + the existing `subst-D-suc` let `gc-coassoc` close as a six-step `≡-Reasoning` chain. Stdlib's `+-assoc (suc m) n p` reduces *definitionally* to `cong suc (+-assoc m n p)`, so the two ℕ-equation proofs at the chain ends are syntactically identical and **ℕ-UIP is not needed for `gc-coassoc` itself** (`gc-counit-l` still uses ℕ-UIP, which is K-free via Hedberg / decidable equality). ## Mechanised content of F1 * Grade monoid `(ℕ, +, 0)`; `D 0 A = A`; `D (suc r) A = R (D r A)` where `R X = X × Bool` — a non-collapsing residue layer. * `mapD r f` functorial (`mapD-id`, `mapD-∘`). * `ε : D 0 A → A` — counit at the unit grade. * `δ : D (m + n) A → D m (D n A)` — **NESTED** comultiplication. * `gc-counit-r` (definitional), `gc-counit-l` (induction on grade), `gc-coassoc` (this PR). * `D2-nontrivial` — separating witness that `D r` is not `⊤` / a prop. * Echo is the grade-unit object: `D 0 (Echo f y) ≡ Echo f y`. `--safe --without-K`, **zero postulates**, zero escape pragmas, no funext. Wired into `All.agda` and pinned in `Smoke.agda`. ## Scope (please re-read with care) F1 earns back the **existence** of a graded comonad with Echo as the grade-unit object — that's the claim R-2026-05-18 retracted at its strongest reading. It does **NOT** retroactively make `EchoGraded` itself a graded comonad: `EchoGraded` remains a thin-poset reindexing modality on a three-element lattice, with no nested family, no monoid multiplication, no `D r r' ⇒ D r ∘ D r'`. The paper's title and central thesis (Echo as a reindexing modality) stand unchanged; F1 enters the codebase as an *additional* mechanised contribution beside `EchoGraded`. ## What this unblocks Gate **F3** — a genuinely independent second model of the comonad at a different grade monoid (e.g. tropical or multiplicative semiring), without a `× ⊤` carrier or a `⊑-prop`-equivalent field — is now in scope. F3 is **not** started by this PR. ## Doc changes (gated, scoped) * `docs/echo-types/earn-back-plan.adoc` — ledger row A1 + Status entry (F1 PASSED 2026-05-20), with the scope qualifier pinned. * `docs/retractions.adoc` — follow-up **F-2026-05-20a** appended (append-only revision policy preserved); no edits to other doc bodies. * `paper.adoc`, `types-abstract.adoc`, `conservativity.adoc` — **intentionally untouched** in this PR. Their bodies are about `EchoGraded`'s thin-poset structure, which F1 does not change. Whether to add a bounded new-contribution paragraph mentioning the F1 side-construction is **owner-gated**. ## Test plan * [x] `agda proofs/agda/All.agda` exit 0 under `--safe --without-K` * [x] `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K` * [x] `grep -nE '^\s*postulate\b|BUILTIN REWRITE|NON_TERMINATING|TERMINATING' proofs/agda/EchoGradedComonadF1.agda` returns no matches in code * [x] `--safe --without-K` OPTIONS line preserved on the F1 module * [ ] (owner) confirm the scope language in `retractions.adoc` F-2026-05-20a matches intent * [ ] (owner) decide whether `paper.adoc` / `types-abstract.adoc` / `conservativity.adoc` should gain a bounded contribution paragraph in a separate PR ## Non-overlap with parallel sessions Touches: `EchoGradedComonadF1.agda` (existing 2026-05-18 spike, finishing it), `All.agda` (one-line F1 import), `Smoke.agda` (F1 pin block), `earn-back-plan.adoc`, `retractions.adoc`. Stays clear of: * `proofs/agda/Ordinal/**` — the Brouwer-arithmetic / `_<ᵇ⁻_` / rank-mono session's territory. * Any module the recent estate PRs (#80 EchoSearch, #81 EchoExampleProvenance, #83 EchoExampleParser) added — restored their imports cleanly during the rebase onto fresh `origin/main`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
Third wave of the same merge regression pattern that the prior fix-up commits (8950855 for #83 EchoExampleParser, 549f219 for #80 EchoSearch) already addressed: between the last main-merge and now, PR #81 landed on main, adding EchoExampleProvenance.agda and its imports/pins. Resolution: keep this PR's EchoExampleAbsInt additions and add the EchoExampleProvenance additions from main alongside them (additive on both sides — no semantic conflict, both examples coexist). * proofs/agda/All.agda — both `open import EchoExampleAbsInt` and `open import EchoExampleProvenance` retained; EchoExamples (which the conflict block had duplicated) appears once. * proofs/agda/Smoke.agda — both the Example 10 (AbsInt) pin block and the Example 5 (Provenance) pin block retained, in that order. * proofs/agda/EchoExampleProvenance.agda — restored from main (new file on this branch). Build invariant restored: `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`. All examples added by parallel sessions (#80 EchoSearch, #81 EchoExampleProvenance, #83 EchoExampleParser, plus this PR #82 EchoExampleAbsInt) are wired in together. No postulates, no escape pragmas. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
…landed (#89) Updates the `Current rung state (2026-05-20)` block to record Wave 3 of today's swarm and refresh the next-Claude plan. ## What this captures * 5 Wave-3 PRs (`#80` EchoSearch, `#81` provenance, `#82` absint, `#83` parser, `#85` EchoCost) and 2 parallel-session merges (`#84` Pillar E Evaluation, `#86` F1 gc-coassoc). * Axis 8 is now 4-of-4 (decidability + graded access + cost + search). * Next-Claude plan refreshed: ordinal-track unbudgeted WF is the named next bottleneck; EchoApprox examples 6/8 still open; EchoSearch sequential/product composition deferred. ## Two minor lessons memorialised * Per-lane Smoke `open import ... using ( ... )` blocks should be separate (with header comments), not shared paren-blocks — cuts swarm merge-conflict noise. * During swarm-merge sequences, re-fetch the branch before any force-push: parallel claude sessions may be concurrently rebasing the same PR (observed on `#82`). ## Invariants * Doc-only change; no Agda touched. * `--safe --without-K` invariant unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
4 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
…luster landed (#92) ## Summary Three small accuracy passes through `docs/echo-types/` after the earn-back programme, the §"Theory work — no proof assistant needed" section, and the canonical examples cluster (5/9/10) all closed in this session. Pure prose; no Agda changes. ### 1. `roadmap.md` §"Theory work" — two stale items refreshed * **Axis 8** line said the *decidability-respecting* candidate had shipped but listed the other three as still candidate refinements. All four have now shipped: `EchoDecidable`, `EchoCost` (#85), `EchoAccess` (#68 / #75), `EchoSearch` (#80). Updated to credit all four. * **Negative / co-echoes** line was `[unblocked]`; now `[landed]` — `AntiEcho` (#69), tropical decomposition concrete + generic (#72 + #91), `antiecho-partition-dec` (#90). Names the `coecho.md` §5 obligation-5 / obligation-6 closures explicitly. After these edits, every item in §"Theory work — no proof assistant needed" is either `[landed]` or `[ruled out]`/`[refreshed]` — the section is genuinely closed. ### 2. `roadmap.md` §"Example work" — three items landed * ex. 5 (`EchoExampleProvenance`, #81) → `[landed]` * ex. 9 (`EchoExampleParser`, #83) → `[landed]` * ex. 10 (`EchoExampleAbsInt`, #82) → `[landed]` Only ex. 6 (approximate-echo numeric example) remains `[unblocked]`. ### 3. `earn-back-plan.adoc` — stale `roadmap-gates.adoc` claim corrected * Header note used to say "the gate discipline was historically attributed to a `roadmap-gates.adoc`; that file does not exist in-tree". The file **does** exist (created 2026-05-18; see its preamble). Header rewritten to list `roadmap-gates.adoc` alongside `retractions.adoc` / this plan / `next-questions.adoc` as the four canonical loci. * Ledger row D (the "doesn't exist" entry) marked **CLOSED 2026-05-20** with the cite reflecting current reality. ## Test plan * [x] Pure docs / `.adoc` / `.md` edits — no Agda touched * [x] `agda proofs/agda/All.agda` exit 0 (confirms docs match code) * [x] `agda proofs/agda/Smoke.agda` exit 0 * [x] No retracted-claim language moved; no earned-back claim overclaimed; `paper.adoc` / `types-abstract.adoc` / `conservativity.adoc` untouched ## Scope Disjoint from all currently-open PRs: * #88 (F3) — touches Agda + `retractions.adoc` (different sections) + `earn-back-plan.adoc` Status (different section from header / ledger-D) * #90 (partition-dec) — touches Agda only * #91 (generic-codomain) — touches Agda + preamble comments No retracted claim is moved. No earned-back claim is overclaimed. `paper.adoc` / `types-abstract.adoc` / `conservativity.adoc` are intentionally untouched (owner-gated, per the posture set by #86 / #88). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds
proofs/agda/EchoExampleProvenance.agda— Example 5 from thepresentation-dependence cluster identified by PR #76.
What lands
Rowwith payload (ℕ) + K-provenance Bool annotationproject : Row → ℕ(forgets provenance) — the Echo signalSmoke.agda:provenance-collapses— Σ-witness that projection is non-injectiveecho-prov-true/echo-prov-false— concrete echo witnessesechoes-distinguish-provenance— distinct prov on carriers at thesame projected value ("Echo remembers what projection forgot")
echo-prov-true≢echo-prov-false— the two echoes themselves areconstructively separated
collapse-via-residue— optional tie-in to theEchoResiduelayerAll.agdaalphabetically (beforeEchoExamples)Cluster relationship
Example 5 is the canonical motivating example for "what does Echo
carry?" — the shape is the same as Example 1 (
square9 / SignedNinein
EchoExamples.agda), with provenance semantics making thecarried data load-bearing in the database setting. Module header has
a 4–6 line comment making the analogy explicit.
This slice lands the Agda half for Example 5 specifically; Examples
9 and 10 stay informal per PR #76's §5 "meta-pattern only — no new
Agda module needed" verdict for the cluster as a whole. (One
formalisation does not change that verdict — the cluster still
doesn't motivate a new axis; this is just upgrading the one entry
whose Σ-shape is small enough to ship as a thin slice.)
Invariants
--safe --without-K; no postulates, no funext, no escape pragmasEchoExamples.agdamodifications (new module is cleaner; lanes 4 and 5 also avoid it)All.agda, andSmoke.agda(all exit 0)Refs #76 (presentation-dependence cluster decision).
🤖 Generated with Claude Code
Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com