Finalize RMQ v1.0.0-rc.1

[patternscientist]

Prepare RMQ 1.0.0-rc.1 for release with checked client examples, clearer theorem/model guides, canonical rank/select proof reuse, and reproducible source packaging. The Mathlib-free Lean 4.22 footprint, half-open leftmost RMQ semantics, public theorem contracts, and distinctions between formal costs and native behavior are preserved.

The release tooling now checks package metadata and checkout byte identities, strengthens current-claim and evidence controls, and retains the source/receipt relationships behind qualification. The fresh Astra audit's P2-01 finding is repaired: a negative scanner case must finish normally with exit 1 and the intended diagnostic; a timeout cannot earn a pass. The tag workflow supplies full history and an external log to the existing checks and marks new RC tags as prereleases.

Validation:

• Fresh audit plus its explicit continuation; P2-01 closed, bounded source accepted. Both reports are preserved verbatim in docs/internal/audit_reports/; scope and remaining publication gates are in docs/internal/v1/V1_POST_BLIND_DISPOSITION.md.
• All 15 final source/report checks passed on 02cb4e40b4bbd7e07f8b7bb4ad878dcb401c52f8, including cached lake build, strict claim/design checks, hygiene, paper checks and the full topology regression. All 33 commits passed individual design checks.
• Full policy regression at 143fa1e5 on both Windows shells (unchanged production inputs transfer to the final source): all 134 policy and 21 context cases have exact expected normal exits, with no timeout or overflow and completed cleanup. Final focused controls passed on pwsh, Windows PowerShell 5.1 and POSIX.
• Packaging tests: 11 passed; checkout-byte regression: both tests passed, including the checkout-setting and missing-rule controls.

Historical failures remain explicit. The older Linux aggregate remains failed; its passing components, separately repaired checks and exact-input transfers are documented, rather than relabeled as a successful final aggregate. Hosted Lean gate and Reproduce artifact must pass before protected merge. This PR does not promote the RC to stable or authorize retargeting an existing tag.

The replacement source archive independently matches all 5,090 tracked Git files, modes and hashes. Its Git-free unpacked smoke passed with the explicitly recorded reused cache; source hashes remained unchanged afterward.

CI follow-up at 697e3f0a91e4aa63d177fead41e50388cd0c02d9: the Windows PR job exposed a fixture that switched core.autocrlf without materializing the new checkout. The packager correctly rejected its dirty metadata. The test now checks out the fixture after each setting change, invalidates cached stat matches, and asserts clean status before preserving the same archive/blob/mode checks. The production packager and every Lean source are unchanged. The failed hosted run is retained.

The focused repair passes all 11 packaging tests under both inherited line-ending settings on Windows and POSIX, checkout-byte controls, cached build, strict claim and per-commit design checks, topology baseline and hygiene. Earlier full regressions retain their recorded commits; they are not presented as new runs. Newly authenticated source/evidence archives and a separate versioned delivery receipt identify the repaired head. Hosted checks must succeed for this updated candidate before merge.