[hyperpolymath]

Summary

This draft adds an experiment in Cubical Agda. The experiment decides, for a defined fragment, the strong form of the systemet wager: grades (L2), conversion-only equality (L1) and tropes can replace the coercions and roles of System FC.

A proof is a success. A machine-checked counterexample is also a success.

Status: stages 0 and 1 of 7 are complete. The claim is not decided yet. Keep this pull request as a draft until verification/proofs/agda/Wager/VERDICT.adoc is final.

The experiment claims no ET obligation. It does not change docs/theory/OBLIGATIONS.adoc, AFFIRMATION.adoc or any .a2ml file. A new obligation needs an ADR from the owner.

Changes

• verification/proofs/agda/Wager/: the target calculus and its metatheory (29 Agda modules, --cubical --safe, no postulate).
  • Statements.agda: each headline theorem as a type only, with a plain-English reading. Review this file first.
  • Proofs.agda: one inhabitant for each statement.
  • L1: kinds with graded arrows, types over a signature, DefEq, a total nf, and DefEq t u ↔ nf t ≡ nf u.
  • L2: terms, a declarative graded typing judgement with subusage, and T0 (graded substitution, preservation, progress) for each grade algebra.
  • Two instances: Affine {0,1,ω} with the systemet order, and the 2-point lattice.
  • Examples/Stage1.agda: one accepted and one rejected closed example for each theorem.
  • VERDICT.adoc (draft), RELATION-LEDGER.adoc (no ADDED entry), RULE-DIFF-LEDGER.adoc (empty), DESIGN-CHOICES.adoc, TOOLCHAIN.adoc, PLAN.adoc.
• verification/proofs/agda/MANIFEST and wager.agda-lib.
• .github/workflows/proofs.yml: an agda job. It installs the pinned Agda 2.8.0 tarball (checksum-verified) and the pinned agda/cubical v0.9 commit, and runs scripts/check-proofs.sh agda. It uses the two actions that the workflow already uses.
• docs/status/PROOF-STATUS.adoc: the marker line gate:agda gated=29, one summary row and one section for the experiment.
• verification/proofs/README.adoc, Justfile (test recipe), CHANGELOG.adoc: small updates for the new prover directory.

Findings of Stage 1 that the owner can check in VERDICT.adoc:

• The Lean class GradeAlgebra has 15 law fields and one derived law. The documents say 16 laws.
• With the systemet order of Affine, the grades 0 and 1 are not comparable, so an unused binder of grade 1 is rejected. The anytype order 0 ≤ 1 ≤ ω accepts it.
• T0 uses 14 of the 15 law fields. It does not use le-antisym. It uses a · 0 = 0.

RSR Quality Checklist

Required

• Tests pass (just test or equivalent). Run in the session: scripts/check-proofs.sh agda (PASS, 29 modules), scripts/scan-dangerous.sh (PASS), scripts/check-proof-status.sh (PASS), scripts/check-root-shape.sh (PASS), scripts/check-no-md-in-docs.sh (PASS). Not run in the session: the Lean4 gate (no Lean toolchain there). CI runs it.
• Code is formatted. Not applicable: the repository has no formatter for Agda.
• Linter is clean. A clean build prints no warning. One warning class is silenced in 18 files (UnsupportedIndexedMatch); DESIGN-CHOICES.adoc (DC-0.3) gives the reason.
• No banned language patterns
• No unsafe blocks without // SAFETY: comments (none exist)
• No banned functions
• SPDX license headers present on all new/modified source files
• No secrets, credentials, or .env files included

As Applicable

• .machine_readable/6a2/STATE.a2ml updated. Not done on purpose: this is a file of the owner.
• .machine_readable/6a2/ECOSYSTEM.a2ml updated. Not applicable.
• .machine_readable/6a2/META.a2ml updated. Not applicable: no ADR is filed.
• Documentation updated for user-facing changes
• TOPOLOGY.md updated. Not applicable.
• CHANGELOG or release notes updated
• New dependencies reviewed for license compatibility. Agda and agda/cubical are MIT-style. CI downloads them at pinned versions. Nothing is vendored.
• ABI/FFI changes validated. Not applicable.

Testing

• The gate was watched to fail before its green result was trusted: a false lemma, a postulate (rejected by --safe and by the danger scan), a hole, and a wrong grade table each fail the gate. TOOLCHAIN.adoc has the record.
• The steps of the new CI job were run in the session with an empty home directory: checksum OK, cubical commit OK, gate PASS in about 66 seconds.
• --guardedness is on in each file, because the stock cubical v0.9 library forces it on each importer. No file uses coinduction (DC-0.2).

Screenshots

Not applicable.

---

Generated by Claude Code

[coderabbitai]

Caution

Review failed

The pull request is closed.

Summary

Summary by CodeRabbit

• New Features
  • Added a Cubical Agda proof track for coercions and roles, with proofs covering L1 equality and T0 substitution, preservation and progress.
  • Added examples demonstrating accepted and rejected typing, including affine and two-level grade systems.
  • Added a proof gate to automated checks and the test recipe.
• Documentation
  • Documented the proof track’s scope, status, design choices, toolchain and outstanding stages.

