hyperpolymath · Oct 27, 2026 · Oct 27, 2026 · Oct 27, 2026 · Oct 27, 2026
@@ -200,6 +200,8 @@ https://github.com/hyperpolymath/trope-particularity-workbench/tree/b18eb67dcf10
 * https://hyperpolymath.github.io/trope-particularity-workbench/[the trainer] (source: `assets/particularity-trainer.html`) — drill until you can name the move from the test.
 * `docs/background.adoc` — why the vocabulary is compatible with the metaphysics it
   borrows from.
+* link:docs/status/STATE-OF-THE-STACK.adoc[State of the trope stack] — one table, one row per repo: status, what exists,
+  the obligations it owns, proof/test citations, and the ground-truth command that verifies it.
 * `docs/status/RESEARCH-PROGRAMME.adoc` — the prioritised, trope-stack-wide programme of
   work (what is worth doing next in the field, and who might fund it).
 * `docs/theory/computing/trope-theory-and-neural-representation.adoc` — a position paper

@@ -1,8 +1,8 @@
 // SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = A Programme of Work for Trope Theory
-:revnumber: 0.2 (draft for review; synced to ratified calculus R-2026-07-07 / ADR 0004)
-:revdate: 2026-07-16
+:revnumber: 0.3 (draft for review; synced to calculus v0.2 and ADR 0005, Proposed)
+:revdate: 2026-10-27
 :toc: macro
 :sectnums:
 :sectnumlevels: 3
@@ -33,7 +33,8 @@ This estate has started to build that missing dynamics:
   residual, a use-model, two verdicts), grounded in Williams/Campbell
   (`docs/background.adoc`). Status: *specification*.
 * `trope-checker` — the *graded calculus*, the Trope IR (the trust boundary), and a
-  four-prover verification stack. Status: *alpha, conformance-green*.
+  three-prover (Agda, Idris2, Lean) verification stack plus a Rust fast core. Status:
+  *alpha, conformance-green*.
 * `haec` (front-end language, *design*), `vocarium` (store, *M1 invoke slice; M2
   adapter pending*), `hermeneia` (query, *implementation*).
 
@@ -81,6 +82,11 @@ each companion document refers back to it.
 | Ask whether provenance-enrichment relocates or dissolves the regress (WP-1).
 |===
 
+Security-facing, and new at calculus v0.2: *O6*, the ceiling verdict
+(`trope-checker/spec/calculus.adoc §10`) — the privacy direction, that no more than a
+declared ceiling is retained, which the `Withheld`/`Severed` distinction exists to serve —
+is the dual of the sufficiency verdict and sits on this spine as an open obligation.
+
 == How to read the work packages
 
 Priority is triage, not chronology:
@@ -146,6 +152,11 @@ provide, and the checker's exact relationship to it), or a proof that veridicali
 *not* checkable relative to the IR — with the README/AFFIRMATION references updated to
 match.
 
+*Status.* Delivered: O5 is defined in `trope-checker/spec/calculus.adoc §10` (ADR 0005,
+ratification pending), adopted on 2026-10-13 from
+`../theory/formalisms/defining-o5-veridicality-oracle.adoc` unchanged in substance; what
+remains is its mechanisation (O5-1 as a side condition on an `Oracle`-indexed verdict).
+
 *Closes.* *O5* (define-or-refute).
 
 *Funder fit.* EPSRC / UKRI (formal methods); ARIA _Mathematics for Safe AI_.
@@ -289,7 +300,7 @@ the funding memo.
 | *Essay + ORCID/DOI first* | WP-8's low-cost items unblock every funding application immediately.
 |===
 
-A pragmatic first quarter: WP-2 (define O5) and WP-8's cheap items (ORCID, DOI,
+A pragmatic first quarter: WP-2's remainder (ratify ADR 0005, mechanise O5-1) and WP-8's cheap items (ORCID, DOI,
 corrected citation, the essay) are low-effort and unblock both honesty and funding;
 WP-1 and WP-4 are the two papers most likely to attract a grant; WP-5 is the
 time-critical foundational one.
@@ -315,10 +326,9 @@ for work not yet done, and should be read as such.
   and atoms), and the ratified-carrier proofs
   (`L4Monotonicity.lean`, `EffectAtoms.lean`, `TierTwoComplete.lean`,
   `GradeRatified.lean`, `GradeFactorisationR.lean`).
-  *Caveat:* `trope-checker/docs/status/{ROADMAP,PROOF-STATUS}.adoc`,
-  `AFFIRMATION.adoc`, and `INTEGRATION-REPORT.adoc` were not updated in the
-  ratification wave and still describe the pre-07-07 world — prefer ADR 0004 and the
-  spec where they disagree.
+  *Current as of 2026-10-27:* `trope-checker/docs/status/{ROADMAP,PROOF-STATUS}.adoc` and
+  `AFFIRMATION.adoc` were rewritten to the ratified world in Phase 0;
+  `INTEGRATION-REPORT.adoc` is kept as the historical record under a header note.
 * Founding grounding: `trope-particularity-workbench/docs/background.adoc`.
 * Companion documents: `../theory/computing/trope-theory-and-neural-representation.adoc`,
   `../whitepapers/outreach/baffled-couch-potatoes.adoc`,

