fix: real SHA-pinning check, real Justfile targets, and docs that match the code (#144)

Three independent commits, each droppable on its own. Two fix gates that
could never fail; one fixes documentation that actively misdirects.

---

## 1. `docs:` — two files misstate the code they describe

### `PROOF-NEEDS.md`

Claimed *"1 `Admitted` in `proofs/coq/lambda/LambdaCNO.v` (y_not_cno)"*.
Measured against `absolute-zero 87902bb7`:

```
$ grep -rn "Admitted" absolute-zero --include=*.v | wc -l
0
$ grep -rn "^Axiom"  absolute-zero --include=*.v | wc -l
23
```

**Zero `Admitted`. Twenty-three `Axiom`s across 6 files.** The old
wording was wrong in *both* directions — it overstated the
incompleteness and understated the trusted base 23×.

> **Why this matters operationally:** an `Axiom` **passes** a "no
`sorry` / no `Admitted`" gate silently. Counting only `Admitted`
measures the wrong thing.

`y_not_cno` is a **KEPT AXIOM** with a written rationale
(`LambdaCNO.v:388-399`), not an unproven hole — and it is *not* the
"concrete, closable proof obligation" the old text claimed. The
in-source note explains it needs an invariant closed under the full
reduction congruence, or a coinductive/step-indexed argument.

The doc now defers to the **AXIOM AUDIT** already in
`physics/LandauerDerivation.v`, which 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 are
inaccurate.

**Promoted to the top of "What Needs Proving"** — the audit's own
SOUNDNESS WARNINGS: `prob_nonneg` and `prob_normalized` are false over
unconstrained function-type distributions, and
`shannon_entropy_maximum`'s inequality is **backwards** (asserts uniform
*minimises* entropy). All three are currently **unused** — cheap now,
expensive later.

### `aletheia/CLAUDE.md`

Said *"all core 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, `main.rs` at 121. That instruction would tell the
next agent to **undo the existing structure**.

Also corrected: 23 workflows → 16; `flake.nix` listed but absent; 18
integration tests → 32. Added a prominent warning that those 16 nested
workflows have **never run** (root-only discovery) — the fault that let
this crate stay uncompilable for a month.

---

## 2. `fix(aletheia):` — the SHA-pinning check could never fail

```rust
if line.contains("@v") && !line.contains("@") {
```

`contains("@v")` **implies** `contains("@")`, so the second clause is
always false and `has_unpinned` could never be set. Proven before
changing anything:

```
uses: actions/checkout@v4    old_detects_unpinned=false
```

This is aletheia's Silver-level *"GitHub Actions SHA pinning"* check —
and pointedly, the exact check that would have caught
`SonarSource/sonarqube-scan-action@master`, the unpinned action that
broke this repo's Governance and CodeQL in #139.

Replaced with `uses_line_is_pinned`, requiring 40 hex chars after the
final `@`, which also:
- accepts the inline `- uses:` form (the estate's existing linter
anchors to line-start and misses it)
- ignores a trailing `# v7.0.1` provenance comment, so a correct pin
with a stale comment isn't a false positive
- exempts `./…` local actions/reusables and `docker://` refs

Also replaced `assert!(true)` in `test_file_exists` with a real
assertion, anchored on `env!("CARGO_MANIFEST_DIR")` so it is
deterministic regardless of CWD.

**Verified:** 29 unit tests (was 26) · `cargo fmt --check` clean ·
clippy 25 → 23. End-to-end `cargo run -- .` now reports `[FAIL] GitHub
Actions SHA pinning`, correctly finding the one genuinely unpinned
action — where before the fix it reported a pass.

Refs #125.

---

## 3. `fix(#99):` — root `Justfile` was a fake gate

```make
build:
    @echo "Build not configured yet"
```

`build`, `test`, `fmt`, `lint`, `clean` all printed a string and
**exited 0**. Wired to the same commands root `rust-ci.yml` runs, in the
same order, so `just check` means what CI means.

Two deliberate limits, documented **in the recipes** so nobody "fixes"
them:
- `test` is `--bins` only — the integration suite is a spec for a CLI
that doesn't exist; 27/29 fail by design (#124). Adding `--tests` would
make the bar green by breaking it.
- `lint` is not yet `-D warnings` (#125). When that closes it must be
added **here and to `rust-ci.yml` together**, so local and CI never
disagree.

**Verified by running them, not reading them:** `just deps-check` → `OK:
zero dependencies`; `just test` → 29 passed; `just check` → exit 0.

**And verified the gate can actually fail** — appending badly-formatted
Rust makes `just fmt` exit 1 while `just build` still exits 0; reverting
restores 0. A gate nobody has watched fail is not a gate.

Closes #99.

---

## Not in this PR

- **#124** — still blocked on the source-of-truth question for RSR
checks
- **`guix.scm`** identity/licence clobber — separate, more urgent: #143

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

Author: hyperpolymath

Justfile

@@ -8,25 +8,60 @@ import? "contractile.just"
 default:
     @just --list
 
-# Build the project
+# These recipes mirror the root `.github/workflows/rust-ci.yml` gate exactly, so
+# `just check` locally means the same thing as CI. They MUST fail loudly — a recipe
+# that echoes and exits 0 is a fake gate (issue #99 was exactly that).
+
+# Build aletheia (debug + release, locked)
 build:
-    @echo "Build not configured yet"
+    cd aletheia && cargo build --locked --all-targets
+    cd aletheia && cargo build --locked --release
 
-# Run tests
+# Run aletheia's unit tests (--bins only; see #124 note in recipe)
 test:
-    @echo "Tests not configured yet"
+    # `--bins` is deliberate. The integration suite is a specification for a CLI
+    # that has not been built yet — 27 of 29 fail by design (issue #124).
+    # Do NOT add `--tests` here to make the bar look green.
+    cd aletheia && cargo test --locked --bins
 
-# Format code
+# Check formatting (does not modify files)
 fmt:
-    @echo "Formatting not configured yet"
+    cd aletheia && cargo fmt --check
+
+# Apply formatting
+fmt-fix:
+    cd aletheia && cargo fmt
 
-# Lint code
+# Lint aletheia (not yet -D warnings — issue #125)
 lint:
-    @echo "Linting not configured yet"
+    # 23 findings remain, mostly dead code that exists because the CLI is
+    # unwired (#124). When #125 closes, add `-- -D warnings` here AND to
+    # rust-ci.yml in the same change, so local and CI never disagree about
+    # what "lint passes" means.
+    cd aletheia && cargo clippy --locked --all-targets
+
+# Enforce the zero-dependency RSR Bronze constraint (mirrors rust-ci.yml)
+deps-check:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    cd aletheia
+    if cargo tree --depth 1 | tail -n +2 | grep -q '[a-z]'; then
+      echo "ERROR: Aletheia must have zero dependencies (see aletheia/CLAUDE.md)"
+      cargo tree --depth 1
+      exit 1
+    fi
+    echo "OK: zero dependencies"
+
+# Everything the root CI gate runs, in the same order
+check: build test fmt deps-check
+
+# Self-verify: run aletheia against this repository
+self-verify:
+    cd aletheia && cargo run --locked --quiet -- ..
 
 # Clean build artifacts
 clean:
-    @echo "Clean not configured yet"
+    cd aletheia && cargo clean
 
 # Run panic-attacker pre-commit scan
 assail:

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."*