diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 56de41b..b47f846 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -27,6 +27,10 @@ on: paths: - 'verification/proofs/lean4/**' - 'verification/proofs/agda/**' + - 'verification/pwg.json' + - 'scripts/pwg-derive.sh' + - 'scripts/pwg-check.sh' + - 'docs/status/PROOF-STATUS.adoc' - 'tests/lib/strip-proof-comments.awk' - '.github/workflows/proofs.yml' pull_request: @@ -43,6 +47,27 @@ jobs: # Pure grep over the Lean sources: no toolchain, seconds to run, and it is the # gate that makes "sorry-free" checkable rather than merely stated. Mirrors the # `verify-all` recipe in build/just/proofs.just — keep the two in step. + # The Proof Witness Grade record. PROOF-POLICY §8.4 rule 2: a grade is computed + # from the receipts and the §2.2 records, and "a gate or a bot may recompute it + # at any time and reports the computed value". This job is that recomputation. + # It needs no prover: the kernels already ran, and their receipts are the input. + pwg-record: + name: "PWG record: derived, not asserted" + runs-on: ubuntu-latest + timeout-minutes: 5 + steps: + - uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + - name: Derive every grade and fail on drift + run: | + set -euo pipefail + bash scripts/pwg-check.sh + echo + bash scripts/pwg-derive.sh --census + - name: Prove the gate can fail (canonical-wrongness canaries) + run: bash scripts/test-gate-falsifiability.sh + lean-source-honesty: name: "Lean sources: no sorry / admit / native_decide / user axiom" runs-on: ubuntu-latest @@ -100,8 +125,12 @@ jobs: # 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. + # Smoke.agda typecheck under the PROOF-POLICY §2.1 invocation + # `--safe --without-K --cubical-compatible` — the flags the step below actually + # passes — exit 0 (~100 s). A checksum mismatch fails loudly rather than silently + # testing a different stdlib. NOTE: this job's display name still reads + # "(--safe --without-K)", understating the flags in force; renaming a check is an + # owner decision, since the name is what appears in the checks UI. agda-theorem-b: name: "Agda Theorem B (--safe --without-K)" runs-on: ubuntu-latest diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 6bfde1e..976f692 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,8 +8,184 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Fixed + +* *A comment marker inside a string literal is no longer read as a comment +(2026-11-09).* `+tests/lib/strip-proof-comments.awk+` tracked block comments with +no notion of string literals, so `+def m : String := "/-"+` opened a block +comment that swallowed the rest of the file — and awk still exited `+0+`. An +`+axiom+` declared after such a line was invisible to *every* gate that scans +through the stripper. Measured: three shapes reproduce it (`+"/-"+`, the raw +string `+r"/-"+`, and the hash-delimited `+r#"/-"#+`), and the swallow reached +five call sites, two of them in CI — `+proofs.yml+`'s `+lean-source-honesty+` job +(which exited `+0+` on a planted tree) and its `+declared-axioms+` extraction, +which produced an EMPTY list and so fed the deep axiom audit's own +"never excused" guard with nothing. ++ +Strings are now consumed as units and emitted as `+""+`, which also means a +string whose *content* is the word `+sorry+` can no longer trip the gate. Char +literals are skipped whole, guarded so that primed identifiers (`+h'+`, `+n'+`) +are untouched — that clause is load-bearing, not cosmetic: without it the +`+'"'+` in `+src/idris2/Checker/Json.idr+` opens a string and re-creates the hole +in a different file. An unterminated comment or string is now a loud `+exit 1+`: +a truncated scan must never be reported as a clean one. `+tests/aspect_tests.sh+` +had one `+|| true+` covering the whole pipeline, which would have swallowed that +exit; it now covers the `+find+` and the `+grep+` (no match is the good case) but +never the awk. ++ +Verified: all three exploit shapes now expose the `+axiom+`; the eight real +Lean proof files produce byte-identical stripper output; 38 scanned files produce +no new failure; `+Admitted+` planted behind a string is caught where it was +previously hidden. Lean 4's *nested* block comments are a known remaining +limitation, recorded in the file — that direction fails loudly, not open, so it +is a separable change. + +* *Three fail-open paths in this PR's own gates (2026-11-09).* All three were +mine, found by review and reproduced before being fixed. ++ +`+scripts/pwg-check.sh+` skipped rule 5 silently when the status file was +absent, and still printed "published table and census match". Renaming +`+PROOF-STATUS.adoc+` was therefore enough to forge *every* grade in it and exit +`+0+`; an empty ledger `+{}+` passed the same way, because rules 2–4 read a +`+jq+` failure as "nothing wrong". A missing status file is now drift, every +rule whose verdict comes from a command substitution fails when it fails, and +the control-character check no longer depends on `+grep -P+` being compiled in +(`+2>/dev/null+` had turned a `+grep+` without `+-P+` into a silent pass). ++ +`+scripts/test-gate-falsifiability.sh+` did not check its *own* fixtures. A +canary whose `+jq+` program failed wrote an empty ledger, the gate rejected it +for being invalid JSON rather than for the planted drift, and the canary scored +PASS without exercising its target — measured on all six `+jq+`-driven canaries. +A program that silently selected nothing (a renamed receipt key) left the ledger +unchanged and passed the same way. Each canary now fails if its own transform +fails, fails if the transform changes nothing, and — for a reject case — +declares the reason it expects, so a rejection for an unrelated reason no longer +counts. A dropped canary group used to report `+10/10+` and exit `+0+`; the case +count is now part of the claim. ++ +Added canary 19, the *meta-canary*: it breaks one canary's own `+jq+` program and +asserts the suite reports FAILURE. It fails against the pre-fix harness, which +is what makes it evidence rather than decoration. The suite is *19/19*, and all +four breakages — a corrupted transform, a no-op fixture, a dropped group, and a +suite that cannot see its own breakage — were each confirmed to fail it. + +==== Added + +* *The PWG record is now derived from an evidence ledger, and gated +(2026-11-09).* Owner ruling: a machine-readable ledger rather than prose rows. +`+verification/pwg.json+` holds evidence only — per obligation, each leg's route, +its §5 token, its §2.2 correspondence state and its receipts — and *no grade*. +`+scripts/pwg-derive.sh+` is the only thing that turns evidence into a grade, +implementing §8.1–§8.3 clause by clause; `+scripts/pwg-check.sh+` re-derives on +every run and fails if the published table or census is not what the evidence +yields. A `+pwg+` key in the ledger is itself a gate failure, which is how +§8.4 rule 2 ("grades are derived, not asserted") becomes enforceable rather than +aspirational. ++ +The record is now per *obligation* rather than two coarse groups, and the picture +is far more informative: of 24 theory obligations, **17 are `+PWG-3+`** and 7 are +`+ungraded+` — and the seven split three ways. *Two* are Lean-only with no Agda +source at all (the O1 atom factorisation and the tropical (B′) sighting). +*Three* are Idris2-only, where an engineering restatement is not a leg (§8.1). +*Two* have a real but partial Agda leg, so the Agda token is `+OPEN+`: the +retention order, whose Agda leg proves reflexivity but neither transitivity nor +decidability, and tier-2 membership, where `+TB.Tier+` states six of the +per-element non-cancellativity witnesses and the positive `+Q-cancelʳ+` but not +the exhaustive characterisation — there is no Agda counterpart of +`+grade_leftCancel_iff+` and no Agda witness on the merge coordinate. A missing +Agda source and a partial one are different debts. Verdict soundness is +reclassified engineering, so §8.1 puts it off the ladder entirely. ++ +Wired: `+just pwg+` (census and per-obligation grades), `+just pwg-render+` +(regenerates the table between the `+PWG-TABLE+` markers, verified idempotent), +`+just pwg-check+`, the gate inside `+just verify-all+`, and a `+pwg-record+` +job in `+proofs.yml+` that needs no prover because the kernels already ran. ++ +Falsified, not assumed: `+scripts/test-gate-falsifiability.sh+` gains seven PWG +canaries plus a control, and the suite now runs 18/18. Two are load-bearing — +removing the import cone collapses all 17 `+PWG-3+` to `+ungraded+` (census +`+ungraded+` 24), and flipping one Lean leg to `+RECONCILED+` lifts that +obligation to `+PWG-2i+` — so they fire only if the published table really is +derived. Exercising the whole ladder: with both legs counting and current +receipts, the derivation returns `+PWG-1+`. + ==== Changed +* *Proof Witness Grades recorded, and the proof records reconciled with the +sources (2026-11-09).* `+docs/status/PROOF-STATUS.adoc+` gains the §8.5 PWG record +that `+PROOF-POLICY.adoc+` §8 (owner ruling 2026-11-04) requires, with both theory +groups derived as `+ungraded+` — Theorem B for want of a §2.1-conformant *receipt* +(its flags in force already are §2.1), the Lean-witnessed results for want of an +Agda *source* — plus the §1.1 import-cone record and a census in the form §8.4 +rule 7 allows. Four published rows narrowed to what the provers actually state: L3 +(two-sidedness is stated only for `+Falsified+` in Agda), L4 (Agda covers fate and +fidelity; Lean covers fate; bond, merge and the grade-level lifting have an Idris2 +leg only, which §8.1 excludes from the ladder), Target 3 (`+_↝_+` has two +ε-argument rules, no congruence, preservation definitional, no progress theorem), +and C3 (now cites the ratified `+FateA.dropped_still_not_cancel+`; the +pre-ratification `+dropped_absorbing+` is marked history). The README no longer +attributes the atom and tropical factorisations to Agda and Idris2 — they are +Lean-only. The O1-carrier evidence cell cites the emitted axiom lines and names its +receipt's commit instead of the inert in-source `+#print axioms+` directive, with +the carry-forward from `+4ecba4f+` stated and the proof trees shown identical. The +history section no longer reads as if O1 itself were closed. +* *"Axiom-clean" was an overclaim, and two neighbouring table rows were stale +(2026-11-09).* `+README.adoc+`'s layout table called the Lean grade-boundary +package "sorry-free, axiom-clean", and `+docs/proof-debt.adoc+`'s standing +position said the Idris2 core, the Lean ground truth and the Agda metatheory +"are all axiom-clean for their claimed lemmas". The kernel reports `+propext+` +and `+Quot.sound+`, and `+Classical.choice+` in three theorems, so both now use +the wording already adopted in `+PROOF-STATUS.adoc+` — no `+sorryAx+`, no user +axiom, resting on those three — which is what PROOF-POLICY §8.4 rule 6 requires +to travel with the claim. In the same table, the grade-factorisation verdict +`+(B)+` now says "on the *pre-ratification* carrier" and points at `+(B′)+` and +`+GradeFactorisationR.lean+`, and the Theorem B row names the full §2.1 +invocation rather than `+--safe --without-K+`. +* *Theorem B reaches `+PWG-3+`, the estate's first graded theory theorem +(2026-11-09).* It was recorded as `+ungraded+` earlier the same day, for want of +a receipt rather than a proof: the flags in force already were the PROOF-POLICY +§2.1 invocation, but every written-up Agda result here said +`+--safe --without-K+` only, and §2.1 declassifies prior successes under that +profile. Dispatching `+proofs.yml+` on `+main+` supplied the missing record — +run 42623339243 at `+c0eb4f1+`, log ending `+PASS: All.agda + Smoke.agda +typecheck (--safe --without-K --cubical-compatible; --safe => postulate-free by +construction)+`, with Agda 2.7.0.1 and `+agda-stdlib+` v2.0 pinned by SHA-256 +and the §1.1 import cone now recorded. Nothing about the mathematics changed. +`+PWG-3+` is not a discharge (§8.4 rule 1): §2's recheck obligation is owed in +full and is unreachable until a Rocq development exists. The same run was green +on both Lean packages at the current commit, so every receipt in this file now +names `+c0eb4f1+` and no row carries a carry-forward. +* *The (B′) tropical-factorisation row stated its own theorem backwards +(2026-11-09).* It read "any sighted homomorphism squashes `+Unknown+` to the +deceptive top". `+Unknown+` *is* the deceptive top of the fidelity carrier, and +`+sighted_forces_squash+` concludes the opposite — `+f (atten Delta.unknown) ≠ +Delta.unknown+` — i.e. a sighted homomorphism must send it *away* from that +value. The row now states the theorem, and names the repair that performs the +move (`+squash_top+`, `+squash_ne_unknown+`, `+squash_add+`). The row and the +PWG Lean leg also now name their receipts, as the O1-carrier row already did. +* *`+Trope.Order+` no longer cites Python as the provenance of proof content +(2026-11-09).* Two transitivity lemmas' docstrings read "exhaustive; +Python-verified", naming a language on the estate deny-list as what checked a +proof. What actually enforces exhaustiveness is Idris2's coverage checker under +`+%default total+`, where a missing case is a compile error; the docstrings now +say that. Comments only; no proof term changed. +* *Theorem B interface report brought back to the ratified carrier (2026-11-09).* +`+verification/proofs/agda/theorem-b/INTERFACE-REPORT.adoc+` stated +`+dropped ▷f falsified = dropped+` as the live tier-homomorphism-failure witness. +Amendment (A1) reversed that equation; the report now gives the witness the Agda +actually proves (`+dropped ▷f atten unknown+` against the tier meet) and no longer +claims the retired `+fate-L4-fails+` is a compiled guard theorem. Target 2's verdict +no longer advertises a sharpness refutation that ratification retired, the +toolchain and spec pointers match the pins (Agda 2.7.0.1, stdlib v2.0, spec v0.2), +and the `+fix+` obstruction count is one, not two, per ADR 0004. +* *Local Lean source gate strengthened to match CI (2026-11-09).* +`+verification/proofs/lean4/grade-boundary/justfile+`'s `+falsify+` recipe grepped +raw source and matched `+axiom+` only at line start, so it missed +`+private axiom foo+` and tripped on the honest "sorry-free" prose in the module +docstrings. It now uses the same comment-stripping pass and the same token-based +regexes as `+.github/workflows/proofs.yml+`. Demonstrated on a planted probe: the +old form missed the private axiom and false-positived on comment prose; the new +form catches the axiom, ignores the prose, and still catches a real `+sorry+`. * *Status surfaces reconciled with the spec on O1-carrier (2026-11-04).* `+docs/status/PROOF-STATUS.adoc+`, `+docs/status/ROADMAP.adoc+` and the README status paragraph now say what diff --git a/README.adoc b/README.adoc index 5779422..b05686d 100644 --- a/README.adoc +++ b/README.adoc @@ -71,9 +71,12 @@ rejects them at validation, naming the offending coordinate. The alternative | `src/rust/` | The Rust fast-core: a dep-free (std-only) second checker, validated against the Idris2 reference via the conformance corpus. | `tests/conformance/` | The machine conformance suite: `cases.json` + `fixtures/` + `schema-invalid/`. | `verification/proofs/idris2/` | The verified core (Idris2): grade algebra + L1/L2/⊑/veridicality/generation. -| `verification/proofs/lean4/grade-boundary/` | The grade-algebra ground truth (Lean 4 + Mathlib, sorry-free, axiom-clean): the three-tier honest/deceptive cancellation boundary. -| `verification/proofs/lean4/grade-factorisation/` | The tropical factorisation probe (Lean 4 + Mathlib): imports the carrier and decides whether the grade admits a commutative cost-quotient — verdict *(B) factors but veridicality-blind*. A precondition only; does not address recursion (CO-1). -| `verification/proofs/agda/theorem-b/` | Theorem B — the deferred calculus metatheory (Agda `--safe --without-K`, zero postulates): intrinsic graded calculus, value-substitution, subject reduction (β/let; `fix` open), Honest Generation. +| `verification/proofs/lean4/grade-boundary/` | The grade-algebra ground truth (Lean 4 + Mathlib): the three-tier honest/deceptive cancellation boundary. No `sorryAx` and no user axiom; the kernel reports `propext` and `Quot.sound`, and `Classical.choice` in three theorems. +| `verification/proofs/lean4/grade-factorisation/` | The tropical factorisation probe (Lean 4 + Mathlib): imports the carrier and decides whether the grade admits a commutative cost-quotient. Verdict *(B) factors but veridicality-blind* on the *pre-ratification* carrier; re-run on the ratified carrier it becomes *(B′) sighted on the fate axis* — `piR` +separates honest `Dropped` from deceptive `Falsified`, and reads the four fate slots +only; `psiBond` separates honest from deceptive bonds +(`GradeFactorisation.lean`). A precondition only; does not address recursion (CO-1). +| `verification/proofs/agda/theorem-b/` | Theorem B — the deferred calculus metatheory (Agda `--safe --without-K --cubical-compatible`, the PROOF-POLICY §2.1 invocation; zero postulates): intrinsic graded calculus, value-substitution, subject reduction (β/let; `fix` open), Honest Generation. | `verification/proofs/INTEGRATION-REPORT.adoc` | How the three streams reconcile: the unified R-id ↔ Lean ↔ Agda ↔ status table, the convergence (central open problem), and the divergence adjudication. | `docs/CONTRIBUTING-A-FRONTEND.adoc` | How a new front-end targets the IR (the portability contract). | `docs/status/PROOF-STATUS.adoc` | What is proved vs. stubbed-and-named vs. deferred. @@ -147,12 +150,28 @@ 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, proved on the ratified `GradeR` in -`EffectAtomsRatified.lean`; O1-coord stays open) and the tropical factorisations — pre-ratification -`GradeFactorisation.lean` veridicality-blind, ratified `GradeFactorisationR.lean` -veridicality-sighted — are proved across Agda, Idris2 and Lean; Theorem B gives +monoid with the three deceptive bottoms as two-sided zeros. L1–L6, conicality, +the Honest Generation and Veridicality theorems *all carry an Agda proof*, but coverage differs per result. +The grade-level cancellation boundary (left-cancellative iff ε on the +unquotiented carrier) is proved in Lean; Agda proves finite-fidelity cancellation +and selected non-cancellation counterexamples, not the exhaustive iff. +`docs/status/PROOF-STATUS.adoc` and +`verification/pwg.json` are the per-result record, and they agree row for row. +Only *L1* and *L4* carry a statement in all three, and of the ten results *eight* +lack one entirely. Lean does not state L2, L5, Honest Generation or Veridicality; +Idris2 does not state L3, L6, conicality or the cancellation boundary; L5 is +Agda-only. Where Idris2 does restate a result, PROOF-POLICY §8.1 keeps it off the +Proof Witness Grade ladder as an engineering restatement — the ledger records it +under `reference`, never as a leg, so it can neither raise nor lower a grade. +And *L4 in full* is proved by none of the three: Agda covers the fate coordinate +and the fidelity dimension, Lean covers fate, and bond and merge have an Idris2 +restatement only. Idris2 establishes coordinate-level monotonicity only; the +lifting for `gradeCompose` is not mechanised in Idris2. The atom +factorisation (O1's carrier half, proved on the ratified `GradeR` in +`EffectAtomsRatified.lean`; O1-coord stays open) and the tropical factorisations +— pre-ratification `GradeFactorisation.lean` veridicality-blind, ratified +`GradeFactorisationR.lean` fate-axis veridicality-sighted — are Lean-only: neither carries +an Agda or an Idris2 statement. 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, diff --git a/build/just/proofs.just b/build/just/proofs.just index 696c15b..e1905fb 100644 --- a/build/just/proofs.just +++ b/build/just/proofs.just @@ -236,4 +236,34 @@ verify-all: build-lean build-agda if grep -nE '(^|[^[:alnum:]_.])axiom([^[:alnum:]_]|$)' <<<"$stripped"; then echo "FAIL: user axiom declared in $f"; exit 1; fi done - echo "PASS: verify-all — Lean green & axiom-clean; Agda strict-flags green." + echo "=== verify-all: Proof Witness Grade record ===" + bash scripts/pwg-check.sh + echo "PASS: verify-all — Lean green, no sorryAx and no user axiom; Agda strict-flags green; PWG record derived and in step." + +# Derive every Proof Witness Grade from verification/pwg.json and show the census. +# The ledger holds EVIDENCE only; PROOF-POLICY §8.4 rule 2 says the grade is +# computed from it, never written by hand. +pwg: + @bash scripts/pwg-derive.sh --census + @echo + @bash scripts/pwg-derive.sh --json | jq -r '.[] | " \(.pwg)\t\(.id)\t\(.title)"' + +# Regenerate the PWG table inside docs/status/PROOF-STATUS.adoc from the ledger. +# Rewrites only the region between the PWG-TABLE:BEGIN/END markers. +pwg-render: + #!/usr/bin/env bash + set -euo pipefail + f=docs/status/PROOF-STATUS.adoc + grep -q '^// PWG-TABLE:BEGIN' "$f" || { echo "FAIL: $f has no PWG-TABLE:BEGIN marker"; exit 1; } + grep -q '^// PWG-TABLE:END' "$f" || { echo "FAIL: $f has no PWG-TABLE:END marker"; exit 1; } + tmp=$(mktemp) + awk '/^\/\/ PWG-TABLE:BEGIN/{print; exit} {print}' "$f" > "$tmp" + bash scripts/pwg-derive.sh --table >> "$tmp" + awk 'f{print} /^\/\/ PWG-TABLE:END/{if(!f){print; f=1}}' "$f" >> "$tmp" + mv "$tmp" "$f" + echo "regenerated the PWG table in $f" + +# 🔴 GATE: the ledger is well-formed, asserts no grade, and the published table +# and census are the derived ones. Falsified by scripts/test-gate-falsifiability.sh. +pwg-check: + @bash scripts/pwg-check.sh diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index e2cd555..4794318 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -47,8 +47,12 @@ or *(FP)* a false positive (convention comment — construct forbidden, not used == Standing position * No escape hatch is admitted into the trusted base. The verified Idris2 core, the - Lean grade-algebra ground truth, and the Agda metatheory are all axiom-clean for - their claimed lemmas. + Lean grade-algebra ground truth and the Agda metatheory carry no `sorryAx` and no + user axiom behind their claimed lemmas. "Axiom-clean" would say more than that and + is not used here: the Lean results rest on the standard library's `propext` and + `Quot.sound`, and on `Classical.choice` in three theorems, which PROOF-POLICY + §8.4 rule 6 requires to travel with the claim. The Agda is postulate-free by + construction under `--safe`. * The convention comments are retained deliberately: they document the prohibition at the point of work. The *root* fix for the scanner mismatch is to make `check-trusted-base.sh` comment-aware upstream in `hyperpolymath/standards` diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 9646d29..d2508bc 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -32,12 +32,12 @@ toc::[] | 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. +| Each deceptive bottom (`Falsified`, `Misbound`, `Conflated`, fidelity `Unknown`) is a two-sided zero of its coordinate's composition (A1). `Total` absorbs within fidelity. In Agda both sides are stated only for `Falsified` (`falsified-absorbL`/`-absorbR`); for `Misbound`, `Conflated` and `Unknown` the left form is stated and the right form follows in one step from the coordinate's commutativity (`▷b-comm`, `▷m-comm`, `⊕d-comm`) but is not itself a lemma. | 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}`. +| stem:[\triangleright] is monotone in both arguments w.r.t. stem:[\sqsubseteq] on every coordinate of the ratified carrier. Coverage differs by prover: the Agda covers the fate coordinate (`fateL4Mono{R,L}`) and the fidelity dimension (`dplusMono{R,L}`) only; the bond and merge coordinates have an Idris2 restatement only. Idris2 establishes coordinate-level monotonicity only; the grade-level lifting for `gradeCompose` that spec §7's Knaster–Tarski argument invokes is not mechanised in Idris2. Per PROOF-POLICY §8.1 Idris2 is an engineering prover and is not on the PWG ladder, so bond, merge and the grade-level lifting currently have no gradeable theory leg. +| Idris2 `Trope.Soundness.{fateL4MonoR,fateL4MonoL}`, `Trope.Order.{bondComposeMono,mergeComposeMono}`; Agda `TB.Order.{fateL4MonoR,fateL4MonoL}`; Lean `FateA.{comp_mono_right,comp_mono_left}` (fate coordinate only; `FateA.le` is defined on `Fate` alone and the Lean tree carries no `Bond`, `Merge` or `GradeR` order). | 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. @@ -79,21 +79,21 @@ toc::[] | Tier-2 membership, exhaustive | In the unquotiented model, every honest-but-lossy element is individually witnessed non-cancellative (finite attenuation regains cancellation on A3 normal forms), `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`. +| Lean `TierTwoComplete.lean`: `Bond.withheld_honest_not_cancel`, `Merge.fused_honest_not_cancel`, `Fate.atten_not_cancel`, the `*.leftCancelWitness` family, `Grade.grade_leftCancel_iff`. Agda states six of the per-element witnesses and the positive right-cancellation, all in `TB.Tier`: `unknown-not-cancel`, `total-honest-not-cancel`, `falsified-not-cancel`, `dropped-honest-not-cancel`, `predicated-honest-not-cancel`, `severed-honest-not-cancel`, `Q-cancelʳ`. What Agda does *not* state is the exhaustive step: there is no Agda counterpart of `grade_leftCancel_iff`, and no Agda witness on the merge coordinate, which is why the ledger's Agda token for this row is `OPEN` rather than the row being Lean-only. | 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. +| Lean `FateA.dropped_still_not_cancel` (`L4Monotonicity.lean`, ratified carrier), `fidelity_total_honest_not_cancel` (`GradeBoundary.lean`, over `Delta`, which ratification leaves unchanged); Agda `TB.Tier.fate-tier-meet-hom-fails`, the `TB.Tier` classifiers. (`GradeBoundary.lean`'s `dropped_absorbing` — `dropped * f = dropped` for `Fate.comp` — was cited here previously. It is a true theorem of the *pre-ratification* carrier that file mirrors, but it is not one of the ratified carrier this table is scoped to: amendment (A1) gives `FateA.comp dropped falsified = falsified`. Retained as history only.) 3+^| _Factorisation_ | O1-carrier (atom factorisation) -| Every grade is the stem:[\triangleright]-product of its single-slot projections; nine atom families, each realised, pairwise disjoint. Proved on the ratified `GradeR` (`EffectAtomsRatified.lean`); the coordinate-value classification into nine families (`EffectAtoms.lean`) is carrier-independent and carries over unchanged. `EffectAtoms.lean`'s `Grade.atom_factorization` is the same statement over the historical pre-ratification carrier, retained as history (`spec/calculus.adoc §3.5`, `§10`). -| Lean `EffectAtomsRatified.lean`: `Trope.GradeR.atom_factorization` (its `#print axioms` and the CI axiom audit: no `sorryAx`, no user axiom); `EffectAtoms.lean`: `Trope.nine_families`, `Trope.family_realized`, `Trope.families_disjoint`, `fateFamily_none_iff`. +| *Mechanised:* every grade is the stem:[\triangleright]-product of its six single-slot projections, on the ratified `GradeR` (`EffectAtomsRatified.lean`). *Mechanised separately,* over the coordinate value types `Fate`/`Bond`/`Merge` — which `GradeR` reuses unchanged, so the results are independent of either carrier (`EffectAtoms.lean`): the nine-label type has nine elements (`nine_families`, the cardinality of `AtomFamily`), each label is realised by some coordinate value, and the three classifiers' images are pairwise disjoint. *Not mechanised:* the link between the two. No theorem maps a grade's slot projections to `AtomFamily`, and the `emb*_one` lemmas that would begin that bridge are stated but used by nothing; so "the projections are drawn from the nine families" and "the typology is exhaustive" are argued in the module docstring, not stated as propositions. Exhaustiveness over the coordinate types holds by their being closed inductives and by the totality of the three classifiers, which no proposition records. `EffectAtoms.lean`'s `Grade.atom_factorization` is the factorisation statement over the historical pre-ratification carrier, retained as history (`spec/calculus.adoc §3.5`, `§10`). +| Lean `EffectAtomsRatified.lean`: `Trope.GradeR.atom_factorization`; `EffectAtoms.lean`: `Trope.nine_families`, `Trope.family_realized`, `Trope.families_disjoint`, `fateFamily_none_iff`. Receipt: `proofs.yml` run 42623339243, job "Lean grade-boundary: lake build + sorry-free environment", success at `c0eb4f1a1a50aabfab23b94fd74b53cef267f653` — the current commit, so no carry-forward is involved. The axiom lines quoted here (`'Trope.GradeR.atom_factorization' depends on axioms: [propext]`; `'Trope.nine_families' depends on axioms: [propext, Classical.choice, Quot.sound]`) are from run 41519571355 at `4ecba4f`, whose `verification/proofs/lean4` tree is `5f32026`, identical to `c0eb4f1`'s, so they describe the same sources. The in-source `#print axioms` directive is a request to the kernel, not evidence; the emitted axiom lines are. See the Proof Witness Grades section for this row's grade. | 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`. +| 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 veridicality-sighted homomorphism must send `atten Unknown` *away from* the deceptive top, not onto it — `sighted_forces_squash` concludes `f (atten Delta.unknown) ≠ Delta.unknown` from multiplicativity plus `f dropped ≠ f falsified`. The repair used here is exactly that move: `squash` sends the deceptive top to the honest one (`squash_top : squash Delta.unknown = Delta.total`, never back to it by `squash_ne_unknown`) and is itself additive (`squash_add`). +| Lean `GradeFactorisationR.lean`: `piR_hom`, `piR_one`, `piRHom`, `piR_nontrivial`, `piR_surjective`, `piR_sighted`, `phiR_sighted`, `phiId_not_hom`, `sighted_forces_squash`, `squash_top`, `squash_ne_unknown`, `squash_add`. Receipt: `proofs.yml` run 42623339243, job "Lean grade-factorisation: lake build + sorry-free environment", success at `c0eb4f1a1a50aabfab23b94fd74b53cef267f653`, the current commit. 3+^| _Metatheory (Theorem B, Agda `--safe --without-K`, zero postulates)_ @@ -106,7 +106,7 @@ toc::[] | 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. +| β 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. The fragment is narrow and intrinsic: `TB.Reduction._↝_` has exactly two constructors, `β-app` and `β-let`, each requiring the substituted argument at grade `ε`, with no congruence or evaluation-context rule and no step for any effect former. Because the relation is indexed at the same type *and* the same grade on both sides, preservation holds by construction rather than by induction over a reduction system, as the module header states. There is no progress theorem. | 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 @@ -135,6 +135,238 @@ toc::[] The Rust fast core (`src/rust/`) is not a proof; it agrees with the Idris2 reference over the whole conformance corpus (`just trope-rust`). +== Proof Witness Grades + +Estate policy +link:https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[`PROOF-POLICY.adoc`] +§8 (owner ruling 2026-11-04) requires each *theory* theorem's Proof Witness +Grade to be recorded in its home repository's proof-status file (§8.5). This +section is that record. PWG counts independent machine-checked witnesses for a +theory theorem; *lower is stronger* (§8, the numbers count down). It is not a +status token (§5) and not a statement that the theorem complies with the policy +(§8.4 rule 1). + +The evidence lives in `verification/pwg.json`: per obligation, each leg's route, +its §5 token, its §2.2 correspondence state and its receipts. **No grade is +written there.** §8.4 rule 2 says a grade is computed from the receipts and the +§2.2 records, and that "a grade written by hand that the receipts do not support +is drift" — so `scripts/pwg-derive.sh` is the only thing that turns evidence into +a grade, and `scripts/pwg-check.sh` re-derives on every run and fails if this +table, or the census below, is not what the evidence yields. A `pwg` key in the +ledger is itself a gate failure. + +Per §8.1 the ladder covers theory obligations only. The Idris2 developments are +engineering restatements: the ledger records them under `reference`, never as a +leg, so they can neither raise nor lower a grade. + +// PWG-TABLE:BEGIN +// GENERATED by scripts/pwg-derive.sh --table from verification/pwg.json. +// Do not hand-edit: scripts/pwg-check.sh re-derives and fails on drift. +[cols="2,1,1,3",options="header"] +|=== +| Obligation | `pwg` | Counting legs | Agda · Rocq · Lean (route · §5 token · §2.2 state) + +| L1 (associativity) +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| L2 (unit) +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| L3 (bottom absorption) +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| L4 (monotonicity), in full +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| L5 (deception infectiousness) +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| L6 (commutativity) +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| Retention order is a decidable preorder +| `ungraded` +| 0 of 2 +| re-proved · `OPEN` · `AGDA-PENDING` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| Fate is a chain (A2) +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| Veridicality Derivation +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| Honest Generation +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| The unit is non-deceptive and HC-4-coherent +| `ungraded` +| 0 of 2 +| unavailable · `OPEN` · `AGDA-PENDING` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| C1 (conicality) +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| C2 (the cancellation boundary) +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| Tier-2 membership, exhaustive +| `ungraded` +| 0 of 2 +| re-proved · `OPEN` · `AGDA-PENDING` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| C3 (partition; tier closure is not a homomorphism) +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| O1-carrier (atom factorisation) +| `ungraded` +| 0 of 2 +| unavailable · `OPEN` · `AGDA-PENDING` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| Tropical factorisation, (B-prime) sighted +| `ungraded` +| 0 of 2 +| unavailable · `OPEN` · `AGDA-PENDING` · unavailable · `OPEN` · `NOT-INVENTORIED` · re-proved · `PROVEN-WITH-AXIOMS` · `BRIDGE-PENDING` + +| Theorem B Target 1 - intrinsic graded calculus +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| Theorem B Target 2 - grade-exact substitution +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| Theorem B Target 3 - subject reduction, beta/let core +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| Theorem B Target 4 - Honest Generation and Veridicality +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| Grade soundness, exact lowering +| `ungraded` +| 0 of 2 +| unavailable · `OPEN` · `AGDA-PENDING` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| T-Sub soundness +| `ungraded` +| 0 of 2 +| unavailable · `OPEN` · `AGDA-PENDING` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| Verdict soundness (corollary) +| `not-applicable` +| — (§8.1: not on the ladder) +| unavailable · `OPEN` · `AGDA-PENDING` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` + +| Grade soundness, beta/let core +| `3` +| 0 of 2 +| re-proved · `PROVEN` · `AGDA-VERIFIED` · unavailable · `OPEN` · `NOT-INVENTORIED` · unavailable · `OPEN` · `NOT-INVENTORIED` +|=== +// PWG-TABLE:END + +*Census* (PROOF-POLICY §8.4 rule 7, never a percentage): of 24 theory obligations in this repository, `PWG-3` 17, `PWG-2i` 0, `PWG-2ii` 0, `PWG-1` 0, `ungraded` 7. No obligation here carries `+foundation-diverse` (§8.3). + +Read the census as the policy intends: seventeen obligations have a kernel-checked +Agda witness with a complete §8.2 receipt at the current commit, and *none* has a +counting recheck leg. `PWG-3` is not a discharge (§8.4 rule 1) — every one of the +seventeen still owes both its §2 legs. The seven `ungraded` rows split three ways, +and the distinction is the useful part. *Two* are Lean-only with no Agda source at +all: the O1 atom factorisation and the tropical (B′) sighting. *Three* are +Idris2-only, where an engineering restatement is not a leg (§8.1). *Two* have a +real but incomplete Agda leg, so the Agda token is `OPEN`: the retention order +proves reflexivity but neither transitivity nor decidability, and tier-2 membership +proves six of the non-cancellativity witnesses (`TB.Tier`, fate and bond) plus the +positive `Q-cancelʳ`, but not the exhaustive characterisation — there is no Agda +counterpart of `grade_leftCancel_iff`, and no Agda witness on the merge coordinate. +§8.1 makes all three causes `ungraded` alike; only the second is about engineering +provers. A missing Agda source and a partial one are different debts, and the +ledger records which one each row carries rather than flattening both to +"Lean-only". + +Nothing can reach `PWG-2i`, `PWG-2ii` or `PWG-1` from where this tree stands: no +Rocq development exists in this repository at all, so the ladder has a missing +rung that is independent of any Agda work. + +=== Import cone (§1.1) + +§1.1 lets a checked dependency be recorded as a cone rather than an `ASSUMED` +row, provided the record names the root module, the flags in force, the +postulate count and the library pin. The ledger carries this per receipt; in +full, for the Agda leg: + +* *Root modules*: `verification/proofs/agda/theorem-b/All.agda` (all seven `TB.*` + modules are reachable from it) and `Smoke.agda`. +* *Flags in force*: `--safe --without-K --cubical-compatible`, from + `theorem-b.agda-lib`'s `flags:` block plus the per-module `OPTIONS` pragma, + which additionally carry `--exact-split` and `--warning=error`. CI passes the + same three on the command line, in `proofs.yml`'s "Typecheck Theorem B" step + (named rather than numbered: a line reference goes stale on the next edit). +* *Postulate count*: zero. `--safe` refuses `postulate` outright; independently, + a comment-aware scan of the whole subtree (`hyperpolymath/mathesis`, + `scripts/census/proof-holes.sh`) run over `verification/proofs/agda` at + `c0eb4f1` emits no record of any class. +* *Library*: `agda-stdlib` v2.0, pinned in `proofs.yml` by URL and SHA-256 + `14eecb83d62495f701e1eb03ffba59a2f767491f728a8ab8c8bb9243331399d8`; Agda + 2.7.0.1, pinned by URL and SHA-256 in the same file. + +So the cone is *checked, not assumed* (§1.1). + +=== Mathlib, and what the owner ruled + +Every Lean module here sits in the `import Mathlib` cone (`GradeBoundary.lean:3`, +pinned in `lakefile.toml`), which PROOF-POLICY §2 forbids: "No Mathlib, in Lean or +elsewhere … A proof that needs a large external library to compile is a +dependency, not a proof the estate owns." ADR 0005 D4 meanwhile made "Lean 4 + +Mathlib" this repository's *provenance* prover, a role §1 does not define. + +Owner ruling 2026-11-09: **Lean is a generator, not a leg.** The Lean development +keeps Mathlib and keeps its purpose — finding and stress-testing theorems — and +its results are then restated in core Agda, which is what becomes gradeable. The +Mathlib cone therefore never enters the trusted base, and no Lean row here is or +will be a §2 recheck leg. The ledger records every Lean leg as +`route: re-proved, state: BRIDGE-PENDING`, which does not count (§2.2, §8.2). The +two Lean-only obligations — the O1 atom factorisation and the tropical (B′) +sighting — stay `ungraded` until an Agda statement of them exists at all; tier-2 +membership has its Agda witnesses already and stays `ungraded` only until the +exhaustive step joins them. The census at the head of this section is the +authoritative split. +The amendment to ADR 0005 D4 implementing this is tracked separately; until it +lands, the ADR and the policy disagree on paper and this paragraph is the +operative reading. + +One measurable cost of the dependency, worth keeping in view: `Trope.nine_families` +is proved by `rfl` yet reports `[propext, Classical.choice, Quot.sound]`, reaching +`Classical.choice` only through Mathlib's `Fintype.card`. + == Open Each is specified; none is asserted. Status words follow `spec/calculus.adoc §10`. @@ -190,8 +422,10 @@ 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). +L4/L5 as standalone lemmas were listed open. L4 and L5 are now proved (L4, L5 +rows). Of O1, only the carrier-relative half is mechanised (O1-carrier row); +O1-coord — metaphysical adequacy — stays open, and O1 itself is therefore not +closed. *2026-06-23.* Grade-algebra boundary in Lean (`GradeBoundary.lean`: `grade_mul_not_comm`, `grade_conical`, `grade_not_leftCancel`, diff --git a/scripts/pwg-check.sh b/scripts/pwg-check.sh new file mode 100755 index 0000000..b33b977 --- /dev/null +++ b/scripts/pwg-check.sh @@ -0,0 +1,145 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 🔴 GATE: the Proof Witness Grade record is well-formed, and every published +# grade is the DERIVED one. +# +# PROOF-POLICY 8.4 rule 2 says a grade is computed from the receipts and the 2.2 +# records, and that "a grade written by hand that the receipts do not support is +# drift". This gate is what makes that enforceable here: +# +# 1. the ledger is valid I-JSON and canonical JCS (owner ruling D306); +# 2. the ledger asserts NO grade — a `pwg` key on a theorem is itself a failure, +# because the only legitimate source of a grade is the derivation; +# 3. every leg's receipt reference resolves, and every receipt carries the +# fields 8.2 requires, including a full 40-character commit; +# 4. every section 5 token and every 2.2 state comes from its closed vocabulary; +# 5. the table and census published in docs/status/PROOF-STATUS.adoc are +# byte-identical to what scripts/pwg-derive.sh produces. +# +# Fails loudly and says which rule broke. Usage: pwg-check.sh [REPO_ROOT] +set -uo pipefail + +ROOT="${1:-$(cd "$(dirname "$0")/.." && pwd)}" +LEDGER="$ROOT/verification/pwg.json" +STATUS="$ROOT/docs/status/PROOF-STATUS.adoc" +DERIVE="$ROOT/scripts/pwg-derive.sh" +fail=0 +# Report the message arguments on stdout and mark the gate as failed without +# exiting, so subsequent checks can report further failures. +die() { echo "::error::pwg-check: $*"; fail=1; } + +command -v jq >/dev/null || { echo "::error::pwg-check: jq is required"; exit 2; } +[ -f "$LEDGER" ] || { echo "::error::pwg-check: no ledger at verification/pwg.json"; exit 1; } +[ -x "$DERIVE" ] || { echo "::error::pwg-check: scripts/pwg-derive.sh is missing or not executable"; exit 1; } + +# --- 1. valid I-JSON, canonical JCS --------------------------------------- +if ! jq -e . "$LEDGER" >/dev/null 2>&1; then + die "verification/pwg.json is not valid JSON" +else + if ! jq -cS . "$LEDGER" | cmp -s - "$LEDGER"; then + die "verification/pwg.json is not canonical JCS (owner ruling D306). Rewrite with: jq -cS . verification/pwg.json" + fi +fi +# Not `grep -qP`: -P is a build option, and `2>/dev/null` turned a grep that +# cannot do -P into a silent pass. `tr -d` of every allowed byte leaves exactly +# the disallowed ones, and is POSIX. +if [ "$(LC_ALL=C tr -d '\011\012\015\040-\377' < "$LEDGER" | wc -c)" -gt 0 ]; then + die "verification/pwg.json contains control characters (I-JSON, RFC 7493)" +fi + +# --- 2. the ledger must assert no grade ----------------------------------- +# A grade in the evidence file is drift by construction: it could only have been +# written by hand, since the derivation lives in pwg-derive.sh. +# `2>/dev/null || echo 0` read "this ledger has no parseable .theorems" as "no +# asserted grades" — a malformed ledger passed rule 2 by being malformed. +asserted=$(jq -r '[.theorems[] | select(has("pwg") or has("grade") or has("PWG"))] | length' "$LEDGER") \ + || die "rule 2 could not be evaluated: the ledger has no well-formed .theorems array" +if [ "${asserted:-0}" -gt 0 ]; then + die "$asserted theorem record(s) in the ledger assert a grade. The ledger carries EVIDENCE only; grades are derived (PROOF-POLICY 8.4 rule 2). Remove the pwg/grade keys." +fi + +# --- 3. receipt references resolve, and receipts are complete ------------- +missing=$(jq -r ' + .receipts as $R + | [ .theorems[] as $t + | ($t.legs | to_entries[]) as $e + | ($e.value.receipts // [])[] + | select(($R[.] // null) == null) + | "\($t.id)/\($e.key) -> \(.)" ] + | .[]' "$LEDGER") || die "rule 3 (receipt references) could not be evaluated: malformed theorem/leg shape" +[ -n "$missing" ] && die "unresolved receipt reference(s):"$'\n'"$missing" + +badr=$(jq -r ' + .receipts | to_entries[] + | .key as $k | .value as $v + | [ (if ($v.commit // "" | test("^[0-9a-f]{40}$")) then empty else "\($k): commit is not a full 40-char sha" end), + (if ($v.checker // "" | length) > 0 then empty else "\($k): no checker" end), + (if ($v.checker_version // "" | length) > 0 then empty else "\($k): no checker_version (8.2)" end), + (if ($v.invocation // "" | length) > 0 then empty else "\($k): no invocation (8.2)" end), + (if ($v.inputs_digest // "" | length) > 0 then empty else "\($k): no inputs_digest (8.2)" end), + (if ($v.result // "" | length) > 0 then empty else "\($k): no result (8.2)" end), + (if ($v.evidence // "" | length) > 0 then empty else "\($k): no evidence pointer" end), + (if ($v.state // "" | test("^(current|superseded|regressed)$")) then empty else "\($k): state must be current|superseded|regressed (8.4 rule 5)" end), + (if ($v | has("axioms")) then empty else "\($k): no axioms list (8.4 rule 6 — axioms travel with the grade)" end) ] + | .[]' "$LEDGER") \ + || die "rule 3 (receipt completeness) could not be evaluated over this ledger: malformed theorem/leg/receipt shape" +[ -n "$badr" ] && die "incomplete receipt(s):"$'\n'"$badr" + +# --- 4. closed vocabularies ---------------------------------------------- +# Section 5 tokens, and the 2.2 correspondence states, plus the non-leg marker +# this repository uses for an engineering restatement. +badtok=$(jq -r ' + [ .theorems[] as $t + | ($t.legs | to_entries[]) + | select((.value.token // "") | test("^(PROVEN|PROVEN-WITH-AXIOMS|TESTED|ASSUMED|OPEN)$") | not) + | "\($t.id)/\(.key): token \(.value.token)" ] + | .[]' "$LEDGER") \ + || die "rule 4 (section 5 tokens) could not be evaluated over this ledger: malformed theorem/leg/receipt shape" +[ -n "$badtok" ] && die "token(s) outside the section 5 closed vocabulary:"$'\n'"$badtok" + +badstate=$(jq -r ' + [ .theorems[] as $t + | ($t.legs | to_entries[]) + | select((.value.state // "") | test("^(AGDA-PENDING|AGDA-VERIFIED|COQ-CHECKED|LEAN-CHECKED|BRIDGE-PENDING|RECONCILED|COUNTEREXAMPLE|QUARANTINED|NOT-INVENTORIED)$") | not) + | "\($t.id)/\(.key): state \(.value.state)" ] + | .[]' "$LEDGER") \ + || die "rule 4 (2.2 states) could not be evaluated over this ledger: malformed theorem/leg/receipt shape" +[ -n "$badstate" ] && die "2.2 correspondence state(s) outside the closed vocabulary:"$'\n'"$badstate" + +badroute=$(jq -r ' + [ .theorems[] as $t + | ($t.legs | to_entries[]) + | select((.value.route // "") | test("^(transported|re-proved|waived|unavailable)$") | not) + | "\($t.id)/\(.key): route \(.value.route)" ] + | .[]' "$LEDGER") \ + || die "rule 4 (8.5 routes) could not be evaluated over this ledger: malformed theorem/leg/receipt shape" +[ -n "$badroute" ] && die "leg route(s) outside the 8.5 vocabulary:"$'\n'"$badroute" + +# --- 5. the published table and census are the derived ones --------------- +# A missing status file used to skip rule 5 silently and still print "published +# table and census match". Renaming the file was therefore enough to forge every +# grade in it and pass the gate. +if [ ! -f "$STATUS" ]; then + die "no published status file at docs/status/PROOF-STATUS.adoc — rule 5 cannot be checked. A deleted or moved status file is drift, not a pass." +else + want_table=$(bash "$DERIVE" --ledger "$LEDGER" --table) || die "pwg-derive --table failed" + want_census=$(bash "$DERIVE" --ledger "$LEDGER" --census) || die "pwg-derive --census failed" + got_table=$(awk '/^\/\/ PWG-TABLE:BEGIN/{f=1;next} /^\/\/ PWG-TABLE:END/{f=0} f' "$STATUS") + if [ -z "$got_table" ]; then + die "docs/status/PROOF-STATUS.adoc has no PWG-TABLE:BEGIN/END region to compare" + elif [ "$got_table" != "$want_table" ]; then + die "the PWG table in docs/status/PROOF-STATUS.adoc is not the derived one. Regenerate with: just pwg-render" + diff <(printf '%s\n' "$got_table") <(printf '%s\n' "$want_table") | head -20 >&2 || true + fi + if ! grep -qF "$want_census" "$STATUS"; then + die "the census line in docs/status/PROOF-STATUS.adoc is not the derived one. Expected:"$'\n'"$want_census" + fi +fi + +if [ "$fail" -eq 0 ]; then + n=$(jq -e '.theorems | length' "$LEDGER") || die "the ledger has no .theorems array" + echo "PASS: PWG ledger well-formed, no asserted grades, $n obligation(s) derived, published table and census match" +fi +exit "$fail" diff --git a/scripts/pwg-derive.sh b/scripts/pwg-derive.sh new file mode 100755 index 0000000..02360ad --- /dev/null +++ b/scripts/pwg-derive.sh @@ -0,0 +1,158 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# DERIVE each theorem's Proof Witness Grade from the evidence in +# verification/pwg.json, per PROOF-POLICY section 8. +# +# PROOF-POLICY 8.4 rule 2: "Grades are derived, not asserted. A grade is computed +# from the receipts and the 2.2 records. A grade written by hand that the receipts +# do not support is drift. A gate or a bot may recompute it at any time and +# reports the computed value." +# +# So the ledger carries EVIDENCE — legs, tokens, 2.2 states, receipts — and this +# script is the only thing that turns evidence into a grade. Nothing downstream +# may write a grade by hand; scripts/pwg-check.sh enforces that. +# +# Usage: +# pwg-derive.sh [--ledger PATH] --json derived grade per theorem, as JCS JSON +# pwg-derive.sh [--ledger PATH] --table the AsciiDoc table for PROOF-STATUS +# pwg-derive.sh [--ledger PATH] --census the section 8.4 rule 7 census line +set -uo pipefail + +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +LEDGER="$ROOT/verification/pwg.json" +MODE="" +while [ $# -gt 0 ]; do + case "$1" in + --ledger) LEDGER="$2"; shift 2 ;; + --json|--table|--census) MODE="$1"; shift ;; + *) echo "pwg-derive: unknown argument '$1'" >&2; exit 2 ;; + esac +done +[ -n "$MODE" ] || { echo "pwg-derive: one of --json --table --census is required" >&2; exit 2; } +[ -f "$LEDGER" ] || { echo "pwg-derive: no ledger at $LEDGER" >&2; exit 2; } +command -v jq >/dev/null || { echo "pwg-derive: jq is required" >&2; exit 2; } + +# --------------------------------------------------------------------------- +# The derivation, as one jq program. Every rule cites the policy clause it +# implements, so a reader can check the code against section 8 line by line. +# --------------------------------------------------------------------------- +# shellcheck disable=SC2016 # single quotes are REQUIRED: $a/$c/$l/$t/$R below are +# jq variables, and the shell must not expand them. +DERIVE=' + # A section 5 token that means the kernel accepted it. + def accepted: . == "PROVEN" or . == "PROVEN-WITH-AXIOMS"; + + # A receipt is usable when it is the current one and names a full 40-char commit + # (8.2 PWG-1: "the source repository and its full 40-character commit"). + def usable_receipt($rs): $rs + | map(select(.state == "current" and (.commit | test("^[0-9a-f]{40}$")))) + | length > 0; + + # 8.2 PWG-3 additionally requires the receipt to record the checker version, + # the standard-library pin, the flags actually in force, and the import cone (1.1). + def pwg3_receipt($rs): $rs + | map(select( + .state == "current" + and (.commit | test("^[0-9a-f]{40}$")) + and (.checker_version // "" | length > 0) + and (.stdlib_pin // "" | length > 0) + and (.import_cone // "" | length > 0) + and (.invocation // "" | test("--safe")) + and (.invocation // "" | test("--without-K")) + and (.invocation // "" | test("--cubical-compatible")) + )) + | length > 0; + + # 8.2: "A leg counts when the target kernel accepted it as PROVEN or + # PROVEN-WITH-AXIOMS and its 2.2 correspondence state is RECONCILED." And: + # a waived leg, an unavailable leg and any BRIDGE-PENDING leg do not count. + # Also require at least one current receipt with a full 40-character commit, + # resolving the leg’s receipt IDs through the supplied receipt map. + def counts($leg; $receipts): + ($leg.token | accepted) + and $leg.state == "RECONCILED" + and ($leg.route != "waived" and $leg.route != "unavailable") + and usable_receipt([$leg.receipts[] | $receipts[.]]); + + .receipts as $R + | .theorems + | map( + . as $t + | ($t.legs.agda) as $a + | ($t.legs.rocq) as $c + | ($t.legs.lean) as $l + | ([$a.receipts[] | $R[.]]) as $ar + | (($a.token | accepted) and $a.state == "AGDA-VERIFIED" and pwg3_receipt($ar)) as $agda_ok + | (if counts($c; $R) then 1 else 0 end) as $nc + | (if counts($l; $R) then 1 else 0 end) as $nl + | ($nc + $nl) as $legs + | ( + if $t.kind != "theory" then "not-applicable" # 8.1: PWG applies to theory only + elif ($agda_ok | not) then "ungraded" # 8.1 + elif $legs == 0 then "3" + elif $legs == 1 then "2i" + else + (if (usable_receipt($ar) + and usable_receipt([$c.receipts[] | $R[.]]) + and usable_receipt([$l.receipts[] | $R[.]])) + then "1" else "2ii" end) + end + ) as $grade + | { + id: $t.id, + title: $t.title, + kind: $t.kind, + pwg: $grade, + # 8.3: a non-DTT witness is a TAG beside the grade, never a leg. + foundation_diverse: (($t.foundation_diverse_witness // null) != null), + counting_legs: $legs, + agda_receipt_complete: $agda_ok, + axioms: ([ $ar[]? | .axioms[]? ] | unique), + legs: { + agda: {route: $a.route, token: $a.token, state: $a.state, counts: (counts($a; $R))}, + rocq: {route: $c.route, token: $c.token, state: $c.state, counts: (counts($c; $R))}, + lean: {route: $l.route, token: $l.token, state: $l.state, counts: (counts($l; $R))} + }, + notes: ($t.notes // "") + } + ) +' + +DERIVED="$(jq -cS "$DERIVE" "$LEDGER")" || { echo "pwg-derive: derivation failed" >&2; exit 1; } + +case "$MODE" in + --json) printf '%s\n' "$DERIVED" ;; + + --census) + # 8.4 rule 7: a count per grade WITH THE DENOMINATOR, naming ungraded and the + # lower rungs on the same line. Never a percentage, an average or a score. + printf '%s' "$DERIVED" | jq -r ' + [.[] | select(.kind == "theory")] as $th + | ($th | length) as $d + | "*Census* (PROOF-POLICY §8.4 rule 7, never a percentage): of \($d) theory obligations in this repository, " + + "`PWG-3` \([$th[] | select(.pwg == "3")] | length), " + + "`PWG-2i` \([$th[] | select(.pwg == "2i")] | length), " + + "`PWG-2ii` \([$th[] | select(.pwg == "2ii")] | length), " + + "`PWG-1` \([$th[] | select(.pwg == "1")] | length), " + + "`ungraded` \([$th[] | select(.pwg == "ungraded")] | length). " + + (([$th[] | select(.foundation_diverse)] | length) as $fd + | if $fd == 0 then "No obligation here carries `+foundation-diverse` (§8.3)." + else "\($fd) carry `+foundation-diverse` (§8.3)." end)' + ;; + + --table) + echo '// GENERATED by scripts/pwg-derive.sh --table from verification/pwg.json.' + echo '// Do not hand-edit: scripts/pwg-check.sh re-derives and fails on drift.' + echo '[cols="2,1,1,3",options="header"]' + echo '|===' + # shellcheck disable=SC2016 # a literal AsciiDoc header row; nothing to expand. + echo '| Obligation | `pwg` | Counting legs | Agda · Rocq · Lean (route · §5 token · §2.2 state)' + printf '%s' "$DERIVED" | jq -r '.[] | + "\n| \(.title)\n| `\(.pwg)`\(if .foundation_diverse then " `+foundation-diverse`" else "" end)\n| \(if .kind != "theory" then "— (§8.1: not on the ladder)" else "\(.counting_legs) of 2" end)\n| " + + ([.legs.agda, .legs.rocq, .legs.lean] + | map("\(.route) · `\(.token)` · `\(.state)`") | join(" · "))' + echo '|===' + ;; +esac diff --git a/scripts/test-gate-falsifiability.sh b/scripts/test-gate-falsifiability.sh index e0cf49f..2fe424c 100755 --- a/scripts/test-gate-falsifiability.sh +++ b/scripts/test-gate-falsifiability.sh @@ -124,9 +124,138 @@ c_secret() { else bad "hardcoded secret NOT detected — the security gate is blind to it"; fi } +# --- canaries 10-16: the PWG gate must reject each kind of grade drift ------ +# +# PROOF-POLICY 8.4 rule 2 makes a hand-written grade "drift". That is only +# enforceable if the gate actually catches it, so each canary below plants one +# species of drift in a COPY of the real ledger and asserts scripts/pwg-check.sh +# rejects it. Two of them (missing import_cone, a leg flipped to RECONCILED) are +# the load-bearing ones: they change nothing except the DERIVED grade, so they +# only fire if the derivation is genuinely what the published table comes from. +PWG_GATE="$ROOT/scripts/pwg-check.sh" + +# Build a throwaway repo root carrying the real derive script, the real status +# file and a ledger transformed by the given jq program, then run the real gate. +# A canary is only evidence if it actually plants the drift it names and the gate +# then objects to THAT drift. Three ways this harness used to pass without doing +# either, all measured 2026-11-09: +# (a) the canary's own jq program fails -> jq writes an empty ledger -> the gate +# rejects it for being invalid JSON -> the canary scores PASS having never +# exercised its target. All six jq-driven canaries did this when corrupted. +# (b) the jq program silently selects nothing (a renamed key, a .id that matches +# no theorem) -> the ledger is unchanged -> an unchanged ledger is not a +# wrong fixture, yet the gate's rejection of something else scored PASS. +# (c) the gate rejects for an unrelated reason. "reject" alone is too weak, so a +# reject canary now declares the reason it expects to see. +# $4 is that expected reason, an ERE matched against the gate's combined output. +pwg_case() { + local want="$1" label="$2" jqprog="$3" whynot="${4:-}" + local d got out + d=$(scratch) + mkdir -p "$d/scripts" "$d/verification" "$d/docs/status" + cp "$ROOT/scripts/pwg-derive.sh" "$d/scripts/" 2>/dev/null || { rm -rf "$d"; bad "$label (no pwg-derive.sh to copy)"; return; } + cp "$ROOT/scripts/pwg-check.sh" "$d/scripts/" 2>/dev/null || { rm -rf "$d"; bad "$label (no pwg-check.sh to copy)"; return; } + cp "$ROOT/docs/status/PROOF-STATUS.adoc" "$d/docs/status/" 2>/dev/null || { rm -rf "$d"; bad "$label (no PROOF-STATUS.adoc to copy — rule 5 would be untested)"; return; } + if [ "$jqprog" = "IDENTITY" ]; then + cp "$ROOT/verification/pwg.json" "$d/verification/pwg.json" + elif [ "$jqprog" = "PRETTY" ]; then + # valid JSON, but not canonical JCS: pretty-printed with unsorted keys + if ! jq . "$ROOT/verification/pwg.json" > "$d/verification/pwg.json" 2>"$d/jq.err"; then + local why; why=$(head -1 "$d/jq.err" 2>/dev/null || true) + rm -rf "$d"; bad "$label (the canary's OWN jq transform failed: $why)"; return + fi + else + if ! jq -cS "$jqprog" "$ROOT/verification/pwg.json" > "$d/verification/pwg.json" 2>"$d/jq.err"; then + local why; why=$(head -1 "$d/jq.err" 2>/dev/null || true) + rm -rf "$d"; bad "$label (the canary's OWN jq transform failed: $why)"; return + fi + if jq -cS . "$ROOT/verification/pwg.json" | cmp -s - "$d/verification/pwg.json"; then + rm -rf "$d"; bad "$label (the jq transform changed nothing — the fixture is not actually wrong)"; return + fi + fi + if out=$(bash "$d/scripts/pwg-check.sh" "$d" 2>&1); then got=accept; else got=reject; fi + rm -rf "$d" + if [ "$got" != "$want" ]; then bad "$label (gate said $got, expected $want)"; return; fi + if [ "$want" = reject ] && [ -n "$whynot" ] && ! printf '%s' "$out" | grep -qE "$whynot"; then + bad "$label (rejected, but for the WRONG reason — wanted /$whynot/, got: $(printf '%s' "$out" | head -1))"; return + fi + ok "$label" +} + +pwg_canaries() { + [ -x "$PWG_GATE" ] || { bad "scripts/pwg-check.sh is missing — the PWG gate cannot be falsified"; return; } + + # Control first: a suite that always fires proves nothing. + pwg_case accept "the real PWG ledger and status file are ACCEPTED" IDENTITY + + # 1. A grade asserted in the evidence file is drift by construction. + pwg_case reject "a hand-asserted pwg on a theorem is rejected" \ + '.theorems[0].pwg = "1"' \ + "assert a grade" + + # 2. Canonical JCS is the estate's JSON serialisation (owner ruling D306). + pwg_case reject "a non-canonical (pretty-printed) ledger is rejected" PRETTY + + # 3. Section 5's vocabulary is closed. + pwg_case reject "a section 5 token outside the closed vocabulary is rejected" \ + '.theorems[0].legs.agda.token = "MOSTLY-PROVEN"' \ + "section 5 closed vocabulary" + + # 4. So is 2.2's. + pwg_case reject "a 2.2 correspondence state outside the closed vocabulary is rejected" \ + '.theorems[0].legs.lean.state = "LOOKS-FINE"' \ + "correspondence state\\(s\\) outside the closed vocabulary" + + # 5. 8.2 requires the receipt to name the full 40-character commit. + pwg_case reject "a receipt with a short commit is rejected" \ + '.receipts["agda-c0eb4f1"].commit = "c0eb4f1"' \ + "not a full 40-char sha" + + # 6. LOAD-BEARING: drop the import cone and the Agda leg no longer satisfies + # 8.2's PWG-3 receipt requirement, so every derived grade that rested on it + # falls to ungraded and the published table stops matching. This fires only + # if the table really is derived. + pwg_case reject "removing the import cone changes the derived grades and is rejected" \ + '.receipts["agda-c0eb4f1"].import_cone = ""' \ + "not the derived one" + + # 7. LOAD-BEARING the other way: flip a BRIDGE-PENDING Lean leg to RECONCILED + # and it starts to count, lifting that obligation to PWG-2i. The published + # table must stop matching. + pwg_case reject "flipping a Lean leg to RECONCILED changes the grade and is rejected" \ + '(.theorems[] | select(.id == "L1") | .legs.lean.state) |= "RECONCILED"' \ + "not the derived one" +} + +# --- META (R10 applied to R10): the suite must detect breakage in ITS OWN fixtures. +# A canary whose jq program is broken writes an empty ledger; the gate then rejects +# it for being invalid JSON rather than for the planted drift, and the canary passes +# without ever exercising its target. This plants exactly that and asserts the suite +# reports FAILURE. Measured: this canary FAILS against the pre-fix harness. +meta_canary() { + local out + out=$( PASS=0; FAIL=0 + pwg_case reject "meta-probe (expected to be reported as FAILING)" '.theorems[0].pwg = ' >/dev/null 2>&1 + printf 'FAILCOUNT=%s' "$FAIL" ) + if printf '%s' "$out" | grep -q 'FAILCOUNT=1'; then + ok "a canary whose own jq program is broken is reported as FAILURE (meta-canary)" + else + bad "a BROKEN canary still reported PASS — the suite cannot detect its own breakage" + fi +} + wellknown_canaries; valid_canary; live_canary c_weak_crypto; c_plaintext_http; c_secret +pwg_canaries +meta_canary echo +# A canary group that silently stops running used to report "10/10" and exit 0. +# The count is part of the claim. +EXPECTED_CASES=19 +if [ "$((PASS+FAIL))" -ne "$EXPECTED_CASES" ]; then + echo "gate falsifiability canaries: $((PASS+FAIL)) cases ran, $EXPECTED_CASES expected — a canary group did not run" + exit 1 +fi if [ "$FAIL" -gt 0 ]; then echo "gate falsifiability canaries: $PASS/$((PASS+FAIL)) — FAILED" echo "A gate whose canary does not fire cannot fail, and is not a gate." diff --git a/tests/aspect_tests.sh b/tests/aspect_tests.sh index cec788d..47cb0c3 100755 --- a/tests/aspect_tests.sh +++ b/tests/aspect_tests.sh @@ -90,15 +90,39 @@ fi # So it failed the repo for documenting that it is clean. Now: proof source # extensions only, comment lines stripped, and `sorry` must not be part of # `sorry-free`. +# This block used to end with one `|| true` covering the WHOLE substitution, which +# masked three different non-zero statuses at once. Each now gets what it deserves: +# - the `find`: an absent directory is not a finding -> || true +# - the `grep`: no match is the GOOD case, not a failure -> || true +# - the `awk`: a non-zero stripper means it scanned a TRUNCATED file, so a +# clean grep over its output proves nothing. That must NOT be masked; it is +# recorded per file and raised as a hard failure below. Swallowing it would +# reproduce the exact fail-open this scan exists to prevent. +# `set -euo pipefail` is in force, so the grep's no-match status would otherwise +# abort the script through the assignment. +STRIP_FAILED="" +STRIP_FAIL_LOG="${TMPDIR:-/tmp}/aspect-strip-failed.$$" DANGEROUS_PROOF=$( while IFS= read -r f; do - awk -f tests/lib/strip-proof-comments.awk "$f" 2>/dev/null \ + if ! stripped=$(awk -f tests/lib/strip-proof-comments.awk "$f"); then + printf '%s\n' "$f" >> "$STRIP_FAIL_LOG" + continue + fi + printf '%s\n' "$stripped" \ | grep -nE '\bAdmitted\b|\bsorry\b|\bunsafeCoerce\b|\bObj\.magic\b' \ - | sed "s|^|$f:|" + | sed "s|^|$f:|" || true done < <(find src verification -type f \ \( -name '*.v' -o -name '*.lean' -o -name '*.agda' \ - -o -name '*.idr' -o -name '*.thy' -o -name '*.rs' -o -name '*.zig' \) 2>/dev/null) || true + -o -name '*.idr' -o -name '*.thy' -o -name '*.rs' -o -name '*.zig' \) 2>/dev/null || true) ) +if [ -f "$STRIP_FAIL_LOG" ]; then + STRIP_FAILED=$(cat "$STRIP_FAIL_LOG") + rm -f "$STRIP_FAIL_LOG" +fi +if [ -n "$STRIP_FAILED" ]; then + fail "Comment stripper could not scan these files (truncated input, not a clean scan):" + printf '%s\n' "$STRIP_FAILED" | head -5 +fi if [ -n "$DANGEROUS_PROOF" ]; then fail "Dangerous proof patterns found:" echo "$DANGEROUS_PROOF" | head -5 diff --git a/tests/lib/strip-proof-comments.awk b/tests/lib/strip-proof-comments.awk index ffad89f..fef8a42 100644 --- a/tests/lib/strip-proof-comments.awk +++ b/tests/lib/strip-proof-comments.awk @@ -7,8 +7,31 @@ # reported as a dangerous construct -- i.e. the repo was failed for DOCUMENTING # that it forbids Admitted. # +# A comment marker inside a STRING LITERAL is not a comment. Measured 2026-11-09: +# `def m : String := "/-"` opened a block comment that swallowed the rest of the +# file, so an `axiom` declared after it was invisible to every gate that scans +# through here -- while awk still exited 0. Strings are therefore consumed as +# units and emitted as `""`. Emitting them blank is strictly safer than verbatim: +# a string whose CONTENT is the word `axiom` or `sorry` can no longer trip the +# gate either. +# +# Char literals ('c', '\n', '"') are skipped whole, because they cannot contain a +# digraph -- but only where the quote is not a prime on an identifier. Both halves +# of that are load-bearing. Without the skip, the `'"'` in +# `src/idris2/Checker/Json.idr` opens a string and swallows the lines after it, +# which re-creates this very hole in another file. Without the prime guard, the +# primed identifiers Lean and Idris2 use everywhere (h', n') are read as quotes. +# +# Unterminated block comment or string => exit 1, loudly. A truncated scan must +# never be reported as a clean one; that is what made the hole above invisible. +# # Handles: (* *) /- -/ {- -} /* */ plus the line forms -- and // -BEGIN { inblk = 0 } +# +# KNOWN LIMITATION, deliberately not fixed here: Lean 4 block comments NEST, and +# this stripper closes on the first `-/`. That direction is fail-LOUD (an honest +# file can be failed for text inside a nested comment), not fail-open, so it is a +# separable change rather than a hole. Tracked separately. +BEGIN { inblk = 0; instr = 0 } { line = $0; out = ""; i = 1; n = length(line) while (i <= n) { @@ -17,12 +40,36 @@ BEGIN { inblk = 0 } if (two == close_tok) { inblk = 0; i += 2; continue } i++; continue } + if (instr) { + c = substr(line, i, 1) + if (c == "\\") { i += 2; continue } + if (c == "\"") { instr = 0; i++; continue } + i++; continue + } if (two == "(*") { inblk = 1; close_tok = "*)"; i += 2; continue } if (two == "/-") { inblk = 1; close_tok = "-/"; i += 2; continue } if (two == "{-") { inblk = 1; close_tok = "-}"; i += 2; continue } if (two == "/*") { inblk = 1; close_tok = "*/"; i += 2; continue } if (two == "--" || two == "//") { break } - out = out substr(line, i, 1); i++ + c = substr(line, i, 1) + if (c == "'" && substr(line, i - 1, 1) !~ /[A-Za-z0-9_'?!]/) { + rest = substr(line, i) + if (match(rest, /^'\\.'/) || match(rest, /^'\\[^']*'/) || match(rest, /^'[^'\\]'/)) { + i += RLENGTH; continue + } + } + if (c == "\"") { instr = 1; out = out "\"\""; i++; continue } + out = out c; i++ } print out } +END { + if (inblk) { + print "strip-proof-comments: unterminated block comment (" close_tok " missing) -- refusing to report a truncated scan as clean" > "/dev/stderr" + exit 1 + } + if (instr) { + print "strip-proof-comments: unterminated string literal -- refusing to report a truncated scan as clean" > "/dev/stderr" + exit 1 + } +} diff --git a/verification/proofs/agda/theorem-b/INTERFACE-REPORT.adoc b/verification/proofs/agda/theorem-b/INTERFACE-REPORT.adoc index 99c3527..8ba8317 100644 --- a/verification/proofs/agda/theorem-b/INTERFACE-REPORT.adoc +++ b/verification/proofs/agda/theorem-b/INTERFACE-REPORT.adoc @@ -51,8 +51,11 @@ Consequences for this report: == What this is Theorem B is the deferred metatheory of the trope-particularity *calculus* (spec -`spec/calculus.adoc`, `:revnumber: 0.1`) over the grade algebra. It is developed -*intrinsically* in Agda 2.8.0 + agda-stdlib, `--safe --without-K`, in +`spec/calculus.adoc`, `:revnumber: 0.2`) over the grade algebra. It is developed +*intrinsically* in Agda 2.7.0.1 + agda-stdlib v2.0 (both pinned by URL and SHA-256 +in `.github/workflows/proofs.yml`), under `--safe --without-K --cubical-compatible` +— the PROOF-POLICY §2.1 invocation, which CI passes at `proofs.yml:167` and the +local recipe at `build/just/proofs.just:87,212` — in `verification/proofs/agda/theorem-b/`, REUSING the echo-types graded-reindexing *style* (`echo-types/proofs/agda/EchoGraded.agda` — the thin-poset reindexing modality; `EchoIndexed.agda` — indexed functoriality; these are the @@ -90,7 +93,7 @@ deceptive (`falsified`/`misbound`/`conflated`/`unknown`, left zeros ⇒ L5 irrev ⊊ finite-fidelity cancellative core (Q embeds (ℕ,+,0), cancels). |=== -Fences respected: spec is v0.1 (O1 seven-effects completeness OUT OF SCOPE, +Fences respected: spec is v0.2, ratified carrier R-2026-07-07 (O1 seven-effects completeness OUT OF SCOPE, untouched); "CF" (cancellative+conical ⇒ special-Frobenius) NOT assumed — it is refuted-as-universal by both F2 and L5. @@ -148,7 +151,7 @@ rule `(g₁ ⊔ g₂) ▷ label` is recorded but not built (orthogonal lattice m no bearing on F2/F4). These are deliberate scoping choices, stated loudly, not silent weakenings. -=== Target 2 — substitution-admissibility / reindexing ("tropes follow values through cut") — *PROVED + sharpness refutation* +=== Target 2 — substitution-admissibility / reindexing ("tropes follow values through cut") — *PROVED (grade-exact); the v0.1 sharpness refutation is RETIRED* The substitution lemma `subst : Subst Γ Δ → Γ ⊢ A ! g → Δ ⊢ A ! g` preserves the grade `g` *EXACTLY* — the conclusion's grade is the same `g`, no ▷ reorder anywhere. @@ -156,12 +159,17 @@ This is the machine-checked form of "tropes follow values through cut". It is insensitive to F2 precisely because a value (and a variable) carries ε, the two-sided unit of ▷; single substitution `_[_]` inherits exactness. -The F2 boundary is itself a *theorem*, not a gap: `cut-left-grade` pins the oriented -cut grade `g₁ ▷ g₂`; `cut-orientation-matters` exhibits computations whose forward -composition differs from the swapped one (witness `dropped`/`falsified`); and -`cut-symmetric-fails` refutes any orientation-free computational-cut law. So the -value lemma is *sharp* — F2 forbids its symmetric generalisation. This is exactly -the predicted F2 wall, delivered as a refutation rather than an unproven obligation. +HISTORICAL (pre-ratification, v0.1 carrier): the F2 boundary was itself a theorem — +`cut-orientation-matters` exhibited computations whose forward composition differed +from the swapped one (witness `dropped`/`falsified`), and `cut-symmetric-fails` +refuted any orientation-free computational-cut law, so the value lemma was *sharp*. + +On the ratified carrier that wall is gone. Amendment (A1) made ▷ commutative, both +theorems were retired, and they are REPLACED by `TB.Substitution.cut-grade-comm : ∀ +(g₁ g₂ : Grade) → g₁ ▷ g₂ ≡ g₂ ▷ g₁`, proved from `grade-comm`. Neither +`cut-orientation-matters` nor `cut-symmetric-fails` occurs in any source; the cut is +reorderable, so the symmetric generalisation the v0.1 development forbade is now +available. `cut-left-grade` still pins the oriented cut grade. === Target 3 — subject reduction respecting the three-tier F4 boundary — *PARTIAL (β/let core PROVED; `fix` NOT-REACHED)* @@ -191,23 +199,57 @@ and cancels), and the six `*-not-cancel` witnesses (three-tier strictness). .FINDING (F2×F4): tier-preservation is CLOSURE, not a homomorphism ==== The naive single-tier meet-homomorphism `tierOf (g ▷ h) ≡ tierOf g ⊓ tierOf h` is -*FALSE* on the fate coordinate — `fate-tier-meet-hom-fails`: `dropped ▷f falsified -= dropped` (honest), but `fateTier dropped ⊓ fateTier falsified = deceptive`. The -honest left-absorbing head `dropped` *shields* a later deceptive `falsified`. This -is the same non-commutativity phenomenon (F2) as the L4-monotonicity failure -(`fate-L4-fails`, ported from `Soundness.idr`). It is *why* tier-preservation had to -be stated as set-membership closure and *why* the ⊑/L4 route is unsound — both are -kept as compiled guard theorems so no later work re-introduces the wrong route. +*FALSE* on the fate coordinate. On the ratified carrier the witness is +`fate-tier-meet-hom-fails` (`TB.Tier`): `dropped ▷f atten unknown = dropped` +(honestLossy), but `fateTier dropped ⊓ᵗ fateTier (atten unknown) = honestLossy ⊓ +deceptive = deceptive`. The honest-but-lossy left-absorbing head `dropped` *shields* +a later deceptive fidelity top. + +NOTE: an earlier revision of this box gave the witness as +`dropped ▷f falsified = dropped`. That is the *pre-ratification* equation. Amendment +(A1) of R-2026-07-07 reversed it: `TB.Grade` now computes +`dropped ▷f falsified = falsified` ("the lie survives the drop", +`TB.Grade.dropped▷falsified`), so the old pair agrees with the meet and is no longer +a witness. The failure above is the residual, fate-internal one, and it does not +launder the grade-level `Deceptive` predicate — `TB.Tier.deceptive-absorbs-▷` is +total. + +The two live together because they are *different notions of deceptive*, and it is +worth being exact about which one closes. The tier classifier is deceptive on +`atten unknown`, since `fateTier (atten unknown) = dTier unknown = deceptive`. The +`Deceptive` predicate is not: it is a predicate on *grades*, defined by equality to +the genuine zeros — `falsified` on any of the four fate coordinates, `misbound` on +the bond, `conflated` on the merge — so a grade carrying `atten unknown` and no +other deceptive coordinate does not satisfy it. (The four coordinates are +`Fate`-typed; "fidelity" in this development is the `Δ` *inside* `atten`, which is +exactly why the two notions come apart here.) Hence the *tier* class is not closed +under stem:[\triangleright]: `dropped ▷f atten unknown = dropped`, whose tier is +`honestLossy`, while the meet of the two tiers is `deceptive`. And hence +`deceptive-absorbs-▷` is not weakened by that: it establishes closure for the +narrower `Deceptive` predicate, which such a grade was never in. A claim that +"deceptive is closed" is true of the predicate and false of the tier class, so this +report always names which. + +This is *why* tier-preservation had to be stated as set-membership closure. The L4 +guard it used to be paired with, `fate-L4-fails`, is RETIRED by R-2026-07-07 and is +not compiled: L4 is restored on the ratified carrier, with positive proofs in both +arguments at `TB.Order.fateL4MonoR` and `TB.Order.fateL4MonoL`. Only +`fate-tier-meet-hom-fails` is a live guard theorem. ==== NOT-REACHED — subject reduction through `fix`/lfp (calculus §7). Honestly -characterised in `TB.Reduction` (and *not postulated*): two things are genuinely -missing — (1) an operational model (no ↝ rule for `fix`, no observed-retention ρ; -the spec is a type discipline), and (2) the O4 limit carrier for ordering iterated -attenuation beyond ω (Conat-vs-tag). The lfp's fidelity endpoint lands in the +characterised in `TB.Reduction` (and *not postulated*): one thing is genuinely +missing — an operational model (no ↝ rule for `fix`, no observed-retention ρ; the +spec is a type discipline). What was once listed as a second obstruction, the O4 +limit carrier for ordering iterated attenuation beyond ω (Conat-vs-tag), is +RESOLVED by ADR 0004: the finitary carrier ℕ ∪ {∞, ⊤} suffices, because +transfinitely deep `fix` nesting is inexpressible in finitary syntax. The lfp's +fidelity endpoint lands in the ▷-fixed absorbing tops `{total, unknown}`, so the *grade* is tier-stable; the unproven part is the operational unfold-preserves-tier step. This obstruction is -the missing operational semantics + O4, NOT a defect of the grade algebra. +the missing operational semantics, NOT a defect of the grade algebra. (O4 is no +longer part of it: ADR 0004 resolved the limit-carrier question, as the paragraph +above records.) === Target 4 — Honest Generation (HC-*) and Veridicality (L*) — *PROVED* (reached because 1–3 landed) diff --git a/verification/proofs/idris2/Trope/Order.idr b/verification/proofs/idris2/Trope/Order.idr index 60874a5..215ad6b 100644 --- a/verification/proofs/idris2/Trope/Order.idr +++ b/verification/proofs/idris2/Trope/Order.idr @@ -95,7 +95,9 @@ fateLteTrans Dropped Predicated Falsified _ q = absurd q fateLteTrans Dropped Dropped c _ q = q fateLteTrans Dropped Falsified c p _ = absurd p -||| Transitivity of ⊑ on Bond (exhaustive; Python-verified). +||| Transitivity of ⊑ on Bond. The clause table below is exhaustive, and +||| Idris2's coverage checker under `%default total` is what enforces that: +||| a missing case is a compile error, not a silent gap. export bondLteTrans : (a, b, d : Bond) -> bondLte a b = True -> bondLte b d = True -> bondLte a d = True bondLteTrans Intact Intact Intact _ _ = Refl @@ -163,7 +165,9 @@ bondLteTrans Misbound Misbound Withheld _ _ = Refl bondLteTrans Misbound Misbound Severed _ _ = Refl bondLteTrans Misbound Misbound Misbound _ _ = Refl -||| Transitivity of ⊑ on Merge (exhaustive; Python-verified). +||| Transitivity of ⊑ on Merge. The clause table below is exhaustive, and +||| Idris2's coverage checker under `%default total` is what enforces that: +||| a missing case is a compile error, not a silent gap. export mergeLteTrans : (a, b, d : Merge) -> mergeLte a b = True -> mergeLte b d = True -> mergeLte a d = True mergeLteTrans Single Single Single _ _ = Refl diff --git a/verification/proofs/lean4/grade-boundary/justfile b/verification/proofs/lean4/grade-boundary/justfile index a62b910..60e9a1a 100644 --- a/verification/proofs/lean4/grade-boundary/justfile +++ b/verification/proofs/lean4/grade-boundary/justfile @@ -11,8 +11,24 @@ build *args: # the development is not sorry-free, smuggles axioms/native_decide, or stops building. falsify: @echo "[falsify] no forbidden tactics/axioms in source…" - @! grep -nE '(:=|by|;|<;>|=>|\|)[[:space:]]*(sorry|admit)\b|\bnative_decide\b' *.lean || (echo "FAIL: forbidden tactic" && exit 1) - @! grep -nE '^[[:space:]]*axiom\b' *.lean || (echo "FAIL: user axiom declared" && exit 1) + # Same pipeline as .github/workflows/proofs.yml: strip -- and /- -/ comments + # first (line numbers preserved), then match bare TOKENS. Line-initial and + # raw-source matching missed `private axiom foo` and tripped on the honest + # "sorry-free" prose in the module docstrings. + @fail=0; \ + for f in *.lean; do \ + stripped=$(awk -f ../../../../tests/lib/strip-proof-comments.awk "$f") || { \ + echo "FAIL: could not strip comments from $f — refusing to scan partial output"; \ + fail=1; continue; \ + }; \ + if grep -nE '(^|[^[:alnum:]_.])(sorry|admit|unsafe)([^[:alnum:]_]|$)|\bnative_decide\b|\bsorryAx\b|\bofReduceBool\b|\bextern\b|\bimplemented_by\b|\baddDecl\b|\baxiomDecl\b' <<<"$stripped"; then \ + echo "FAIL: forbidden Lean construct in $f"; fail=1; \ + fi; \ + if grep -nE '(^|[^[:alnum:]_.])axiom([^[:alnum:]_]|$)' <<<"$stripped"; then \ + echo "FAIL: user axiom declared in $f"; fail=1; \ + fi; \ + done; \ + [ "$fail" -eq 0 ] || exit 1 @echo "[falsify] build is green…" lake build @echo "[falsify] axiom audit contains no sorryAx…" diff --git a/verification/pwg.json b/verification/pwg.json new file mode 100644 index 0000000..2ca1fc8 --- /dev/null +++ b/verification/pwg.json @@ -0,0 +1 @@ +{"commit":"c0eb4f1a1a50aabfab23b94fd74b53cef267f653","note":"Evidence ledger. The pwg field of each theorem is DERIVED from the legs and receipts below by scripts/pwg-derive.sh, never written by hand; scripts/pwg-check.sh re-derives and fails on drift (PROOF-POLICY 8.4 rule 2). Idris2 appears as a reference, not a leg: 8.1 excludes engineering provers from the ladder.","policy":{"commit":"9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5","path":"3-practice/PROOF-POLICY.adoc","repo":"metadatastician/standards","section":"8"},"receipts":{"agda-c0eb4f1":{"axioms":[],"checker":"agda","checker_version":"2.7.0.1","commit":"c0eb4f1a1a50aabfab23b94fd74b53cef267f653","evidence":"https://github.com/hyperpolymath/trope-checker/actions/runs/42623339243","import_cone":"root modules All.agda and Smoke.agda; all seven TB.* modules reachable from All.agda; postulate count 0 (--safe refuses postulate; independently scanned with hyperpolymath/mathesis scripts/census/proof-holes.sh over verification/proofs/agda at this commit, which emitted no record of any class)","inputs_digest":"git-tree verification/proofs/agda = 8d3370e7da58023b9bfa0802e710860105ace73a","invocation":"agda --safe --without-K --cubical-compatible All.agda ; agda --safe --without-K --cubical-compatible Smoke.agda","observed":"PASS: All.agda + Smoke.agda typecheck (--safe --without-K --cubical-compatible; --safe => postulate-free by construction)","repo":"hyperpolymath/trope-checker","result":"pass","state":"current","stdlib_pin":"agda-stdlib v2.0 sha256:14eecb83d62495f701e1eb03ffba59a2f767491f728a8ab8c8bb9243331399d8"},"lean-boundary-c0eb4f1":{"axioms":["propext","Quot.sound","Classical.choice"],"checker":"lean","checker_version":"4.16.0 (lake, leanchecker)","commit":"c0eb4f1a1a50aabfab23b94fd74b53cef267f653","evidence":"https://github.com/hyperpolymath/trope-checker/actions/runs/42623339243","import_cone":"every module of grade-boundary sits in the import Mathlib cone via GradeBoundary.lean:3","inputs_digest":"git-tree verification/proofs/lean4 = 5f32026d26810845d94d42b5a1281da3c2a06146","invocation":"lake build --wfail ; leanchecker ; axiom audit against the allowlist {propext, Classical.choice, Quot.sound}","observed":"job 'Lean grade-boundary: lake build + sorry-free environment' success; 'Trope.GradeR.atom_factorization' depends on axioms: [propext]; 'Trope.nine_families' depends on axioms: [propext, Classical.choice, Quot.sound]","repo":"hyperpolymath/trope-checker","result":"pass","state":"current","stdlib_pin":"mathlib4 rev v4.16.0 (lakefile.toml) -- see the Mathlib note: PROOF-POLICY 2 forbids this dependency for a recheck leg"},"lean-factorisation-c0eb4f1":{"axioms":["propext","Quot.sound","Classical.choice"],"checker":"lean","checker_version":"4.16.0 (lake, leanchecker)","commit":"c0eb4f1a1a50aabfab23b94fd74b53cef267f653","evidence":"https://github.com/hyperpolymath/trope-checker/actions/runs/42623339243","import_cone":"grade-factorisation requires gradeBoundary, so the import Mathlib cone covers it","inputs_digest":"git-tree verification/proofs/lean4 = 5f32026d26810845d94d42b5a1281da3c2a06146","invocation":"lake build --wfail ; leanchecker ; axiom audit against the allowlist {propext, Classical.choice, Quot.sound}","observed":"job 'Lean grade-factorisation: lake build + sorry-free environment' success","repo":"hyperpolymath/trope-checker","result":"pass","state":"current","stdlib_pin":"mathlib4 rev v4.16.0, transitively via the gradeBoundary path dependency"}},"repo":"hyperpolymath/trope-checker","schema_version":"1.0.0","theorems":[{"foundation_diverse_witness":null,"id":"L1","kind":"theory","legs":{"agda":{"declarations":["TB.Grade.gmonoid-assoc"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":["FateA.comp_assoc"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"","reference":{"idris2":{"declarations":["Trope.Laws.gradeAssoc","Trope.Coords.fateAssoc","Trope.Coords.bondAssoc","Trope.Coords.mergeAssoc","Trope.Fidelity.dplusAssoc"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"L1 (associativity)"},{"foundation_diverse_witness":null,"id":"L2","kind":"theory","legs":{"agda":{"declarations":["TB.Grade.gmonoid-unit"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"","reference":{"idris2":{"declarations":["Trope.Grade.gradeUnitL","Trope.Grade.gradeUnitR","Trope.Coords.fateUnitL","Trope.Fidelity.dplusZeroR"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"L2 (unit)"},{"foundation_diverse_witness":null,"id":"L3","kind":"theory","legs":{"agda":{"declarations":["TB.Grade.falsified-absorbL","TB.Grade.falsified-absorbR","TB.Grade.misbound-absorbL","TB.Grade.conflated-absorbL","TB.Grade.unknown-absorbL","TB.Grade.total-absorb-Q","TB.Tier.deceptive-absorbs-|>"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":["FateA.falsified_two_sided_zero","GradeR.gBotR_two_sided_zero"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Agda states both sides only for Falsified. For Misbound, Conflated and Unknown the left form is stated; the right follows in one step from the coordinate's commutativity but is not itself a lemma.","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"L3 (bottom absorption)"},{"foundation_diverse_witness":null,"id":"L4","kind":"theory","legs":{"agda":{"declarations":["TB.Order.fateL4MonoR","TB.Order.fateL4MonoL","TB.Order.dplusMonoR","TB.Order.dplusMonoL"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":["FateA.comp_mono_right","FateA.comp_mono_left"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Coverage differs by prover. Agda covers the fate coordinate and the fidelity dimension; Lean covers fate only (FateA.le is defined on Fate alone). Bond and merge have an Idris2 restatement only, which 8.1 excludes from the ladder. Idris2 establishes coordinate-level monotonicity only; the grade-level lifting for gradeCompose that spec section 7's Knaster-Tarski argument invokes is not mechanised in Idris2. Bond, merge and the grade-level lifting have no gradeable theory leg.","reference":{"idris2":{"declarations":["Trope.Soundness.fateL4MonoR","Trope.Soundness.fateL4MonoL","Trope.Order.bondComposeMono","Trope.Order.mergeComposeMono"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"L4 (monotonicity), in full"},{"foundation_diverse_witness":null,"id":"L5","kind":"theory","legs":{"agda":{"declarations":["TB.Tier.deceptive-absorbs-|>","TB.Reduction.attenuate-stays-deceptive","TB.Reduction.project-stays-deceptive"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"L5 (deception infectiousness)"},{"foundation_diverse_witness":null,"id":"L6","kind":"theory","legs":{"agda":{"declarations":["TB.Grade.grade-comm"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":["GradeR.instCommMonoid","FateA.comp_comm"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"L6 ratification is still subject to the open owner ruling tracked on trope-checker issue 106.","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"L6 (commutativity)"},{"foundation_diverse_witness":null,"id":"retention-order","kind":"theory","legs":{"agda":{"declarations":["TB.Order.|=-refl"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-PENDING","token":"OPEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Agda proves reflexivity only. Transitivity and decidability exist in the Idris2 reference, which 8.1 excludes from the ladder, so the preorder claim has no complete theory leg. The Agda leg is OPEN, not PROVEN, for this obligation.","reference":{"idris2":{"declarations":["Trope.Laws.decGradeLte","Trope.Soundness.gradeLteTrans","Trope.Coords.fateLteRefl","Trope.Coords.bondLteRefl","Trope.Coords.mergeLteRefl","Trope.Fidelity.dLteRefl"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"Retention order is a decidable preorder"},{"foundation_diverse_witness":null,"id":"A2-chain","kind":"theory","legs":{"agda":{"declarations":["TB.Order.fateDroppedLtePredicated","TB.Order.fatePredicatedNotLteDropped"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":["FateA.le_total","FateA.le_refl"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"What is proved is the two directional facts of A2. Totality is stated in Lean (FateA.le_total); transitivity and antisymmetry are not mechanised in any prover, so 'chain' is stronger than the mechanised content.","reference":{"idris2":{"declarations":["Trope.Soundness.fateDroppedLtePredicated","Trope.Soundness.fatePredicatedNotLteDropped"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"Fate is a chain (A2)"},{"foundation_diverse_witness":null,"id":"veridicality-derivation","kind":"theory","legs":{"agda":{"declarations":["TB.Honest.fate-deceptive-unique","TB.Honest.bond-deceptive-unique","TB.Honest.merge-deceptive-unique"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"The 'exactly three' half rests on the three uniqueness lemmas plus the construction of Grade; Trope.Veridicality.deceptiveDuals is a tuple value and states no proposition, so it is not cited as evidence here.","reference":{"idris2":{"declarations":["Trope.Veridicality.fateDeceptiveUnique","Trope.Veridicality.bondDeceptiveUnique","Trope.Veridicality.mergeDeceptiveUnique"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"Veridicality Derivation"},{"foundation_diverse_witness":null,"id":"honest-generation","kind":"theory","legs":{"agda":{"declarations":["TB.Honest.genFate","TB.Honest.genBond","TB.Honest.genMerge","TB.Honest.honest-closed-|>"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"","reference":{"idris2":{"declarations":["Trope.Generation.genFate","Trope.Generation.genBond","Trope.Generation.genMerge"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"Honest Generation"},{"foundation_diverse_witness":null,"id":"hc4-coherence","kind":"theory","legs":{"agda":{"declarations":[],"receipts":[],"route":"unavailable","state":"AGDA-PENDING","token":"OPEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Idris2 only. No Agda source, so ungraded under 8.1 however sound the Idris2 proof is.","reference":{"idris2":{"declarations":["Trope.Veridicality.epsilonHonest","Trope.Grade.epsilonCoherent"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"The unit is non-deceptive and HC-4-coherent"},{"foundation_diverse_witness":null,"id":"C1","kind":"theory","legs":{"agda":{"declarations":["TB.Grade.grade-conical"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":["GradeR.conical","FateA.conical"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"C1 (conicality)"},{"foundation_diverse_witness":null,"id":"C2","kind":"theory","legs":{"agda":{"declarations":["TB.Tier.Q-cancel-r","TB.Tier.core-closed-|>"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":["GradeR.gradeR_leftCancel_iff","GradeR.gradeR_not_leftCancel","GradeR.gDroppedR_not_cancel","FateA.atten_cancel_on_normalForms"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"The normal-form half is proved on the fate coordinate only (FateA.atten_cancel_on_normalForms); there is no grade-level normal-form cancellation theorem. Amendment (A3) is not modelled in the Agda, whose carrier is the unnormalised one.","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"C2 (the cancellation boundary)"},{"foundation_diverse_witness":null,"id":"tier2-membership","kind":"theory","legs":{"agda":{"declarations":["TB.Tier.unknown-not-cancel","TB.Tier.total-honest-not-cancel","TB.Tier.falsified-not-cancel","TB.Tier.dropped-honest-not-cancel","TB.Tier.predicated-honest-not-cancel","TB.Tier.severed-honest-not-cancel","TB.Tier.Q-cancelʳ"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-PENDING","token":"OPEN"},"lean":{"declarations":["Bond.withheld_honest_not_cancel","Merge.fused_honest_not_cancel","Fate.atten_not_cancel","Grade.grade_leftCancel_iff","GradeR.gradeR_leftCancel_iff","FateA.leftCancelWitness"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Agda states six of the non-cancellativity witnesses (fate and bond) plus the positive right-cancellation Q-cancelʳ, so the Agda leg is NOT unavailable. It is OPEN because the exhaustive characterisation is not stated in Agda: there is no Agda counterpart of grade_leftCancel_iff, and no Agda witness on the merge coordinate. Lean carries the exhaustive iff. Grade.grade_leftCancel_iff is over the historical pre-ratification carrier; the ratified restatement is GradeR.gradeR_leftCancel_iff. Ungraded because the Agda token is OPEN (§8.1), not for want of an Agda source.","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"Tier-2 membership, exhaustive"},{"foundation_diverse_witness":null,"id":"C3","kind":"theory","legs":{"agda":{"declarations":["TB.Tier.fate-tier-meet-hom-fails"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":["FateA.dropped_still_not_cancel","Delta.fidelity_total_honest_not_cancel"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"The ratified witness is dropped |>f atten unknown against the tier meet. The pre-ratification witness dropped |>f falsified = dropped was reversed by amendment (A1) and is retained as history only.","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"C3 (partition; tier closure is not a homomorphism)"},{"foundation_diverse_witness":null,"id":"O1-carrier","kind":"theory","legs":{"agda":{"declarations":[],"receipts":[],"route":"unavailable","state":"AGDA-PENDING","token":"OPEN"},"lean":{"declarations":["Trope.GradeR.atom_factorization","Trope.nine_families","Trope.family_realized","Trope.families_disjoint","Trope.fateFamily_none_iff"],"receipts":["lean-boundary-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Lean only, so ungraded under 8.1. Mechanised: the factorisation into six slot projections, and separately the nine-label classification over the coordinate value types. NOT mechanised: the link between them. No theorem maps a grade's slot projections to AtomFamily, and the emb*_one lemmas that would begin that bridge are stated but used by nothing, so 'drawn from the nine families' and 'exhaustive' are argued in a docstring rather than stated.","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"O1-carrier (atom factorisation)"},{"foundation_diverse_witness":null,"id":"tropical-Bprime","kind":"theory","legs":{"agda":{"declarations":[],"receipts":[],"route":"unavailable","state":"AGDA-PENDING","token":"OPEN"},"lean":{"declarations":["piR_hom","piR_one","piRHom","piR_nontrivial","piR_surjective","piR_sighted","phiR_sighted","phiId_not_hom","sighted_forces_squash","squash_top","squash_ne_unknown","squash_add"],"receipts":["lean-factorisation-c0eb4f1"],"route":"re-proved","state":"BRIDGE-PENDING","token":"PROVEN-WITH-AXIOMS"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Lean only, so ungraded under 8.1. sighted_forces_squash concludes f (atten Delta.unknown) /= Delta.unknown: a sighted homomorphism must send atten Unknown AWAY from the deceptive top, not onto it.","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"Tropical factorisation, (B-prime) sighted"},{"foundation_diverse_witness":null,"id":"theorem-b-t1","kind":"theory","legs":{"agda":{"declarations":["TB.Syntax","TB.Grade","TB.Tier"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"Theorem B Target 1 - intrinsic graded calculus"},{"foundation_diverse_witness":null,"id":"theorem-b-t2","kind":"theory","legs":{"agda":{"declarations":["TB.Substitution.cut-preserves-grade","TB.Substitution.cut-grade-comm"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"The v0.1 sharpness refutation (cut-orientation-matters, cut-symmetric-fails) was retired by amendment (A1) and is replaced by cut-grade-comm: the cut is reorderable.","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"Theorem B Target 2 - grade-exact substitution"},{"foundation_diverse_witness":null,"id":"theorem-b-t3","kind":"theory","legs":{"agda":{"declarations":["TB.Reduction.beta-app","TB.Reduction.beta-let","TB.Reduction.let-redex-grade","TB.Reduction.let-tier-preserved","TB.Reduction.seq-stays-core"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Narrow and intrinsic. The step relation has exactly two constructors, each requiring the substituted argument at grade epsilon, with no congruence rule and no step for any effect former. Preservation holds by construction because the relation is indexed at the same type and grade on both sides, not by induction. There is no progress theorem. The fix case is open (CO-1).","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"Theorem B Target 3 - subject reduction, beta/let core"},{"foundation_diverse_witness":null,"id":"theorem-b-t4","kind":"theory","legs":{"agda":{"declarations":["TB.Honest"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"Theorem B Target 4 - Honest Generation and Veridicality"},{"foundation_diverse_witness":null,"id":"grade-soundness-exact","kind":"theory","legs":{"agda":{"declarations":[],"receipts":[],"route":"unavailable","state":"AGDA-PENDING","token":"OPEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Idris2 only, so ungraded under 8.1.","reference":{"idris2":{"declarations":["Trope.Soundness.soundFromExact"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"Grade soundness, exact lowering"},{"foundation_diverse_witness":null,"id":"tsub-soundness","kind":"theory","legs":{"agda":{"declarations":[],"receipts":[],"route":"unavailable","state":"AGDA-PENDING","token":"OPEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Idris2 only, so ungraded under 8.1.","reference":{"idris2":{"declarations":["Trope.Soundness.subSound"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"T-Sub soundness"},{"foundation_diverse_witness":null,"id":"verdict-soundness","kind":"engineering","legs":{"agda":{"declarations":[],"receipts":[],"route":"unavailable","state":"AGDA-PENDING","token":"OPEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Classified engineering: the statement is about the shipped checker's verdict function over its own types, so 8.1 puts it off the ladder entirely and it carries section 5 tokens only. Note that verdictSound is typed over Grade while the shipped checker's floor is a different type decided by a different predicate, and no lemma connects them.","reference":{"idris2":{"declarations":["Trope.Soundness.verdictSound"],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"PROVEN"}},"title":"Verdict soundness (corollary)"},{"foundation_diverse_witness":null,"id":"grade-soundness-core","kind":"theory","legs":{"agda":{"declarations":["TB.Reduction","TB.Substitution.cut-preserves-grade"],"receipts":["agda-c0eb4f1"],"route":"re-proved","state":"AGDA-VERIFIED","token":"PROVEN"},"lean":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"},"rocq":{"declarations":[],"receipts":[],"route":"unavailable","state":"NOT-INVENTORIED","token":"OPEN"}},"notes":"Inherits Target 3's fragment: the beta/let core only, with the fix case open (CO-1).","reference":{"idris2":{"declarations":[],"state":"not-a-leg (PROOF-POLICY 8.1 excludes engineering provers from the PWG ladder)","token":"OPEN"}},"title":"Grade soundness, beta/let core"}]}