Audit all compiled Cap declarations and harden auditor controls

.github/workflows/cap-first-exit-lean.yml

@@ -22,7 +22,7 @@ permissions:
 jobs:
   kernel-evidence:
     runs-on: ubuntu-latest
-    timeout-minutes: 30
+    timeout-minutes: 60
     env:
       LEAN_NUM_THREADS: 2
       PYTHONDONTWRITEBYTECODE: '1'
@@ -50,6 +50,15 @@ jobs:
           lint: 'false'
           use-mathlib-cache: 'true'
           use-github-cache: 'false'
+      - name: Auditor self-test with actual pinned Lean (both Python modes)
+        working-directory: frontiers/cap_first_exit_lean_20261002
+        run: |
+          set -euo pipefail
+          LEAN_EXECUTABLE="$(lake env which lean)"
+          test -n "$LEAN_EXECUTABLE"
+          test -x "$LEAN_EXECUTABLE"
+          test ! -e .lake/auditor-selftest
+          python -B -S run_cbz_mutations.py --lean "$LEAN_EXECUTABLE" --output .lake/auditor-selftest
       - name: Fresh build, leanchecker replay, axiom audit, negative controls
         run: python -B -S frontiers/cap_first_exit_lean_20261002/gate.py --execute
       - name: Tracked tree unchanged
@@ -59,7 +68,9 @@ jobs:
         uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9
         with:
           name: cap-first-exit-lean-${{ github.run_id }}-${{ github.run_attempt }}
-          path: frontiers/cap_first_exit_lean_20261002/.lake/evidence/
+          path: |
+            frontiers/cap_first_exit_lean_20261002/.lake/evidence/
+            frontiers/cap_first_exit_lean_20261002/.lake/auditor-selftest/
           include-hidden-files: true
           if-no-files-found: error
           retention-days: 90

frontiers/cap_first_exit_lean_20261002/CBZ_ADMISSION.md

