docs: correct two files that misstate the code they describe

PROOF-NEEDS.md claimed "1 `Admitted` in proofs/coq/lambda/LambdaCNO.v".
Measured against absolute-zero @87902bb7: there are ZERO `Admitted` anywhere.
`y_not_cno` is a KEPT AXIOM with a written rationale (LambdaCNO.v:388-399).

The old wording was wrong in both directions — it overstated the incompleteness
and understated the trusted base by a factor of 23. There are 23 `Axiom`
declarations across 6 .v files, already classified by an in-source AXIOM AUDIT
(end of physics/LandauerDerivation.v), which this file now points at as the
authoritative record instead of duplicating it.

Operationally the distinction matters: an `Axiom` PASSES a "no sorry / no
Admitted" gate silently, so counting only `Admitted` measures the wrong thing.

Promoted to the top of "What Needs Proving": the audit's own SOUNDNESS WARNINGS
— `prob_nonneg`, `prob_normalized` (false over unconstrained function-type
distributions) and `shannon_entropy_maximum` (stated inequality is backwards).
All three are currently unused, which makes them cheap to fix now and expensive
to discover later. Removed `y_not_cno` from that list: the in-source rationale
explains it needs an invariant closed under the full reduction congruence, or a
coinductive argument — out of scope, not "concrete and closable".

aletheia/CLAUDE.md said all logic lives in src/main.rs (~950 lines) and "don't
split into modules unless >1000 lines". It has been 5 modules / 995 lines for a
while, with main.rs at 121. That instruction would have told the next agent to
undo the existing structure. Also corrected: 23 workflows -> 16, flake.nix
listed but absent, 18 integration tests -> 32.

Added to aletheia/CLAUDE.md a prominent warning that those 16 nested workflows
have NEVER run (Actions reads .github/workflows/ at the repo root only) — the
fault that let this crate stay uncompilable for a month — and a note on the
#124/#125 gap explaining why the integration suite is a UI contract, not a spec.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -6,29 +6,73 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 ## Current State
 
