Repository navigation
Phase 0: make the status surfaces true (trope-checker) - #102
Open
hyperpolymath wants to merge 16 commits into
Open
hyperpolymath wants to merge 16 commits into
hyperpolymath wants to merge 16 commits into
Conversation
… on the ratified carrier spec/calculus.adoc was a v0.1 document (revnumber 0.1, 2026-06-22) with the 2026-07-07 ratification spliced in as notes, a separate never-merged v0.2 addendum (spec/calculus-v0.2-draft.adoc, 2026-06-23), and two design notes carrying the operational model and the L4 analysis. It still said "seven effects" while the vocabulary, EffectAtoms.lean and the IR say nine. A reader — or an agent — following the spec alone got the pre-ratification world. This folds the four into one v0.2 spec. What changed, section by section: - §1: the object is stated as "property-instances as particulars", which every instance ontology supplies (tropes, modes, moments, qualities, SDCs), rather than as a commitment to one-category trope theory; §2 names the two constructs (attenuate, detach/FloatingQuality) that need instances to be particulars and would not survive a change of ontology. - §3: the fate chain, bond fibring (HC-4) and merge are stated on the ratified carrier with A1–A3 inline; new §3.5 gives the nine-effect / nine-atom-family table (EffectAtoms.lean) and the two structure theorems, so "seven" and "nine" are reconciled: nine families, six writable, three faults. - §4: L3 and L5 cover all three deceptive bottoms (two-sided zeros, A1); L4 is stated as holding in full with the Idris2/Lean/Agda lemma names; L6 (commutativity) is new; the addendum's R-2026-06-23-02..04 become the cancellation structure C1–C3 with the ratified lemma names; the tropical factorisation re-run is recorded as (B′) sighted, with the pre-ratification (B) result kept as history. - §5 T-Fuse: ⊔ is written ⊓ — the retention-order meet, "no better than its worse constituent" — matching the CO-1 note. Same meaning, one symbol. - §6: the prevent/detect decision now names all three deceptive duals. - §7: restated as greatest post-fixed point in the retention order with the decidable T-Fix-Decl rule, from the CO-1 note; the operational model is marked DESIGNED and its mechanisation OPEN. - §8: each soundness result carries its status (exact lowering and β/let PROVED; conservative lowering and fix OPEN); the third firewall now cites a defined O5. - §9.3: prover roles per the 2026-10-12 kernel ruling (Agda kernel, Idris2 executable reference, Lean provenance, Rust fast core) — see ADR 0005. - §10: O1 split into O1-carrier (PROVED) and O1-coord (OPEN, with the bond-transfer probe recorded as the live falsifier); O4 RESOLVED (ADR 0004); O5 DEFINED (adopted from the workbench proposal of 2026-07-17); O6 (ceiling verdict) newly opened; CO-1 listed with its DESIGNED/OPEN split. Every lemma name cited in the spec was checked against the source files on this branch (Idris2 Trope.*, Agda TB.*, Lean grade-boundary/* and grade-factorisation/*). No normative rule changes semantics; the IR stays 0.2. The README's repo map, firewall 3 and Status paragraph are brought into step; INTEGRATION-REPORT.adoc gets a header note marking it historical rather than being rewritten. CHANGELOG, ADR 0003 and PROOF-STATUS's dated history keep their references to the addendum as records of what was true when written.
…n source The `agda-theorem-b` job installed Agda from the runner's apt. ubuntu-latest is 24.04, whose agda-stdlib is 1.7.3, and Theorem B imports Data.Product.Base (stdlib >= 2.0): the job fails at scope checking (exit 42). Reproduced here 2026-10-13 with Agda 2.6.3 / stdlib 1.7.3, exactly the runner's pair. The workflow's own comment records a green run "under 2.6.4.3", which was a Debian machine, not the runner. Because the workflow is paths-filtered to verification/proofs/**, it has not run since the last proof change and the red was never seen. Fix: fetch the Agda 2.7.0.1 release binary and the agda-stdlib v2.0 archive, verify both SHA-256 sums, register the stdlib under the name theorem-b.agda-lib depends on (`standard-library`; the 2.0 archive calls itself `standard-library-2.0`), set Agda_datadir and a UTF-8 locale. Verified 2026-10-13 with exactly these artefacts and sums: All.agda and Smoke.agda typecheck under --safe --without-K, exit 0 (~100 s cold). The stdlib sum is of the GitHub-generated tag archive (no release asset exists); if GitHub ever regenerates it the checksum step fails loudly instead of testing something else. Also: `lean-source-honesty` and the mirroring `verify-all` recipe gated only the two v0.1 files (GradeBoundary, GradeFactorisation). The spec now cites GradeRatified, L4Monotonicity, TierTwoComplete, EffectAtoms and GradeFactorisationR, so both now iterate every tracked Lean source. All eight files pass the gate's regexes as they stand (run here). actionlint -shellcheck= on proofs.yml: clean. The job's real run is still needed: this sandbox has no Lean, so the lean-build matrix was not exercised.
What was wrong: PROOF-STATUS.adoc (revdate 2026-06-23) described the v0.1
carrier — a non-commutative ▷, a lax L4 that "fails on fate", CO-1 "gated by
O4", the OPEN-B/B′/C documentation gaps, "10/10" conformance — and listed as
open several results (O1 exhaustiveness, L4/L5 as lemmas) that are now proved.
A reader following it alone got the pre-ratification world.
What changed: one "Proved" table on the ratified carrier (Carrier & laws /
Cancellation / Factorisation / Metatheory / Soundness), citing only lemma names
that exist in the Idris2, Agda and Lean sources; one "Open" list matching
spec/calculus.adoc §10 (CO-1 mechanisation, O1-coord, O2, O3, O5 mechanisation,
O6) with where each is specified; the four modelling notes carried over; the
06-22 / 06-23 / 06-29 sections collapsed to one dated paragraph each under
"History", prefixed as superseded by R-2026-07-07 where they disagree.
What I ran: every cited identifier checked present by grep over
verification/proofs/{idris2/Trope,agda/theorem-b/TB,lean4} (38 + 43 + 44 names,
none missing); the acceptance grep for the stale phrases outside "== History"
returns nothing.
What I did not run: no prover in this commit (the AFFIRMATION commit carries
the runs).
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
What was wrong: ROADMAP listed v0.2 as "in progress" with the v0.1 vocabulary (CO-1 "gated by O4", the lax-L4 argument, OPEN-B/B′/C, a separate spec addendum) although the carrier was ratified on 2026-07-07 and the spec consolidated at v0.2. What changed: "Shipped (v0.2)" lists the ratified carrier (ADR 0004), the Agda carrier migration, L4 in full and L6, the atom factorisation (O1-carrier), TierTwoComplete, the sighted factorisation re-run and the spec consolidation; "Open problems" defers to spec/calculus.adoc §10 by reference and names CO-1 mechanisation as the next proof work; Deferred items kept. What I ran: grep for "gated by O4|lax|OPEN-B|OPEN-C" over the file — no hits. What I did not run: nothing else; documentation-only. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
What was wrong: the newest AFFIRMATION entry (2026-06-29) described the v0.1 carrier and cited 10/10 conformance cases and 8 schema-invalid fixtures; the corpus has been 13 + 9 for months and the carrier was ratified on 2026-07-07. What changed: a dated entry with an anchor (branch, commit, UTC time, exact toolchain), one bullet per command, a short proved/open paragraph naming only identifiers that exist, and two findings; :revdate: bumped. What I ran (all in this session, on this branch): idris2 --typecheck verification/proofs/idris2/trope.ipkg -> exit 0 just trope-build && bash tests/conformance/run.sh -> 13 + 9, all pass just trope-rust -> 13 + 9, all pass just build-agda -> PASS (All + Smoke) apt agda 2.6.3 + agda-stdlib 1.7.3 on All.agda -> exit 42 (finding 1) lean-source-honesty regexes over 8 .lean files -> clean What I did not run: just build-lean (no lake / Mathlib reachable here) — written as NOT RUN with the command named; the proofs.yml lean-build job is the attestation and is cited in the PR. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
…n CO-1 alone What was wrong: the NOT-REACHED footer of TB/Reduction.agda listed two obstructions to fix-subject-reduction, the second being "a LIMIT CARRIER … the open O4 fork (Conat-vs-tag)". ADR 0004 resolved O4 on 2026-07-07 (the finitary carrier suffices; transfinitely deep fix is inexpressible), and the operational model has since been designed. What changed (comment only, no code): the footer now states one obstruction — the operational model — DESIGNED in spec/notes/2026-07-07-co1-operational-model.adoc (λ-trope, tagged values, T-Fix-Decl) with its mechanisation plan (that note's §6, steps 1–5, extending this module), records O4 as RESOLVED by ADR 0004, and keeps "NOT-REACHED, NO postulate" and the tier-stability remark. What I ran: just build-agda (agda --safe --without-K All.agda + Smoke.agda) with this edit in the tree -> PASS, exit 0. What I did not run: nothing else applies. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
What was wrong: verification/proofs carried TypeSafety.v (Coq), StateMachine.tla (TLA+) and Properties.agda — mint templates whose own text says "Replace with your project's …", never instantiated — and the trees, usage lines and recipes advertised a fourth and fifth prover the roles ruling does not assign here. What changed: git rm of the three files; their lines dropped from the verification/proofs/README.adoc and docs/status/PROOF-NEEDS.adoc trees and the `just proof-check-coq` usage line; proof-check-coq removed from proof-check-all and the Coq/TLA+ lines from proof-status (proof-scan-dangerous keeps its harmless -name '*.v'); the awk's historical false-positive note no longer names the removed file by path. The INTEGRATION-REPORT mention stays as history. What I ran: git grep -n "TypeSafety\|StateMachine\|Properties.agda" -> only INTEGRATION-REPORT.adoc; just proof-status -> runs (Idris2 14, Lean4 8, Agda 9 files); just proof-check-all -> runs and is red for pre-existing reasons unrelated to this change (per-file idris2/agda checks from the repo root cannot resolve module names; the ABI/Types Idris2 mint templates do not typecheck) — recorded in AFFIRMATION and as an issue; just proof-scan-dangerous -> PASS. What I did not run: coqc / tlc (not installed, and no longer referenced). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
…er roles (Proposed) What was wrong: the spec consolidation of 2026-10-13 adopted O5, opened O6, wrote the prover roles into §9.3 and cited "ADR 0005" for all of it, but no ADR 0005 existed; the carrier-as-parameter question had no recorded home. What changed: docs/decisions/0005-…adoc in the 0004 layout — Status (Proposed, owner to accept), Context, Decisions D1–D6 (D1 v0.2 normative; D2 O5 adopted from the workbench proposal of 2026-07-17 unchanged in substance; D3 O6 opened; D4 prover roles per the 2026-10-12 kernel ruling; D5 three provers, templates removed; D6 recorded-not-decided: fidelity carrier as a parameter, Phase 1A), Consequences, Rejected alternatives. What I ran: nothing to run; the referenced files and identifiers were checked present (workbench note path, spec §9.3/§10, the removed templates). What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
What was wrong: CHANGELOG [Unreleased] stopped at the IR 0.2 normalisation and the 2026-06 developments; the spec consolidation, the proofs.yml pin, the status rewrites, ADR 0005 and the template removal were unrecorded. What changed: the v0.2 consolidation line from the foot of spec/calculus.adoc; one line each for the status-surface rewrites (T1–T4), the proofs.yml pin, ADR 0005 (Added) and the template removal (Removed). docs/status/READINESS.adoc was grepped for the same stale phrases as PROOF-STATUS and has none, so it is untouched (it remains the unfilled CRG template, which is not false). What I ran: grep -nE "non-commutative|lax L4|L4 fails|OPEN-B|OPEN-C|gated by O4|10/10|8 schema" docs/status/READINESS.adoc -> no hits. What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 12 minutes. View limit details
📝 Summary
Merge Risk:
 |
| Check name | Status | Explanation |
|---|---|---|
| Title check |  |
The title clearly identifies the Phase 0 objective and accurately summarises the main status and verification updates. |
| Description check | |
The description includes the required Summary, Changes, RSR Quality Checklist, Testing, and Screenshots sections. It records completed checks, limitations, pre-existing failures, and owner-only action… |
| Docstring Coverage | |
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Documentation-only edits and deletions within survi… |
| Linked Issues check | |
Check skipped because no linked issues were found for this pull request. |
| Out of Scope Changes check | |
Check skipped because no linked issues were found for this pull request. |
Full details: Description check
-
Explanation
The description includes the required Summary, Changes, RSR Quality Checklist, Testing, and Screenshots sections. It records completed checks, limitations, pre-existing failures, and owner-only actions with sufficient detail.
Full details: Docstring Coverage
-
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 0 files. (14 skipped: 14 unsupported.)
Finishing Touches
-
🛠️ Fix failing CI checks
-
- Commit to this branch
- Create a new PR
-
- Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.
Comment @coderabbitai help to get the list of available commands.
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
This was referenced Oct 27, 2026
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
…I Lean run What was wrong: spec §9.3, PROOF-STATUS and verification/proofs/README said the Lean developments' axiom audits show "propext/Quot.sound only". The proofs.yml lean-build run on this branch (40472568287) prints the audit: Trope.nine_families (EffectAtoms.lean), FateA.Q_add_left_cancel and FateA.atten_cancel_on_normalForms (GradeRatified.lean) also depend on Classical.choice. GradeBoundary.lean's own footer had listed Classical.choice all along; the surfaces overclaimed. What changed: the three surfaces now say "no sorryAx, no user axiom; propext, Quot.sound and, in three theorems, Classical.choice"; the AFFIRMATION entry's Lean bullet cites the CI run (lake build succeeded for both packages; the job is red only in lean-action's optional nanoda step, which cannot compile its lean4export under the v4.16.0 toolchain, as on main — issue #104) and records this as finding (3). What I ran: read the job logs of run 40472568287 (both Lean jobs): "Build completed successfully", one axiom line per theorem, then "nanoda check failed". What I did not run: lake build locally (unchanged: no lake here). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
Owner
Author
CI triage on this PR (head
|
… ratified carrier What was wrong (review findings on #102): the Reduction.agda footer said "the gfp's fidelity lands in the absorbing tops {total, unknown}" for every fix; that holds for a body that attenuates and recurses without bound, not for F(γ) = γ (gfp Present) or a body that ignores its binder (finite gfp). PROOF-NEEDS.adoc rows DOM-1/2/6/7/8 still described a non-commutative ▷, CO-1 "gated by O4", a "lax L4", and "propext/Quot.sound only". What changed: the footer restricts the absorbing-top argument to unbounded attenuation and names the other cases the fix proof must cover (comment only); DOM-1 marks non-commutativity historical and points at GradeRatified.lean, DOM-2 drops "non-commutative", DOM-6 records CO-1 as DESIGNED (O4 resolved) with mechanisation OPEN, DOM-7 drops the lax-L4 framing, DOM-8 records the (B′) re-run; "propext/Quot.sound only" becomes "no user axiom". What I ran: just build-agda after the footer edit -> PASS (All.agda + Smoke.agda); grep -n "non-commutative\|gated by O4\|lax L4\|Quot.sound" docs/status/PROOF-NEEDS.adoc -> none. What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
Owner
Author
Review round 1 — summary and hand-back stateChanged since the CI triage comment (head now
Review threads
Not run here: Owner-only: accept ADR 0005; sign the AFFIRMATION commit on landing; decide D6; the two open normative threads above; #103 / #104 / #105; SonarCloud. Generated by Claude Code |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3d907be7d2
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
… theorem is on Review round 2 (Codex, CodeRabbit) on PR #102: - proofs.yml lean-source-honesty and the `verify-all` recipe strip comments with tests/lib/strip-proof-comments.awk and match the bare `sorry`/`admit` tokens, so `:= by` followed by an indented `sorry` on the next line fails the gate (the old line-anchored regex passed it; ApiTypes.lean is not built by either Lake package, so the gate was its only check). Tested: all eight tracked .lean files still PASS; synthetic multiline sorry/admit now FAIL; "sorry-free" prose in comments still PASSes. actionlint clean. - README / ROADMAP: "carry no axioms" -> "no `sorryAx` and no user axiom", the wording the axiom audit supports (propext, Quot.sound, Classical.choice x3). - PROOF-STATUS, README, AFFIRMATION: the atom factorisation (`EffectAtoms.lean`) imports GradeBoundary and is a theorem about the v0.1 `Grade`; no GradeR restatement exists. Recorded as Open (O1-carrier on GradeR) and as AFFIRMATION finding (4); the spec's §6/§10 wording is left for the owner. - PROOF-NEEDS DOM-3: symmetric cut holds on the ratified carrier (`cut-grade-comm`); the v0.1 refutation is historical. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
Owner
Author
|
Review round 2 (Codex on 3d907be) — pushed as 70a8109. Fixed:
Deferred to the owner, threads left open, collected in #106: L3 vs CI on this head: still the pre-existing reds only (Lean jobs red in lean-action's Generated by Claude Code |
hyperpolymath
enabled auto-merge (squash)
October 27, 2026 11:04
|
✅ Coding Agent task started: View task and status The task will inspect the CI failures, validate its fix, and commit the fix to this branch automatically.
⏭️ Checks skipped: 4 · already failing on `main` (not caused by this PR)
|
|
Add Carrot credits or activate Agent usage billing to use Autofix |
hyperpolymath
added a commit
to hyperpolymath/vocarium
that referenced
this pull request
Oct 27, 2026
## Summary
Phase 0 of the trope-stack plan ("make the truth legible"): reconcile
this repo's status surfaces with what actually runs. Tasks V1–V2 of the
Phase 0 brief (V3 is filed as an issue, not changed here). One commit
per task. Documentation only; no code changed.
Sibling PRs: [trope-checker
#102](hyperpolymath/trope-checker#102) ·
[trope-particularity-workbench
#77](hyperpolymath/trope-particularity-workbench#77)
· [haec #81](hyperpolymath/haec#81) · [hermeneia
#76](hyperpolymath/hermeneia#76). Suggested
landing order: trope-checker, workbench, haec, hermeneia, this one.
Deferred: [#43 A2ML
retirement](#43), [#44
TROPECHECK_PIN
bump](#44).
## Changes
- **V1** `AFFIRMATION.adoc` — the estate template is filled. The two
executable claims (`zig build test`; the invoke-slice gate
`tests/e2e/invoke_slice.sh`) are marked **NOT RUN here** with the exact
command and the reason: the session could not execute Zig 0.16.0
(ziglang.org and all community mirrors were unreachable through the
proxy; a checksummed conda-forge 0.16.0 binary was fetched but the
session's permission classifier refused to run it). The CI workflow
`vocarium-ci.yml` (mlugg/setup-zig pinned to 0.16.0 → `zig build test` →
the gate) is named as the attestation; its run on this PR is cited below
once it completes. The store-format / wire-boundary claim is "affirmed
(by reading)". "What we do NOT claim":
evoke/convoke/transvoke/provoke/revoke, the M2 `StoreProvider` adapter,
Haec ingestion, `neighbours`, and that nothing of `voc` was executed in
the session. The gate's own checker pin `69221ad6` is recorded.
- **V2** `README.adoc` — new `## Where this repo sits` with the
five-repo map paragraph, verbatim.
- **V3** — recorded as issue #44, not changed: bump `TROPECHECK_PIN` in
`tests/e2e/invoke_slice.sh` to a post-ratification checker commit once
Phase 0 lands upstream.
## RSR Quality Checklist
### Required
- [ ] Tests pass — `zig build test` NOT RUN in the authoring session
(see above); CI on this PR is the check
- [x] Code is formatted (no code changed)
- [x] Linter is clean (no code changed)
- [x] No banned language patterns
- [x] No `unsafe` blocks without `// SAFETY:` comments (none added)
- [x] No banned functions
- [x] SPDX license headers present on all new/modified source files
- [x] No secrets, credentials, or `.env` files included
### As Applicable
- [ ] `vocarium_chora.deed` — not applicable (A2ML still in place here;
retirement is issue #43)
- [x] Documentation updated for user-facing changes
- [ ] `docs/architecture/TOPOLOGY.adoc` — architecture unchanged
- [ ] `CHANGELOG` — not touched (docs-only status pass)
- [ ] New dependencies — none
- [ ] ABI/FFI changes — none
## Testing
Nothing of `voc` was run in the authoring session; the AFFIRMATION says
so in each row rather than copying a result. The checks that were run
elsewhere in the same session and that this repo's claims depend on:
`tropecheck-rs` built from trope-checker `44020f9`; its conformance
corpus 13 + 9 passing.
Not run: `zig build test`; `TROPECHECK_BIN=<tropecheck-rs> bash
tests/e2e/invoke_slice.sh`. Expected from CI: `GATE PASS: invoke slice
proven (use-relativity + warrant door + unit tests)`.
## Owner-only items
- Sign the AFFIRMATION commit on landing.
- A2ML retirement in this repo (issue #43).
- The `TROPECHECK_PIN` bump (issue #44) once the trope-checker Phase 0
PR lands.
## Screenshots
n/a
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
---------
Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
hyperpolymath
added a commit
to hyperpolymath/trope-particularity-workbench
that referenced
this pull request
Oct 27, 2026
#77) ## Summary Phase 0 of the trope-stack plan ("make the truth legible"): one ground-truthed table for the whole stack, and the research programme brought into step with the consolidated calculus (spec v0.2, ADR 0005 Proposed). Tasks W1–W2 of the Phase 0 brief. One commit per task. Documentation only. Sibling PRs: [trope-checker #102](hyperpolymath/trope-checker#102) · [haec #81](hyperpolymath/haec#81) · [hermeneia #76](hyperpolymath/hermeneia#76) · [vocarium #42](hyperpolymath/vocarium#42). Suggested landing order: trope-checker, this one, haec, hermeneia, vocarium. ## Changes - **W1** `docs/status/STATE-OF-THE-STACK.adoc` (new, CC-BY-SA-4.0) — one table, one row per repo: status · what exists · obligations it owns · proof/test citations · ground-truth command · last verified; the five-repo map paragraph; a Known gaps list (A2ML still in haec/hermeneia/vocarium; vocarium's checker pin `69221ad6`; this repo's stuck Pages run and cancelled Secret scan; Lean not run in the Phase 0 session). Linked from `README.adoc` "Where to go next". - **W2** `docs/status/RESEARCH-PROGRAMME.adoc` — "four-prover verification stack" → "three-prover (Agda, Idris2, Lean) verification stack plus a Rust fast core"; WP-2 gains a Status line (delivered: O5 is defined in `trope-checker/spec/calculus.adoc §10`, ADR 0005, ratification pending); one sentence puts O6 (the ceiling verdict) on the spine as the security-facing obligation; the References caveat about stale checker status files becomes "Current as of 2026-10-27"; `:revnumber:` 0.3, `:revdate:` 2026-10-27. ("gated by O4" does not occur in the file.) `docs/theory/formalisms/defining-o5-veridicality-oracle.adoc` Status section now opens with "Adopted into trope-checker spec §10 on 2026-10-13 (ADR 0005, pending owner ratification)." ## RSR Quality Checklist ### Required - [x] Tests pass (`bash tests/check-vocabulary.sh` → nine effects consistent) - [x] Code is formatted (no code) - [x] Linter is clean (no code) - [x] No banned language patterns - [x] No `unsafe` blocks (n/a) - [x] No banned functions (n/a) - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ### As Applicable - [ ] `trope-particularity-workbench_chora.deed` — project state unchanged (documentation repo) - [x] Documentation updated for user-facing changes - [ ] `docs/architecture/TOPOLOGY.adoc` — n/a - [ ] `CHANGELOG` — not touched - [ ] New dependencies — none - [ ] ABI/FFI changes — none ## Testing Run in the session on workbench `ae42fdf`, 2026-10-27: ``` bash tests/check-vocabulary.sh vocabulary-check: nine effects consistent across vocabulary/ (9), trainer, map, README grep -n "four-prover\|gated by O4\|Caveat" docs/status/RESEARCH-PROGRAMME.adoc -> no hits ``` The dates in the STATE-OF-THE-STACK table are the dates the cited commands were run in the same session (recorded in the sibling repos' AFFIRMATION entries). The vocarium row says NOT RUN and points at CI. ## Owner-only items - Unstick the GitHub Pages (trainer) run queued since 2026-10-06 and the cancelled Secret scan (repository settings). - Accept ADR 0005 upstream (trope-checker #102), on which the WP-2 "delivered" line depends. ## Screenshots n/a 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --------- Co-authored-by: Claude <noreply@anthropic.com>
|
🤖 Completed: Fix CodeRabbit issues in PR #102 — View commit |
hyperpolymath
disabled auto-merge
October 27, 2026 14:34
hyperpolymath
enabled auto-merge (squash)
October 27, 2026 14:34
hyperpolymath
added a commit
to hyperpolymath/hermeneia
that referenced
this pull request
Oct 27, 2026
## Summary
Phase 0 of the trope-stack plan ("make the truth legible"): reconcile
this repo's status surfaces with what actually runs, from commands run
in the session that wrote them. Tasks H1–H3 of the Phase 0 brief. One
commit per task. Documentation only; no code or semantics changed.
Sibling PRs: [trope-checker
#102](hyperpolymath/trope-checker#102) ·
[trope-particularity-workbench
#77](hyperpolymath/trope-particularity-workbench#77)
· [haec #81](hyperpolymath/haec#81) · [vocarium
#42](hyperpolymath/vocarium#42). Suggested
landing order: trope-checker, workbench, haec, this one, vocarium.
Deferred: [#77 A2ML
retirement](#77).
## Changes
- **H1** `AFFIRMATION.adoc` — the estate template is filled from a real
run: `cargo test --workspace` (39 tests: gate 4, store 7, ir 11, core 8,
syntax 9) and the e2e invoke slice (7 tests). Anchor: commit `21b1593`,
2026-10-27T07:50Z, rustc 1.97.0, checker binary built from trope-checker
`44020f9`. "What we do NOT claim": the six unimplemented vokes, `show
loss` / `show warrant`, nothing Integrated (stub store), no proofs of
our own.
- **H2** `docs/THEORY.adoc` — "six-coordinate grade" (5 occurrences) →
"three coordinate kinds — fate (per field), bond, merge — over six
slots", matching `trope-checker/spec/calculus.adoc §3`; the open
question becomes "whether the three coordinate kinds are complete"
(calculus O1-coord).
- **H3** `README.adoc` — under the voke-family table: "Implemented
end-to-end and tested: `invoke`. The other six parse and are refused as
unimplemented — status table in `docs/SPEC.adoc`."; new `## Where this
repo sits` with the five-repo map paragraph. No other README claim
changed.
## RSR Quality Checklist
### Required
- [x] Tests pass (`cargo test --workspace` → 39 passed; e2e slice → 7
passed)
- [x] Code is formatted (no code changed)
- [x] Linter is clean (no code changed)
- [x] No banned language patterns
- [x] No `unsafe` blocks without `// SAFETY:` comments (none added)
- [x] No banned functions
- [x] SPDX license headers present on all new/modified source files
- [x] No secrets, credentials, or `.env` files included
### As Applicable
- [ ] `hermeneia_chora.deed` updated — not applicable (A2ML still in
place here; retirement is a deferred issue)
- [x] Documentation updated for user-facing changes
- [ ] `docs/architecture/TOPOLOGY.adoc` — architecture unchanged
- [ ] `CHANGELOG` — not touched (docs-only status pass)
- [ ] New dependencies — none
- [ ] ABI/FFI changes — none
## Testing
Run in the session, on hermeneia `21b1593` (Ubuntu 24.04 container,
rustc 1.97.0):
```
cargo test --workspace -> 39 passed, 0 failed
HERMENEIA_TROPECHECK=<tropecheck-rs> cargo test -p hermeneia-cli --features e2e --test slice
-> 7 passed, 0 failed
grep -n -i "six-coordinate\|six coordinates" docs/THEORY.adoc -> no hits
```
`tropecheck-rs` was built with `cargo build --release` from
trope-checker `44020f9` (`main` 216f23b plus the two Phase 0 spec/CI
patches, which do not touch `src/rust`).
Not run: nothing else is claimed.
## Owner-only items
- Sign the AFFIRMATION commit on landing.
- Decide whether the README demotion in H3 should go further.
- A2ML retirement in this repo (deferred; issue #77).
## Screenshots
n/a
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
hyperpolymath
added a commit
to hyperpolymath/haec
that referenced
this pull request
Oct 27, 2026
## Summary
Phase 0 of the trope-stack plan ("make the truth legible"): reconcile
this repo's status surfaces with what actually runs, from commands run
in the session that wrote them. Tasks A1–A2 of the Phase 0 brief. One
commit per task. Documentation only.
Sibling PRs: [trope-checker
#102](hyperpolymath/trope-checker#102) ·
[trope-particularity-workbench
#77](hyperpolymath/trope-particularity-workbench#77)
· [hermeneia #76](hyperpolymath/hermeneia#76) ·
[vocarium #42](hyperpolymath/vocarium#42).
Suggested landing order: trope-checker, workbench, this one, hermeneia,
vocarium. Deferred: [#82 A2ML
retirement](#82).
## Changes
- **A1** `README.adoc` — the five-repo map paragraph, verbatim, appended
to "Where it sits — the three-repo picture".
- **A2** `AFFIRMATION.adoc` — a `== As of 2026-10-27` entry from
`TROPECHECK_BIN=<tropecheck-rs> bash tests/check-examples.sh`: 3
examples well-formed, the vendored `design/trope-ir.schema.json` matches
the canonical checker schema, 3 round-trips to the stated verdicts
(`faithful-record` sufficient, `survey-collapse` insufficient at
`e_collapse/fate.quality`, `station-average` sufficient). The honest
scope is kept: no compiler, no LSP, no runtime, O2 stated not
discharged, no proofs. `:revdate:` bumped.
## RSR Quality Checklist
### Required
- [x] Tests pass (`tests/check-examples.sh` → all ok)
- [x] Code is formatted (no code changed)
- [x] Linter is clean (no code changed)
- [x] No banned language patterns
- [x] No `unsafe` blocks without `// SAFETY:` comments (none added)
- [x] No banned functions
- [x] SPDX license headers present on all new/modified source files
- [x] No secrets, credentials, or `.env` files included
### As Applicable
- [ ] `haec_chora.deed` — not applicable (A2ML still in place here;
retirement is issue #82)
- [x] Documentation updated for user-facing changes
- [ ] `docs/architecture/TOPOLOGY.adoc` — architecture unchanged
- [ ] `CHANGELOG` — not touched (docs-only status pass)
- [ ] New dependencies — none
- [ ] ABI/FFI changes — none
## Testing
Run in the session on haec `e9bee39`, 2026-10-27T07:49Z:
```
TROPECHECK_BIN=<tropecheck-rs> bash tests/check-examples.sh
ok faithful-record.haec → faithful-record.ir.json (well-formed IR, expects p-sufficient)
ok survey-collapse.haec → survey-collapse.ir.json (well-formed IR, expects p-insufficient)
ok station-average.haec → station-average.ir.json (well-formed IR, expects p-sufficient)
ok vendored design/trope-ir.schema.json matches the canonical checker schema
ok round-trip faithful-record.ir.json → p-sufficient
ok round-trip survey-collapse.ir.json → p-insufficient (witness e_collapse/fate.quality)
ok round-trip station-average.ir.json → p-sufficient
examples: all lower to valid Trope IR
```
`tropecheck-rs` built from trope-checker `44020f9` (`main` 216f23b plus
the two Phase 0 spec/CI patches, which do not touch `src/rust`).
Not run: nothing else is claimed.
## Owner-only items
- Sign the AFFIRMATION commit on landing.
- A2ML retirement in this repo (issue #82).
## Screenshots
n/a
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
---------
Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
|
hyperpolymath
disabled auto-merge
October 28, 2026 14:28
hyperpolymath
added a commit
that referenced
this pull request
Oct 28, 2026
…lus knots Review-thread remediation for PRs #102/#107 (Codex + CodeRabbit): - proofs.yml axiom audit could hide a source axiom given a compiler-internal-looking name (private axiom forged_spec): the old filter excused any component containing _spec/_cstage/_unfold as a substring and dropped violations by declaration shape. Now: anchored compiler-minted component shapes only; any axiom DECLARED in the gated sources is never excused; a violation is dropped only when nothing non-allowlisted remains in it. The source tripwire is token-based (private/protected axiom now caught) and also rejects addDecl/axiomDecl. - workflow-linter resolver deduplicated by (repo, ref), so only the first reusable-workflow path per repo@SHA was existence-checked (eight of nine standards paths were unchecked). Dedup is now per coordinate; commit/tag resolution still happens once per (repo, ref). - ci/CI-CRITICALITY.toml: the retired static-analysis-gate entry is gone (its earlier removal was clobbered) and fork-governance is actually listed. - spec/calculus.adoc: 'deceptive' disambiguated into grade-deceptive (Falsified/Misbound/Conflated) vs fidelity-tier-deceptive (Unknown/top), at the Veridicality Derivation, L3 and C3, so Dropped absorbing Attenuated(top) no longer reads as laundering; C2 stated per carrier (unquotiented iff epsilon; A3-normalized finite core); O1-carrier now cites EffectAtomsRatified.GradeR.atom_factorization, the proof on the carrier in use; the detect profile is defined uniformly for all three deceptive duals (trope-ir aligned). - tests/workflows/review_regressions_test.sh: regression cases for the per-coordinate path check and for the axiom filter (extracted verbatim from proofs.yml; forged_spec declared/undeclared, internal-decl + sorryAx, genuine IR placeholders). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
hyperpolymath
enabled auto-merge (squash)
October 28, 2026 23:00
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Phase 0 of the trope-stack plan ("make the truth legible"): one normative spec on the ratified carrier, a CI pin that actually typechecks Theorem B, and every status surface rewritten from commands run in the session that wrote it. Nine commits, one per task: the two pre-existing patches (spec v0.2 consolidation;
proofs.ymlAgda pin + Lean gate) followed by T1–T7 of the Phase 0 brief. No semantics changed; no theorem proved; the IR stays 0.2.Sibling PRs: hermeneia #76 · vocarium #42 · haec #81 · trope-particularity-workbench #77. Suggested landing order: this one first, then workbench, haec, hermeneia, vocarium.
Changes
spec/calculus.adocconsolidated at v0.2: nine effects with the atom-family table, A1–A3 inline, L1–L6 with lemma names (L6 commutativity new), cancellation structure C1–C3, tropical factorisation recorded as (B′) sighted, §7 as greatest post-fixed point + T-Fix-Decl, §8 soundness with per-result status, §9.3 prover roles, §10 with O1 split / O4 RESOLVED / O5 DEFINED / O6 opened / CO-1 DESIGNED-mechanisation-OPEN.spec/calculus-v0.2-draft.adocfolded in and removed; README and INTEGRATION-REPORT aligned.proofs.yml: the Agda job fetches Agda 2.7.0.1 + agda-stdlib 2.0 by SHA-256 (ubuntu-latest's apt pair, 2.6.3 + 1.7.3, fails atData.Product.Base); the Lean honesty gate andverify-allcover all eight.leanfiles.actionlintclean.docs/status/PROOF-STATUS.adocrewritten to the ratified world: one Proved table (Carrier & laws / Cancellation / Factorisation / Metatheory / Soundness) citing only identifiers that exist (grep-verified: 38 Idris2 + 43 Agda + 44 Lean names); Open list = spec §10; modelling notes carried over; 06-22/06-23/06-29 collapsed into dated History paragraphs.docs/status/ROADMAP.adoc: Shipped (v0.2); Open problems by reference to §10; "gated by O4", lax L4 and OPEN-B/B′/C gone as current items.AFFIRMATION.adoc: a 2026-10-27 entry from a full re-run (below), with two findings.TB/Reduction.agdafooter (comment only): O4 is RESOLVED by ADR 0004; the single remaining obstruction is the operational model, DESIGNED in the CO-1 note, mechanisation plan §6 steps 1–5 extending this module; "NOT-REACHED, NO postulate" kept.just build-agdastill exits 0.coq/TypeSafety.v,tlaplus/StateMachine.tla,agda/Properties.agda) removed with their tree and recipe references;git grepfor their names now hits only INTEGRATION-REPORT (history).docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc(Proposed — owner to accept): D1 v0.2 normative; D2 O5 adopted from the workbench proposal of 2026-07-17; D3 O6 opened; D4 prover roles (Agda kernel, Idris2 reference, Lean provenance, Rust fast core); D5 three provers; D6 recorded-not-decided: fidelity carrier as a parameter (resource-algebra), Phase 1A.CHANGELOG.adoc: the v0.2 line and one line each for T3–T6.docs/status/READINESS.adocgrepped for the stale phrases: none, left untouched.RSR Quality Checklist
Required
just trope-build && bash tests/conformance/run.sh(13 + 9),just trope-rust(13 + 9),just build-agda(exit 0);just build-leanNOT RUN locally (see Testing) —proofs.ymlon this branch is the checkactionlint -shellcheck= -pyflakes= .github/workflows/proofs.ymlclean)unsafeblocks without// SAFETY:comments (none added)grep -rnE 'believe_me|assert_total|postulate'over the Idris2 trees → none; Lean honesty regexes over 8 files → clean; Agda--safe).envfiles includedAs Applicable
trope-checker_chora.deed— not touched (brief: deeds are owner-only)docs/architecture/TOPOLOGY.adoc— architecture unchangedCHANGELOGupdatedTesting
All on this branch, 2026-10-27, Ubuntu 24.04 container; toolchain Agda 2.7.0.1 + agda-stdlib 2.0 (tag v2.0), Idris2 0.8.0 (built from tag v0.8.0 on Chez 9.5.8), rustc 1.97.0, just 1.40.0:
Not run locally:
just build-lean— nolake, and the Lean toolchain and Mathlib cache hosts are unreachable from the container. Theproofs.ymllean-buildmatrix on this branch is the attestation; it is paths-filtered, so it has beenworkflow_dispatched onclaude/new-session-snuoroand its run will be cited here when green.Observed, not fixed (pre-existing, issue filed):
just proof-check-allis red onmaintoo:proof-check-idris2/proof-check-agdarun per-file checks from the repo root so module names do not resolve, and theverification/proofs/idris2/ABI/*+Types.idrmint templates do not typecheck. The gates that mean something (just check,build-agda,trope-rust,verify-all) are green.Owner-only items
mainas of the brief (scorecard, hypatia-scan, governance, Secret scan, Trope conformance) will be triaged on this PR's checks as they report.Screenshots
n/a
Generated by Claude Code