@@ -0,0 +1,47 @@
+# Cap compiled admission
+
+This repair closes a specific auditor coverage gap. It preserves the original152 visible declarations—138theorems,13definitions and one structure—and all their mathematical hypotheses, proof bytes, bounds and imported source pins. It does not identify these conditional statements with a global elder-pairing/persistence theorem, prove their premises satisfiable in a particular model, or grant scientific acceptance.
+
+The legacy source gate admitted a digest-rebound unlisted private theorem. The observed reproduction, on unchanged Math9f8dbb4 source, ran two tests in each Python mode: the exact-bound baseline passed; the desired rejection assertion failed because the actual source_check accepted the extra theorem. No Lean run was claimed by that reproduction. The repair adds a source precheck and complete compiled admission; the source precheck alone is not the proof of compiled coverage.
+
+## Verification commands
+
+Run from `frontiers/cap_first_exit_lean_20261002/` with the documented Python runtime and verified Lean4.34.1 release5045d0056413266e57c625dcd7c365b10e377c52 on PATH. Lake manifests pin Mathlibd13f23b723b8a846827a245b89c10fc7d3f11612 and all eight transitive revisions. Keep dependencies at those exact commits and clean before/after execution.
+
+```sh
+python3 -B -S -m unittest discover -s . -p 'test_*.py' -v
+python3 -B -O -S -m unittest discover -s . -p 'test_*.py' -v
+python3 -B -S run_cbz_mutations.py --lean /verified/lean-4.34.1/bin/lean --output /new/external/mutation-report
+python3 -B -S gate.py
+LEAN_NUM_THREADS=2 python3 -B -S gate.py --execute
+```
+
+Source-only output certifies only its byte/pin/visible-source inventory checks. Actual execution performs a fresh package build, kernel recheck, the retained152-target axiom audit and all-constant compiled module census/axiom closure, a copied unchanged baseline, four real compiled package mutations, and the three retained axiom rejection controls. Only the three declared imported axioms are allowed. Logs retain actual stdout, stderr, exits, generated program hash, injected source hashes and full encoded declaration identities. A failing or unqualified execution cannot supply a new kernel receipt. Consumers must match its exact source identity and actual process outcome; a caller-supplied or historical receipt is not current execution evidence. Prior execution evidence is archived under `.lake/evidence-history/`.
+
+## Why a compiled census
+
+Lean itself enumerates the owned module table, including unused/private/generated constants. Complete module counts and exact fixed support bindings prevent a manifest target list from silently narrowing the audit. Type/value dependencies of every owned constant contribute to the union axiom closure. Owned axioms, unsafe/partial declarations, unsupported owned opaque/quot declarations and unbound, duplicated or count-mismatched IR/codegen extras refuse. All eight actual IR names have separate exact bindings and are not treated as additional logical theorems. Missing references refuse.
+
+Lean names use canonical UTF8-hex/string and decimal/numeric components. Unicode subscripts, private numeric components and quoted string components therefore retain their identities. Rendered names are display only.
+
+Structure-generated proof projections need a narrow exception: pinned Lean marks Prop-valued projections as theorem/user because generated fields carry source ranges. The exporter obtains their names from actual StructureInfo metadata for the visible CapHyp inductive. Exact observed support bindings and those structural relations are required. Prefixes, a source range, a compiler-shaped name or an entry newly added to the manifest are not sufficient admission. Other extra user theorems and unrecognized user definitions refuse.
+
+## Tool verification and limits
+
+The finite Python tests use synthetic transcripts explicitly. They test parser/policy behavior and source admission, not the actual compiled inventory. Named source mutations must reach their designated assertion, with positive baseline and collected count; import/syntax/process/foreign-test failures are not kills. A separate actual pinned-Lean fixture proves that an unsafe opaque constant is exported as unsafe, and detects removal of the exporter guard in both Python modes. No Python assert is relied upon for optimized-mode checking.
+
+Production support bindings must come from actual pinned compilation and module-table export, inspected against exact source/runtime identities. Normal gate execution compares against the fixed binding; it never writes its own allowlist. A supplied transcript or consistency JSON does not authenticate an execution. Mathematical evidence remains actual source-bound build/recheck/audit/control output.
+
+Maintenance owner: none—component-local, self-contained. Serves the bounded A2/A8 compiled admission obligation and G0/G2/G3/G4/G6/G11 within this packet. It is not a federation-wide Layer A auditor or CBZ-0 qualification. Changed source/runtime/dependencies require new verification.
+
+## Actual source-bound discovery cut
+
+The unchanged326607-byte Cap proof has SHA256 `040aa91fcbdf25ccdaced1c828dd779318217a7c41ac928f87e8d17a8d3c3ef0` at Math commit `9f8dbb4d18b9f3ebd9ffac6b0caa42df9f343966`. Actual discovery compilation/export observed206 owned kernel constants:152 visible declarations plus54 support records, and8 separately bound IR/codegen names. The transitive axiom collector visited47659 names and reported only the declared three axioms. Five generated Prop projections account for143 user/theorem-kind constants despite only138 visible theorem statements. Three actual Abel tactic auxiliaries have the explicit `_abel_N_M` suffix and still require exact bindings and a real parent.
+
+The retained default `leanchecker CapFirstExit` successfully rechecked the target module against its imported environment. This is not a fresh empty-kernel replay of Mathlib or an external verifier. An accidental all-import `--fresh` experiment and unsupported `--help` probe were interrupted and receive no passing credit. Actual final repaired-gate qualification belongs only to its newly observed receipt and raw streams; the discovery cut does not claim it.
+
+The finite auditor mutation threshold is all12 named mutations in each Python mode:11 Python policy guards and one actually compiled unsafe-opaque exporter guard. The runner requires the designated method, one collected test, one failure, no errors, the exact removed-guard `ValueError not raised` assertion or explicit actual safety marker, and no timeout. Generic same-method failures do not kill mutants. Prior22-mutation development observations precede the final codegen/name/process repairs and cannot qualify later bytes.
+
+Normal gate execution performs at most two independent compiled controls concurrently, each with two Lean threads. Each full-source mutation uses the successful Lake-generated compiler setup, private object/interface/C outputs, readonly pinned dependency artifacts, owned default kernel replay, all152 original target axiom reports and actual complete census. Receipts bind exact setup and output-object hashes before/after audit, mutated source hashes and full injected identities. The copied positive baseline must reproduce the real census. Private theorem, private sorry theorem, unused sorry definition and range-less compiler-shaped theorem must each reject for exactly their own findings.
+
+The commands support relative CLI output paths by resolving output/runtime paths before child working-directory changes. The workflow-equivalent `--output .lake/auditor-selftest` is a required positive integration route. Timeout cleanup owns the launched process group, retains partial stdout/stderr/exit/timed_out metadata and refuses even a SIGTERM handler that exits0.