diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 03ed992..15d1361 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -53,16 +53,23 @@ jobs: run: | set -euo pipefail fail=0 - for f in verification/proofs/lean4/grade-boundary/GradeBoundary.lean \ - verification/proofs/lean4/grade-factorisation/GradeFactorisation.lean; do + # Every Lean source, not only the two v0.1 files: the ratified-carrier + # results (GradeRatified, L4Monotonicity, TierTwoComplete, EffectAtoms, + # GradeFactorisationR) are what the current spec cites. + for f in $(git ls-files 'verification/proofs/lean4/*.lean' 'verification/proofs/lean4/*/*.lean'); do if [ ! -f "$f" ]; then echo "::error::gated file is missing: $f"; fail=1; continue fi echo "--- gating $f ---" - if grep -nE '(:=|by|;|<;>|=>|\|)[[:space:]]*(sorry|admit)\b|\bnative_decide\b' "$f"; then + # Comment-aware and token-based: strip -- and /- -/ comments first + # (tests/lib/strip-proof-comments.awk; line numbers preserved), then match + # the bare tokens, so `:= by` with an indented `sorry` on the NEXT line is + # caught while the honest "sorry-free" prose in comments is not. + stripped=$(awk -f tests/lib/strip-proof-comments.awk "$f") + if grep -nE '(^|[^[:alnum:]_.])(sorry|admit)([^[:alnum:]_]|$)|\bnative_decide\b' <<<"$stripped"; then echo "::error file=$f::forbidden Lean tactic (sorry/admit/native_decide)"; fail=1 fi - if grep -nE '^[[:space:]]*axiom\b' "$f"; then + if grep -nE '^[[:space:]]*axiom\b' <<<"$stripped"; then echo "::error file=$f::user axiom declared"; fail=1 fi done @@ -73,41 +80,49 @@ jobs: # so this is a real check of postulate-freedom and not a word-grep (a grep would # false-positive on the honest "postulate-free" prose in the comments). # - # NOTE ON THE VERSION PIN: theorem-b.agda-lib is developed against Agda 2.8.0 - # (ADR 0003). The runner's packaged Agda is older. The version is printed, not - # asserted, because asserting a version the runner cannot supply produces a - # permanently-red gate rather than a signal — and the substantive guarantee here - # comes from --safe --without-K, which holds across versions. Verified locally - # under 2.6.4.3: All.agda and Smoke.agda both typecheck, exit 0. + # TOOLCHAIN: pinned release artefacts, not the runner's apt. ubuntu-latest is + # 24.04, whose agda-stdlib is 1.7.3; Theorem B imports Data.Product.Base, which + # exists from stdlib 2.0, so `apt-get install agda agda-stdlib` there fails at + # scope checking (exit 42) — reproduced 2026-10-13. The job now fetches the + # Agda 2.7.0.1 release binary and the stdlib v2.0 source archive, verifies + # both SHA-256 sums, and registers the stdlib under the name the .agda-lib + # depends on. Verified 2026-10-13 with exactly these artefacts: All.agda and + # Smoke.agda typecheck under --safe --without-K, exit 0 (~100 s). A checksum + # mismatch fails loudly rather than silently testing a different stdlib. agda-theorem-b: name: "Agda Theorem B (--safe --without-K)" runs-on: ubuntu-latest timeout-minutes: 30 steps: - uses: actions/checkout@v7.0.1 - - name: Install Agda and register the standard library + - name: Install Agda 2.7.0.1 and agda-stdlib 2.0 (pinned, checksummed) shell: bash + env: + AGDA_URL: https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz + AGDA_SHA256: 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a + STDLIB_URL: https://github.com/agda/agda-stdlib/archive/refs/tags/v2.0.tar.gz + STDLIB_SHA256: 14eecb83d62495f701e1eb03ffba59a2f767491f728a8ab8c8bb9243331399d8 run: | set -euo pipefail - sudo apt-get update -qq - sudo apt-get install -y -qq --no-install-recommends agda agda-stdlib - echo "agda --version -> $(agda --version | head -1)" - echo "ratified pin (ADR 0003) is Agda 2.8.0; --safe --without-K is the substantive check" - - # Installing the package is not enough: Agda only sees a library that is - # listed in its `libraries` file, and a fresh runner has none. WHICH path - # that file lives at is VERSION-DEPENDENT (~/.agda vs ~/.config/agda), so - # point AGDA_DIR at a directory we control rather than guessing, and - # resolve the .agda-lib from the package rather than hardcoding it. - lib="$(dpkg -L agda-stdlib | grep -m1 'standard-library\.agda-lib$' || true)" - if [ -z "$lib" ]; then - echo "::error::agda-stdlib is installed but standard-library.agda-lib was not found" - exit 1 - fi - mkdir -p "${RUNNER_TEMP}/agda" - echo "$lib" > "${RUNNER_TEMP}/agda/libraries" - echo "AGDA_DIR=${RUNNER_TEMP}/agda" >> "$GITHUB_ENV" - echo "registered standard-library at: $lib" + mkdir -p "${RUNNER_TEMP}/agda-toolchain" && cd "${RUNNER_TEMP}/agda-toolchain" + curl -sSL -o agda.tar.xz "$AGDA_URL" + echo "$AGDA_SHA256 agda.tar.xz" | sha256sum -c - + curl -sSL -o stdlib.tar.gz "$STDLIB_URL" + echo "$STDLIB_SHA256 stdlib.tar.gz" | sha256sum -c - + tar -xJf agda.tar.xz && tar -xzf stdlib.tar.gz + # theorem-b.agda-lib depends on `standard-library`; the 2.0 archive names + # itself `standard-library-2.0`, so register a lib file under the depended-on name. + printf 'name: standard-library\ninclude: src\nflags:\n --warning=noUnsupportedIndexedMatch\n' \ + > agda-stdlib-2.0/standard-library.agda-lib + mkdir -p "${RUNNER_TEMP}/agda-dir" + echo "$PWD/agda-stdlib-2.0/standard-library.agda-lib" > "${RUNNER_TEMP}/agda-dir/libraries" + { + echo "AGDA_DIR=${RUNNER_TEMP}/agda-dir" + echo "Agda_datadir=$PWD/Agda-v2.7.0.1/data" + echo "LC_ALL=C.UTF-8" + } >> "$GITHUB_ENV" + echo "$PWD/Agda-v2.7.0.1/bin" >> "$GITHUB_PATH" + "$PWD/Agda-v2.7.0.1/bin/agda" --version - name: Typecheck Theorem B shell: bash working-directory: verification/proofs/agda/theorem-b diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 153f531..2afafcc 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -2,7 +2,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-License-Identifier: CC-BY-SA-4.0 = AFFIRMATION — trope-checker -:revdate: 2026-06-24 +:revdate: 2026-10-27 A dated, ground-truthed honesty snapshot (the README/EXPLAINME/AFFIRMATION trio). This is the brief's "STATUS" deliverable: what is proved, what is stubbed-and-named, @@ -78,3 +78,64 @@ Documentation gaps OPEN-B/B′ (`Falsified`/`Misbound` absent from v0.1 §3.1/§ proved-vs-missing picture: `verification/proofs/INTEGRATION-REPORT.adoc`. — Authored by the build agent under owner direction; signed in git history. + +== As of 2026-10-27 — Phase 0 re-run on the ratified world + +*Anchor.* Branch `claude/new-session-snuoro` at `444e4cf` (`main` 216f23b + the v0.2 +consolidation + the `proofs.yml` pin), 2026-10-27T07:56Z, in an Ubuntu 24.04 cloud +container. Toolchain: Agda 2.7.0.1 + agda-stdlib 2.0 (tag `v2.0`, commit `2b8fff1`); +Idris2 0.8.0 (built from tag `v0.8.0` on Chez Scheme 9.5.8); rustc 1.97.0; just 1.40.0. + +*Ground truth (commands run here):* + +* `idris2 --typecheck verification/proofs/idris2/trope.ipkg` → exit 0; 8 modules, all + `%default total`; no `believe_me` / `assert_total` / `postulate` in + `verification/proofs/idris2` or `src/idris2`. +* `just trope-build && bash tests/conformance/run.sh` → the reference `tropecheck` + builds; *13* verdict cases pass with the expected witness edge and coordinate; *9* + schema-invalid documents are rejected at the named slot; "conformance: all pass". +* `just trope-rust` → `tropecheck-rs` builds; the same 13 + 9 pass — the Rust fast core + and the Idris2 reference agree over the whole corpus. +* `just build-agda` → `agda --safe --without-K All.agda` and `Smoke.agda` exit 0 + (77 s and 5 s cold; 12 s together with cached interfaces). +* `just build-lean` → *NOT RUN here*: `lake` is not installed and the Lean toolchain + and Mathlib cache hosts were unreachable from this container. The + `lean-source-honesty` regexes of `proofs.yml` were run by hand over all 8 tracked + `.lean` files: no `sorry` / `admit` / `native_decide`, no user `axiom`. On this + branch the `proofs.yml` `lean-build` job (run 40472568287, 2026-10-27T08:18Z) built + both packages — `lake build` "Build completed successfully", one axiom line per + theorem — and then failed in lean-action's optional `nanoda` step (its lean4export + does not compile under the v4.16.0 toolchain), exactly as on `main`; that step, not + the build, is why the job is red. + +*Proved* (machine-checked; names in `docs/status/PROOF-STATUS.adoc`): L1–L6 on the +ratified carrier, L4 in full (`fateL4MonoR/L`, `bondComposeMono`, `mergeComposeMono`); +the decidable retention preorder; the Veridicality Derivation and Honest Generation; +C1–C3 (`GradeR.conical`, `gradeR_leftCancel_iff`, `TierTwoComplete`, +`fate-tier-meet-hom-fails`); O1-carrier (`atom_factorization`, stated on the v0.1 `Grade` — finding 4); the sighted tropical +factorisation (`piR_sighted`); Theorem B Targets 1, 2, 4 and the β/let case of 3 +(`cut-preserves-grade`, `β-app`, `β-let`); grade soundness for exact lowering, +T-Sub and verdict soundness (`soundFromExact`, `subSound`, `verdictSound`). *Open* +(`spec/calculus.adoc §10`): CO-1 mechanisation (the `fix` case; designed, not +mechanised), O1-coord, O2, O3, O5 mechanisation, O6. + +*Four findings.* (1) Ubuntu 24.04's apt pair (Agda 2.6.3, agda-stdlib 1.7.3) cannot +typecheck Theorem B: `agda --safe --without-K All.agda` exits 42, `Data.Product.Base` +not found — stdlib ≥ 2.0 is required, which is why `proofs.yml` now pins Agda 2.7.0.1 ++ stdlib 2.0 by checksum (reproduced here, 58 s). (2) The 2026-06-22 entry's "10/10" +and "8 schema-invalid" were stale: the corpus is 13 + 9. Also observed: `just +proof-check-all` is red for reasons that predate this pass (per-file `idris2 --check` +and `agda --safe` from the repo root cannot resolve module names; the ABI/Types Idris2 +mint templates do not typecheck) — recorded as an issue, not fixed here; the gates +that mean something are `just check`, `just build-agda`, `just trope-rust` and +`verify-all`. (3) The CI axiom audit shows `Trope.nine_families` (`EffectAtoms.lean`), +`FateA.Q_add_left_cancel` and `FateA.atten_cancel_on_normalForms` (`GradeRatified.lean`) +depend on `Classical.choice` as well as `propext`/`Quot.sound`; the "`propext`/`Quot.sound` +only" wording in spec §9.3, PROOF-STATUS and the proofs README overclaimed and now reads +"no `sorryAx`, no user axiom". `GradeBoundary.lean`'s own footer had said so all along. (4) `EffectAtoms.lean` imports +`GradeBoundary`, so the atom factorisation cited for O1-carrier is a theorem about the +v0.1 `Grade`; no `GradeR` restatement exists. The factorisation is componentwise and +should transfer, but that is an argument, not a proof — recorded in PROOF-STATUS (Open) +and left for the owner where `spec/calculus.adoc §6/§10` cite it as ratified-carrier. + +— Run by the Phase 0 agent; the owner signs on landing. diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 9623b93..35758e8 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -10,6 +10,26 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. ==== Changed +* *Spec v0.2 consolidation (2026-10-13).* `+docs(spec)+`: consolidate the calculus +at v0.2 — nine effects with the atom table, ratified carrier inline (A1–A3), L6 +commutativity and the cancellation structure as laws, the tropical factorisation +recorded as sighted, §7 restated as greatest post-fixed point with T-Fix-Decl, O5 +defined and O6 (ceiling verdict) opened, prover roles per ADR 0005. +`+spec/calculus-v0.2-draft.adoc+` folded in and removed; README and +INTEGRATION-REPORT aligned. +* *Phase 0 — status surfaces made true (2026-10-27).* +`+docs/status/PROOF-STATUS.adoc+` rewritten to the ratified carrier (one proved +table citing only existing lemma names; open list = spec §10; history collapsed); +`+docs/status/ROADMAP.adoc+` ships v0.2; `+AFFIRMATION.adoc+` gains a 2026-10-27 +entry from re-run checks (13 + 9 conformance on both checkers, Agda green, Lean +NOT RUN in that session); the `+fix+` footer of +`+verification/proofs/agda/theorem-b/TB/Reduction.agda+` names the designed CO-1 +model and records O4 as resolved. +* *`+proofs.yml+`* pins Agda 2.7.0.1 + agda-stdlib 2.0 by SHA-256 (the runner's apt +pair fails at `+Data.Product.Base+`); the Lean honesty gate and `+verify-all+` cover +every tracked `+.lean+` file and are comment-aware and token-based (a `+sorry+` on the +line after `+:= by+` is caught; "sorry-free" prose in comments is not). + * *IR 0.2 — A3 `+Attenuated(0)+` ingest normalization (R-2026-07-07-03, ADR 0004, #28).* Both checkers (Idris2 reference, Rust fast-core) rewrite `+Attenuated(0)+` to `+Present+` at the IR ingest boundary, @@ -25,6 +45,12 @@ fault. New conformance fixtures prove `+Atten(0)+` ≡ `+Present+` ==== Added +* *ADR 0005* (`+docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc+`, +Proposed): spec v0.2 normative; O5 adopted from the workbench proposal of +2026-07-17; O6 opened; prover roles (Agda kernel, Idris2 reference, Lean +provenance, Rust fast core); templates removed; the carrier-as-parameter question +(D6) recorded, not decided. + * *Grade-algebra ground truth (Lean 4 + Mathlib).* `+verification/proofs/lean4/grade-boundary/+`: a sorry-free, axiom-clean (`+propext+`/`+Quot.sound+` only) formalisation of the honest/deceptive @@ -75,3 +101,11 @@ prose. central open problem. * `+.gitignore+` now excludes `+.lake/+` (Lean build artifacts + vendored Mathlib clones). + +==== Removed + +* The never-instantiated prover templates `+verification/proofs/coq/TypeSafety.v+`, +`+verification/proofs/tlaplus/StateMachine.tla+` and +`+verification/proofs/agda/Properties.agda+`, with their tree and recipe references +(`+proof-check-all+` no longer runs the Coq recipe; `+proof-status+` reports three +provers). diff --git a/Justfile b/Justfile index 7a7f3fe..5b3c659 100644 --- a/Justfile +++ b/Justfile @@ -140,15 +140,9 @@ test-smoke: @echo "Smoke test..." # TODO: Add basic sanity checks -# Run end-to-end tests (full pipeline: build → run → verify) +# Run end-to-end conformance tests (build first with `just trope-build`). e2e: - @echo "Running E2E tests..." - # TODO: Replace with your E2E test command. Examples: - # bash tests/e2e.sh # Shell-based E2E - # npx playwright test # Browser E2E - # mix test test/integration/e2e_test.exs # Elixir E2E - # cargo test --test end_to_end # Rust E2E - @echo "E2E tests passed!" + bash tests/e2e.sh # Run aspect tests (cross-cutting concern validation) aspect: diff --git a/README.adoc b/README.adoc index d1d8967..c618248 100644 --- a/README.adoc +++ b/README.adoc @@ -45,8 +45,10 @@ an existing language could emit the same IR and be checked by the same checker. (calculus O2), discharged per front-end, not here. . *Veridicality is declared and propagated, not checked.* Detecting that a value claimed faithful is in fact false needs a ground-truth oracle the checker does - not have (calculus O5). The checker guarantees only that deception does not - compose away and that deceptive grades fail every honest floor. + not have — and cannot have: veridicality is undecidable relative to the IR + (calculus §10-O5, Remark O5-a). The checker guarantees only that deception does + not compose away and that deceptive grades fail every honest floor; a deployment + MAY bind an external oracle under the O5-1..3 conditions. == Deploy variant: prevent (R-2026-06-22) @@ -62,8 +64,7 @@ rejects them at validation, naming the offending coordinate. The alternative [cols="1,3",options="header"] |=== | Path | What lives there -| `spec/calculus.adoc` | The normative calculus (source of truth, `:revnumber: 0.1`). -| `spec/calculus-v0.2-draft.adoc` | v0.2 *draft addendum*: the proved grade-algebra obligations `R-2026-06-23-01..04` (non-commutative product monoid; conicality; three-tier cancellation boundary; `Dropped`/`Total` honest). Does not edit v0.1. +| `spec/calculus.adoc` | The normative calculus (source of truth, `:revnumber: 0.2` — consolidated 2026-10-13: ratified carrier, nine effects, O5 defined, O6 opened). | `spec/trope-ir.adoc` | The normative IR spec: nodes, edges, grade algebra, verdict. | `schemas/trope-ir.schema.json` | The Trope IR JSON Schema — the trust boundary (prevent profile). | `src/idris2/` | The executable checker (Idris2): JSON parser + IR decoder + checker, reusing the verified core; plus `Main` → the `tropecheck` binary. @@ -142,15 +143,23 @@ https://github.com/hyperpolymath/trope-checker/tree/8f58d2409227b065fed01a898c02 == Status -Alpha. The schema, executable checker, and conformance suite are green; the -verified core typechecks with no axioms behind its claimed lemmas. The grade-algebra -*honest/deceptive cancellation boundary* is now proved in Lean (sorry-free, -axiom-clean) and its metatheory developed in Agda (Theorem B). Grade soundness (the -full `g ⊑ ρ` theorem) and the *operational model for `fix`/routing* (the central open -problem, CO-1, gated by O4) remain the named open problems in -`docs/status/PROOF-STATUS.adoc`; see `verification/proofs/INTEGRATION-REPORT.adoc` for -the full proved-vs-missing picture. A Rust fast-core is drafted in `src/rust/` -(dep-free, validated against the Idris2 reference via the conformance corpus). +Alpha. The IR schema, the executable checker and the conformance suite are green, +and the verified developments carry no `sorryAx` and no user axiom behind their +claimed lemmas (the Lean results rest on the standard library's `propext`/`Quot.sound`, +and `Classical.choice` in three theorems). On the ratified carrier (ADR 0004, R-2026-07-07) the grade algebra is a commutative +monoid with the three deceptive bottoms as two-sided zeros; L1–L6, conicality, the +cancellation boundary (left-cancellative iff ε), the Honest Generation and +Veridicality theorems, the atom factorisation (O1's carrier half — stated on the v0.1 `Grade`, +not yet restated on `GradeR`) and a veridicality-sighted tropical factorisation are proved across Agda, Idris2 and +Lean; Theorem B gives grade-exact substitution and β/let subject reduction. The +named open problems are *CO-1* — the operational model for `fix` is designed +(`spec/notes/2026-07-07-co1-operational-model.adoc`) and awaits mechanisation, +which is what stands between the exact-lowering soundness already proved and +full grade soundness — plus O2 (per producer), O3, O5's mechanisation, O6 and +O1-coord, all listed in `spec/calculus.adoc §10` with their status. Ground truth: +`AFFIRMATION.adoc`; the proved-vs-open table: `docs/status/PROOF-STATUS.adoc`. The +Rust fast core in `src/rust/` (dependency-free) agrees with the Idris2 reference +over the conformance corpus. == Licence diff --git a/build/just/proofs.just b/build/just/proofs.just index 6850a3f..03eb33b 100644 --- a/build/just/proofs.just +++ b/build/just/proofs.just @@ -4,12 +4,12 @@ # FORMAL VERIFICATION (PROOFS) # # Imported by ../../Justfile via `import? "build/just/proofs.just"`. -# Recipes here check formal proofs across Idris2, Lean4, Agda, and Coq, plus +# Recipes here check formal proofs across Idris2, Lean4 and Agda, plus # scan for dangerous/unsafe constructs and report status. Run via # `just proof-check-all` for the full sweep. -# Check all formal proofs (Idris2 + Lean4 + Agda + Coq) -proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous +# Check all formal proofs (Idris2 + Lean4 + Agda) +proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-scan-dangerous @echo "=== All proof checks complete ===" # Check Idris2 proofs (ABI, types, dependent type proofs) @@ -150,8 +150,6 @@ proof-status: echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null | wc -l) files" echo "Lean4: $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null | wc -l) files" echo "Agda: $(find verification/proofs/agda -name '*.agda' 2>/dev/null | wc -l) files" - echo "Coq: $(find verification/proofs/coq -name '*.v' 2>/dev/null | wc -l) files" - echo "TLA+: $(find verification/proofs/tlaplus -name '*.tla' 2>/dev/null | wc -l) files" echo "" # PROOF-STATUS may live at root, docs/status/ (post-#20), .md or .adoc (post-#23) for candidate in docs/status/PROOF-STATUS.adoc docs/status/PROOF-STATUS.md PROOF-STATUS.adoc PROOF-STATUS.md; do @@ -191,6 +189,8 @@ build-agda: #!/usr/bin/env bash set -euo pipefail echo "=== build-agda: Theorem B metatheory (--safe --without-K) ===" + # Needs Agda >= 2.6.4 and agda-stdlib >= 2.0 (Data.Product.Base); the CI job + # pins Agda 2.7.0.1 + stdlib 2.0 by checksum — see proofs.yml agda-theorem-b. cd verification/proofs/agda/theorem-b agda --safe --without-K All.agda agda --safe --without-K Smoke.agda @@ -204,12 +204,14 @@ verify-all: build-lean build-agda #!/usr/bin/env bash set -euo pipefail echo "=== verify-all: Lean source honesty gate ===" - for f in verification/proofs/lean4/grade-boundary/GradeBoundary.lean \ - verification/proofs/lean4/grade-factorisation/GradeFactorisation.lean; do + # Every Lean source (mirrors proofs.yml lean-source-honesty; keep the two in step). + for f in $(git ls-files 'verification/proofs/lean4/*.lean' 'verification/proofs/lean4/*/*.lean'); do echo "--- gating $f ---" - if grep -nE '(:=|by|;|<;>|=>|\|)[[:space:]]*(sorry|admit)\b|\bnative_decide\b' "$f"; then + # Comment-aware, token-based (mirrors proofs.yml; keep the two in step). + stripped=$(awk -f tests/lib/strip-proof-comments.awk "$f") + if grep -nE '(^|[^[:alnum:]_.])(sorry|admit)([^[:alnum:]_]|$)|\bnative_decide\b' <<<"$stripped"; then echo "FAIL: forbidden Lean tactic (sorry/admit/native_decide) in $f"; exit 1; fi - if grep -nE '^[[:space:]]*axiom\b' "$f"; then + if grep -nE '^[[:space:]]*axiom\b' <<<"$stripped"; then echo "FAIL: user axiom declared in $f"; exit 1; fi done echo "PASS: verify-all — Lean green & axiom-clean (propext/Quot.sound only); Agda --safe --without-K green." diff --git a/docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc b/docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc new file mode 100644 index 0000000..9b58d5d --- /dev/null +++ b/docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc @@ -0,0 +1,118 @@ +// SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +// SPDX-License-Identifier: CC-BY-SA-4.0 += ADR 0005 — Spec v0.2 consolidation, O5 adopted, O6 opened, prover roles, template removal; the carrier-as-parameter question recorded +:revdate: 2026-10-27 + +== Status + +*Proposed — owner to accept.* Drafted in the Phase 0 pass ("make the status +surfaces true"); the spec consolidation it ratifies landed as +`docs(spec): consolidate the calculus at v0.2` (2026-10-13). Nothing here changes +a semantics; D6 is recorded, not decided. + +== Context + +After ADR 0004 (R-2026-07-07) the normative text was split across four +documents written against two different carriers: `spec/calculus.adoc` v0.1 +(2026-06-22) with the ratification spliced in as notes, the never-merged +addendum `spec/calculus-v0.2-draft.adoc` (2026-06-23), and the two design notes +of 2026-07-07 (the L4 boundary and atoms; the CO-1 operational model). The spec +still said "seven effects" while the vocabulary, `EffectAtoms.lean` and the IR +said nine. The third firewall ("veridicality is declared and propagated, not +checked") cited an obligation O5 that §10 never defined; the workbench proposed +the missing entry on 2026-07-17 +(`trope-particularity-workbench/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc`). +T-Sub's one-sidedness means the verdict certifies sufficiency only, which the +privacy direction (a ceiling on retention) cannot use. The estate's proof-kernel +ruling of 2026-10-12 fixed the role of each prover across repositories, and this +repo still described itself as a "four-prover" stack and carried three +never-instantiated Coq / TLA+ / Agda templates from the repository mint. + +== Decisions + +[cols="1,3",options="header"] +|=== +| ID | Decision + +| *D1 (one normative document)* | `spec/calculus.adoc` v0.2 (the consolidation +of 2026-10-13) is the normative text. The addendum is folded in and removed; the +two 2026-07-07 notes and `verification/proofs/INTEGRATION-REPORT.adoc` are +history and analysis, cited from the spec where they carry the argument, never +the other way round. Where any older status surface disagrees with the spec, the +spec wins. + +| *D2 (O5 adopted)* | §10 gains O5, the veridicality oracle, adopted from the +workbench proposal of 2026-07-17 unchanged in substance: Remark O5-a +(IR-relative undecidability of veridicality), the oracle interface with O5-1 +soundness, O5-2 attestation and O5-3 no-laundering, the falsifier, and the +upgrade path (mechanise O5-1 as a side condition on an `Oracle`-indexed verdict +judgement). Status in §10: DEFINED; mechanisation OPEN. Vocarium's warrants are +O5-2 attestations; Hermeneia's _licensed_ band is where O5-backed claims sit. + +| *D3 (O6 opened)* | §10 gains O6, the ceiling verdict: the dual theorem +stem:[\rho \sqsubseteq g_{\mathrm{ceiling}}] that a "no more than this may be +retained" use-model needs, which T-Sub's downward-only weakening does not give for +conservative lowering. Deliverable: the dual verdict proved for the exact-lowering +fragment and stated as unavailable for the conservative one, or a second, +upper-bound grade on edges. Status: OPEN. + +| *D4 (prover roles)* | The estate kernel ruling of 2026-10-12 applied here +(§9.3): *Agda* is the normative kernel (Theorem B; CO-1 mechanisation targets it); +*Idris2* is the executable reference (the verified core and the reference +`tropecheck`); *Lean 4 + Mathlib* is provenance (the grade-algebra boundary, the +atom and tropical factorisations, kept with their axiom audits); *Rust* is the +fast core, validated against the reference over the conformance corpus. +Consequence: `docs/status/PROOF-STATUS.adoc` leads with Agda, and new +metatheory goes to Agda unless an ADR says otherwise. + +| *D5 (three provers; templates removed)* | `verification/proofs/coq/TypeSafety.v`, +`verification/proofs/tlaplus/StateMachine.tla` and +`verification/proofs/agda/Properties.agda` — mint templates whose own text says +"Replace with your project's …", never instantiated — are removed, with their +tree and recipe references. The repository describes itself as three provers +(Agda, Idris2, Lean) plus a Rust fast core. + +| *D6 (recorded, not decided)* | Whether the fidelity carrier should be a +*parameter* — any resource algebra with two adjoined tops, instantiated from +`hyperpolymath/resource-algebra` — rather than the one instance +stem:[\mathbb{N}\cup\{\infty,\top\}]. This would answer the "uncalibrated +ordinal arithmetic" objection (the finite part of the carrier adds losses whose +unit is unstated) by making the unit the instance's business. O4 is RESOLVED for +the instance (ADR 0004); the parameterisation is Phase 1A work and is *not* +decided by this ADR. +|=== + +== Consequences + +* One place to read the calculus; "nine effects" throughout, reconciled with + "seven" as nine atom families of which six are writable and three are faults. +* The third firewall now cites a defined obligation. O5 is dischargeable in + principle (mechanise O5-1) and refutable (its falsifier is stated). +* The privacy direction has a named obligation (O6) instead of an unstated gap; + the verdict's one-sidedness is written down as a limitation, not hidden. +* Status surfaces (`PROOF-STATUS`, `ROADMAP`, `AFFIRMATION`, the Agda `fix` + footer) are rewritten to the ratified world in the same pass; the Lean + honesty gate and `verify-all` cover every tracked Lean source. +* `just proof-check-all` no longer invokes the Coq recipe; `just proof-status` + reports three provers. The historical mention of the templates in + `INTEGRATION-REPORT.adoc` stays as the record of what was there. +* D6 leaves the carrier an instance; downstream (vocarium, hermeneia) may keep + reading `Attenuated(δ)` with stem:[\delta \in \mathbb{N}]. + +== Rejected alternatives + +* *Keep the addendum as a separate v0.2 document* — rejected: two normative + texts on two carriers is how readers and agents kept landing in the + pre-ratification world. +* *"Four-prover" wording, Rust as a prover* — rejected: the fast core proves + nothing; it is validated against the reference. Naming it a prover overclaims. +* *Keep the Coq / TLA+ / Agda templates as future placeholders* — rejected: they + were never instantiated, each advertises a prover the roles ruling does not + assign here, and `proof-check-coq` skipping silently is a gate that cannot fail. +* *Decide D6 now (make the carrier a parameter in this pass)* — rejected: it + changes the carrier every proof development is stated over; it belongs to + Phase 1A with `resource-algebra` as the instance supplier, after CO-1 + mechanisation lands on the fixed instance. +* *Leave O5 as the workbench proposal* — rejected: an obligation cited by the + checker's firewalls must live in the checker's spec, not in a proposal + downstream cannot cite as normative. diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 11f5cc7..0386936 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -60,14 +60,14 @@ These proofs come from the rsr-template-repo and MUST be present in every repo: |=== | # | Proof Needed | Category | Prover | Priority | File(s) -| DOM-1 | Grade-algebra honest/deceptive cancellation boundary (non-commutative product monoid; full-carrier conicality; three-tier strict boundary, cancellation only on the finite-fidelity core) | DOM/ALG | Lean 4 | T1 | `verification/proofs/lean4/grade-boundary/GradeBoundary.lean` — *PROVED* (sorry-free; `propext`/`Quot.sound` only) -| DOM-2 | Theorem B Target 1 — intrinsic graded calculus over the non-commutative `▷` | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/{Grade,Syntax,Order}.agda` — *PROVED* -| DOM-3 | Theorem B Target 2 — grade-exact value substitution ("tropes follow values through cut"); symmetric cut impossible | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/Substitution.agda` — *PROVED (+ refutation)* +| DOM-1 | Grade-algebra honest/deceptive cancellation boundary (full-carrier conicality; three-tier strict boundary, cancellation only on the finite-fidelity core; the v0.1 carrier's non-commutativity is historical — the ratified carrier is commutative, L6) | DOM/ALG | Lean 4 | T1 | `verification/proofs/lean4/grade-boundary/GradeBoundary.lean` (v0.1 carrier) and `GradeRatified.lean` (ratified mirror) — *PROVED* (sorry-free; no user axiom) +| DOM-2 | Theorem B Target 1 — intrinsic graded calculus over `▷` | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/{Grade,Syntax,Order}.agda` — *PROVED* +| DOM-3 | Theorem B Target 2 — grade-exact value substitution ("tropes follow values through cut"); on the ratified carrier the cut is symmetric (`cut-grade-comm`, L6) — the v0.1 refutation `cut-symmetric-fails` is historical, retired with (A1) | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/Substitution.agda` — *PROVED* (refutation historical) | DOM-4 | Theorem B Target 3 — subject reduction respecting the three-tier boundary | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/{Reduction,Tier}.agda` — *PARTIAL* (β/let proved; `fix`/lfp NOT-REACHED, blocked on CO-1) | DOM-5 | Theorem B Target 4 — Honest Generation (HC-3): honesty closed under `▷`, deceptive grades unreachable | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/Honest.agda` — *PROVED* -| DOM-6 | CO-1 — operational model for `fix`/routing (gated by O4); enables full subject reduction | DOM | — | T2 | named in `docs/status/PROOF-STATUS.adoc` — *OPEN, not attempted* -| DOM-7 | Grade soundness for conservative lowering over fate (needs lax L4; strict L4 proved to fail) | ALG | — | T2 | named in `docs/status/PROOF-STATUS.adoc` — *OPEN* -| DOM-8 | Tropical factorisation precondition — the grade admits a *nontrivial* monoid homomorphism onto the *commutative* fidelity carrier `Δ`, and *every* such map is forced to identify honest `dropped` with deceptive `falsified` (the commutative cost-quotient is *veridicality-blind* on the fate axis; bond/merge deception stays separable) | DOM/ALG | Lean 4 | T1 | `verification/proofs/lean4/grade-factorisation/GradeFactorisation.lean` — *PROVED* (verdict B; sorry-free; `propext`/`Quot.sound` only; four theorems axiom-free). *Precondition only* — does not address CO-1. +| DOM-6 | CO-1 — operational model for `fix`/routing; enables full subject reduction | DOM | Agda | T2 | DESIGNED in `spec/notes/2026-07-07-co1-operational-model.adoc` (O4 resolved by ADR 0004); mechanisation — *OPEN* +| DOM-7 | Grade soundness for conservative lowering over fate (L4 holds in full on the ratified carrier; needs the CO-1 mechanisation) | ALG | Agda | T2 | named in `docs/status/PROOF-STATUS.adoc` — *OPEN* +| DOM-8 | Tropical factorisation precondition — the grade admits a *nontrivial* monoid homomorphism onto the *commutative* fidelity carrier `Δ`, and *every* such map is forced to identify honest `dropped` with deceptive `falsified` (the commutative cost-quotient is *veridicality-blind* on the fate axis; bond/merge deception stays separable) | DOM/ALG | Lean 4 | T1 | `verification/proofs/lean4/grade-factorisation/GradeFactorisation.lean` — *PROVED* (verdict B on the v0.1 carrier; sorry-free; no user axiom). Re-run on the ratified carrier in `GradeFactorisationR.lean`: verdict (B′) factors and veridicality-sighted — *PROVED*. *Precondition only* — does not address CO-1. |=== == Dangerous Patterns (BANNED) @@ -113,12 +113,8 @@ verification/proofs/ │ └── *.idr # Project-specific Idris2 proofs ├── lean4/ # Lean4 proofs (algebra, lattices) │ └── *.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── *.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── *.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── *.tla +└── agda/ # Agda proofs (induction, metatheory) + └── *.agda ---- == References diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index c6cfe66..9930ab0 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -1,210 +1,219 @@ // SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) // SPDX-License-Identifier: CC-BY-SA-4.0 -// SPDX-License-Identifier: CC-BY-SA-4.0 -= Proof status — trope-checker verified core -:revdate: 2026-06-23 += Proof status — trope-checker +:revdate: 2026-10-27 :toc: macro :stem: latexmath -What is *proved* (machine-checked, no axioms), *stubbed-and-named* (an open -problem stated, never asserted as done — HC-5), and *deferred*. Ground-truth: -`idris2 --typecheck verification/proofs/idris2/trope.ipkg` (exit 0). No -`believe_me`, `assert_total`, or `postulate` stands behind any claim below. +What is *proved* (machine-checked: in Lean no `sorryAx` and no user axiom — the +audits show `propext`, `Quot.sound` and, in three theorems, `Classical.choice`; `--safe --without-K` in Agda; `%default total` with no escape hatch in +Idris2) and what is *open* (named, specified, not asserted), on the ratified +carrier of `spec/calculus.adoc` v0.2 (R-2026-07-07, ADR 0004). Prover roles per +ADR 0005: Agda is the normative kernel, Idris2 the executable reference, Lean the +provenance development, Rust the fast core. Ground truth is the latest entry of +`AFFIRMATION.adoc`; every name below is a definition in the proof sources. toc::[] -== Proved (machine-checked) +== Proved -[cols="1,2,2",options="header"] -|=== -| Lemma | Statement | Where -| Fidelity L1 | `dplus` (tropical loss addition, ⊤ absorbs ∞ absorbs finite) is associative | `Trope.Fidelity.dplusAssoc` -| Fidelity unit/refl | `Q 0` right-unit of `dplus`; `dLte` reflexive | `Trope.Fidelity.dplusZeroR`, `dLteRefl` -| Coordinate L1 | `▷` associative on fate, bond, merge | `Trope.Coords.{fateAssoc,bondAssoc,mergeAssoc}` -| Coordinate L2 | unit of `▷` on each coordinate | `Trope.Coords.{fateUnitL/R,bondUnitL/R,mergeUnitL/R}` -| Coordinate ⊑ refl | retention order reflexive on each coordinate | `Trope.Coords.{fateLteRefl,bondLteRefl,mergeLteRefl}` -| Grade L1 (assoc) | `▷` associative on the full three-coordinate grade | `Trope.Laws.gradeAssoc` -| Grade L2 (unit) | `ε ▷ g = g = g ▷ ε` | `Trope.Grade.{gradeUnitL,gradeUnitR}` -| Decidability of ⊑ | `⊑` is decidable on grades | `Trope.Laws.decGradeLte` -| Veridicality Derivation | exactly three deceptive duals, one per coordinate (Falsified/Misbound/Conflated), each the unique deceptive inhabitant | `Trope.Veridicality.{fate,bond,merge}DeceptiveUnique`, `deceptiveDuals` -| Honest Generation | the five atoms (attenuate/predicate/drop/sever/fuse) + ε generate exactly the honest fragment of each coordinate; the atoms never produce a deceptive dual | `Trope.Generation.{genFate,genBond,genMerge,movesHonest*}` -| ε honest & coherent | ε is non-deceptive and HC-4-coherent | `Trope.Veridicality.epsilonHonest`, `Trope.Grade.epsilonCoherent` +[cols="1,3,3",options="header"] |=== +| Result | Statement | Where -== Stubbed-and-named (open problems — NOT asserted) +3+^| _Carrier and laws_ -[cols="1,3",options="header"] -|=== -| ID | Open problem -| *Grade soundness* (calculus §8) | `Γ ⊢ e : A ! g ⟹ g ⊑ ρ(in,out)` — the declared grade never claims more retention than execution delivers. Requires an operational model of execution (`ρ`); the term language is out of the verified core's scope this pass. Stated in the calculus; *not* claimed proved here. PARTIAL ADVANCE 2026-06-22 (see "Soundness advance" below): the verdict corollary, T-Sub soundness, and grade soundness for EXACT faithful lowering are now machine-checked; what remains open is the term-language/fix operational model and conservative composition over fate. -| *L4 monotonicity / L5 infectiousness as theorems* | Hold by the bottom/absorbing structure of each coordinate (used implicitly); not yet extracted as standalone Idris lemmas. Tractable; deferred to the next pass. -| *O1 exhaustiveness of the effects* | That the five atoms (plus the three duals) are the _true generators_ of all particularity-affecting operations is a well-chosen list, not yet a theorem derived from the three axes. Calculus O1. Philosophy-of-individuation question O1-coord is logged, not coded. -|=== +| L1 (associativity) +| stem:[(g_1 \triangleright g_2)\triangleright g_3 = g_1 \triangleright (g_2 \triangleright g_3)] on the full three-coordinate grade; per coordinate and on the fidelity dimension. +| Idris2 `Trope.Laws.gradeAssoc`, `Trope.Coords.{fateAssoc,bondAssoc,mergeAssoc}`, `Trope.Fidelity.dplusAssoc`; Agda `TB.Grade.gmonoid-assoc`; Lean `GradeR.instCommMonoid` (`GradeRatified.lean`), `FateA.comp_assoc` (`L4Monotonicity.lean`). + +| L2 (unit) +| stem:[\varepsilon \triangleright g = g = g \triangleright \varepsilon]. +| Idris2 `Trope.Grade.{gradeUnitL,gradeUnitR}`, `Trope.Coords.fateUnitL`, `Trope.Fidelity.dplusZeroR`; Agda `TB.Grade.{gmonoid-unitL,gmonoid-unitR}`. + +| L3 (bottom absorption) +| Each deceptive bottom (`Falsified`, `Misbound`, `Conflated`, fidelity `Unknown`) is a two-sided zero of its coordinate's composition (A1). `Total` absorbs within fidelity. +| Agda `TB.Grade.{falsified-absorbL,falsified-absorbR,misbound-absorbL,conflated-absorbL,unknown-absorbL,total-absorb-Q}`, `TB.Tier.deceptive-absorbs-▷`; Lean `FateA.falsified_two_sided_zero`, `GradeR.gBotR_two_sided_zero`. + +| L4 (monotonicity), in full +| stem:[\triangleright] is monotone in both arguments w.r.t. stem:[\sqsubseteq] on every coordinate of the ratified carrier. +| Idris2 `Trope.Soundness.{fateL4MonoR,fateL4MonoL}`, `Trope.Order.{bondComposeMono,mergeComposeMono}`; Agda `TB.Order.{fateL4MonoR,fateL4MonoL}`; Lean `FateA.{comp_mono_right,comp_mono_left}`. + +| L5 (deception infectiousness) +| Once a coordinate is at its deceptive bottom no composition restores an honest value; applying any further effect to a deceptive term keeps it deceptive. A corollary of L3. +| Agda `TB.Tier.deceptive-absorbs-▷`, `TB.Reduction.{attenuate-stays-deceptive,project-stays-deceptive}`. + +| L6 (commutativity) +| stem:[g_1 \triangleright g_2 = g_2 \triangleright g_1] on the ratified carrier. +| Lean `GradeR.instCommMonoid`, `FateA.comp_comm`; Agda `TB.Grade.grade-comm`. + +| Retention order is a decidable preorder +| stem:[\sqsubseteq] is decidable, reflexive and transitive on grades. +| Idris2 `Trope.Laws.decGradeLte`, `Trope.Coords.{fateLteRefl,bondLteRefl,mergeLteRefl}`, `Trope.Fidelity.dLteRefl`, `Trope.Order.{fateLteTrans,bondLteTrans,mergeLteTrans,dLteTrans}`, `Trope.Soundness.gradeLteTrans`. + +| Fate is a chain (A2) +| `Dropped ⊑ Predicated` and `Predicated ⋢ Dropped`; the v0.1 antichain is dissolved in the stated direction only. +| Idris2 `Trope.Soundness.{fateDroppedLtePredicated,fatePredicatedNotLteDropped}`; Agda `TB.Order.{fateDroppedLtePredicated,fatePredicatedNotLteDropped}`. + +| Veridicality Derivation +| Exactly three deceptive duals, one per coordinate kind (`Falsified`, `Misbound`, `Conflated`), each the unique deceptive inhabitant of its coordinate. +| Idris2 `Trope.Veridicality.{fateDeceptiveUnique,bondDeceptiveUnique,mergeDeceptiveUnique,deceptiveDuals}`; Agda `TB.Honest.{fateDeceptiveUnique,bondDeceptiveUnique,mergeDeceptiveUnique,deceptiveDuals}`. + +| Honest Generation +| The five atoms `attenuate`, `predicate`, `drop`, `sever`, `fuse` with stem:[\varepsilon] generate exactly the honest fragment of each coordinate and never produce a deceptive dual; honesty is closed under stem:[\triangleright]. +| Idris2 `Trope.Generation.{genFate,genBond,genMerge}`; Agda `TB.Honest.{genFate,genBond,genMerge}`, `TB.Honest.honest-closed-▷`. + +| stem:[\varepsilon] is honest and coherent +| The unit is non-deceptive and HC-4-coherent. +| Idris2 `Trope.Veridicality.epsilonHonest`, `Trope.Grade.epsilonCoherent`. + +3+^| _Cancellation_ + +| C1 (conicality) +| stem:[g_1 \triangleright g_2 = \varepsilon \Rightarrow g_1 = g_2 = \varepsilon]. +| Lean `GradeR.conical`, `FateA.conical`; Agda `TB.Grade.grade-conical`. + +| C2 (the cancellation boundary) +| An element is left-cancellative iff it is stem:[\varepsilon]; cancellation holds only on the finite-fidelity core and fails on the honest-but-lossy and deceptive tiers alike. +| Lean `GradeR.{gradeR_leftCancel_iff,gradeR_not_leftCancel,gDroppedR_not_cancel}`; Agda `TB.Tier.{Q-cancelʳ,core-closed-▷}`, `TB.Tier.{dropped,predicated,severed,total}-honest-not-cancel`, `TB.Tier.{falsified,unknown}-not-cancel`. + +| Tier-2 membership, exhaustive +| Every honest-but-lossy element is individually witnessed non-cancellative, `Withheld` and `Fused` included; the per-element witnesses feed the iff. +| Lean `TierTwoComplete.lean`: `Bond.withheld_honest_not_cancel`, `Merge.fused_honest_not_cancel`, `Fate.atten_not_cancel`, the `*.leftCancelWitness` family, `Grade.grade_leftCancel_iff`. + +| C3 (partition; tier closure is not a homomorphism) +| `Dropped`, `Total`, `Severed`, `Predicated`, `Withheld`, `Fused` are honest non-cancellative elements; `Falsified`, `Misbound`, `Conflated`, `Unknown` are the deceptive ones. `tierOf (g ▷ h) = tierOf g ⊓ tierOf h` is false on fate; tier preservation is closure. +| Lean `dropped_absorbing`, `fidelity_total_honest_not_cancel` (`GradeBoundary.lean`); Agda `TB.Tier.fate-tier-meet-hom-fails`, the `TB.Tier` classifiers. + +3+^| _Factorisation_ -== Deferred (named, not attempted this pass) +| O1-carrier (atom factorisation) +| Every grade is the stem:[\triangleright]-product of its single-slot projections; nine atom families, each realised, pairwise disjoint. Stated on the v0.1 `Grade` (`EffectAtoms.lean` imports `GradeBoundary`): the construction is componentwise and does not touch the clause (A1) changed, but a restatement on `GradeR` is not mechanised (see Open). +| Lean `EffectAtoms.lean`: `Trope.Grade.atom_factorization`, `Trope.nine_families`, `Trope.family_realized`, `Trope.families_disjoint`, `fateFamily_none_iff`. -* Full Haec compiler / codegen / runtime (scaffolded in the `haec` repo). -* A Rust fast-core — *DRAFTED 2026-06-22* (`src/rust/`, dep-free, std-only; agrees with the Idris2 reference bit-for-bit over the conformance corpus, via `just trope-rust`). Further hardening (fuzzing, perf) deferred. -* The produce/demand adjunction (calculus O3); the fidelity-carrier question (O4). +| Tropical factorisation, (B′) sighted +| A nontrivial surjective monoid homomorphism stem:[\pi_R] onto the commutative tropical fidelity carrier exists and distinguishes `Dropped` (stem:[\infty]) from `Falsified` (stem:[\top]); the verbatim-payload map is not a homomorphism, and any sighted homomorphism squashes `Unknown` to the deceptive top. +| Lean `GradeFactorisationR.lean`: `piR_hom`, `piR_one`, `piRHom`, `piR_nontrivial`, `piR_surjective`, `piR_sighted`, `phiR_sighted`, `phiId_not_hom`, `sighted_forces_squash`. -== Modelling notes (faithful-but-simplified, recorded for honesty) +3+^| _Metatheory (Theorem B, Agda `--safe --without-K`, zero postulates)_ + +| Target 1 — intrinsic graded calculus +| The typing judgement stem:[\Gamma \vdash e : A \mathbin{!} g] over the ratified grade monoid, with the F4 tiers as closures. +| Agda `TB.Syntax`, `TB.Grade`, `TB.Tier`. + +| Target 2 — grade-exact substitution +| Cut preserves the grade exactly; grade commutes with cut. +| Agda `TB.Substitution.{cut-preserves-grade,cut-grade-comm}`. + +| Target 3 — subject reduction, β/let core +| β and `let` steps preserve type and grade exactly; the redex grade is the contractum grade; the tier is preserved; sequencing two core computations stays in the core. +| Agda `TB.Reduction.{β-app,β-let,let-redex-grade,let-tier-preserved,seq-stays-core}`. (The `fix` case is open: see CO-1 below.) + +| Target 4 — Honest Generation and Veridicality +| As in the carrier rows above, at the level of terms. +| Agda `TB.Honest`. + +3+^| _Soundness_ + +| Grade soundness, exact lowering +| If the declared grade equals the observed retention, stem:[g \sqsubseteq \rho]. +| Idris2 `Trope.Soundness.soundFromExact`. + +| T-Sub soundness +| stem:[g' \sqsubseteq g \wedge g \sqsubseteq \rho \Rightarrow g' \sqsubseteq \rho]. +| Idris2 `Trope.Soundness.subSound`. + +| Verdict soundness (corollary) +| stem:[\mathrm{floor}(U) \sqsubseteq g \wedge g \sqsubseteq \rho \Rightarrow \mathrm{floor}(U) \sqsubseteq \rho]. +| Idris2 `Trope.Soundness.verdictSound`. + +| Grade soundness, β/let core +| Reduction in the exact fragment preserves the grade (Theorem B Target 3 above). +| Agda `TB.Reduction`, `TB.Substitution.cut-preserves-grade`. +|=== + +The Rust fast core (`src/rust/`) is not a proof; it agrees with the Idris2 +reference over the whole conformance corpus (`just trope-rust`). + +== Open + +Each is specified; none is asserted. Status words follow `spec/calculus.adoc §10`. + +* *CO-1 mechanisation* — the operational model (λ-trope, tagged values, + T-Fix-Decl) is DESIGNED in `spec/notes/2026-07-07-co1-operational-model.adoc`; + its mechanisation in Agda, steps 1–5 of that note's §6 extending `TB.Reduction`, + is OPEN. It closes Theorem B Target 3 (`fix`, NOT-REACHED, no postulate) and + grade soundness for conservative lowering (`spec/calculus.adoc §7–§8`). +* *O1-carrier on `GradeR`* — `atom_factorization` and the nine-family results + (`EffectAtoms.lean`) are theorems about the v0.1 `Grade`; porting them to the + ratified `GradeR` — expected to be mechanical, the factorisation being + componentwise — is OPEN. Until then the ratified-carrier reading in + `spec/calculus.adoc §6` and `§10` rests on that transfer argument, not a proof. +* *O1-coord* — whether `fate`, `bond`, `merge` are exhaustive ways to + individuate-and-lose; live probe: the bond-transfer move (`spec/calculus.adoc + §10`; workbench WP-5). +* *O2* — lowering correctness, per producer; no producer has discharged it + (`spec/calculus.adoc §8` firewall 2, `§10`). +* *O3* — the produce/demand adjunction; the verdict is a subsumption until the + triangle laws are checked (`spec/calculus.adoc §6.2`, `§10`). +* *O5 mechanisation* — O5 is DEFINED (`spec/calculus.adoc §10`, ADR 0005); + mechanising O5-1 as a side condition on an `Oracle`-indexed verdict is OPEN. +* *O6* — the ceiling verdict, stem:[\rho \sqsubseteq g_{\mathrm{ceiling}}], for + the privacy direction (`spec/calculus.adoc §5` note on T-Sub, `§10`). + +== Modelling notes + +Faithful-but-simplified choices, recorded for honesty: * *Provenance tags on `Fused` are erased* in the verified core (they are metadata that does not affect the lattice laws); the executable checker carries them. * *Deceptive duals are modelled as each coordinate's bottom* (worst retention, absorbing), which is how the calculus orders `Conflated`; this makes every honest floor fail against a deceptive grade (HC-2) by construction. -* *L2 is stated with ε's literal value* in Idris (a bare top-level `epsilon` as a - function argument does not reduce under the unifier); since - `epsilon = MkGrade Present Present Present Present Intact Single` definitionally, - the statement is `ε ▷ g = g`. -* *The use-model floor is a partial per-coordinate demand, not a grade value.* HC-4 - (the Σ-coherence: bond⊣bearer-fate) is enforced on edge grade VALUES, where it - makes incoherent states unrepresentable; the floor is a set of independent +* *L2 is stated with stem:[\varepsilon]'s literal value* in Idris (a bare top-level + `epsilon` as a function argument does not reduce under the unifier); since + `epsilon = MkGrade Present Present Present Present Intact Single` + definitionally, the statement is stem:[\varepsilon \triangleright g = g]. +* *The use-model floor is a partial per-coordinate demand, not a grade value.* + HC-4 (the Σ-coherence: bond⊣bearer-fate) is enforced on edge grade VALUES, where + it makes incoherent states unrepresentable; the floor is a set of independent minimum-demands (each coordinate optional), so an author CAN write an incoherent floor (e.g. bearer-Dropped + bond-Intact). This is harmless — each demanded - coordinate is checked independently — but is an author-error surface, not covered - by the HC-4 unrepresentability claim. (Audit 2026-06-22.) - -== Soundness advance (2026-06-22) - -Newly machine-checked in `Trope.Order` + `Trope.Soundness` (no axioms): - -* *⊑ is a preorder* — reflexivity (Trope.Coords) + *transitivity* (`fateLteTrans`, - `bondLteTrans`, `mergeLteTrans`, `dLteTrans`, assembled to `gradeLteTrans`). -* *Verdict-soundness corollary* (`verdictSound`) — `floor ⊑ g ∧ g ⊑ ρ ⟹ floor ⊑ ρ`. - This is the calculus §8 corollary, now proved (it is exactly transitivity of ⊑). -* *T-Sub soundness* (`subSound`) — `g' ⊑ g ∧ g ⊑ ρ ⟹ g' ⊑ ρ`. -* *Grade soundness for EXACT faithful lowering* (`soundFromExact`) — if the declared - grade equals the observed retention (the strongest faithful lowering, O2), then - `g ⊑ ρ`, via congruence of ▷ + reflexivity. No L4 needed. -* *L4 monotonicity holds for the chain coordinates* bond and merge - (`bondComposeMono`, `mergeComposeMono`). - -=== FINDING: strict L4 monotonicity FAILS for the fate coordinate - -`Trope.Soundness.fateL4MonotonicityFails` machine-checks a counterexample: -`Dropped ⊑ Present` and `Predicated ⊑ Predicated`, yet -`Dropped ▷ Predicated = Dropped` while `Present ▷ Predicated = Predicated`, and -`Dropped ⋢ Predicated` (Predicated and Dropped are *intentionally incomparable*, -calculus §3.1). So strict L4 does not hold for fate; the calculus's "L4 is a *lax* -compatibility" (§5 note) is load-bearing. Consequence: grade soundness for -*conservative* (inexact) steps cannot be composed by naive L4 over the fate -coordinate; the *exact* route (`soundFromExact`) sidesteps it, and bond/merge remain -monotone. - -=== Still open (narrowed) - -* Grade soundness for *conservative* lowering over fate — needs the lax argument the - calculus hints at, not strict L4. -* The operational model of the term language + `fix` (calculus §7) and a definition - of observed retention `ρ` over executions — the deeper part of the open problem. - *This is now named CO-1, the repository's central open problem (see the next - section); the two streams converge on it.* - -== Grade-algebra boundary + Theorem B metatheory (2026-06-23) - -Two work-streams landed against the *authoritative Lean ground truth* -`verification/proofs/lean4/grade-boundary/GradeBoundary.lean` (Lean 4 v4.16.0 + -Mathlib, sorry-free; `#print axioms` = `propext`/`Quot.sound` only — built green this -date, no `sorryAx`/user-`axiom`/`native_decide`): - -* *Stream A* — `spec/calculus-v0.2-draft.adoc`: a v0.2 spec addendum lifting the - proved algebra into obligations `R-2026-06-23-01..04`. -* *Stream B* — `verification/proofs/agda/theorem-b/` (Agda `--safe --without-K`, - *zero postulates*; `All.agda`/`Smoke.agda` green this date): the calculus - metatheory (Theorem B). - -Full reconciliation — the unified R-id ↔ Lean ↔ Agda ↔ status table, the convergence -analysis, and the divergence adjudication — is in -`verification/proofs/INTEGRATION-REPORT.adoc`. Headlines: - -=== Proved (this date) - -[cols="1,3",options="header"] -|=== -| Result | Where - -| *Three-tier strict cancellation boundary* stem:[\mathcal{C} \subsetneq \mathcal{H} - \subsetneq \mathcal{G}] — cancellation holds *only* on the finite-fidelity core and - fails on the honest-but-lossy and deceptive tiers alike (the non-cancellative set - *strictly* contains the deceptive set) -| Lean `honest_fidelity_cancel` (core) + `grade_not_leftCancel` (L5) + absorbing & - honest-not-cancel witnesses; Agda `TB.Tier` (`core-closed-▷`, `Q-cancelʳ`, six - `*-not-cancel`, `deceptive-absorbs-▷`). (A: R-2026-06-23-03; B: F4.) - -| *F2 — `▷` is non-commutative* (witness `dropped`/`falsified`), so `CommMonoid` / - special-Frobenius cannot model it — *now strengthened* by B's impossibility result: - *symmetric (orientation-free) computational cut is impossible* -| Lean `grade_mul_not_comm`, `Fate.not_comm`; Agda `grade-not-comm`, - `cut-symmetric-fails` (= `grade-not-comm`), `cut-orientation-matters`. (A: - R-2026-06-23-01; B: F2 + Target 2 refutation.) - -| *F2×F4 interaction — tier-preservation is CLOSURE, not a homomorphism.* The naïve - `tierOf (g ▷ h) ≡ tierOf g ⊓ tierOf h` is *false* on fate (`dropped ▷ falsified = - dropped` honest, shielding a later deceptive `falsified`); same phenomenon as the - strict-L4 failure -| Agda `TB.Tier.fate-tier-meet-hom-fails`, guarded by `fate-L4-fails` - (≡ Idris `Soundness.fateL4MonotonicityFails`). (B: F2×F4 finding.) - -| *Partition correction — `Dropped` and `Total` are HONEST*, not deceptive (absorbing - yet truthful). The non-cancellative set partitions as honest-but-lossy - (`dropped`/`predicated`/`severed`/`total`, +`withheld`/`fused`) versus deceptive - (`falsified`/`misbound`/`conflated`/`unknown`) -| Lean `dropped_absorbing`, `fidelity_total_honest_not_cancel`, `total_add_Q`, - `total_add_unknown`; Agda `TB.Tier` classifiers. (A: R-2026-06-23-04; B: F4.) - -| *Value substitution is grade-exact* ("tropes follow values through cut"); *honesty - is closed under ▷* so deceptive grades are unreachable from honest terms (HC-3) -| Agda `TB.Substitution.subst`/`cut-preserves-grade` (Target 2); - `TB.Honest.honest-closed-▷` + atom-honesty (Target 4). -|=== - -=== Theorem B — true per-target status (NOT rounded up) - -[cols="1,3",options="header"] -|=== -| Target | Status - -| *1* — encode the grade as a non-commutative graded structure (intrinsic calculus) | *PROVED* -| *2* — substitution-admissibility / reindexing | *PROVED* (+ `cut-symmetric-fails` refutation) -| *3* — subject reduction respecting the F4 boundary | *PARTIAL — INCOMPLETE.* β/let core PROVED (intrinsic SR; tier preserved exactly); *`fix`/lfp NOT-REACHED* (no postulate), blocked on CO-1 + O4. *There is no full subject reduction and no operational model yet.* -| *4* — Honest Generation (HC-*) + Veridicality (L*) | *PROVED* -|=== - -=== CO-1 — CENTRAL OPEN PROBLEM (the repository's headline gap) - -*The calculus has no operational model (reduction dynamics) for its grade-routing / -iterating constructs.* v0.1 is a pure type-and-grade discipline; reduction beyond the -β/let core is undefined. The two streams *converge on this single hole* from opposite -sides — recorded as ONE item, not two: - -* *Spec face (= A's OPEN-A):* the lossless fractional *split / rejoin / routing* - operator whose cancellability R-2026-06-23-03 constrains-in-advance is referenced - but *undefined* (no typing rule, no dynamics). -* *Proof face (= B's Target-3 fixpoint case):* `fix`/lfp subject reduction is - *NOT-REACHED* — no ↝ rule for `fix`, no observed-retention `ρ`. -* *Additionally gated by v0.1 O4* (the `Conat`-vs-tag limit carrier for ordering - iterated attenuation beyond stem:[\omega]) — B's second missing piece, which *is* - v0.1's pre-existing O4. - -The grade algebra is *not* at fault (the lfp endpoint stem:[\{total, unknown\}] is -already ▷-fixed and tier-stable). *Entanglement:* v0.1 §7 justifies the `fix` lfp -grade "by L4 monotonicity", but strict L4 is machine-proved to *fail on fate* -(`fate-L4-fails`) — so even the grade-side `fix` justification rests on a monotonicity -now known only to be lax. - -=== Documentation-reconciliation gaps (recorded, not filled — for the merge author) - -* *OPEN-A* — folded into CO-1 above. -* *OPEN-B* — `Falsified` (fate's deceptive bottom, dual of honest `Dropped`) is in the - proved carrier but absent from v0.1 §3.1's four-inhabitant fate table. *OPEN-B′ - (surfaced during integration)* — the analogous gap holds for `Misbound` (bond's - deceptive bottom), absent from v0.1 §3.2's three-inhabitant bond table. (Merge's - `Conflated` is already in v0.1 §3.3.) Whether to amend v0.1 §3.1/§3.2 normatively is - a documentation decision, not fixed by F1–F4. -* *OPEN-C* — tier-2 membership is recorded, not exhaustively proved: the harness - witnesses *representative* honest-but-lossy elements non-cancellative - (`predicated`/`severed`/`total`, +`dropped`); `Withheld` and `Fused` sit in tier 2 - by the carrier's order structure but carry no individual named non-cancellation - witness in either development. + coordinate is checked independently — but is an author-error surface, not + covered by the HC-4 unrepresentability claim. (Audit 2026-06-22.) + +== History + +Superseded by R-2026-07-07 (ADR 0004) where they disagree. The pre-ratification +theorems are retained in their files under provenance notes and remain true of +the v0.1 carrier. + +*2026-06-22.* First verified core (Idris2): L1, L2, decidability of ⊑, +Veridicality Derivation, Honest Generation, ε honest and coherent. Soundness +advance: ⊑ a preorder, `verdictSound`, `subSound`, `soundFromExact`, +monotonicity for bond and merge. A machine-checked FINDING that strict L4 fails +on the v0.1 fate coordinate (`fateL4MonotonicityFails`, since removed with the +carrier it described) made L4 lax and blocked conservative grade soundness; +both are resolved on the ratified carrier (L4 row above). O1 exhaustiveness and +L4/L5 as standalone lemmas were listed open; both are now proved (O1-carrier, +L4, L5 rows). + +*2026-06-23.* Grade-algebra boundary in Lean (`GradeBoundary.lean`: +`grade_mul_not_comm`, `grade_conical`, `grade_not_leftCancel`, +`honest_fidelity_cancel`, `fidelity_unknown_not_cancel`, +`fidelity_total_honest_not_cancel`, `dropped_absorbing`) and Theorem B in Agda +(Targets 1, 2, 4 proved; Target 3 partial). The v0.1 carrier's ▷ was shown not +commutative, symmetric cut impossible, and tier preservation closure rather than +a homomorphism; the first two were artefacts of the clause (A1) removed and the +third survives (C3 row). CO-1 was named the central open problem and recorded as +additionally gated by the limit-carrier question O4, which ADR 0004 resolved. +Documentation gaps on the v0.1 fate and bond tables and on tier-2 witnesses were +recorded; the tables are complete in spec v0.2 §3 and the witnesses are +`TierTwoComplete.lean`. + +*2026-06-29.* Tropical factorisation probe on the v0.1 carrier +(`GradeFactorisation.lean`: `forced_collapse_general`, `forced_collapse_grade`): +a homomorphism onto the commutative tropical carrier existed but every such map +was forced to identify `Dropped` with `Falsified`. Re-run on the ratified +carrier the verdict is (B′) sighted (Factorisation row above). The probe was and +is a precondition, not a recursion result. diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 3c78303..8fc5ff0 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -4,12 +4,11 @@ == Current status -Alpha. The schema, executable checker (Idris2), and conformance suite are green; the -verified core typechecks with no axioms behind its claimed lemmas. The grade-algebra -*honest/deceptive cancellation boundary* is proved in Lean (sorry-free, axiom-clean) -and its metatheory partially developed in Agda (Theorem B). Ground truth and true -statuses: `docs/status/PROOF-STATUS.adoc`, `AFFIRMATION.adoc`, -`verification/proofs/INTEGRATION-REPORT.adoc`. +Alpha. The schema, the Idris2 reference checker, the Rust fast core and the +conformance suite are green; the verified developments carry no `sorryAx` and no user +axiom behind their claimed lemmas. Spec v0.2 is the normative document; what is proved and +what is open: `docs/status/PROOF-STATUS.adoc`, `AFFIRMATION.adoc`, +`spec/calculus.adoc §10`. == Shipped (v0.1) @@ -19,34 +18,32 @@ statuses: `docs/status/PROOF-STATUS.adoc`, `AFFIRMATION.adoc`, * [x] Soundness advance: ⊑-preorder, verdict-soundness corollary, T-Sub soundness, grade soundness for *exact* faithful lowering (machine-checked). -== In progress (v0.2 — grade algebra + metatheory) - -* [x] Grade-algebra boundary proved in Lean 4 + Mathlib (`grade-boundary/`): non-commutative - product monoid; full-carrier conicality; three-tier strict cancellation boundary. -* [x] Spec v0.2 addendum: obligations `R-2026-06-23-01..04` bound to the governing Lean theorems. -* [x] Theorem B (Agda, `--safe --without-K`, zero postulates): Targets 1/2/4 PROVED. -* [~] Theorem B Target 3 (subject reduction respecting the boundary): *PARTIAL* — β/let proved; - `fix`/lfp NOT-REACHED (blocked on CO-1). -* [x] Tropical factorisation probe (`grade-factorisation/`, Lean 4 + Mathlib): verdict *(B) factors but - veridicality-blind* — a nontrivial commutative cost-quotient exists, but every commutative-target hom - is forced to collapse honest `dropped` / deceptive `falsified` (blindness co-located with the fate-axis - non-commutativity). A *precondition only*; recursion stays parked behind CO-1 (issue #10). - -== Open problems (named, not solved) - -* *CO-1 (central):* the calculus has *no operational model* for `fix`/routing dynamics — there is - no reduction rule for `fix` and no observed-retention `ρ`. Gated additionally by v0.1's *O4* (the - limit carrier for ordering iterated attenuation beyond ω, the `Conat`-vs-tag fork). Resolving CO-1 - unblocks full subject reduction (Theorem B Target 3). -* Grade soundness for *conservative* (inexact) lowering over fate — needs the lax-L4 argument - (strict L4 is machine-proved to fail on fate). -* *O1* exhaustiveness of the seven effects; *O2* per-front-end lowering correctness; *O3* the - produce/demand adjunction. -* Documentation reconciliation: *OPEN-B/B′* (`Falsified`/`Misbound` absent from v0.1 §3.1/§3.2); - *OPEN-C* (`Withheld`/`Fused` tier-2 membership not individually witnessed). +== Shipped (v0.2) + +* [x] Ratified carrier (ADR 0004, R-2026-07-07): two-sided deceptive zeros (A1), the fate + chain (A2), `Attenuated(0)` normalisation at ingest (A3); IR 0.2 semantics. +* [x] Agda Theorem B migrated to the ratified carrier (`--safe --without-K`, zero postulates): + Targets 1, 2, 4 proved; Target 3 β/let proved. +* [x] L4 monotonicity in full, both arguments, every coordinate (Idris2, Lean, Agda); L6 + commutativity. +* [x] Atom factorisation — O1-carrier proved (`EffectAtoms.lean`): nine atom families. +* [x] Tier-2 cancellation membership exhaustive (`TierTwoComplete.lean`). +* [x] Tropical factorisation re-run on the ratified carrier: (B′) factors and + veridicality-sighted (`GradeFactorisationR.lean`). +* [x] Spec consolidated at v0.2: one normative document on the ratified carrier; O5 defined, + O6 opened; prover roles per ADR 0005 (Proposed). + +== Open problems + +The authoritative list is `spec/calculus.adoc §10` — O1-coord, O2, O3, O5 mechanisation, +O6, CO-1 mechanisation — each with its status word; `docs/status/PROOF-STATUS.adoc` "Open" +restates it with where each is specified. CO-1 mechanisation (Agda, steps 1–5 of +`spec/notes/2026-07-07-co1-operational-model.adoc §6`) is the next proof work; it closes +Theorem B Target 3 and conservative grade soundness. == Deferred * Full Haec compiler / codegen / runtime (the `haec` repo). -* Rust fast-core hardening (drafted in `src/rust/`, dep-free, validated against the Idris2 reference). +* Rust fast-core hardening (fuzzing, perf); it already agrees with the Idris2 reference over + the conformance corpus (`just trope-rust`). * Filing the panic-attack signed-suppression proposal (`docs/proposals/`) upstream. diff --git a/spec/calculus-v0.2-draft.adoc b/spec/calculus-v0.2-draft.adoc deleted file mode 100644 index 03cde08..0000000 --- a/spec/calculus-v0.2-draft.adoc +++ /dev/null @@ -1,410 +0,0 @@ -// SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) -// SPDX-License-Identifier: MPL-2.0 -// SPDX-License-Identifier: CC-BY-SA-4.0 -= The Trope-Particularity Calculus — v0.2 grade-algebra addendum (proved obligations) -:revnumber: 0.2-draft -:revdate: 2026-06-23 -:toc: macro -:sectnums: -:sectnumlevels: 2 -:stem: latexmath -:icons: font - -[abstract] -This is a *draft addendum* to the trope-particularity calculus v0.1 -(`spec/calculus.adoc`, `:revnumber: 0.1`). It records, as dated normative -obligations, four facts about the grade algebra that are now *machine-proved* in -the Lean 4 + Mathlib development at `verification/proofs/lean4/grade-boundary/` -(sorry-free; `#print axioms` = `propext`/`Quot.sound` only). The work here is -*documentation only*: the algebra is already established; this document lifts it -into normative spec text and binds each new obligation to its governing theorem. -It does *not* edit v0.1 — it is written as a separate file precisely so the merge -step can diff it against v0.1 — and it neither re-derives the theorems nor reopens -the proved algebra; it binds each fact to its Lean name. v0.1's open obligation -*O1* (completeness of the seven -effects) is untouched and remains open throughout. - -The key words *MUST*, *MUST NOT*, *SHALL*, *SHALL NOT*, *SHOULD*, *MAY*, and -*OPTIONAL* are to be interpreted as in RFC 2119/8174. - -toc::[] - -== Provenance, and what is being recorded (invent nothing) - -The four obligations below are *not* new claims. Each is a lift, in substance, of a -green theorem from the grade-boundary harness, which is itself the single source -of truth for the algebra. The carrier the theorems range over is, exactly: - -* fidelity `Delta = WithTop (WithTop ℕ)` (`dplus = (+)`, unit `Q 0 = 0`); -* `Fate = Present | Atten Delta | Predicated | Dropped | Falsified`; -* `Bond = Intact | Withheld | Severed | Misbound`; -* `Merge = Single | Fused | Conflated`; -* `Grade` = the flat record `Fate⁴ × Bond × Merge`, with *independent* fields. - -[IMPORTANT] -.Two firewalls carried forward in substance from the harness, not to be laundered -==== -. *No Frobenius / cancellative / conical framing exists in v0.1.* A grep of -`calculus.adoc` finds none (its only near-hit, *O3*, is the unrelated -produce/demand *adjunction* conjecture). The obligations below are therefore *new -recordings of proved structure*, not transcriptions of existing v0.1 prose. - -. *"CF" (cancellative + conical ⇒ a lossless special-Frobenius split/merge) is -refuted as universal*, and this document MUST NOT be read as reinstating it. It is -ruled out twice over: by left-absorption of the deceptive bottoms -(R-2026-06-23-03, *L5*, `grade_not_leftCancel`) and, independently, by -non-commutativity of the full operation (R-2026-06-23-01, `grade_mul_not_comm`). -What survives CF's refutation is *cancellation on the finite-fidelity core* -(R-2026-06-23-03) — that algebraic fact alone, and no splitting or merging law, -global or core-local. -==== - -=== Existing numbering recorded (the non-collision basis) - -So that the new ids are demonstrably consistent and non-colliding, v0.1's scheme -is recorded here as it stands at the time of writing: - -[cols="1,3",options="header"] -|=== -| Namespace (v0.1 / siblings) | Meaning, and its status under this addendum - -| `L1`–`L5` (v0.1 §4) | The composition laws. *Untouched.* `L5` is *constrained and - sharpened* by R-2026-06-23-03 (this addendum's §4), not replaced. -| `O1`–`O4` (v0.1 §10) | The open obligations/falsifiers. *Untouched and still open*; - `O1` (seven-effects completeness) in particular is out of scope here. -| `R-2026-06-22` (v0.1 §6.1) | The sole v0.1 decision-log id (the conflation-as-fault - decision). The `R-YYYY-MM-DD` shape is reused below. -| `HC-*`, `L-*` | Reserved by the grade-boundary README for the *separate Agda* - development (Honest Generation; Veridicality). *Not touched, not collided with.* -|=== - -New obligations take the form *`R-2026-06-23-NN`*: the same `R-YYYY-MM-DD` -decision-log prefix as `R-2026-06-22`, with a two-digit sequence suffix that -extends the one-entry-per-date convention to carry several same-date records. -This collides with none of `L\d`, `O\d`, `R-2026-06-22`, `HC-*`, or `L-*`. - -[NOTE] -==== -*Source-of-truth toolchain.* All five primary governing theorems (`instMonoid`, -`grade_mul_not_comm`, `grade_conical`, `grade_not_leftCancel`, -`honest_fidelity_cancel`) are discharged under Lean `v4.16.0` + Mathlib `v4.16.0`, -sorry-free, with `#print axioms` reporting `propext`/`Quot.sound` only — no -`sorryAx`, no user `axiom`, no `native_decide`. The R-id ↔ theorem table in §7 -below (where one R-id binds a pair) is the claims-match-proofs contract; it is the -artifact the merge step keys on. -==== - -== R-2026-06-23-01 — the grade is a *non-commutative* product monoid - -[cols="1,4",options="header"] -|=== -| ID | Obligation (normative) - -| *R-2026-06-23-01* | The grade carrier under composition stem:[\triangleright] is -a *monoid*, formed as the *componentwise product* of its coordinate monoids -(`Fate⁴ × Bond × Merge`); this is the *degenerate-to-product* structure, confirmed -constructively (`instMonoid`). That product *MUST NOT* be assumed commutative: it -is *non-commutative* (`grade_mul_not_comm`). Consequently any algebraic model of -the operation stem:[\triangleright] *MUST* treat it as order-sensitive, and -*SHALL NOT* assume `CommMonoid`, `AddCommMonoid`, or special-Frobenius structure -for it. The non-commutativity is a property of the *full* operation, witnessed by -elements outside the cancellative core (the disagreeing heads `Dropped` and -`Falsified`); special-Frobenius is moreover unavailable across the honest region, -whose non-cancellative honest-but-lossy tier obstructs its comonoid leg -(R-2026-06-23-03). -|=== - -This records v0.1 *L1–L2* (monoid) at full strength while adding the order -discipline v0.1 left implicit. The witness to non-commutativity is intrinsic to -the `Fate` coordinate: it carries *two* distinct left-absorbing heads, `Dropped` -and `Falsified`, which disagree (`Dropped ▷ Falsified = Dropped` but -`Falsified ▷ Dropped = Falsified`), so swapping operands changes the result -(`Fate.not_comm`, lifted to the `fQuality` field by `grade_mul_not_comm`). - -[IMPORTANT] -==== -*Order matters, not merely grade-sum.* Because stem:[\triangleright] is -non-commutative, two effect sequences with the *same multiset* of per-step grades -*MAY* compose to *different* total grades. A checker, an IR producer, or any -optimiser *MUST NOT* reorder effect edges (v0.1 §9) under the assumption that -composition is symmetric. This is the precise sense in which special-Frobenius — -which presupposes a commutative comonoid/monoid interaction — is *unavailable*: -the obstruction is structural (order-sensitivity), independent of, and additional -to, the cancellation obstruction of R-2026-06-23-03. -==== - -== R-2026-06-23-02 — conicality of the full grade - -[cols="1,4",options="header"] -|=== -| ID | Obligation (normative) - -| *R-2026-06-23-02* | The full grade carrier is *conical*: for all grades -stem:[a, b], if stem:[a \triangleright b = \varepsilon] then stem:[a = \varepsilon] -*and* stem:[b = \varepsilon] (`grade_conical`). The unit grade stem:[\varepsilon] -(full presence, intact bond, single merge) *MUST NOT* be treated as reachable -under composition by any pair other than stem:[\varepsilon \triangleright \varepsilon]. -|=== - -Conicality holds on the *entire* carrier (not only the core), and is proved -fieldwise from per-coordinate conicality (`Fate.conical`, `Bond.conical`, -`Merge.conical`). Operationally: no amount of loss can be *manufactured from* the -unit, and the loss-free state cannot be *re-attained* except from itself. A -verdict engine *MAY* rely on this — a final grade of stem:[\varepsilon] -witnesses a genuinely loss-free pipeline, never an accidental cancellation of -losses against gains, because there are no gains. - -== R-2026-06-23-03 — the three-tier cancellation boundary (headline) - -[cols="1,4",options="header"] -|=== -| ID | Obligation (normative) - -| *R-2026-06-23-03* | The carrier is stratified by cancellability into *three -strict tiers*. Write stem:[\mathcal{C}] for the *cancellative core*, -stem:[\mathcal{H}] for the *honest* region, and stem:[\mathcal{G}] for the *full* -carrier. Then the inclusions are *strict*: -stem:[\mathcal{C} \subsetneq \mathcal{H} \subsetneq \mathcal{G}]. *Cancellation -holds ONLY on the finite-fidelity core stem:[\mathcal{C}]* -(`honest_fidelity_cancel`), and *fails everywhere above it* — on the -honest-but-lossy tier and on the deceptive tier alike; the full carrier is -*non-left-cancellative* (`grade_not_leftCancel`). Accordingly, *should* a future -revision introduce a lossless fractional split, rejoin, or routing operator (none -exists today — see OPEN-A), that operator *MUST* be licensed *ONLY* on -stem:[\mathcal{C}], the sole region carrying the cancellation it would rely on; -on stem:[\mathcal{H} \setminus \mathcal{C}] and on -stem:[\mathcal{G} \setminus \mathcal{H}] it *MUST* be treated as lossy and -irreversible, and *MUST NOT* be presented as recoverable. -|=== - -The three tiers, by their inhabitants: - -[cols="1,1,3",options="header"] -|=== -| Tier | Region | Inhabitants and cancellation status - -| *1* | *Cancellative core* stem:[\mathcal{C}] -| The finite-fidelity region — `Atten(Q n)` with stem:[n \in \mathbb{N}], where - `Delta.Q` embeds stem:[(\mathbb{N}, +, 0)] injectively and additively — together - with the coordinate units (`Present`, `Intact`, `Single`). *Cancellation holds* - here and *only* here (`honest_fidelity_cancel`). - -| *2* | *Honest-but-lossy* stem:[\mathcal{H} \setminus \mathcal{C}] -| `Dropped`, `Predicated`, `Severed`, `Withheld`, `Fused`, and `Total` (honest - stem:[\infty]). These are *honest* — they tell no lie about what was lost — yet - they are *non-cancellative* (`Fate.predicated_honest_not_cancel`, - `Bond.severed_honest_not_cancel`, `fidelity_total_honest_not_cancel`; `Withheld` - and `Fused` belong here by the carrier's order structure but carry no individual - witness yet — OPEN-C). Honest loss is still loss: it cannot be undone. - -| *3* | *Deceptive, absorbing bottoms* stem:[\mathcal{G} \setminus \mathcal{H}] -| `Falsified` (fate), `Misbound` (bond), `Conflated` (merge), and `Unknown` - (fidelity). Each is a *left zero* (`Fate.falsified_absorbing`, - `Bond.misbound_absorbing`, `Merge.conflated_absorbing`, - `Delta.unknown_absorbing`): it absorbs everything composed after it, so it - cannot be cancelled back out. This is *L5*. -|=== - -[WARNING] -.Two strict inclusions, two distinct witnesses — do not collapse them -==== -The boundary is *three-tier, not two-tier*: the non-cancellative set is -*strictly larger* than the deceptive set. - -. stem:[\mathcal{C} \subsetneq \mathcal{H}] is witnessed by an *honest* element -that nonetheless fails to cancel — e.g. `Total`, `Severed`, or `Predicated` -(`fidelity_total_honest_not_cancel`, `Bond.severed_honest_not_cancel`, -`Fate.predicated_honest_not_cancel`). "Honest" does *not* imply "cancellative". - -. stem:[\mathcal{H} \subsetneq \mathcal{G}] is witnessed by a *deceptive* element -— e.g. `Falsified` — at which left-cancellation fails outright -(`grade_not_leftCancel`). - -Conflating these two would mis-state the algebra: it would either (wrongly) license -splitting on honest-but-lossy elements, or (wrongly) brand honest loss as -deception. Both are forbidden. -==== - -[IMPORTANT] -.The split / rejoin / routing constraint is a constraint-in-advance -==== -The licensing constraint above is the frozen consequence both the calculus and its -proof harness must respect: any fractional split / rejoin / routing is licensed -*only* on the cancellative core stem:[\mathcal{C}] (tier 1), is order-sensitive -(F2 / R-2026-06-23-01), and is *forbidden* on tiers 2 and 3. The order-sensitivity -attaches to the routing *operation*, not to the internal composition of core -grades: within stem:[\mathcal{C}] the grade product reduces to fidelity addition -(`Delta.Q_add`), which is commutative *and* cancellative, so the core licenses -*both* losslessness and commutative reassembly. It is the operation's general form -— which may move grades between coordinates and tiers — that the order discipline -of R-2026-06-23-01 governs. - -This addendum *defines no split / rejoin / routing operator* — none exists in -v0.1. The obligation here *constrains in advance* any such operator a future -revision may introduce; the operator itself is listed as OPEN-A in §8. -==== - -== R-2026-06-23-04 — partition correction: `Dropped` and `Total` are *honest* - -[cols="1,4",options="header"] -|=== -| ID | Correction (normative, dated for the decision-log) - -| *R-2026-06-23-04* | `Dropped` and `Total` *MUST* be classified as *honest*, not -deceptive. `Dropped` is *honest withholding* — a field withheld entirely, the -clean omission whose *deceptive dual* is the distinct fate `Falsified`. `Total` -is the *honest* stem:[\infty] — total quantified loss — whose deceptive -counterpart is the fidelity bottom `Unknown` (loss of *unknown* amount). -Documentation, taxonomy tables, and tooling *MUST NOT* enumerate `Dropped` or -`Total` in the deceptive tier (tier 3 of R-2026-06-23-03). -|=== - -This correction is recorded explicitly because it *contradicts informal -phrasings* that treat any absorbing or bottom-like element as deceptive. Both -`Dropped` and `Total` are *absorbing* in their coordinate yet *truthful*: -`Dropped` is left-absorbing on `Fate` (`Fate.dropped_absorbing`) while remaining -an honest omission; `Total` absorbs finite fidelity (`Delta.total_add_Q`) and is -itself absorbed only by the deceptive `Unknown` (`Delta.total_add_unknown`), -yet asserts no falsehood. The distinction *absorbing-but-honest* versus -*absorbing-and-deceptive* is the whole reason the boundary is three-tier -(R-2026-06-23-03): it is *precisely* because `Dropped`, `Total`, `Severed`, and -`Predicated` are honest-yet-non-cancellative that "cancellation fails stem:[\iff] -deception" is *false*. - -[NOTE] -==== -*Carrier reconciliation.* The proved `Fate` coordinate has *five* inhabitants — -it includes `Falsified`, the deceptive fate-bottom dual to honest `Dropped`. v0.1 -§3.1's fate table lists only *four* (`Present`, `Attenuated(δ)`, `Predicated(P)`, -`Dropped`) and predates `Falsified`. This addendum records `Falsified` as -established by the carrier; whether v0.1 §3.1 should be amended to introduce it is -a documentation-reconciliation decision for the merge author, logged as OPEN-B -(§8). Nothing here edits v0.1 §3.1. -==== - -== Relationship to the v0.1 obligations - -*R-2026-06-23-03 constrains, and does not replace, L5.* v0.1's *L5* ("conflation -infectiousness": once the merge coordinate is `Conflated`, no composition restores -`Fused` or `Single`) stands unchanged. R-2026-06-23-03 makes L5's irreversibility -*precise* — it is *left-absorption of the deceptive bottom* — and *generalises* it -from the merge coordinate alone to *every* coordinate's deceptive bottom -(`Falsified`, `Misbound`, `Conflated`, `Unknown`), with the full-carrier -consequence `grade_not_leftCancel`. Read together: v0.1's L5 is the merge-coordinate -instance of the general left-absorption fact that R-2026-06-23-03 records. - -*L1–L3 are reinforced; the L4 relationship is sharpened.* R-2026-06-23-01 records -the L1–L2 monoid at full strength and adds the order discipline (non-commutativity) -that L1's associativity alone does not capture. L3 (bottom-absorption) is the -per-coordinate left-absorption that R-2026-06-23-03 makes precise. The tier -stratification, however, is a *cancellation* property and does *not* presuppose the -retention order: strict *L4 monotonicity is only lax — it fails on the fate -coordinate* (machine-proved downstream as `fate-L4-fails`, the same F2×F4 -phenomenon), so tier-preservation is set-membership *closure*, not an -order-homomorphism, and v0.1 §7's appeal to *strict* L4 to justify the `fix` grade -needs the lax/closure route (part of CO-1, below). - -*O1 is untouched and remains open.* v0.1's *O1* — that the seven effects are -*exhaustive* — is a separate completeness question and is *not* addressed, -advanced, or closed here. The algebraic facts recorded in this addendum concern -the *structure of the grade monoid*, not the *enumeration of the effects that -populate it*; the two are orthogonal. O2–O4 are likewise untouched. - -== Interface table — the claims-match-proofs contract - -This table is the keystone artifact: each new obligation is bound *1:1 where -possible* to its governing theorem(s) in -`verification/proofs/lean4/grade-boundary/GradeBoundary.lean` (namespace -`Trope`, sub-namespaces `Trope.Grade`, `Trope.Fate`, `Trope.Bond`, -`Trope.Merge`, `Trope.Delta`). An implementation claiming conformance to an R-id -below *MUST* be checkable against the named theorem(s). - -[cols="1,2,3",options="header"] -|=== -| R-id | Established fact (frozen interface) | Governing Lean theorem(s) - -| *R-2026-06-23-01* | F1 + F2 — non-commutative product monoid -| `Trope.Grade.instMonoid` (degenerate-to-product); `Trope.Grade.grade_mul_not_comm` - (non-commutative). _Coordinate witness:_ `Trope.Fate.not_comm`. - -| *R-2026-06-23-02* | F3 — conicality of the full grade -| `Trope.Grade.grade_conical`. _Fieldwise:_ `Trope.Fate.conical`, - `Trope.Bond.conical`, `Trope.Merge.conical`. - -| *R-2026-06-23-03* | F4 — three-tier strict cancellation boundary -| _Core (cancellation):_ `Trope.Grade.honest_fidelity_cancel`. _Upper inclusion - (L5, non-left-cancellative):_ `Trope.Grade.grade_not_leftCancel`. _Deceptive - left-zeros:_ `Trope.Fate.falsified_absorbing`, `Trope.Bond.misbound_absorbing`, - `Trope.Merge.conflated_absorbing`, `Trope.Delta.unknown_absorbing`. _Honest-but- - lossy witnesses (lower strict inclusion):_ `Trope.Fate.predicated_honest_not_cancel`, - `Trope.Bond.severed_honest_not_cancel`, `Trope.Grade.fidelity_total_honest_not_cancel`. - -| *R-2026-06-23-04* | Partition correction — `Dropped`, `Total` honest -| `Trope.Fate.dropped_absorbing` (honest yet absorbing); `Trope.Grade.fidelity_total_honest_not_cancel` - and `Trope.Delta.total_add_Q`, `Trope.Delta.total_add_unknown` (`Total` honest - yet absorbing, absorbed only by `Unknown`). _Embedding of the honest core:_ - `Trope.Delta.Q_add`, `Trope.Delta.Q_injective`, `Trope.Delta.Q_zero`. -|=== - -R-2026-06-23-01, -02, and -04 are 1:1 on a primary theorem; R-2026-06-23-03 (the -headline) is intrinsically a *pair* of primaries — `grade_not_leftCancel` -(the upper strict inclusion / L5) and `honest_fidelity_cancel` (the core) — with -the absorbing and honest-not-cancel lemmas as supporting witnesses for the two -strict inclusions. - -== OPEN, for author review - -The following surfaced while authoring and are *genuine gaps* that F1–F4 and the -partition correction do *not* settle. In line with the brief, they are *recorded, -not filled*. - -* *OPEN-A — the split / rejoin / routing operator is referenced but undefined.* - R-2026-06-23-03 (and the frozen consequence it records) governs the - cancellability of *fractional split / rejoin / routing*, yet no such operator is - defined in v0.1 or in the grade-boundary harness. The obligation constrains an - operation that does not yet exist. Whether to introduce it — and if so, with what - typing rule — is for author review; until then R-2026-06-23-03 stands as a - *constraint-in-advance*. _Now elevated:_ integrating this addendum with the Agda - metatheory (Theorem B) showed OPEN-A and Theorem B's unreached `fix`/lfp - subject-reduction case to be *one and the same* underspecification — the calculus - defines no operational (reduction) model for its grade-routing / iterating - constructs beyond the β/let core — now tracked as the repository's central open - problem *CO-1* (itself gated by v0.1's O4, the limit carrier). See - `verification/proofs/INTEGRATION-REPORT.adoc` §4 and ADR 0003. - -* *OPEN-B — `Falsified` is absent from v0.1 §3.1.* The proved `Fate` coordinate is - five-ary, but v0.1 §3.1's fate table lists four inhabitants and does not mention - `Falsified` (the deceptive dual of `Dropped`). This addendum records `Falsified` - as carrier-established; whether the eventual v0.2 should amend v0.1 §3.1 to - introduce it normatively — and how that interacts with the v0.1 §6.1 - conflation-as-fault story - for the *fate* coordinate — is a documentation-reconciliation decision, not one - fixed by F1–F4. - -* *OPEN-B′ — `Misbound` is absent from v0.1 §3.2.* Surfaced when this addendum was - swept against the Agda metatheory (Theorem B): the bond coordinate carries a - *deceptive dual* `Misbound` — bond's order-bottom, the dual of honest `Severed` — - exactly as the fate coordinate carries `Falsified`, yet v0.1 §3.2 lists only three - bonds (`Intact`, `Withheld`, `Severed`) and omits it. This is the precise analogue - of OPEN-B for the bond coordinate; merge's deceptive bottom `Conflated` is, by - contrast, already present in v0.1 §3.3. The Idris2 core both enumerates the three - deceptive duals (`Trope.Veridicality.deceptiveDuals` = `(Falsified, Misbound, - Conflated)`) and proves each the *unique* deceptive inhabitant of its coordinate - (`Trope.Veridicality.bondDeceptiveUnique` for `Misbound`). Whether to amend v0.1 - §3.2 is the same documentation-reconciliation decision as OPEN-B, to be taken - together with it. - -* *OPEN-C — tier-2 membership is recorded, not exhaustively proved.* The harness - proves *representative* honest-but-lossy elements non-cancellative (`Predicated`, - `Severed`, `Total`). That `Withheld` and `Fused` also sit in tier 2 (honest, - non-cancellative) is asserted here from the carrier's order structure but is not - individually witnessed by a named theorem in the current harness. Whether to add - those witnesses, or to prove tier-2 membership uniformly, is for author review. - -''' -_Suggested CHANGELOG line:_ `docs: draft trope-particularity calculus v0.2 -addendum (proved grade algebra: non-commutative product monoid [R-2026-06-23-01]; -full-carrier conicality [R-2026-06-23-02]; three-tier strict cancellation boundary, -cancellation only on the finite-fidelity core [R-2026-06-23-03]; Dropped/Total -honest-not-deceptive partition correction [R-2026-06-23-04]; R-id↔Lean-theorem -contract; L5 sharpened not replaced; O1 untouched).` diff --git a/spec/calculus.adoc b/spec/calculus.adoc index 68d87bd..1f36fd2 100644 --- a/spec/calculus.adoc +++ b/spec/calculus.adoc @@ -1,9 +1,8 @@ -// SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) -// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = The Trope-Particularity Calculus — a normative core -:revnumber: 0.1 (draft for review) -:revdate: 2026-06-22 +:revnumber: 0.2 (consolidated; ratified carrier R-2026-07-07, ADR 0004; O5 adopted per ADR 0005) +:revdate: 2026-10-13 :toc: macro :sectnums: :sectnumlevels: 2 @@ -14,15 +13,20 @@ This document specifies the type-level discipline of *trope-particularity*: a graded effect system over a Turing-complete term language, in which each operation on a property-instance carries a declared *loss-shape* grade, grades -compose by fixed algebra, and a declared *use-model* yields a decidable verdict. -It pins the loss-shape category, gives the seven effects as typing rules, states -the composition and order laws normatively, fixes the interaction with general -recursion, defines the verdict, states the soundness target with its firewalls, -and defines a language-neutral interchange (the Trope IR) so that a *tropechecker* -can be implemented portably and independently of any one source language. - -The key words *MUST*, *MUST NOT*, *SHALL*, *SHOULD*, *MAY*, and *OPTIONAL* are to -be interpreted as in RFC 2119/8174. +compose by a fixed algebra, and a declared *use-model* yields a decidable +verdict. It pins the loss-shape carrier, names the nine effects of the +vocabulary and gives the six writable ones as typing rules, states the +composition and order laws normatively, fixes the interaction with general +recursion, defines the verdict, states the soundness results with their +firewalls, defines the language-neutral interchange (the Trope IR) so that a +*tropechecker* can be implemented portably, and lists the open obligations. + +This is the v0.2 consolidation: it folds the v0.1 text (2026-06-22), the +grade-algebra addendum (2026-06-23) and the two ratification notes of +2026-07-07 into one normative document. Where a law or result is machine-checked +it is cited by its name in the proof developments (§9.3); where it is open it is +listed in §10. The key words *MUST*, *MUST NOT*, *SHALL*, *SHOULD*, *MAY*, and +*OPTIONAL* are to be interpreted as in RFC 2119/8174. toc::[] @@ -38,7 +42,7 @@ conflating them is itself a modelling error this calculus exists to forbid. | trope-the-valuation | The bottleneck (max–min) grading of a path by its weakest link, with the argmin locating the edge to repair. (The *invariant-path* sense.) Used below - only by analogy, for the verdict witness. + only by analogy, for the verdict witness (§6.2). | trope-the-residual | A residual treated as a sum-typed object rather than a scalar error term, @@ -46,9 +50,12 @@ conflating them is itself a modelling error this calculus exists to forbid. (The *typed-residual* sense.) Reused below as the grade. | *trope-the-particular* -| An *abstract particular* in the sense of Williams and Campbell: a property - considered as a non-repeatable, situated instance — *this* quality, here, - borne by *this* bearer. *This is the object of the present calculus.* +| A *property-instance*: a property considered as a non-repeatable, situated + instance — *this* quality, here, borne by *this* bearer. The classical home + of the notion is trope theory (Williams, Campbell); the calculus needs only + what every instance ontology supplies — that property-instances are + particulars — and not the further theses of any one of them (bundle theory, + one-category ontology). *This is the object of the present calculus.* |=== A classical trope is _quality borne by a bearer_. This calculus works on a @@ -62,7 +69,8 @@ explicitly so that downstream readers do not attribute it to Williams. content_ of a property-instance: how much of its being-this-one-in-this-situation survives an operation. It is *graded and use-relative*, not binary and absolute. Classical particularity is the limiting case where the only admissible verdicts -are "identical" and "not identical"; this calculus refines that to a lattice. +are "identical" and "not identical"; this calculus refines that to a chain per +coordinate. ==== == The object: property-instances @@ -82,40 +90,50 @@ A trope whose quality has been severed from its bearer is a distinct type, `FloatingQuality`, with no bearer field. Collapse of a quality to a predicate yields a non-trope type — the predicate's codomain (typically `Bool`). -== The grade: the loss-shape category +Two of the calculus's constructs are the ones that require property-instances +to be particulars rather than universals: *attenuation* (only an instance can +lose fidelity; a universal is exact) and *detaching* (a quality that survives +severance as a free-standing `FloatingQuality` is an instance with no bearer; +severing a universal from its instance leaves the universal, which was never +_this_). Everything else in the calculus would survive a change of ontology; +these two would not. + +== The grade: the loss-shape carrier A grade records what an operation did to a trope. It is *not a scalar*: two operations can lose the same _amount_ yet differ in _kind_ and in _honesty_. -A grade stem:[g] is a record of three orthogonal coordinates, +A grade stem:[g] is a record of three coordinate *kinds*, [stem] ++++ g \;=\; (\mathsf{fate},\ \mathsf{bond},\ \mathsf{merge}), ++++ -each living in its own lattice. Composition (§4) and the order (§5) act -*componentwise*, which is what keeps the algebra decidable while the term -language stays Turing complete (§7). +where `fate` is itself indexed by the four fields of stem:[\Phi]. A grade +therefore has *six slots* (four fates, one bond, one merge) over *three +coordinate kinds*; both descriptions are used in the stack and mean the same +carrier. Composition (§4) and the order (§5) act *slot-wise*, which is what +keeps the algebra decidable while the term language stays Turing complete (§7). === Coordinate 1 — field fate A *fate* records, per field, what survived. Let stem:[\delta \in \mathbb{N}\cup\{\infty,\top\}] be a fidelity element, where finite stem:[\delta] is a quantified loss in the -tropical (min-plus) order, stem:[\infty] is total quantified loss, and -stem:[\top] is loss of *unknown amount*. +tropical (min-plus) order, stem:[\infty] (`Total`) is total quantified loss, +and stem:[\top] (`Unknown`) is loss of *unknown amount*. [cols="1,3",options="header"] |=== | Fate | Reading -| `Present` | The field survives faithfully. (Lattice top.) -| `Attenuated(δ)` | Survives, fidelity degraded by stem:[\delta]. `Attenuated(0) = Present`. +| `Present` | The field survives faithfully. (Chain top.) +| `Attenuated(δ)` | Survives, fidelity degraded by stem:[\delta]. `Attenuated(0)` is identified with `Present` by normalization (A3, below). | `Predicated(P)` | (`quality` only.) Survives *only* as the value of predicate `P` over it — the checkbox. | `Dropped` | Withheld entirely. (Honest bottom.) -| `Falsified` | *Deceptive dual:* a value asserted faithful that is in fact false. (Lattice bottom; fails every honest floor. Not writable in source — a lowering fault, §6.) +| `Falsified` | *Deceptive dual:* a value asserted faithful that is in fact false. (Chain bottom; fails every honest floor. Not writable in source — a lowering fault, §6.) |=== -The fate order is a *chain* (R-2026-07-07 (A2); originally a lattice with a +The fate order is a *complete chain* (R-2026-07-07 (A2); v0.1 had a `Predicated ∥ Dropped` antichain): [stem] @@ -127,7 +145,7 @@ The fate order is a *chain* (R-2026-07-07 (A2); originally a lattice with a `Present` is top; `Attenuated(δ)` decreases as stem:[\delta] increases; `Predicated(P)` sits below every attenuation and above `Dropped` — a checkbox -retains at least as much of the quality as nothing at all. What the original +retains at least as much of the quality as nothing at all. What the v0.1 incomparability protected is preserved: a use-model needing the full quality rejects both `Predicated(P)` and `Dropped`; a use-model needing only the predicate accepts `Predicated(P)` but rejects `Dropped`. @@ -135,12 +153,17 @@ predicate accepts `Predicated(P)` but rejects `Dropped`. [NOTE] ==== *Ratification record (R-2026-07-07, ADR 0004; analysis in -`spec/notes/2026-07-07-l4-boundary-and-atoms.adoc`).* (A2) `Dropped ⊑ -Predicated` dissolves the antichain — one of the two machine-proved sources of -L4 failure — and makes the fate order a complete chain. (A3) the -`Attenuated(0) = Present` identification is *imposed by normalization at IR -ingest* (validators rewrite `Attenuated(Q 0)` to `Present`; composition -preserves normal forms), so carrier datatypes stay as-is. +`spec/notes/2026-07-07-l4-boundary-and-atoms.adoc`).* (A1) each deceptive +bottom is a *two-sided* zero of its coordinate's composition — in particular +`Dropped ▷ Falsified = Falsified`, replacing the v0.1 clause +`Dropped ▷ Falsified = Dropped` that let an upstream honest drop erase a +downstream lie and was the sole source of the algebra's non-commutativity +after erasing predicate and fusion labels. +(A2) `Dropped ⊑ Predicated`, dissolving the antichain. (A3) `Attenuated(0) = +Present` is *imposed by normalization at IR ingest*: validators rewrite +`Attenuated(Q 0)` to `Present` before grading, and composition preserves normal +forms (finite tropical addition reaches 0 only from 0+0), so carrier datatypes +stay as-is and stored and composed grades are normal forms. ==== `Predicated` is well-formed *only* on the `quality` field. A grade asserting @@ -157,15 +180,18 @@ The *bond* records the constitutive quality–bearer tie. | `Intact` | Bearer present, tie holds. (Top.) | `Withheld` | Bearer field dropped by projection; tie *recoverable in principle*. | `Severed` | Tie cut, quality asserted free-standing; *irrecoverable*. (Honest bottom.) -| `Misbound` | *Deceptive dual:* the quality presented as borne by a bearer that is not in fact its bearer. (Lattice bottom; fails every honest floor. Not writable in source — a lowering fault, §6.) +| `Misbound` | *Deceptive dual:* the quality presented as borne by a bearer that is not in fact its bearer. (Chain bottom; fails every honest floor. Not writable in source — a lowering fault, §6.) |=== -Ordered `Intact ⊐ Withheld ⊐ Severed ⊐ Misbound`. The distinction between `Withheld` and -`Severed` is the whole content of detaching versus projecting-away-the-bearer: -both leave no bearer, but the former is a clean named drop and the latter is a -constitutive severance. *This distinction surfaces in the type, not only the -grade* — detaching changes `Trope[S]` to `FloatingQuality`, so any downstream -operation needing a bearer fails to typecheck. +Ordered `Intact ⊐ Withheld ⊐ Severed ⊐ Misbound`. The distinction between +`Withheld` and `Severed` is the whole content of detaching versus +projecting-away-the-bearer: both leave no bearer, but the former is a clean +named drop and the latter a constitutive severance. *This distinction surfaces +in the type, not only the grade* — detaching changes `Trope[S]` to +`FloatingQuality`, so any downstream operation needing a bearer fails to +typecheck. The bond coordinate is *fibred over the bearer's fate* (HC-4): a +grade with the bearer `Present` and the bond `Severed`, or the bearer absent and +the bond `Intact`, is incoherent and unrepresentable at the validation boundary. === Coordinate 3 — merge (cardinality and honesty) @@ -184,17 +210,18 @@ honestly. Ordered `Single ⊐ Fused(τ) ⊐ Conflated` by recoverable plurality. `Conflated` is the *deceptive* collapse — the tag that would reveal the merge is discarded, so downstream is silently wrong about at least one constituent; `Fused(τ)` is -the *faithful* collapse. This is precisely the faithful/deceptive veridicality -axis of the typed-residual framework, instantiated on cardinality. +the *faithful* collapse. This is the faithful/deceptive veridicality axis of +the typed-residual framework, instantiated on cardinality. [IMPORTANT] ==== -*`Conflated` is reachable in the grade lattice but not by well-formed terms.* -The lattice is complete — it has its bottom — because the soundness story and the -use-model order require it as a formal element, and because a front end that -lowers some source operation to an untagged merge must have its output *named* -as `Conflated` when the validator rejects it (§6, §9). But no well-formed term -of the source language produces it: see the conflation decision in §6. +*`Conflated` is reachable in the grade carrier but not by well-formed terms.* +The carrier is complete — it has its bottom — because the soundness story and +the use-model order require it as a formal element, and because a front end +that lowers some source operation to an untagged merge must have its output +*named* as `Conflated` when the validator rejects it (§6, §9). But no +well-formed term of the source language produces it: see the conflation +decision in §6.1. ==== === The unit @@ -208,69 +235,163 @@ The unit grade is — full presence on every field, intact bond, no merge. `preserve` introduces it. +=== The nine effects and the nine atom families + +The vocabulary (`trope-particularity-workbench`) names *nine* effects. The +calculus realises them as follows. An *atom* is a grade that differs from +stem:[\varepsilon] in exactly one slot; atoms come in nine families, one per +non-unit coordinate value kind, and *every grade factors as a ▷-product of its +single-slot projections* (`EffectAtoms.lean`: `atom_factorization`, +`nine_families`, `family_realized`, `families_disjoint` — this is O1's +carrier-relative half, §10). + +[cols="2,1,1,2,1",options="header"] +|=== +| Vocabulary effect | Coordinate | Value | Calculus status | Veridicality + +| `p-preserving` | — | stem:[\varepsilon] | writable (`preserve`) | faithful +| `p-projecting` | fate / bond | `Dropped` / `Withheld` | writable (`project[S]`); composite of the `drop` atoms | faithful +| `p-collapsing` | fate | `Predicated(P)` | writable (`collapse[P]`); composite of `predicate` + `drop` | faithful +| `p-detaching` | bond | `Severed` | writable (`detach`); composite of `sever` + `drop` | faithful +| `p-attenuating` | fate | `Attenuated(δ)` | writable (`attenuate[δ]`); the `attenuate` atom | faithful +| `p-fusing` | merge | `Fused(τ)` | writable (`fuse[τ]`); the `fuse` atom | faithful +| `p-falsifying` | fate | `Falsified` | *not writable* — validation fault | deceptive +| `p-misbinding` | bond | `Misbound` | *not writable* — validation fault | deceptive +| `p-conflating` | merge | `Conflated` | *not writable* — validation fault (R-2026-06-22) | deceptive +|=== + +Two structure theorems fix this table rather than leaving it a list: + +* *Honest Generation.* The five atomic moves `attenuate`, `predicate`, `drop`, + `sever`, `fuse` together with stem:[\varepsilon] generate exactly the honest + fragment of each coordinate, and never produce a deceptive dual + (`Trope.Generation.{genFate,genBond,genMerge}`; Agda `TB.Honest.genFate` etc., + `honest-closed-▷`). +* *Veridicality Derivation.* The deceptive fragment has exactly three + inhabitants, one per coordinate kind — `Falsified`, `Misbound`, `Conflated` — + each the unique deceptive element of its coordinate + (`Trope.Veridicality.{fate,bond,merge}DeceptiveUnique`; Agda + `TB.Honest.{fate,bond,merge}DeceptiveUnique`). One cannot deceptively assert + a loss; the only deceptions are false value, false bearer, false singleness. + +So "seven effects" (six writable plus the conflation fault), which earlier +versions of this document used, and "nine effects" (the vocabulary) describe the +same carrier: nine atom families, of which six are writable surface effects +and three are faults. This document uses *nine* throughout. + == Composition and order — the normative laws === Composition Sequencing two effects (apply the second to the residual of the first) composes -grades by stem:[\triangleright], defined componentwise. +grades by stem:[\triangleright], defined slot-wise. -*Fate composition* (per field), the partial operation stem:[f_1 \triangleright f_2]: +*Fate composition* (per field), stem:[f_1 \triangleright f_2], on the ratified carrier: [source] ---- Present ▷ f = f f ▷ Present = f -Attenuated(δ₁) ▷ Attenuated(δ₂)= Attenuated(δ₁ + δ₂) -- tropical: losses add -Attenuated(_) ▷ Predicated(P) = Predicated(P) -- collapse subsumes prior fidelity loss -Attenuated(_) ▷ Dropped = Dropped +Attenuated(δ₁) ▷ Attenuated(δ₂)= Attenuated(δ₁ + δ₂) -- tropical: losses add; ⊤ absorbs ∞ absorbs finite +Attenuated(_) ▷ Predicated(P) = Predicated(P) -- collapse subsumes prior fidelity loss (and symmetrically) +Attenuated(_) ▷ Dropped = Dropped -- (and symmetrically) Predicated(_) ▷ Predicated(Q) = Predicated(Q) -- predicate of the bit; rare, defined for totality -Predicated(_) ▷ Dropped = Dropped -Dropped ▷ _ = Dropped -- nothing further can be lost from nothing +Predicated(_) ▷ Dropped = Dropped -- (and symmetrically) +Dropped ▷ Dropped = Dropped +Falsified ▷ _ = Falsified -- two-sided zero (A1) +_ ▷ Falsified = Falsified ---- -*Bond composition* — meet in `Intact ⊐ Withheld ⊐ Severed`, `Severed` absorbing. -*Merge composition* — meet in `Single ⊐ Fused ⊐ Conflated`, with -`Fused(τ₁) ▷ Fused(τ₂) = Fused(τ₁ ⊗ τ₂)` (nested honest merge, label is the -pair), and `Conflated` absorbing. +*Bond composition* — meet in `Intact ⊐ Withheld ⊐ Severed`, with `Misbound` a +two-sided zero. *Merge composition* — meet in `Single ⊐ Fused ⊐ Conflated`, +with `Fused(τ₁) ▷ Fused(τ₂) = Fused(τ₁ ⊗ τ₂)` (nested honest merge, label is the +pair) and `Conflated` a two-sided zero. + +The verified developments (§9.3) erase predicate and fusion labels: +`Predicated(P)` becomes `Predicated` and `Fused(τ)` becomes `Fused`, with all +other components unchanged. Erasure preserves composition. The laws below +apply to this erased grade carrier; equality of labels is outside the proof +contract. In particular, the right-predicate rule above need not commute on +labels: `Predicated(P) ▷ Predicated(Q) = Predicated(Q)`, whereas reversing the +operands gives `Predicated(P)`. Nested fusion pairs need neither commute nor +associate as literal labels: `(τ₁, τ₂)` differs from `(τ₂, τ₁)`, and +`((τ₁, τ₂), τ₃)` differs from `(τ₁, (τ₂, τ₃))`. -The laws stem:[g] must satisfy, to be enforced by the verified core (§8): +The laws the erased grade MUST satisfy, each enforced by the verified developments: [cols="1,4",options="header"] |=== | ID | Law -| *L1 (associativity)* | stem:[(g_1 \triangleright g_2)\triangleright g_3 = g_1 \triangleright (g_2 \triangleright g_3)]. -| *L2 (unit)* | stem:[\varepsilon \triangleright g = g = g \triangleright \varepsilon]. -| *L3 (bottom-absorption)* | In each coordinate, the *deceptive* lattice bottom is a *two-sided zero* of that coordinate's composition (R-2026-07-07 (A1)): `Falsified`, `Misbound`, and `Conflated` absorb from both sides — no honest absorber launders deception. The *honest* bottoms (`Dropped`, `Severed`) absorb from the left *within the honest fragment*, and `Attenuated(⊤)` is absorbing within the fidelity dimension. -| *L4 (monotonicity)* | stem:[\triangleright] is monotone in each argument w.r.t. the retention order stem:[\sqsubseteq] (§5). Composing after more loss never yields more retention. (*Holds in full on the ratified carrier* — R-2026-07-07 (A1)+(A2) removed the two machine-proved failure points of the original v0.1 carrier, the `Predicated ∥ Dropped` antichain and the `Dropped ▷ Falsified` clause; the §7 least-fixed-point argument is thereby restored. History and proofs: `spec/notes/2026-07-07-l4-boundary-and-atoms.adoc`, `verification/proofs/lean4/grade-boundary/L4Monotonicity.lean`.) -| *L5 (conflation infectiousness)* | Once the merge coordinate is `Conflated`, no composition restores `Fused` or `Single`. (A corollary of L3, stated separately because it is the non-compositionality-of-deceptive-channels result and the moral core.) +| *L1 (associativity)* | stem:[(g_1 \triangleright g_2)\triangleright g_3 = g_1 \triangleright (g_2 \triangleright g_3)]. (`Trope.Laws.gradeAssoc`; Agda `gmonoid-assoc`; Lean `GradeR.instCommMonoid`.) +| *L2 (unit)* | stem:[\varepsilon \triangleright g = g = g \triangleright \varepsilon]. (`Trope.Grade.{gradeUnitL,gradeUnitR}`; Agda `gmonoid-unit{L,R}`.) +| *L3 (bottom-absorption)* | Each *deceptive* bottom — `Falsified`, `Misbound`, `Conflated`, and fidelity's `Unknown` — is a *two-sided zero* of its coordinate's composition (R-2026-07-07 (A1)): no honest absorber launders deception, in either composition order. (Lean `FateA.falsified_two_sided_zero`, `GradeR.gBotR_two_sided_zero`; Agda `falsified-absorb{L,R}`, `misbound-absorbL`, `conflated-absorbL`, `deceptive-absorbs-▷`.) The *honest* bottoms (`Dropped`, `Severed`) absorb within the honest fragment, and `Attenuated(⊤)` within the fidelity dimension. +| *L4 (monotonicity)* | stem:[\triangleright] is monotone in each argument with respect to the retention order stem:[\sqsubseteq] (§5): composing after more loss never yields more retention. *Holds in full on the ratified carrier.* (Idris2 `Trope.Soundness.{fateL4MonoR,fateL4MonoL}`, `Trope.Order.{bondComposeMono,mergeComposeMono}`; Lean `FateA.comp_mono_{right,left}`; Agda `TB.Order.fateL4Mono{R,L}`.) History: strict L4 failed on the v0.1 carrier at exactly the two points (A1)/(A2) amended — `spec/notes/2026-07-07-l4-boundary-and-atoms.adoc`, `L4Monotonicity.lean` (`comp_not_monotone_{right,left}`, retained as theorems about the pre-ratification carrier). +| *L5 (deception infectiousness)* | Once any coordinate is at its deceptive bottom, no composition restores an honest value. A corollary of L3, stated separately because it is the non-compositionality-of-deceptive-channels result and the moral core; it covers `Conflated` (v0.1's statement), `Falsified` and `Misbound` alike. +| *L6 (commutativity)* | For grades with predicate and fusion labels erased, stem:[g_1 \triangleright g_2 = g_2 \triangleright g_1]. New at v0.2: on this ratified carrier the grade monoid is *commutative* (Lean `GradeR.instCommMonoid`, `FateA.comp_comm`; Agda `grade-comm`). These proofs carry no predicate or fusion labels and assert no equality between labelled grades. The v0.1 non-commutativity (`GradeBoundary.grade_mul_not_comm`) was an artefact of the clause (A1) removed. Order-sensitivity of erased loss-shapes MUST come from DAG structure (§9.1); label metadata may retain composition order. |=== [NOTE] ==== -L1–L2 make stem:[(\text{grades}, \triangleright, \varepsilon)] a monoid, hence -the effect system is a *graded monad* on the term category with this monoid as -its grade object. L4 makes the order a *lax* compatibility, which is what the -verdict subsumption (§5, §6) needs. None of L1–L5 is novel as a _shape_; the -content is that the three-coordinate loss-shape monoid is the right grade object -for trope-particularity, which §10-O1 marks as the open completeness question. +L1–L2 make stem:[(\text{erased grades}, \triangleright, \varepsilon)] a monoid, +L6 a commutative one; the effect system is a *graded monad* on the term +category with this erased monoid as its grade object. Label metadata is +retained separately and is not covered by these monoid equalities. +L4 is what the verdict subsumption +(§5–§6) and the recursion rule (§7) need. None of L1–L6 is novel as a _shape_; +the content is that this carrier is the right grade object for +trope-particularity, which §10-O1 marks as the open adequacy question. ==== +=== The cancellation structure + +Three further facts about the carrier are normative because downstream designs +(splitting, rejoining, any cut) must respect them (R-2026-06-23-02..04, as +amended by R-2026-07-07): + +[cols="1,4",options="header"] +|=== +| ID | Fact + +| *C1 (conicality)* | stem:[g_1 \triangleright g_2 = \varepsilon \Rightarrow g_1 = g_2 = \varepsilon]: nothing lossy composes back to no-loss. (Lean `GradeR.conical`, `FateA.conical`; Agda `grade-conical`.) +| *C2 (the cancellation boundary)* | Cancellation holds *only* on the finite-fidelity core stem:[\mathcal{C}] (the additive submonoid `Q ℕ ≅ (ℕ,+,0)` of the fidelity dimension) and fails on the honest-but-lossy and deceptive tiers alike: an element of the grade monoid is left-cancellative *iff* it is stem:[\varepsilon]. (Lean `Grade.grade_leftCancel_iff`, `GradeR.gradeR_leftCancel_iff`, with the per-element witnesses of `TierTwoComplete.lean`; Agda `TB.Tier.Q-cancelʳ` and the six `*-not-cancel` lemmas.) Consequence: a lossless *split / rejoin* can be cancellative only inside stem:[\mathcal{C}]; any such operator (§10, CO-1) MUST be stated against this boundary. +| *C3 (partition)* | `Dropped`, `Total` (stem:[\infty]), `Severed`, `Predicated`, `Withheld` and `Fused` are *honest* non-cancellative elements; `Falsified`, `Misbound`, `Conflated` and `Unknown` (stem:[\top]) are the *deceptive* ones. Absorbing is not the same as lying. (Lean `dropped_absorbing`, `fidelity_total_honest_not_cancel`; Agda `TB.Tier` classifiers.) Tier preservation under composition is *closure*, not a homomorphism: `tierOf (g ▷ h) = tierOf g ⊓ tierOf h` is false on fate even on the ratified carrier (`TB.Tier.fate-tier-meet-hom-fails`). +|=== + +=== The tropical factorisation + +A nontrivial monoid homomorphism stem:[\pi_R : (\mathrm{GradeR}, \triangleright, \varepsilon) \to (\Delta, +, Q\,0)] +onto the commutative tropical fidelity carrier exists and is +*veridicality-sighted*: `Dropped ↦ ∞` and `Falsified ↦ ⊤`, so the hom is blind +to *which honest* absorber acted but not to *whether the absorber was honest* +(`GradeFactorisationR.lean`: `piR_hom`, `piR_nontrivial`, `piR_surjective`, +`piR_sighted`). The naive hom that reads the attenuation payload off verbatim is +*not* a homomorphism on the ratified carrier (`phiId_not_hom`); the repair +squashes `Unknown` to the deceptive top. On the v0.1 carrier every such hom was +forced to collapse `Dropped` with `Falsified` (`GradeFactorisation.lean`, +`forced_collapse_general`) — a theorem about the pre-ratification carrier only. +This factorisation is a *precondition*, not a recursion result: whether a +fixpoint's grade lives in the commutative part is a CO-1 question (§10). + === The retention order and use-models Define stem:[\sqsubseteq] as the *retention order*: stem:[x \sqsubseteq y] means "stem:[y] retains at least as much particularity as stem:[x]" — i.e. stem:[y] is -higher (less lossy) in every coordinate lattice. stem:[\sqsubseteq] is the -componentwise product order; it is decidable because each coordinate lattice has -decidable order (finite, except the fidelity dimension stem:[\mathbb{N}\cup\{\infty,\top\}], -which is a decidable linear order with two adjoined tops). +higher (less lossy) in every slot. stem:[\sqsubseteq] is the slot-wise product +order; it is decidable because each coordinate is a decidable chain (the +fidelity dimension stem:[\mathbb{N}\cup\{\infty,\top\}] is a decidable linear +order with two adjoined tops). (`Trope.Laws.decGradeLte`; reflexivity and +transitivity in `Trope.Coords`/`Trope.Order`, `gradeLteTrans`.) A *use-model* stem:[U] declares a *floor* stem:[\mathrm{floor}(U)] — the minimum -retained particularity the use requires, possibly specified per field. The floor +retained particularity the use requires, possibly specified per slot. The floor is data the author *declares*; it is the only place a use enters the calculus. +The floor is a partial per-slot demand, not a grade value; HC-4 coherence is +enforced on edge grades, and an author MAY write an incoherent floor (each +demanded slot is then checked independently — harmless, but an author-error +surface, not covered by the unrepresentability claim). -== The seven effects as typing rules +== The six writable effects as typing rules The typing judgement is @@ -283,8 +404,8 @@ The typing judgement is types carry latent grade: stem:[A \xrightarrow{g} B] is "applying produces loss stem:[g]." The structural rules (variable, abstraction, application, `let`, `fix`) are standard; `let` is where composition enters and `fix` is in §7. The -six *writable* effects and the subsumption rule follow. (The seventh, -conflation, is treated in §6.1.) +six *writable* effects and the subsumption rule follow; the three deceptive +duals are not term formers (§6.1). .T-Preserve [%hardbreaks] @@ -346,13 +467,14 @@ leaves `bond` and `merge` unchanged. .... Γ ⊢ e₁ : A ! g₁ Γ ⊢ e₂ : A ! g₂ ───────────────────────────────────────────────────── -Γ ⊢ fuse[τ] e₁ e₂ : A ! (g₁ ⊔ g₂) ▷ label(τ) +Γ ⊢ fuse[τ] e₁ e₂ : A ! (g₁ ⊓ g₂) ▷ label(τ) .... where `label(τ)` sets `merge = Fused(τ)`, fates `Present` (the labelled blend is -faithful), `bond` the meet of the inputs'. The `⊔` joins the two input grades -(the fused value is no better than its worse constituent in any coordinate). The -tag `τ` is *required*: a fusion term with no tag does not parse (§6.1). +faithful), `bond` the meet of the inputs'. The stem:[\sqcap] meets the two input +grades in the retention order (the fused value is no better than its worse +constituent in any slot). The tag `τ` is *required*: a fusion term with no tag +does not parse (§6.1). .T-Sub — conservative weakening: you MAY always claim more loss than occurred [%hardbreaks] @@ -364,40 +486,44 @@ tag `τ` is *required*: a fusion term with no tag does not parse (§6.1). [NOTE] ==== -T-Sub weakens *downward* in retention only. Claiming *less* loss than occurred is -unsound and has no rule. This one-sidedness is what makes the verdict (§6) a -safe over-approximation. +T-Sub weakens *downward* in retention only. Claiming *less* loss than occurred +is unsound and has no rule. This one-sidedness is what makes the verdict (§6) a +safe over-approximation — and it is also why the calculus, as it stands, +certifies *sufficiency* (enough retained) and not *discretion* (no more than a +ceiling retained): a declared grade is a lower bound on retention, never an +upper bound. A ceiling verdict needs the dual theorem (§10, O6). ==== == The conflation decision, and the verdict -=== Decision: conflation is not a source primitive +=== Decision: deception is not a source primitive [cols="1,4",options="header"] |=== | ID | Decision (dated, for the decision-log) -| *R-2026-06-22* | Conflation SHALL NOT be a writable primitive. `fuse[τ]` *requires* a tag; an untagged merge is a syntax error and does not elaborate. `Conflated` exists only as the absorbing bottom of the merge coordinate (§3.3); a well-formed term never produces it. Conflation therefore arises *only* as a *lowering fault*: when a front end lowers a source operation to a merge and fails to supply a tag, the resulting IR is malformed and the validator (§9) rejects it, *naming* the offending node's merge as `Conflated`. The tropechecker is, operationally, a *conflation detector at the lowering boundary*. +| *R-2026-06-22* | Conflation SHALL NOT be a writable primitive. `fuse[τ]` *requires* a tag; an untagged merge is a syntax error and does not elaborate. `Conflated` exists only as the absorbing bottom of the merge coordinate (§3.3); a well-formed term never produces it. Conflation therefore arises *only* as a *lowering fault*: when a front end lowers a source operation to a merge and fails to supply a tag, the resulting IR is malformed and the validator (§9) rejects it, *naming* the offending node's merge as `Conflated`. The same holds, by construction, for `Falsified` and `Misbound` (the validator rejects them as not writable in the *prevent* profile). The tropechecker is, operationally, a *deception detector at the lowering boundary*. |=== This is the door-too-small reading: the dangerous state exists in the semantics but is structurally unreachable by well-formed terms. It makes the moral content -— _do not silently merge particulars_ — a validation error rather than a -guideline. +— _do not silently merge particulars, do not misattribute, do not substitute_ — +a validation error rather than a guideline. [IMPORTANT] -.Normative variant (conflation as a verdict-boundary primitive) +.Normative variant (deception as a verdict-boundary primitive) ==== Implementations MAY instead admit conflation as a writable primitive caught at the verdict rather than at validation. Exactly three things change, and nothing else: -. *Add* a rule `T-Conflate : Γ ⊢ e₁ : A ! g₁, Γ ⊢ e₂ : A ! g₂ ⟹ Γ ⊢ conflate e₁ e₂ : A ! (g₁ ⊔ g₂) ▷ unlabel`, where `unlabel` sets `merge = Conflated`. +. *Add* a rule `T-Conflate : Γ ⊢ e₁ : A ! g₁, Γ ⊢ e₂ : A ! g₂ ⟹ Γ ⊢ conflate e₁ e₂ : A ! (g₁ ⊓ g₂) ▷ unlabel`, where `unlabel` sets `merge = Conflated`. . *Relax* T-Fuse so an untagged merge is well-formed and elaborates to `conflate`. . *Move* the conflation check from the validation boundary (§9) to the verdict (§6.2): a `Conflated` grade is then rejected only when `floor(U)` demands `merge ⊒ Fused`. The recommended reading (R-2026-06-22) is _prevent_; the variant is _detect_. -An implementation MUST pick one and state which in its conformance profile. +An implementation MUST pick one and state which in its conformance profile. The +reference and fast cores ship *prevent*. ==== === The verdict @@ -412,7 +538,7 @@ Given a closed program with final grade stem:[g] and a use-model stem:[U]: If the check fails, the verdict is `p-insufficient`, and the report MUST carry a *witness*: the operation (DAG edge, §9) whose composition first pushed the -running grade below stem:[\mathrm{floor}(U)] in some coordinate. This witness is +running grade below stem:[\mathrm{floor}(U)] in some slot. This witness is the trope-particularity analogue of the invariant-path argmin — it names the edge to repair, not merely that repair is needed. @@ -430,57 +556,74 @@ comonad form an adjunction whose unit/counit are exactly produce/demand is a == General recursion, and why it does not break the checker -`fix` is what makes the term language Turing complete. Its grade rule takes the -*least fixed-point grade* of the body's grade functional: +`fix` is what makes the term language Turing complete. Its grade is the +*tightest declaration the rule can certify*: in the retention order, the +*greatest post-fixed point* of the body's grade functional (equivalently, the +least fixed point in the loss order — v0.1's phrasing). The functional +stem:[F(\gamma)] — the body's derived latent grade under the assumption that the +recursive binder has latent grade stem:[\gamma] — is computable, and monotone in +stem:[\gamma] by L4; each coordinate is a complete chain; so Knaster–Tarski gives +stem:[\mathrm{gfp}\,F = \bigsqcup\{\gamma : \gamma \sqsubseteq F(\gamma)\}]. -[%hardbreaks] -.... -Γ, x : (A ─g→ B) ⊢ e : (A ─g→ B) g = lfp(λγ. grade-of(e)[γ]) -───────────────────────────────────────────────────────────────── -Γ ⊢ fix x. e : (A ─g→ B) ! ε -.... +*The rule (T-Fix-Decl).* The author declares stem:[\gamma]; the checker accepts +iff + +[stem] +++++ +\gamma \;\sqsubseteq\; F(\gamma) +++++ + +— decidable (stem:[F] is computable on grades, stem:[\sqsubseteq] is +decidable), and no fixed point is ever computed. Kleene iteration and +ω-continuity are not needed: existence by Knaster–Tarski, checking by the +post-fixed-point test, soundness by induction on call depth of a terminating +run (`spec/notes/2026-07-07-co1-operational-model.adoc` §4). -The least fixed point exists because each coordinate lattice is complete and, by -*L4*, the grade functional is monotone. A recursive trope-transformer that can -attenuate without bound has fidelity grade stem:[\top] — and that is *correct*, -not a failure: an unbounded loop of lossy steps yields an unknown residual, the -checker reports stem:[\top], and any use-model demanding better than stem:[\top] -rejects it. +A recursive trope-transformer that can attenuate without bound has fidelity +grade stem:[\top] — and that is *correct*, not a failure: no finite-δ +signature is a post-fixed point, the strongest accepted signatures sit at +`Attenuated(∞)`/`Attenuated(⊤)`, the checker reports stem:[\top], and any +use-model demanding better rejects it. [IMPORTANT] ==== *Turing-completeness does not break the checker; it means some grades are stem:[\top], and stem:[\top] is an honest answer.* The checker stays total -because it computes on the grade lattice, never on the term. The undecidability +because it computes on the grade carrier, never on the term. The undecidability that Rice's theorem guarantees is discharged honestly into the stem:[\top] -element, exactly as the Aletheia design discharges it into an honest "cannot -guarantee." +element. ==== *Inference versus checking.* Synthesising the minimal grade of an arbitrary fixpoint is undecidable. The checker SHALL therefore be *bidirectional*: grades are *checked* against *declared* loss-signatures at every recursive and effectful -boundary (the author annotates the loss signature of a recursive -trope-transformer, as one annotates an effect signature), and *inferred* only -through the straight-line, non-recursive fragment (decidable, convenient). -Declared signatures at the boundaries; inference in between. +boundary, and *inferred* only through the straight-line, non-recursive fragment. +Declared signatures at the boundaries; inference in between. The T-Fix-Decl side +condition is an obligation of the *front end* at its recursive boundaries; the +IR checker sees only the declared signature. + +*Status.* The operational model this section relies on — the core language +λ-trope, its instrumented small-step semantics with tagged values, and observed +retention stem:[\rho] read off the output tag — is DESIGNED +(`spec/notes/2026-07-07-co1-operational-model.adoc`). Its mechanisation is OPEN +(§10, CO-1): Theorem B's `fix` case is NOT-REACHED and not postulated. == Soundness, and the firewalls Let stem:[\rho(\text{in}, \text{out})] be the *observed retention* of one -execution: the grade read off by comparing the input and output trope records. -The verified core (§9) targets: +execution: the grade read off by comparing the input and output trope records +(in λ-trope, the output value's tag). The results, with their status: -[cols="1,4",options="header"] +[cols="1,4,1",options="header"] |=== -| ID | Statement +| ID | Statement | Status -| *Grade soundness* | If stem:[\Gamma \vdash e : A \mathbin{!} g] then for every well-typed input, stem:[g \sqsubseteq \rho(\text{in}, \text{out})]: the declared grade never claims more retention than the execution delivers (equivalently, it over-approximates loss). -| *Verdict soundness* (corollary) | If the checker reports `p-sufficient` (i.e. stem:[\mathrm{floor}(U)\sqsubseteq g]) then by transitivity stem:[\mathrm{floor}(U)\sqsubseteq \rho], so the real residual meets the use-model. +| *Grade soundness* | If stem:[\Gamma \vdash e : A \mathbin{!} g] then for every well-typed input, stem:[g \sqsubseteq \rho(\text{in}, \text{out})]: the declared grade never claims more retention than the execution delivers (it over-approximates loss). | *Exact lowering:* PROVED (`Trope.Soundness.soundFromExact`). *β/let core:* PROVED, with the grade preserved exactly (Agda `TB.Reduction`, `TB.Substitution.cut-preserves-grade`). *Conservative lowering and `fix`:* OPEN — CO-1 mechanisation (§10). +| *Verdict soundness* (corollary) | If the checker reports `p-sufficient` (i.e. stem:[\mathrm{floor}(U)\sqsubseteq g]) then by transitivity stem:[\mathrm{floor}(U)\sqsubseteq \rho], so the real residual meets the use-model. | PROVED, given grade soundness (`Trope.Soundness.verdictSound`; `subSound` for T-Sub). |=== [WARNING] -.Two firewalls — state both, do not let the theorem launder them +.Three firewalls — state all three, do not let the theorems launder them ==== . *Soundness, not completeness.* The checker MAY be conservative: it MAY report `p-insufficient` where the true residual would in fact have sufficed. This is the @@ -490,9 +633,13 @@ safe direction and is acceptable. No completeness is claimed. *IR-level* grades. It does *not* prove that a front end's claim "this source operation _is_ a `collapse[P]`" is true. *Lowering correctness is a separate, per-front-end proof obligation* (§10-O2) and is NOT discharged by this theorem. -This is the same firewall as "the analogy is not an instance": the core's -guarantee is conditional on faithful lowering, and that conditionality lives in -the spec, in the open, not hidden in a footnote. + +. *Veridicality is declared and propagated, not checked.* The checker cannot +decide whether a value claimed faithful is in fact false; that needs ground +truth the IR does not carry. What the calculus guarantees instead is L3/L5: +deceptive grades are two-sided zeros, do not compose away, and fail every honest +floor. The precise statement, and the interface a deployment may bind to do +better, is §10-O5. ==== == The portable tropechecker @@ -502,7 +649,7 @@ depends only on a language-neutral interchange. === The Trope IR -The portable artifact is a *Trope IR*: a labelled DAG. +The portable artefact is a *Trope IR*: a labelled DAG. * *Nodes* are property-instances, each carrying its field-presence over stem:[\Phi] and its type tag (`Trope[S]`, `FloatingQuality`, or a collapse @@ -511,70 +658,96 @@ codomain). * A distinguished *use-model node* carries stem:[\mathrm{floor}(U)]. The IR's *canonical wire format SHALL be a JSON-schema-validated document* -(`schemas/trope-ir.schema.json`); an AsciiDoc normative spec accompanies it; an -*OPTIONAL* Nickel authoring contract MAY be offered front-side. (This mirrors, -deliberately and verbatim, the invariant-path I/O-contract decision: -author-side contracts are courtesy, generated from the schema; the schema is the -trust boundary.) The grade algebra — stem:[\triangleright], stem:[\sqsubseteq], -and stem:[\mathrm{floor}] — SHALL be specified *in the IR spec itself*, -language-neutrally, so that two independent checker implementations agree by -construction. +(`schemas/trope-ir.schema.json`; normative prose in `spec/trope-ir.adoc`, +version 0.2 — R-2026-07-07 changed verdict semantics only, and implementations +MUST accept `0.1` and `0.2` documents and grade both under 0.2 semantics after +normalization). An *OPTIONAL* Nickel authoring contract MAY be offered +front-side; the schema is the trust boundary. The grade algebra — +stem:[\triangleright], stem:[\sqsubseteq], and stem:[\mathrm{floor}] — is +specified in the IR spec itself, language-neutrally, so that two independent +checker implementations agree by construction. Order-sensitivity of erased +loss-shapes lives in the DAG (routing, multi-parent nodes); predicate and +fusion labels may retain composition order (L6). === The checker as a pure function The tropechecker is a *pure function from Trope IR to a verdict object*: `p-sufficient` / `p-insufficient`, plus the witness edge (§6.2). It performs -grade composition over the DAG and the final floor-subsumption. *It MUST NOT -parse, execute, or otherwise depend on source.* That independence is what makes -it portable: it is a checker *of the IR*, and the IR is the contract. +normalization (A3), validation (HC-4 coherence; the prevent profile's rejection +of deceptive values), grade composition over the DAG, and the final +floor-subsumption. *It MUST NOT parse, execute, or otherwise depend on source.* [cols="1,3",options="header"] |=== | Property | Consequence -| *Independence* | Own repository, own versioned IR schema, own conformance suite. The Turing-complete language is the *first* front end that lowers to the IR — dogfooding without coupling. -| *Multi-producer* | A static analyser for an *existing* language MAY emit Trope IR for code it did not author (e.g. lowering a dataframe pipeline's operations to `project` / `collapse` / `fuse` edges). The same checker then trope-checks it. -| *Honest trust boundary* | Front-end grade annotations are *claims*. The checker validates the *composition* of claims; it cannot validate that a source operation truly *is* a given effect. That is lowering correctness (§10-O2), per front end. +| *Independence* | Own repository, own versioned IR schema, own conformance suite. The Turing-complete language (Haec) is the *first* front end that lowers to the IR — dogfooding without coupling. +| *Multi-producer* | A static analyser for an *existing* language MAY emit Trope IR for code it did not author (e.g. lowering a dataframe pipeline's operations to `project` / `collapse` / `fuse` edges). The same checker then trope-checks it. The store (`vocarium`) and the query layer (`hermeneia`) are producers of this kind. +| *Honest trust boundary* | Front-end grade annotations are *claims*. The checker validates the *composition* of claims; it cannot validate that a source operation truly *is* a given effect (O2) or that a claimed-faithful value is true (O5). |=== -=== Verified core, fast core, conformance suite - -The *reference* tropechecker SHOULD be an Agda development that *defines* the -loss-shape category, *proves* L1–L5 and the decidability of stem:[\sqsubseteq], -and *proves* grade soundness (§8). That Agda artifact is the portable -*semantics*. The *shipping* checker (Rust is the recommended target, continuing -the shape-IR lineage, for speed) is validated against the Agda reference by a -*conformance suite*: a corpus of `IR-fragment → expected-verdict` pairs that any -implementation MUST pass. The particularity trainer is, in effect, a *human* +=== Verified kernel, executable reference, fast core, conformance suite + +Per the estate's proof-kernel ruling of 2026-10-12 (ADR 0005), the roles are: + +* *Normative kernel — Agda* (`verification/proofs/agda/theorem-b/`, `--safe + --without-K`, zero postulates): the carrier, the laws, the cancellation + boundary, the intrinsic calculus, substitution and β/let subject reduction + (Theorem B); the CO-1 mechanisation extends it. This is the portable + *semantics*: "portable" means *means-the-same-everywhere* because the meaning + is a checked artefact. +* *Executable reference — Idris2* (`verification/proofs/idris2/`, `src/idris2/`): + the same carrier and laws in quantitative types, and the reference + `tropecheck` executable built on them. The verified core + (`verification/proofs/idris2/Trope/*`) is `%default total`; the executable’s + JSON parser, decoder and checker driver (`src/idris2/`) are `%default covering`, + because a parser is not structurally total without fuel. Neither uses + `believe_me`, `assert_total` or `postulate`. +* *Provenance — Lean 4 + Mathlib* (`verification/proofs/lean4/`): the + grade-algebra boundary and its ratified mirror, the atom factorisation and the + tropical factorisation probe — the Mathlib-facing results, retained with + their axiom audits: no `sorryAx`, no user axiom; `propext`, `Quot.sound` and, + in three theorems (`nine_families`, `Q_add_left_cancel`, + `atten_cancel_on_normalForms`), `Classical.choice`. +* *Fast core — Rust* (`src/rust/`, dependency-free): the shipping checker, + validated against the reference bit-for-bit over the conformance corpus. + +The *conformance suite* (`tests/conformance/`) is a corpus of +`IR-fragment → expected-verdict` pairs plus schema-invalid documents that MUST be +rejected at the named slot; any implementation claiming conformance MUST pass it +in its declared profile. The particularity trainer is, in effect, a *human* conformance suite for the taxonomy; the machine suite is its formal sibling. -"Portable" thereby means *means-the-same-everywhere* — because the meaning is a -checked Agda artifact and the suite enforces agreement — not merely -*runs-everywhere*. == Open obligations and falsifiers -[cols="1,4",options="header"] +[cols="1,4,1",options="header"] |=== -| ID | Obligation / falsifier - -| *O1 (completeness of the seven)* | The claim that the writable effects are _exhaustive_ is, at present, a well-chosen list, not a theorem. *Falsifier:* exhibit a particularity-affecting operation that is none of the six writable forms (plus the conflation fault). *Upgrade path:* if the three axes — loss-structure × bond-integrity × cardinality/honesty — are the true generators, *derive* the typology as the inhabited cells of their product and *prove* exhaustiveness relative to those axes, turning the list into a theorem (the same move that turned "three layers in a pipeline" into "one substrate, two analyses, one law"). This decision SHOULD be taken *before* the IR schema is frozen. -| *O2 (lowering correctness)* | Per front end: a proof that each source construct it lowers to an effect edge *is* that effect. Separate from grade soundness (§8, firewall 2). Not dischargeable by the core. -| *O3 (the produce/demand adjunction)* | Whether the producing graded monad and the demanding graded comonad form an adjunction with produce/demand as unit/counit. Conjecture; requires the grade category pinned (O1) and the triangle laws checked. Until then, the verdict is a subsumption, *not* an adjunction cancellation. -| *O4 (fidelity carrier)* | Whether the fidelity dimension stem:[\mathbb{N}\cup\{\infty,\top\}] suffices, or a transfinite/coinductive carrier is needed once iterated attenuation must be ordered beyond stem:[\omega] (the standing `Conat`-vs-tag fork from the choreographic-typing line). Defer until a second instance demands it. +| ID | Obligation / falsifier | Status + +| *O1-carrier (exhaustiveness relative to the carrier)* | Every grade factors as a ▷-product of single-slot projections drawn from the nine atom families; the effect typology is exhaustive *relative to the three-coordinate carrier*. | PROVED (`EffectAtoms.lean`: `atom_factorization`, `nine_families`, `family_realized`, `families_disjoint`). +| *O1-coord (metaphysical adequacy)* | Are `fate`, `bond`, `merge` themselves exhaustive as ways to individuate-and-lose? A claim about the world, not the algebra. *Falsifier:* a particularity-affecting operation that no atom family captures. *Live probe:* the transposition of a quality between bearers (the classic *swapping* problem) is not expressible — it is neither `sever` nor `fuse` nor any bond value — and a *bond-transfer* move with an honest (labelled) and a deceptive (`Misbound`) form is the candidate tenth family. Either it reduces to the existing atoms or it is a fourth generator; the adequacy argument must say which. | OPEN (workbench WP-5). +| *O2 (lowering correctness)* | Per front end: a proof that each source construct it lowers to an effect edge *is* that effect. Separate from grade soundness (§8, firewall 2). Not dischargeable by the core. | OPEN per producer; no producer has discharged it. +| *O3 (the produce/demand adjunction)* | Whether the producing graded monad and the demanding graded comonad form an adjunction with produce/demand as unit/counit. Requires the triangle laws checked against the ratified carrier (now pinned, so no longer gated by O1-carrier). Until then, the verdict is a subsumption, *not* an adjunction cancellation. | OPEN (conjecture). +| *O4 (fidelity carrier)* | Whether stem:[\mathbb{N}\cup\{\infty,\top\}] suffices for ordering iterated attenuation. | RESOLVED (ADR 0004): it does — transfinite carriers would require transfinitely deep `fix` nesting, which finitary syntax cannot express. Whether the carrier should be a *parameter* (any resource algebra with two adjoined tops) rather than this one instance is a separate design question recorded in ADR 0005. +| *O5 (the veridicality oracle)* | *Remark O5-a (IR-relative undecidability).* A valid Trope IR is a set of claims. For any IR document stem:[D] and any slot, there exist two worlds — one in which the claimed value is the value the trope in fact had, one in which it is not — inducing the same stem:[D]; since the checker is a pure function of stem:[D], no checker can decide veridicality. What is guaranteed instead is L3/L5. *Interface.* An implementation MAY bind a *veridicality oracle*, an external judgement `Oracle ⊨ record r faithful-to trope t` (per slot), subject to: *O5-1 (soundness)* if the oracle affirms a slot, the honest grade claimed for it is true of the world, and the oracle MUST NOT affirm a `Falsified`, `Misbound` or `Conflated` situation; *O5-2 (attestation)* every oracle verdict MUST be carried as evidence — who checked, against what access to the world, when — and that attestation enters the `record` slot's provenance, not the quality's value; *O5-3 (no laundering)* an oracle verdict upgrades *confidence*, never *grade*: a checked `Attenuated(δ)` is still `Attenuated(δ)`. *Falsifier:* a deployment where an interface satisfying O5-1..3 lets a deceptive grade reach `p-sufficient` against an honest floor. *Upgrade path:* mechanise O5-1 as a side condition on an `Oracle`-indexed variant of the verdict judgement. Vocarium's warrants are O5-2 attestations; Hermeneia's *licensed* band is the verdict band O5-backed claims occupy. | DEFINED (adopted from the workbench proposal of 2026-07-17 by ADR 0005); mechanisation OPEN. +| *O6 (the ceiling verdict)* | New at v0.2. The verdict certifies sufficiency only. A *ceiling* use-model — "no more than this may be retained" (the privacy direction: a `Withheld` bond is a recoverable, hence still-personal, record; `Severed` is not) — needs the dual theorem stem:[\rho \sqsubseteq g_{\mathrm{ceiling}}], which T-Sub's one-sidedness does not give for conservative lowering. *Deliverable:* either the dual verdict proved for the exact-lowering fragment and stated as unavailable for the conservative one, or a second, upper-bound grade on edges. | OPEN. +| *CO-1 (the operational model)* | The calculus's reduction dynamics for `fix` and routing. The grade algebra is not at fault (the gfp endpoint is ▷-fixed and tier-stable). | DESIGNED (λ-trope, tagged values, T-Fix-Decl: `spec/notes/2026-07-07-co1-operational-model.adoc`); MECHANISATION OPEN (Agda, steps 1–5 of that note's §6; closes Theorem B Target 3 and conservative grade soundness). |=== == Provenance of the ideas (so nothing is overclaimed) Graded monads, coeffects, and effect rows are established machinery -(Katsumata; Gaboardi; Petricek, Orchard, Mycroft; Uustalu). Tropes as abstract -particulars are established metaphysics (Williams; Campbell). The -graded-monad-for-loss reading is the echo-types line. What is assembled *here* — -a graded effect discipline tracking *which kind* of particularity-loss an -operation inflicts on a provenance-enriched metaphysical trope, with -conflating/fusing as the deceptive/faithful collapse, checked against a -use-model coeffect demand, lowered to a language-neutral IR — is, as a *named -combination*, the contribution. The atoms are mostly already named; the -unclaimed ground is the unification and the three-coordinate loss-shape grade. +(Katsumata; Gaboardi; Petricek, Orchard, Mycroft; Uustalu). Property-instances +as particulars are established metaphysics (Williams; Campbell) and established +applied ontology (UFO's moments, DOLCE's qualities, BFO's specifically dependent +continuants). The graded-monad-for-loss reading is the echo-types line. What is +assembled *here* — a graded effect discipline tracking *which kind* of +particularity-loss an operation inflicts on a provenance-enriched +property-instance, with the three deceptive duals as faults rather than moves, +checked against a use-model coeffect demand, lowered to a language-neutral IR — +is, as a *named combination*, the contribution. The atoms are mostly already +named; the unclaimed ground is the unification, the three-coordinate loss-shape +grade, and the structure theorems (§3.5, §4.2) that fix it. == Worked check (the duck, end to end) @@ -583,15 +756,17 @@ This is `collapse[isQuack]`: the residual grade has `fate(quality)=Predicated(isQuack)`, all other fields `Dropped`, `bond=Withheld`, `merge=Single`. Against a use-model whose floor demands the call's spectral content — `floor(U)` requires `quality ⊒ Attenuated(δ)` for some finite stem:[\delta] -— we check `floor(U) ⊑ g`. Since `Predicated(isQuack)` is *incomparable to and -below* any `Attenuated(δ)` in the fate lattice (§3.1), the check fails: verdict -`p-insufficient`, witness = the `collapse` edge. The same call recorded losslessly -with ring number, pond, date and weather is `preserve`, grade stem:[\varepsilon], -which dominates every floor: `p-sufficient`. The trainer's intuition and the +— we check `floor(U) ⊑ g`. Since `Predicated(isQuack)` sits *strictly below* +every `Attenuated(δ)` in the fate chain (§3.1), the check fails: verdict +`p-insufficient`, witness = the `collapse` edge (conformance fixture +`duck-collapse`). The same call recorded losslessly with ring number, pond, date +and weather is `preserve`, grade stem:[\varepsilon], which dominates every +floor: `p-sufficient` (`duck-preserve`). The trainer's intuition and the calculus agree, which is the point. ''' -_Suggested CHANGELOG line:_ `docs: pin trope-particularity calculus v0.1 -(three-coordinate loss-shape grade; six writable effects + conflation-as-fault -[R-2026-06-22]; composition laws L1–L5; verdict = floor-subsumption; grade -soundness target + lowering firewall; portable Trope IR)._` +_CHANGELOG line:_ `docs(spec): consolidate the calculus at v0.2 — nine effects +with the atom table, ratified carrier inline (A1–A3), L6 commutativity and the +cancellation structure as laws, the tropical factorisation recorded as sighted, +§7 restated as greatest post-fixed point with T-Fix-Decl, O5 defined and O6 +(ceiling verdict) opened, prover roles per ADR 0005._ diff --git a/tests/e2e.sh b/tests/e2e.sh index 8cf64b0..6ea94d7 100755 --- a/tests/e2e.sh +++ b/tests/e2e.sh @@ -2,141 +2,14 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# RSR Standard E2E Test Template +# Run the checker end to end against the shared conformance corpus: IR verdicts, +# witness edges and coordinates, and rejection of schema-invalid input. +# Build the reference checker with `just trope-build` first, or select an +# alternative compiled checker with TROPECHECK_BIN (as `just trope-rust` does). +# The conformance runner checks jq and the binary and propagates failures. # -# End-to-end tests validate the full pipeline: build → run → verify output. -# Customise this file for your project. Delete the examples that don't apply. -# -# Usage: -# bash tests/e2e.sh -# just e2e -# -# Merge requirements (STANDING): All 6 test categories must pass before merge: -# P2P, E2E (this file), aspect, execution, lifecycle, benchmarks - +# Usage: bash tests/e2e.sh or just e2e set -euo pipefail SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" -PROJECT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)" - -PASS=0 -FAIL=0 -SKIP=0 - -# ─── Colour helpers ────────────────────────────────────────────────── -green() { printf '\033[32m%s\033[0m\n' "$*"; } -red() { printf '\033[31m%s\033[0m\n' "$*"; } -yellow(){ printf '\033[33m%s\033[0m\n' "$*"; } -bold() { printf '\033[1m%s\033[0m\n' "$*"; } - -# ─── Assertion helpers ─────────────────────────────────────────────── - -# check