@@ -0,0 +1,98 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+= State of the trope stack — 2026-10-27
+:toc: macro
+
+One table, one row per repository: what each one is, what exists, which open
+obligations it owns, where its proofs and tests are, and the command that
+verifies the row. "Last verified" is the date the command in that row was run
+and the result observed; a row that could not be run says so and names the CI
+run that attests it instead.
+
+toc::[]
+
+== The table
+
+[cols="1,1,3,2,2,2,1",options="header"]
+|===
+| Repo | Status | What exists | Obligations it owns | Proof / test citations | Ground-truth command | Last verified
+
+| trope-particularity-workbench
+| specification
+| The nine effects (`vocabulary/`), the particularity trainer, the pipeline map,
+the research programme, the O5 proposal (adopted upstream into
+`trope-checker/spec/calculus.adoc §10`, ADR 0005 pending ratification).
+| O1-coord metaphysical adequacy (WP-5).
+| `tests/check-vocabulary.sh` (nine effects consistent across vocabulary, trainer,
+map, README).
+| `bash tests/check-vocabulary.sh`
+| 2026-10-27
+
+| trope-checker
+| alpha
+| Spec v0.2 (one normative document on the ratified carrier), Trope IR 0.2 +
+JSON schema, Idris2 reference checker + Rust fast core, Agda kernel (Theorem B),
+Lean provenance developments, conformance suite.
+| CO-1 mechanisation; O3; O5 and O6 mechanisation; O2 for its own fixtures only.
+| `docs/status/PROOF-STATUS.adoc` (proved table / open list), `AFFIRMATION.adoc`
+2026-10-27 entry: 13 verdict + 9 schema-invalid conformance cases pass on both
+checkers; `All.agda`/`Smoke.agda` under `--safe --without-K` exit 0.
+| `just check`, `just build-agda`, `just trope-rust`; `just build-lean` (needs lake
++ Mathlib; CI `proofs.yml`)
+| 2026-10-27; Lean: `proofs.yml` run 40472568287 (2026-10-27T08:18Z) — `lake build`
+succeeded for both packages, the job is red only in lean-action's `nanoda` step
+(trope-checker #104)
+
+| haec
+| design
+| Grammar (`design/grammar.ebnf`), elaboration table with per-construct O2
+obligations, three example program/IR pairs that round-trip through the checker.
+| O2 lowering correctness for its constructs.
+| `AFFIRMATION.adoc` 2026-10-27: 3 well-formed, schema matches canonical, 3
+round-trips to the stated verdicts.
+| `TROPECHECK_BIN=/path/to/tropecheck-rs bash tests/check-examples.sh`
+| 2026-10-27
+
+| hermeneia
+| implementation (M1)
+| `invoke` end to end against the checker; the other six vokes parse and are
+refused as unimplemented; `show loss` refused (needs the checker's loss vector);
+stub store.
+| None of the calculus's; O2 as a producer, once it emits IR from a real store.
+| `AFFIRMATION.adoc` 2026-10-27: `cargo test --workspace` 39 pass; e2e slice 7
+pass (`src/hermeneia-cli/tests/slice.rs`).
+| `cargo test --workspace`; `HERMENEIA_TROPECHECK=/path/to/tropecheck-rs cargo test -p
+hermeneia-cli --features e2e --test slice`
+| 2026-10-27
+
+| vocarium
+| M1 invoke slice
+| `voc` store engine (pure Zig, ADR-0002 wire-not-link): JSONL replay, warrant
+door, `voc invoke` emitting Trope IR 0.2; the use-relativity gate. M2
+StoreProvider adapter pending.
+| None of the calculus's; O2 as a producer; O5-2 attestations are its warrants.
+| `AFFIRMATION.adoc` 2026-10-27 (NOT RUN in that session; CI `vocarium-ci.yml`
+runs `zig build test` and the gate on pushes to `main`, pull requests and dispatch).
+| `zig build test`; `TROPECHECK_BIN=/path/to/tropecheck-rs bash tests/e2e/invoke_slice.sh`
+| CI run 40472451463, job "invoke-slice gate": success, 2026-10-27T08:17Z (vocarium #42)
+|===
+
+== The five-repo map
+
+Vocabulary track: trope-particularity-workbench → haec → trope-checker (verdict).
+Store/query track: haec → vocarium → hermeneia → trope-checker (verdict).
+trope-checker depends on nothing (HC-1); the workbench depends on nothing;
+vocarium and hermeneia meet at the M2 StoreProvider adapter (vocarium ADR-0002:
+wire, do not link).
+
+== Known gaps
+
+* A2ML machine-readable files are still present in haec, hermeneia and vocarium
+  (retired in this repo and in trope-checker); retirement is written up as an
+  issue per repo, not done in Phase 0.
+* vocarium's gate pins checker commit `69221ad6`, which predates the spec v0.2
+  consolidation; the pin is to be bumped once Phase 0 lands upstream (issue).
+* This repo's GitHub Pages (trainer) run has been queued since 2026-10-06 and a
+  Secret scan run was cancelled; both are repository settings, owner-only.
+* `trope-checker`'s `just build-lean` was not run in the Phase 0 session (no
+  Lean toolchain reachable there); its `proofs.yml` CI job is the attestation.
@@ -97,6 +97,12 @@ right slots, which is evidence the definition carves at a real joint:
   world-access vouched (O5-1) and left an attestation (O5-2).
 
 == Status and next step
+*Status update, 2026-10-27.* The text below was written when `spec/calculus.adoc §10`
+stopped at O4. Since the consolidation of 2026-10-13 that section carries O5, adopted
+from this note unchanged in substance (trope-checker ADR 0005, *Proposed*); owner
+ratification is pending, so the "proposal" and "never written down" language below is
+historical — the normative text is now the spec's, and this note is its derivation.
+
 
 This note is the WP-2 deliverable in its *define* branch (the *refute* branch — that no
 useful oracle interface exists — is answered by the constructions above existing).