Proofs red on main since b7c780f (#174): census requires CNO.MalbolgeCore; FilesystemCNO.lean does not compile

Measured

Proofs on main has been red since b7c780f (PR fix: resolve repository issues, port Lean FilesystemCNO, and unify Coq tags #174, merged 2026-09-26T20:45Z). Run 36270649306: job Coq — CNO + OND (14 theories) fails at step 7 "Axiom dependency census"; job Lean — core CNO (6 modules + axiom audit) fails at step 4. Agda and Z3 jobs are green.
The same two jobs were already red on PR fix: resolve repository issues, port Lean FilesystemCNO, and unify Coq tags #174's own head 8841dfe (run 36267465903, pull_request). The rule suite records the merge to main as bypass. The last green main run is 35842500950 at 877ede2 (2026-09-23).
Earlier steps in the Coq job pass on b7c780f: ASSUMPTIONS-CHECK OK: 17/17 theorems closed under the global context, AXIOM-TAGS-CHECK OK: all declarations across 14 theories tagged with unified grammar, and both negative controls bite.

Cause 1 — Coq census assumes every theory lives under `CNO.`

proofs/coq/census-assumptions.sh (new in #174) walks eight directories including malbolge/ and emits Require CNO.$base. for each theory (line 56). _CoqProject binds malbolge to the logical root Malbolge, not CNO:

-R malbolge Malbolge

so the generated driver dies:

File "/tmp/az-census.2kk56v/Census.v", line 15, characters 0-25:
Error: Cannot find a physical path bound to logical path CNO.MalbolgeCore.
CENSUS FAILED: coqc exited with 1

Cause 2 — the Lean `FilesystemCNO` port does not compile

proofs/lean4/FilesystemCNO.lean (+372/−131 in #174, claimed as the #167 port) fails in the Mathlib-free build:

FilesystemCNO.lean:268:4: error: alternative 'Directory' has not been provided
FilesystemCNO.lean:268:4: error: alternative 'Symlink' has not been provided
FilesystemCNO.lean:310:17: error: unknown identifier 'p''   (also 331, 352)
FilesystemCNO.lean:381:10: error: unknown identifier 'set_path_id'
FilesystemCNO.lean:395:10: error: unknown identifier 'path_of_set_path'
FilesystemCNO.lean:589:8: error: tactic 'rewrite' failed, did not find instance of the pattern
FilesystemCNO.lean:590:8: error: tactic 'rewrite' failed, did not find instance of the pattern

Acceptance criteria

census-assumptions.sh takes each theory's logical root from _CoqProject (-R <dir> <Root>) instead of hardcoding CNO.; the census step is green on main and its table lists the malbolge/ theorems under Malbolge..
Negative control: a directory bound to a non-CNO root is censused, not skipped. Skipping it would turn the miss into a vacuous pass.
FilesystemCNO.lean builds in the six-module job and #print axioms on its headline theorems shows no sorryAx. If the port is not finished, the file is restored to the last revision that compiled and Lean: port the Coq concrete filesystem model so the FilesystemCNO law axioms become theorems (follow-up to #125/#165) #167 stays open with the port as its own acceptance criterion; a half-port must not sit red on main.
A Proofs run on main is green at the curing commit and PROOF-STATUS.adoc cites that run id.

Context: Proofs is not a required check (#161), which is how a red PR could merge; this issue records the red, it does not re-litigate the merge.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57

PR #177 (fix/176-census-roots-restore-filesystemcno, head a360533cd57a62f11cfeb131aa93ec0611866ffe) implements both of this issue's fixes and the target gate is green, but the PR is not being merged because three other checks on its head are red. Per the owner's "land only fully green" rule, this is triaged here instead of landed.

The fix itself: verified green

Proofs (run 36706314479): SUCCESS — all four jobs pass:

Lean — core CNO (6 modules + axiom audit): SUCCESS
Coq — CNO + OND (14 theories): SUCCESS, including Axiom dependency census (issue step
Agda — CNO + OND: SUCCESS
Z3 — CNO + OND bounded checks: SUCCESS

The census now reads each theory's logical root from _CoqProject's own -R <dir> <Root> bindings instead of hardcoding CNO., censuses malbolge/ under Malbolge. (Malbolge.MalbolgeCore | 7 | 7 | 0), and hard-fails on any directory with no -R binding rather than skipping it. FilesystemCNO.lean and AxiomAudit.lean are restored to 877ede2 (last green main), building clean with no sorryAx. Full verbatim evidence, both mutants, and the acceptance-criteria mapping are in the PR body.

Why it is not merged: three red checks on the PR head, all pre-existing on `main`

Confirmed via gh run list --branch main: all three were already red or startup-failing at main's current head (d11effe1, run set 2026-09-06/07) before this PR's branch was cut — none are caused by this change.

Governance / Actions lockfile verify — FAILURE. Step Verify actions.lock (or SHA pins during the grace window) fails. Same workflow is failure on main at d11effe1.
Scorecards supply-chain security / Run Scorecard PR — FAILURE. Step Fail if reconciliation did not succeed fails (native-pin reconciliation). Same workflow is startup_failure on main at d11effe1 and at two earlier main heads (f416f1d, df5226f).
CodeQL Security Analysis — startup_failure (zero check runs emitted, i.e. the job never started). Also startup_failure on main at d11effe1.

Per owner doctrine, a new scanner finding is an issue with acceptance criteria, not a merge blocker — but these are not new findings from this PR; they are estate-wide infrastructure red already present on main, and the binding rule for this task is stricter than that doctrine: land only if every check on the PR head is green, explicitly including pre-existing red. So this PR sits open, fully reviewed and evidenced, pending either (a) a separate fix to the Governance/Scorecard/CodeQL infrastructure landing on main first, or (b) an owner decision to merge over these specific pre-existing reds.

Recommendation

This PR is ready to merge as soon as main's Governance/Scorecard/CodeQL red is cleared (or the owner explicitly waives it for this PR) — no further work on the census or Lean-restore fix is needed. #167 remains open with finishing the FilesystemCNO.lean port as its own acceptance criterion; this PR does not touch that.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57

fix(ci): regenerate actions.lock for codeql-action v4.38.1 and wiki-s…

fix(proofs): census reads logical roots from _CoqProject; restore Fil…

Navigation Menu

Repository navigation

Proofs red on main since b7c780f (#174): census requires CNO.MalbolgeCore; FilesystemCNO.lean does not compile #176

Measured

Cause 1 — Coq census assumes every theory lives under `CNO.`

Cause 2 — the Lean `FilesystemCNO` port does not compile

Acceptance criteria

The fix itself: verified green

Why it is not merged: three red checks on the PR head, all pre-existing on `main`

Recommendation

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Proofs red on main since b7c780f (#174): census requires CNO.MalbolgeCore; FilesystemCNO.lean does not compile #176

Description

Measured

Cause 1 — Coq census assumes every theory lives under CNO.

Cause 2 — the Lean FilesystemCNO port does not compile

Acceptance criteria

Activity

hyperpolymath commented on Sep 30, 2026

The fix itself: verified green

Why it is not merged: three red checks on the PR head, all pre-existing on main

Recommendation

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions

Cause 1 — Coq census assumes every theory lives under `CNO.`

Cause 2 — the Lean `FilesystemCNO` port does not compile

Why it is not merged: three red checks on the PR head, all pre-existing on `main`