Set 4 Proof, Authority, and Runtime Bundle

Proof-authority claims are recomputed from source

A single component bundles seven easily overclaimed source files into one inspectable unit: proof search, an Erdos #257 Lean kernel, reasoning-authority fences, completion, bitemporal logging, task-policy wrapping, and context-yield. batch4_proof_authority_runtime is one Microcosm component that gathers a group of source files that are easy to overclaim and checks them as a single inspectable unit. The files cover proof search, a copied Lean certificate kernel for Erdos #257, reasoning-authority fences, completion planning, bitemporal claim logging, macOS task-policy wrapping, and context-yield attribution.

Two runtime paths share one authority boundary

It never runs those systems: it reads their copied public source, checks each mechanism against required anchors, recomputes one negative case per mechanism, and writes a metadata-only result record. The component does not run any of those systems. It reads their copied public source, checks each declared mechanism against named required anchors, recomputes a negative case per mechanism from that source, and writes a result record. The record carries source references, digests, anchor counts, and bounded outcomes. It does not carry source bodies or live private state.

A passing fixture does not establish a theorem

The only positive claim is narrow: copied source is present, its required anchors are in place, and the copied Lean kernel is free of proof placeholders, with everything stronger refused openly. Its positive claim is narrow. The copied source is present, its required anchors are in place, and the copied Lean kernel is free of proof placeholders. Everything stronger is refused in the open.

Purpose

Each mechanism invites an overclaim

Each bundled mechanism looks like more than it is: proof search like solving open problems, the Lean kernel like a solution, a grant like a live sandbox, a wrapper like orchestration. These mechanisms sit next to claims a reader will want to make on their behalf. A proof-search benchmark looks like solving open problems. A copied CertificateKernel.lean for Erdos #257 looks like a solution. A reasoning grant looks like a live sandbox. A task-policy wrapper looks like live orchestration.

One narrow question per mechanism

The component asks only whether each mechanism can be shown as copied, anchored public source without inheriting an authority it lacks, making the import auditable. A loose import surface would let any of those read as more than it is. The component answers one narrow question per mechanism: can this be shown to a reader as copied, anchored, public source, without inheriting an authority it does not have. It makes the import auditable and forces every stronger statement into a visible limit.

How it works

Two entry shapes over one gate

run takes a fixture directory and run_batch4_bundle takes the exported bundle, but both forward to run_crown_jewel_organ with _evaluate, so they share one gate. There are two entry shapes. run consumes a fixture input directory. run_batch4_bundle consumes the exported bundle directory. Both forward to run_crown_jewel_organ with _evaluate as the evaluator, so they share one gate. main exposes them as the run and validate-bundle subcommands.

_evaluate drives the checks in order:

1. _load_manifest reads batch4_probe_manifest.json. Invalid JSON returns BATCH4_PROBE_MANIFEST_INVALID; a non-object returns BATCH4_PROBE_MANIFEST_NOT_OBJECT.
2. _module_rows builds a module-id to row map from the exported source_module_manifest.json. _evaluate checks that all seventeen ids in EXPECTED_MODULE_IDS are present; a gap emits BATCH4_SOURCE_MODULES_MISSING.
3. It checks the manifest's mechanism set equals the twelve ids in EXPECTED_MECHANISMS exactly. Any missing or extra id emits BATCH4_MECHANISM_SET_MISMATCH.
4. _mechanism_status checks, per mechanism, that each named source module is present and that every string in that module's required_anchors appears in the copied file text. A missing module or anchor marks the mechanism blocked.
5. _synthetic_runtime_exercises reads the copied module texts and derives three bundles: a proof bundle, an authority bundle, and a runtime bundle. Each bundle is a set of anchor-presence facts computed from the copied source, not a live run.
6. _erdos_static_scan runs a regular expression over the copied CertificateKernel.lean and rejects the tokens sorry, admit, and axiom. It counts declarations and samples a few names. A banned token blocks the scan. This is a token scan, not a Lean proof check.
7. _lean_lake_probe optionally runs lake env lean over the copied kernel under the source Lake project. A zero-exit run records live_compile_pass; a missing lean/lake binary or an unavailable Mathlib dependency records unavailable; a nonzero exit records blocked. Every branch fixes proof_authority_delta to none, so a compile pass is an availability signal, not formal-result correctness.
8. _semantic_negative_case_proofs recomputes the twelve negative cases and reports how many were rejected.

Negative verdicts re-derived from source

_computed_negative_case_verdict ignores the fixture's declared verdict and re-derives each one from source evidence, an overclaim-shape check, and a runtime probe, rejecting only when the source supports it. The negative-case step is the part worth reading closely. _computed_negative_case_verdict does not trust the fixture to declare its own verdict. It re-derives each verdict from source-observed evidence, an overclaim-shape check on the mechanism's declared ceiling, and a runtime probe, then marks the row declared_fixture_ignored. A case counts as rejected only when the source itself supports the rejection.