The pull request adds a Cubical Agda wager experiment with grade algebras, L1 normalisation and equality proofs, and an L2 graded calculus with substitution, preservation and progress proofs. It adds examples, experiment records, and proof-check integration in local and CI workflows.

Changes: Cubical Agda Wager Experiment

Layer / File(s)	Summary
Proof gate and experiment setup .github/workflows/proofs.yml, Justfile, verification/proofs/agda/MANIFEST, verification/proofs/agda/wager.agda-lib, verification/proofs/README.adoc, verification/proofs/agda/Wager/Everything.agda, verification/proofs/agda/Wager/TOOLCHAIN.adoc, verification/proofs/agda/Wager/PLAN.adoc, docs/status/PROOF-STATUS.adoc, CHANGELOG.adoc	The workflow pins Agda and the cubical-library commit, verifies the Agda archive checksum and library commit, and runs the proof check. The manifest lists gated modules. The local test recipe, documentation and status records include the Agda experiment and its stated proof status.
Grade algebra foundations verification/proofs/agda/Wager/Grade/*, verification/proofs/agda/Wager/L2/Usage.agda, verification/proofs/agda/Wager/L2/UsageLaws.agda	The modules define grade operations and laws, finite-carrier law checks, affine and two-point-level grade algebras, and usage-vector and matrix operations with their laws.
L1 syntax and normaliser verification/proofs/agda/Wager/L1/Signature.agda, Syntax.agda, SyntaxLemmas.agda, Normal.agda, Eval.agda, Conversion.agda, Heads.agda, Kinding.agda, verification/proofs/agda/Wager/DESIGN-CHOICES.adoc	The L1 modules define signatures, kinded types, renaming and substitution, normal forms, evaluation-based normalisation, definitional equality, head analysis and graded kinding. The design record documents Stage 1 choices.
L1 normalisation and equality proofs verification/proofs/agda/Wager/L1/Soundness.agda, Completeness.agda, Equality.agda	The proofs establish soundness and completeness for normalisation and derive both directions between definitional equality and equality of normal forms.
L2 terms, typing and usage verification/proofs/agda/Wager/L2/Signature.agda, Term.agda, Typing.agda, Inversion.agda, Usage.agda, UsageLaws.agda	The modules define L2 signatures, scoped terms, values, reductions, graded typing and usage operations. Inversion lemmas recover typing information for variables, literals and applications.
L2 renaming and substitution proofs verification/proofs/agda/Wager/L2/Renaming.agda, Substitution.agda	The proofs transport typing through renaming and establish typing preservation for parallel substitution and top-variable substitutions, with usage bounds derived from usage matrices.
L2 preservation, progress and examples verification/proofs/agda/Wager/L2/Preservation.agda, Progress.agda, verification/proofs/agda/Wager/Statements.agda, Proofs.agda, Examples/Stage1.agda, RELATION-LEDGER.adoc, RULE-DIFF-LEDGER.adoc, VERDICT.adoc	The metatheory proves preservation and progress. The statements, proof witnesses and examples cover the grade algebras, L1 equality and T0 properties. The ledgers and verdict record the experiment’s classifications and proof status.

Estimated code review effort: 5 (Critical) | ~90 minutes

Change: Feature

Merge Risk: Low · up to 222c3

The change adds a proof experiment and CI gate with no runtime impact. Two documentation fixes remain, one stale status statement and one install command that can overwrite a developer's existing Agda library registrations. Both are small and safe to merge with a follow-up.

- [ ] 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.

Share

• X
• Mastodon
• Reddit
• LinkedIn

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

[chatgpt-codex-connector]

Codex Review Summary: ❌ Failed

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	❌ Failed 2026-11-10T02:54:47.637796Z We couldn’t complete this review. Comment @codex review to try again.	222c3f7	Draft marked ready

ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

[hyperpolymath]

CI status on the head 222c3f7.

Pass, and from this pull request: agda proof gate (wager experiment) (new job) and lean4 proof gate (it includes the danger scan and the status drift gate).

Fail, but not from this pull request. Each of these 4 checks also fails on main at the base commit 6570d46:

Check	Cause in the log	Same on main	Fix
lint-workflows	"missing SPDX header" for every workflow file. The check reads line 1 only, and line 1 of each file is the banner of gh actions-lock.	yes (Workflow Security Linter, run 200)	Proposal, not applied here: let the check read the first 5 lines (head -5) in .github/workflows/workflow-linter.yml.
Validate K9 contracts	11 errors in 18 K9 files ("Missing pedigree block"). This branch changes no K9 file.	yes (Dogfood Gate, run 194)	None from this branch. The K9 files need their pedigree blocks.
Hypatia neurosymbolic scan	"Hypatia found 6 critical security issue(s)".	yes, the same count of 6 (Static Analysis Gate, run 194)	None from this branch. The count did not change, so this branch adds no critical finding.
SonarQube	"Not authorized or organization not found".	yes (SonarQube, run 192)	None from this branch. The scanner credentials or the organization key need a fix.

I did not widen this pull request to fix these checks.

---

Generated by Claude Code