+*Re-measured 2026-07-27 against the `absolute-zero` submodule at `87902bb7`.*
+
 - **src/abi/*.idr**: NO
-- **Dangerous patterns**: 1 `Admitted` in `proofs/coq/lambda/LambdaCNO.v` (y_not_cno theorem)
+- **`Admitted` count**: **0** (`grep -rn Admitted absolute-zero --include=*.v`)
+- **Trusted base**: **23 `Axiom` declarations across 6 `.v` files**, each classified
+  in-source. See the **AXIOM AUDIT** block at the end of
+  `proofs/coq/physics/LandauerDerivation.v` — that audit, not this file, is the
+  authoritative record.
 - **LOC**: ~22,700 (Rust + Coq)
 - **ABI layer**: Missing
-- **Existing proofs**: Coq proofs for lambda CNO (3/4 proven), quantum mechanics exactness
+- **Existing proofs**: Coq proofs for lambda CNO, Landauer derivation chain,
+  quantum mechanics exactness
+
+> **Correction (2026-07-27).** This file previously claimed *"1 `Admitted` in
+> `proofs/coq/lambda/LambdaCNO.v` (y_not_cno)"*. There are **zero** `Admitted`
+> anywhere. `y_not_cno` is a **KEPT AXIOM** — a declared trust assumption with a
+> written rationale (`LambdaCNO.v:388-399`), not an unproven hole. The old wording was
+> wrong in both directions: it overstated the incompleteness *and* understated the
+> trusted base by a factor of 23.
+>
+> The distinction matters operationally: an `Axiom` **passes** a "no `sorry` /
+> no `Admitted`" gate silently, so counting only `Admitted` measures the wrong thing.
+> Any proof gate for this repo must scan for `Axiom` too.
+
+### Axiom classification (summarised from the in-source audit)
+
+| Class | Count | Meaning |
+|---|---|---|
+| METAL-BOUNDARY | 6 | genuine empirical physics, not derivable (k_B, temperature, Second Law, isothermal work bound, Landauer lower bound, reversible ⇒ zero dissipation) |
+| SPECIFICATION | 4 | sound, but not dischargeable while `shannon_entropy` / `product_dist` stay opaque |
+| NOT-YET-DISCHARGED (class A) | 2 | `cno_preserves_shannon_entropy`, `cno_zero_energy_dissipation_derived` |
+| SOUNDNESS WARNINGS | 3 | **false as stated**, currently **unused** — see below |
+
+The audit is notably self-critical: it records that
+`cno_zero_energy_dissipation_derived` is an axiom **despite its `_derived` name**, and
+that the triage docs' "DISCHARGE" marks on it and on `reversible_zero_dissipation` are
+**inaccurate**. Both are kept honestly rather than fake-derived.
 
 ## What Needs Proving
 
 | Component | What | Why |
 |-----------|------|-----|
-| Y combinator non-CNO (y_not_cno) | Close the remaining Admitted proof | 1 of 4 lambda CNO theorems is incomplete |
+| **Unsound-but-unused axioms** | Fix or delete `prob_nonneg`, `prob_normalized` (false over unconstrained function-type distributions — need a bundled distribution type) and `shannon_entropy_maximum` (**stated inequality is backwards** — asserts uniform *minimises* entropy) | They are false. Unused today, so harmless today; the moment anything cites one, it proves anything. **Highest priority.** |
+| `cno_preserves_shannon_entropy` | Discharge, or accept as a stated postulate | class A — carrier/quotient issue |
+| `cno_zero_energy_dissipation_derived` | Rename, or supply `internal_energy` CNO-invariance | `internal_energy` is an opaque `Parameter` with no preservation law, so this cannot be a pure derivation |
 | Absolute-zero brainfuck interpreter | Interpreter preserves CNO properties | Claims of computational zero need formal backing |
-| Absolute-zero whitespace interpreter | Same as brainfuck — CNO preservation | Both esoteric interpreters need same guarantee |
+| Absolute-zero whitespace interpreter | Same as brainfuck — CNO preservation | Both esoteric interpreters need the same guarantee |
 | Aletheia verification checks | Verification pipeline produces sound results | Rhodibot extraction depends on correct checks |
 | Quantum mechanics proofs | Extend QuantumMechanicsExact.v coverage | Existing proofs are partial |
 
+**Not on this list: `y_not_cno`.** It is not a "concrete, closable proof obligation".
+The in-source rationale explains why: a rigorous proof must rule out reaching the
+argument under *every* interleaving of `beta_reduce` (which permits reduction under
+binders and on either side of an application), requiring an invariant closed under the
+full reduction congruence, or a coinductive / step-indexed non-termination argument.
+Genuinely out of scope, not merely tedious.
+
 ## Recommended Prover
 
-**Coq** — Existing proof infrastructure is in Coq. The `y_not_cno` Admitted needs to be closed in Coq. Aletheia (Rust) verification would benefit from an **Idris2** ABI layer.
+**Coq** — the existing proof infrastructure is in Coq. Aletheia (Rust) verification
+would benefit from an **Idris2** ABI layer.
 
 ## Priority
 
-**MEDIUM** — Has existing proof infrastructure with one known gap. The Admitted y_not_cno is a concrete, closable proof obligation. Aletheia verification correctness is more important long-term.
+**MEDIUM** — the proof infrastructure is real and its trusted base is honestly
+documented. The one genuinely urgent item is the three **unsound** axioms: they are
+currently unused, so this is cheap to fix now and expensive to discover later.
 
 ## Template ABI Cleanup (2026-03-29)
 

aletheia/CLAUDE.md

@@ -49,26 +49,56 @@ Aletheia maintains **zero unsafe blocks** for RSR compliance.
 
 ## Architecture Principles
 
-### Single-File Implementation
+### Module Layout (updated 2026-07-27 — this section was stale)
 
-All core logic lives in `src/main.rs` (~950 lines). This design is intentional:
+> **This file used to say "all core logic lives in `src/main.rs` (~950 lines)" and
+> "don't split into modules unless >1000 lines". Both were out of date.** The crate has
+> been split for some time. Measured 2026-07-27:
 
-**Benefits**:
-- Easy to audit (one file to read)
-- Minimal complexity
-- Clear code flow
-- No hidden abstractions
+| File | Lines | Contents |
+|---|---|---|
+| `src/main.rs` | 121 | CLI entry, arg parsing, `verify_repository`, exit policy |
+| `src/checks.rs` | 316 | `check_documentation`, `check_spdx_headers`, `check_workflow_pins`, `check_path_security`, glob matching |
+| `src/config.rs` | 243 | `.aletheia.toml` loading, hand-rolled TOML parse |
+| `src/output.rs` | 226 | human / JSON / SARIF report printing, date+time formatting |
+| `src/types.rs` | 89 | `ComplianceLevel`, `CheckResult`, `ComplianceReport`, … |
+| **total** | **995** | |
+
+The single-file rationale still applies *in spirit* — prefer few, auditable files over
+deep abstraction — but do not "restore" the single-file layout, and do not treat 1000
+lines as a threshold that has not yet been crossed.
 
 **When to add more files**:
 - Integration tests in `tests/` directory
 - Examples in `examples/` directory
 - Documentation in `docs/` directory
 
 **When NOT to add files**:
-- Don't split into modules unless >1000 lines
 - Don't create abstractions prematurely
 - Don't add utility files for one-off functions
 
+### Known gap: the CLI is unfinished (issues #124 / #125)
+
+`main.rs` parses only `<repo-path>` plus `--json` / `--sarif`, and wires **three**
+checks. `tests/integration_tests.rs` is 806 lines / 32 tests describing a much larger
+tool (16 Bronze checks plus Silver, `--help`, `--version`, `--verbose`, `--badge`,
+`--init-hook`, `--format=`, HTML output). **2 pass, 27 fail.**
+
+Two things to know before touching it:
+
+1. **Those tests assert on stdout substrings**, e.g.
+   `assert!(stdout.contains("Bronze-level RSR compliance: ACHIEVED"))`. They pin the
+   *wording* of the report and say nothing about what the checks must verify — so they
+   can be satisfied by checks that verify nothing. Treat them as a UI contract, not a
+   specification.
+2. **A definition of RSR conformance already exists** elsewhere in the estate (hypatia's
+   `rsr-conformance` oracle). Writing checks to satisfy these strings risks creating a
+   second, divergent definition. Resolve the source-of-truth question first.
+
+Most of the clippy findings in #125 are dead code that exists *because* those modules
+are unwired. **Do not silence them with `#![allow(dead_code)]`** — the root Rust CI
+header forbids it, and that dead code is the specification of the missing feature.
+
 ### Type Safety First
 
 Leverage Rust's type system:
@@ -274,23 +304,26 @@ When making changes, ensure these remain true:
 
 ```
 aletheia/
-├── src/
-│   └── main.rs              # Core implementation (~950 lines)
+├── src/                     # 5 modules, 995 lines total — see Module Layout above
+│   ├── main.rs              # CLI entry (121)
+│   ├── checks.rs            # compliance checks (316)
+│   ├── config.rs            # .aletheia.toml (243)
+│   ├── output.rs            # human/JSON/SARIF (226)
+│   └── types.rs             # core types (89)
 ├── tests/
-│   └── integration_tests.rs # Integration tests (18 tests)
+│   └── integration_tests.rs # 32 tests — 2 pass, 27 fail (issue #124)
 ├── benches/                 # Performance benchmarks
 ├── examples/                # Usage examples
 ├── fuzz/                    # Fuzzing infrastructure
 ├── .well-known/
 │   ├── security.txt         # RFC 9116 security contact
 │   ├── ai.txt               # AI training policies
 │   └── humans.txt           # Human attribution
-├── .github/workflows/       # 23 GitHub Actions workflows
+├── .github/workflows/       # 16 files — ⚠ ALL INERT, see below
 ├── Cargo.toml               # Zero dependencies, MSRV 1.80
 ├── Cargo.lock               # Lock file (commit this)
 ├── Justfile                 # Build automation
-├── flake.nix                # Nix reproducible builds
-├── .gitlab-ci.yml           # CI/CD pipeline
+├── .gitlab-ci.yml           # CI/CD pipeline (GitLab mirror)
 ├── .gitignore               # Git ignore patterns
 ├── README.adoc              # User documentation (AsciiDoc)
 ├── SECURITY.md              # Security policy
@@ -305,6 +338,22 @@ aletheia/
 └── META.scm                 # Project metadata and ADRs
 ```
 
+### ⚠ The 16 workflows in `aletheia/.github/workflows/` have NEVER run
+
+`aletheia/` is **vendored into `maa-framework` as plain tracked files** (mode 100644),
+not a submodule, and GitHub Actions reads `.github/workflows/` **at the repository root
+only**. There is no standalone `hyperpolymath/aletheia` repo running them either — it was
+deleted around January 2026 and its content vendored here.
+
+Consequence: editing anything under `aletheia/.github/workflows/` has **no effect on
+CI whatsoever**. This is not hypothetical — it is how commit `b5322c2` (2026-06-17) left
+this crate **failing to compile for over a month** with nobody noticing.
+
+**The real gate is `/.github/workflows/rust-ci.yml` at the repository root.** It runs
+`cargo build` (debug + release), `cargo test`, `cargo fmt --check` and a zero-dependency
+assertion, with `working-directory: aletheia`. Add gates there, not here. See
+`aletheia/.github/workflows/README.md`.
+
 ## Troubleshooting
 
 ### "Dependency detected" error
@@ -368,7 +417,7 @@ For questions about this document or Aletheia development:
 
 ---
 
-**Last Updated**: 2026-02-05
-**Version**: 1.1
+**Last Updated**: 2026-07-27
+**Version**: 1.2
 
 *"Alētheia is not just absence of falsehood, but active unconcealment of truth."*