DRB-9: Compress formal policy and generated-output carriers through the formal integrator

[metaphorics]

Problem

formal/extension_policy.md carries exact inventory counts and a generated-authority rule that duplicate executable constants and the generated manifest/ledger. Any concurrent formal work will silently drift the prose from the generated source of truth.

Exact conflicts

• Inventory totals: formal/extension_policy.md:105-108 says the locked inventory is 80 Lean + 74 Quint + 110 Redex = 264 rows, owner P0.7. formal/ledger_wiring.rs:34-43 defines EXPECTED_P07_ROWS = 264, FORMAL_LEAN_ROWS = 80, FORMAL_QUINT_ROWS = 74, FORMAL_REDEX_ROWS = 110, and a compile-time assert! that the sum equals EXPECTED_P07_ROWS.
• Enforcement: formal/ledger_wiring.rs:314-322 and 322-329 reject any universe whose per-catalog or total counts differ from those constants.
• Generated-authority duplication: formal/extension_policy.md:17-24 (do not hand-edit verification/manifest.lock.json / proof/completeness-ledger.json) repeats the generated-authority rule also found in AGENTS.md:7 and docs/release/runbook.md:53-85, without pointing at a single generated-surface registry.

Scope of change

• Keep formal/extension_policy.md as workflow/rationale prose only (admission source, G4 authority, forbidden shortcuts, PASS semantics).
• Remove the literal inventory counts from the markdown; point to formal/ledger_wiring.rs constants and the generated manifest/ledger as the source of truth.
• Centralize the generated-output ownership rule for formal artifacts in a single registry (generated-surface table or formal/ledger_wiring.rs documentation) and replace duplicated text with a stable pointer.
• Route any generated change through the formal cluster integrator so catalog, manifest, ledger, receipt digests, and policy stay consistent.

Source-of-truth predecessors

• Exact formal inventory: formal/ledger_wiring.rs::EXPECTED_P07_ROWS, FORMAL_LEAN_ROWS, FORMAL_QUINT_ROWS, FORMAL_REDEX_ROWS.
• Manifest/ledger authority: verification/manifest.lock.json and proof/completeness-ledger.json.
• Generated-surface registry: consolidation owner identified in .outline/research/docs-rules-build-audit.md (one generated-surface table owning output → source → write command → check command → writer).
• Formal workflow policy: formal/extension_policy.md sections 1–5.

Acceptance

• formal/extension_policy.md no longer contains literal counts 80, 74, 110, 264, or their sum; it references the generated manifest or ledger_wiring.rs constants.
• cargo check -p bamts-verification and cargo test -p bamts-verification pass, proving the counted constants are still the enforced source of truth.
• bamts-verification completion verify --root product (or the current product gate) passes after the prose-only edit.
• A single registry lists the formal generated artifacts (verification/manifest.lock.json, proof/completeness-ledger.json, etc.), their generator commands, and their --check commands.

Blockers

• The formal cluster integrator must be used for any generated/manifest change.
• Concurrent P0.7 formal work must freeze at the counted constants before the prose is rewritten, to avoid landing on a stale sum.

[metaphorics]

Dependencies

This issue is blocked by:

• Formal cluster integrator approval (any generated/manifest change must route through the formal cluster integrator)
• Concurrent P0.7 count freeze (formal work must freeze at the counted constants before the prose is rewritten, to avoid landing on a stale sum)

Parent: #156. Feeds: #185.