Source gate evidence and recovery

The gated scientific source is c749b53b02211901063228f52af123419b0dbaf5. The original source-only worker exited successfully after the full build, all3,985owned declarations, the rejected admitted negative control and all1,525indexed uncached axiom queries. The separate120-slot comparator passed all three kernels.

The original receipt envelope was refused: two documentation files changed during collection, and the cached axiom summaries for ModeData and CubicData reported none whereas their uncached body walks reported the same three permitted foundational axioms. No forbidden axiom was found. That original refusal is retained in recovery-summary.json; it has not been relabeled successful.

A separately sealed collector authenticates completed phases at the exact source/control inventory and records exact log, output and command lineage. Its native receipt is an authenticated phase composite, not another fresh compilation or body traversal. The new report includes complete original kernel types and all original uncached body records. All cached summaries are kept separately in the untouched compressed transcript; precisely two discrepancies are documented in the manifest. The separate negative-control record is linked through the successful original strict checker sequence and matching source snapshot; it was not an inline-sealed segment of the positive transcript. Current compiled-object hashes and effective compiler observations are explicitly later captures, not retroactive pre-build observations.

original-source-worker.log.gz and original-types-and-cached-axioms.txt.gz decompress to the untouched original bytes. Their hashes are bound in phase-composite-manifest.json. The full original worker properties/stdout and original exact driver remain privately archived because they contain local runtime locations. collector-source.py.txt is an explicitly normalized listing; its original and delivered hashes and the exact transformation are stated in recovery-summary.json. These are evidence artifacts, not additional mathematical build inputs.

The .lean-receipts directory contains the accepted collector envelope, compressed composite report and comparator envelope/logs. The release review describes independent source correspondence and recovery review. Coverage remains47verified/23conditional/3excluded overlapping scopes; this is not whole-paper certification.