docs: define archive skill transport policy

[akiezun]

Summary

• records the verified 51-skill archive inventory and clean-room reuse policy
• assigns every skill one disposition, target layer, and replacement owner
• defines dependency-aware PR boundaries for future transport work
• adds tests binding the human plan to the machine-readable manifest

Scope

This is P00 from ARCHIVE_SKILL_TRANSPORT_PLAN.md. The 1,203-line diff exceeds the normal warning threshold because it contains the complete 51-row review, the downstream PR contract, and its machine manifest; it adds no runtime behavior or generated assets.

Non-goals

• no archived skill implementation
• no autonomous execution on main
• no model/provider integration
• no archive redistribution or verbatim reuse
• no PR merges

Dependencies

None. Later P-series work depends on this policy.

Validation

• make lint
• make test: 542 passed, 1 skipped
• make check-example
• plugin validator: passed
• git diff --check

Risk and migration

Documentation, policy data, and tests only. Existing plugin and CLI surfaces are unchanged.

Rollback

Revert commit ccf1302; no runtime or persisted project data is affected.

[Deicyde]

Review result: changes needed.

• FORMALIZATION_QUALITY_GOAL.md:109-123 has fail-open eligibility paths. A statement: formalized leaf without declaration, and a mathlib: true leaf without statement/proof flags, can avoid the required quality evidence.
• not-applicable has no default-deny applicability matrix; omitting origin can make source fidelity disappear.
• The delivery DAG is not deterministic: C00's stated prerequisites conflict with the Phase 4 barrier, and E01 depends on “relevant merged core changes.”
• The manifest tests do not enforce owners, dependency ordering, or rejection of unmanifested transported skills.
• The mandatory plugin-validation command contains an unresolved host-local placeholder.

Please tighten the policy and tests before treating this document as an executable roadmap. Also state how P01-P03 relate to the newer skeleton/read-back work in #12.

[Deicyde]

Second pass on exact head ccf1302. Four additional contract gaps:

• [P1] lean-validity does not require Lean validity. The goal requires compilation at FORMALIZATION_QUALITY_GOAL.md:55-64, but the checker contract and policy tests at lines 214-215 require only declaration resolution. The existing resolver is explicitly lexical: it indexes theorem Broken : True := by definitely_not_a_tactic even though Lean rejects it. Bind this gate to successful build/artifact evidence and add a resolvable declaration with a broken body as a negative fixture.
• [P1] The claimed 51/51 source inventory is not independently auditable. ARCHIVE_SKILL_SOURCE_PROVENANCE.md records a filename and SHA but no retrievable object identifier or generated member inventory, while test_transport_plan_and_manifest_are_the_same_policy only compares two hand-authored derivatives in this PR. A skill omitted from both, incorrect entry counts, or the stated license-file scan cannot be detected. Provide reviewable source-inventory evidence or state this as an external attestation rather than a verified completeness claim.
• [P2] The planned skill omits the supported Muse surface. FORMALIZATION_QUALITY_GOAL.md:154-173 names “both” plugin manifests and tests only Codex and Claude discovery. This repository also ships .muse-plugin/plugin.json, whose commands are explicitly enumerated, so following P01/P03 literally leaves formalization-quality unavailable in Muse while existing plugin tests can remain green. Make all three host surfaces and their discovery tests part of the contract.
• [P2] The licensing manifest is parsed with duplicate-key last-wins semantics. _manifest() uses plain json.loads; a temporary record containing "reuse":"verbatim", "reuse":"none" still produced 5 passed. Reject duplicate keys so the machine authority cannot have parser-dependent authorization semantics; the repository already has a strict object hook in autoform_cli/claims.py.

Validation: manifest tests 5 passed; focused plugin-surface and wheel-runtime tests passed; Ruff and plugin validation passed.

[Deicyde]

I addressed both blocker passes in draft #155, rebased onto current canonical main.

I used a new facebookresearch branch rather than pushing to this contributor-owned fork. The replacement preserves the original policy commit, downgrades the unavailable archive inventory to an external attestation, makes the DAG/owners/stack machine-checkable, rejects duplicate JSON keys, covers Muse, and makes quality eligibility, N/A policy, compiled Lean evidence, read-back evidence, Pages gating, open statements, and external Mathlib evidence fail closed.

Leaving #9 open for the author/maintainers to disposition; please continue technical review on #155.