docs: make archive skill transport policy fail closed

[Deicyde]

Status: premise rejected; do not merge. This PR adds only top-level planning documents, a policy manifest, and tests that validate those newly authored files against one another. No shipped CLI/server/workflow/skill/package path consumes them, and the wheel excludes them. It therefore adds maintenance obligations without changing Autoform behavior. Preserve any genuinely useful future feature as a focused issue or functional PR instead.

Supersedes external contributor PR #9 without writing to its fork. Adam Kiezun's original policy commit remains the first commit with the same patch-id and authorship; this branch merges current canonical main and layers the reviewed fail-closed contract fixes on top.

What this PR does

• Records the unavailable archive inventory/license scan as an explicit external attestation; the repository does not claim independently reproduced 51/51 source coverage.
• Adds strict manifest v2 with registered owners, current repository-skill provenance, approval gates, a topologically checked delivery DAG, and exact plan parity.
• Separates logical target layer, concrete repository, and branch. P/E/D units bind facebookresearch/autoform-bot@main; C00–C05 request main but remain repository-null until companion-repository-approved binds and verifies a real companion.
• Reconciles the plan with merged Skeleton/read-back, Markdown Formalize, project creation, revision-impact, open-statement, and Reject formalized work the Lean cannot back at load time #158 graph-load invariants. It does not revive the deprecated execution branch.
• Defines formalization-quality eligibility independently of authored declaration, rejects evidence on containers/retracted subjects, and requires explicit origin on every quality subject.
• Makes source-fidelity origin/status mapping total and binds cited verdicts to the exact durable article ID, current hashes, nonempty raw read-backs, discrepancy-category decision ordering, cards, and equivalence metadata.
• Makes Mathlib proof applicability depend on hash-bound compiled DeclarationSkeleton.kind plus type_is_prop (Meta.isProof), not an authored label. Mixed, proof-valued def/opaque, data axioms, unknown kinds, missing roots, and spoofed intent all have explicit outcomes and stable finding codes.
• Requires current compiled-environment evidence, including broken-body/stale-artifact negatives and external Mathlib artifacts bound to mathlib_file.
• Covers Codex, Claude Code, and Muse; gates verification and Pages from both project-generation paths.

Scope

This is policy, documentation, manifest, and contract-test work only; it changes no shipped runtime behavior. P01–P07 and specialist/corpus units remain future independently reviewable work. P03 stays blocked until the Cabannes fixture has authorized frozen passages and genuinely independent recorded verdicts; CI must not manufacture those judgments.

The long policy diff contains the complete 51-skill disposition table and the requested negative-test matrix. It adds no production code.

Validation

At exact head e1cab363 on canonical main 7fa6d1d6:

• transport/host/skill contract suites: 46 passed;
• Ruff and git diff --check: pass;
• make check-example: pass, including strict MkDocs;
• three independent agent audits found no blocker; human GitHub review pending;
• exact-head GitHub CI: all 9 checks pass.

Attribution, merge, and rollback

Use a merge commit rather than squash so Adam's original authored commit remains visible. To roll back after merge, revert the PR merge commit; no migration or runtime state is created.

[Deicyde]

Three contract blockers remain despite green CI:

1. The plan says every target_branch is real, but C00–C05 use autoform-corpus/main, which is neither a branch here nor an existing repository/ref; the goal also forbids creating the companion before approval. Represent target repository and branch separately (or leave repository gated/unresolved), keep branch main, and test that state.
2. Omitted origin requires source-fidelity: passed, but only origin: cited has a hash/read-back/passage-bound acceptance rule. Require origin for quality subjects or define omission as exactly the same evidence contract; add positive plus arbitrary-link/stale/bare negatives.
3. Mathlib proof applicability must use the compiled skeleton kind, not authored declaration: metadata. A theorem mislabeled definition must not receive proof-integrity N/A; mixed/unknown sets containing a proof-bearing declaration must remain proof-bearing, and kind mismatches must fail. Add spoofed-kind and mixed-target tests.

Everything else reviewed cleanly: the 51 decisions, ownership, DAG/gates/stack parents, adapted-source assignment, strict JSON, current merged-feature alignment, host coverage, authorship preservation, and external-attestation wording are coherent; all CI and 16 focused tests pass. #9 remains untouched while this draft is corrected.

[Deicyde]

Final repair head is e1cab363, pushed without force. Repository/branch binding, explicit origin, verdict identity, hash-bound type_is_prop, data-axiom/proof-valued-definition handling, exact finding precedence, and plan/manifest baseline parity are all regression-pinned. Local focused suites: 46 passed; lint and check-example pass. Exact-head CI is running. Please merge with a merge commit (not squash) to preserve Adam Kiezun’s original commit attribution.

[Deicyde]

Exact-head verification is complete at e1cab363: all 9 GitHub checks pass, the focused contract suites report 46 passing tests, and the independent final reviews are clean. This is ready for human review. Please preserve Adam Kiezun’s original authored commit by using a merge commit rather than squash.

[Deicyde]

Premise re-review: this exact head changes six files, all policy/planning/self-test artifacts. Repository search finds no production, CI, skill, packaging, or installed-runtime consumer for the manifest or four top-level documents; the wheel packages only autoform_cli and servers. The 741-line test file validates the authored plan/manifest rather than product behavior. Green CI therefore does not establish user value. Removing review: ready and returning this to draft; recommendation is to close it and carry any concrete P01–P07 feature forward as a focused issue/functional PR.