text Challenge.lean Solution.lean config.json formalization.yaml verification.json The package must be reproducible and independently verifiable without SQLite. It ends in the precise status Comparator-ready, never Comparator-verified. ## Trust boundary - Solution.lean is copied byte-for-byte from the selected frozen release replay member and rebound to the exact release formalization, environment, module artifact, declaration, and publication closure. - Challenge.lean is explicit reviewer-controlled source in a closed canonical plan. Packaging does not claim that it matches the solution; only the real Comparator run can establish that. - config.json uses the official Comparator fields and exact theorem/axiom policy. - verification.json binds all stale-sensitive inputs and exact tool commits while asserting constants equivalent to status: ready, comparator_verified: false, and authoritative: false. - This slice never executes Comparator, creates evidence, derives claim status, or trusts a caller-supplied verification result. Upstream contract reviewed at exact Comparator commit 68a064109f01c08f47c8edc9f51d6a2bbffaa188. Initial exact tool pins for the protected exercise are lean4export af5aa64bb914c3c2c781f378088dbd38acf4f804 and landrun 5ed4a3db3a4ad930d577215c6b9abaa19df7f99f. ## Deliverables - Closed Rust-owned comparator_package_plan/1 and comparator_package_verification/1 contracts with committed JSON Schemas. - Offline mcl release export-comparator construction and dry-run support. - Offline mcl release verify-comparator-package deterministic reprojection. - Exact five-file inventory with canonical JSON, deterministic machine-readable YAML, bounded inputs, safe paths, no links, and no overwrite. - Exact bindings for: - source release manifest; - selected formalization object/version and canonical member; - theorem source/module artifact; - environment/dependency manifest; - declaration and theorem names; - challenge and solution bytes; - Comparator configuration; - Comparator, lean4export, and landrun repository/commit pins. - An input fingerprint and expected verification hash that change whenever challenge, solution, dependency manifest, theorem source, or Comparator configuration changes. - Pilot A CLI playtest proving database-independent package construction and verification. Protected publication artifact generation may exercise the boundary, but must not label it Comparator-verified. ## Acceptance criteria - [x] Unknown fields, malformed hashes/commits/names, duplicate theorem or axiom names, oversized source, unsafe member paths, and mismatched release/formalization bindings fail closed. - [x] The exporter first verifies the frozen release and caller-supplied expected release hash. - [x] Solution.lean is exactly the release replay module; substitution is rejected. - [x] Challenge.lean, config.json, formalization.yaml, and every verification binding reproduce deterministically from the canonical plan plus frozen release. - [x] Output contains exactly the five SPEC files; missing, extra, altered, symlinked, or reparse-point members fail verification. - [x] Dry run and materialized export report the same package identity and never overwrite an existing path. - [x] Verification works from a clean location with the operational database absent and no network access. - [x] Changing each stale-sensitive input changes identity or rejects the old expected identity. - [x] Neither package construction nor verification emits comparator_run, authoritative evidence, or a truth verdict. - [x] Rust unit/adversarial tests, CLI tests, formatting, warnings-denied Clippy, full Rust tests, legacy Python tests, and diff checks pass. - [x] Exact-head CI and protected artifact evidence are recorded before closure. ## Non-goals - Running the real Linux systemd-run / landrun / Comparator pipeline. - Promoting Comparator evidence or changing research status. - Claiming Pilot C or all Phase 6 acceptance is complete. - Treating fake-landrun, a normal Lean build, or package integrity verification as Comparator verification. The next slice after this issue is protected real-Comparator execution and evidence ingestion, followed by the BH Pilot C lifecycle.
Activity
Mnehmos commentedon Jul 22, 2026
Phase 6d protected evidence is complete for the deterministic Comparator-ready package boundary.
Reviewed and merged source
36ae9586dc7985785501474c53e1ee3d6067b5f52fe5d00992599a2c22a974c01ec0cdc4fbea286d29893380402— all five required jobs passed29893579467— passed29893579466— passedThe full automated review generated no actionable threads. A final compatibility patch aligned Comparator theorem/axiom names with the existing release contract's ordinary primed Lean identifiers; its full Rust suite, warnings-denied Clippy, and exact-head CI passed.
Retained artifact
8519152437publication-boundary-2fe5d00992599a2c22a974c01ec0cdc4fbea286d478926sha256:642edf93c509407efe953a4dda588fe3190bf7bc66204d03fe1387b9a7e31384Comparator-ready package audit
Challenge.lean,Solution.lean,config.json,formalization.yaml,verification.jsonf268d9da8fa4e19a05ac32d1c85b14e9e427db326dc9a69553b1bb11d3366effa9048a8ac02907993cd1114e3c06510524933c72b891c786d15d5beeb82c7088aee3e4e65754205932caa8cca0937d017965bb7936d7d1cec86117e1d7225898beef8cd5d48d9cee07352f34366db5f34c77bc73b9c685b83ded490618960758019f8848-1478-7512-8a24-240337a61d39/9326a29ecfbe07f68adbbda836029c909ae525ebb300912de676150057b2b3f7MathOS.PilotA.every_prime_other_than_two_is_oddIndependent audit checked every package and source-member hash/size, the headline formalization/environment/module/declaration bindings, exact
Solution.leanequality withreplay/Submission.lean, canonical plan/config/verification JSON, parsed deterministic YAML, and the fixed Comparator/lean4export/landrun repositories and commits. Dry-run, materialized build, retained verification, and independent reprojection all produced the same verification hash and input fingerprint.mcl release verify-comparator-packagesucceeded from a nonexistent instance root withdatabase_independent, inventory, hashes, bindings, and deterministic reprojection all true. Both Lean files elaborate under Lean 4.32.0; only the intentional challengesorrywarning appears, and both protected stderr files are empty.The retained state remains exactly
ready,comparator_verified: false, andauthoritative: false. No Comparator execution, evidence promotion, or truth-status transition is claimed. This satisfies #60's scoped boundary; real protected Comparator execution remains the next slice.Mnehmos commentedon Jul 22, 2026
Completed by implementation PR #61 and protected-evidence docs PR #62. Exact-head CI, merged-tree CI, protected publication run 29893579466, and the independent artifact/package audit are recorded above. The boundary remains ready-only and non-authoritative; real Comparator execution is intentionally deferred to the next issue.