Pass gate and the omission record

_evaluate passes only with no findings and a validated manifest, while result_card attaches AUTHORITY_CEILING and an omission record naming what is left out: source bodies, private runtime state, and model-output data. _evaluate returns pass only when there are no findings and the source manifest validated. result_card projects the outcome into a compact card and attaches AUTHORITY_CEILING plus an omission record naming what is left out of the result: full copied source bodies, raw private runtime state, and live provider or session payloads.

flowchart TD probe["batch4_probe_manifest.json 12 mechanisms + 12 negative cases"] manifest["source_module_manifest.json 17 copied source modules"] evaluate["_evaluate run / validate-bundle"] anchors["_mechanism_status module present + required anchors"] scan["_erdos_static_scan reject sorry / admit / axiom"] probe2["_lean_lake_probe compile availability, delta = none"] negatives["_semantic_negative_case_proofs verdict recomputed from source"] record["metadata-only result record refs, digests, anchor counts, ceiling"] probe --> evaluate manifest --> evaluate evaluate --> anchors evaluate --> scan scan --> probe2 evaluate --> negatives anchors --> record scan --> record negatives --> record

Negative cases

Twelve stable error codes, one per mechanism

The fixture's twelve negative cases, one per mechanism with a stable error code, are the public failure floor stopping the source import from reading as an unbounded proof or runtime claim. The fixture declares twelve negative cases, one per mechanism, each with a stable error code held in EXPECTED_NEGATIVE_CASES. They are the public failure floor that stops a source-import surface from reading as an unbounded proof or runtime claim:

• weak_skeleton_synthesis_failure: BATCH4_WEAK_SKELETON_MUST_NOT_SILENT_PASS
• foundry_low_repair_quarantine: BATCH4_FOUNDRY_REPAIRED_COUNT_BELOW_THRESHOLD
• verisoft_truth_leak: BATCH4_VERISOFT_TRUTH_LEAK_REJECTED
• verisoft_prefix_answer_leakage: BATCH4_VERISOFT_PREFIX_ANSWER_LEAKAGE_REJECTED
• erdos_solution_overclaim: BATCH4_ERDOS257_SOLUTION_OVERCLAIM_REJECTED
• packet_sha256_corruption: BATCH4_PACKET_SHA256_CORRUPTION_REJECTED
• grant_forbidden_context: BATCH4_GRANT_FORBIDDEN_CONTEXT_DENIED
• forward_dirty_unknown_target: BATCH4_FORWARD_POLICY_DIRTY_UNKNOWN_TARGET_BLOCKED
• closeout_stale_head: BATCH4_CLOSEOUT_STALE_HEAD_DEFERS
• bitemporal_expired_claim: BATCH4_BITEMPORAL_EXPIRED_CLAIM_NOT_CURRENT
• taskpolicy_missing_binary: BATCH4_TASKPOLICY_UNAVAILABLE_PASSTHROUGH
• context_accepted_read_guard: BATCH4_CONTEXT_ACCEPTED_SCOPED_READ_NOT_FLAGGED

Rejection requires source support

A case is marked rejected only when the source-observed verdict supports it, never because the fixture said so. Each case is marked rejected only when the source-observed verdict supports it, not because the fixture said so.

Prior Art Grounding

Evidence before authority, from proof-carrying code

It separates the authority to act from the evidence permitting it, borrowing the evidence-before-authority ordering of proof-carrying code and capability security, yielding fixture-bound evidence rather than a verified authorization system. The component keeps the authority to act separate from the evidence that an action is permitted. That ordering is the idea behind proof-carrying code (Necula, 1997) and capability-based security, where a request arrives with evidence of its own legitimacy rather than relying on ambient trust. This module borrows the evidence-before-authority ordering over copied fixtures. The result is fixture-bound evidence, not a verified authorization system.

Validation Result record Path

Run from the microcosm-substrate/ public root:

PYTHONPATH=src python3 -m pytest tests/test_batch4_proof_authority_runtime.py -q
PYTHONPATH=src python3 scripts/build_doctrine_projection.py --check-paper-module-corpus

What the two checks confirm

The focused test covers fixture, bundle, digest, anchor, mutated-Lean-body rejection, and negative-case recomputation, while the corpus check confirms the bundle, Mermaid, Atlas, and Markdown projections stay consistent. The focused test exercises the fixture and bundle expectations, the source digest and anchor checks, the mutated-Lean-body rejection, and the negative-case recomputation. A pass is reader-verifiable evidence only.