v4-engine Sub-A: preregister the attempt budget + stopping rule (FailureDisposition, not carried-forward todo)

[usurobor]

Parent: #102. Reason to change: the v4 engine build must not be able to launder a hard requirement into silence under deadline. Priority: P1. Mode: docs-only. Lands first — governs Sub-B–D. PROPOSED — not dispatched.

Problem

• What exists: OBS-LINEAGE-001 forbids reclassifying a failed receipt, but nothing binds the engine author to a stopping rule when a requirement turns out expensive to mechanize. The archaeology's load-bearing lesson is that v2.3 recorded its 92% braided-witness failure and then quietly replaced the foundation instead of the parser — nobody lied; the failure just stopped being load-bearing.
• What is expected: a preregistered attempt budget with a written stopping rule, committed before any mechanization begins, so a can't-mechanize outcome produces a FailureDisposition + spec amendment, not a carried-forward todo.
• Where they diverge: the temptation to reclassify appears exactly at §8.6, and there is currently no artifact β can check for it.

Impact

Governs the entire wave. Without it, Sub-B (which may find typecheck unmechanizable in OCaml) has no honest exit and defaults to "todo for later."

Status truth

No budget artifact exists today. This sub produces one; it ships no engine code.

Source of truth

Claim / surface	Canonical source	Status
failure-persistence obligation	spec/tsc-conformance.md OBS-LINEAGE-001; spec/tsc-observation-dynamics.md §9	Normative
failure disposition vocabulary	docs/design/foundation-contract-reconciliation/CUTOVER-RECEIPT.md	Shipped
archaeology (92% precedent)	docs/design/foundation-contract-reconciliation/ARCHAEOLOGY.md	Shipped

Acceptance criteria

AC1 — budget artifact exists

• Invariant: a committed doc declares, per requirement targeted by this wave, an attempt budget (time/effort) and a written stopping rule.
• Oracle: file presence + section-schema check.
• Positive: docs/design/foundation-contract-reconciliation/v4-engine-attempt-budget.md names each targeted requirement with a budget and a stopping rule.
• Negative: a targeted requirement with no budget line → incomplete, Sub-B may not start.

AC2 — stopping rule resolves to a disposition, not a todo

• Invariant: the rule states that budget exhaustion yields a FailureDisposition + a named spec/fixture amendment.
• Oracle: prose contains the disposition branch and forbids the carried-forward-todo branch.
• Positive: "requirement R unmechanized within budget → open a FailureDisposition, amend foundation-v4 proof class or the spec, record in lineage."
• Negative: any "defer R to a later cycle" escape clause → rejected.

Non-goals

• No engine code, no fixture change, no version bump.
• Not the FND-TYPE-001 investigation itself (Sub-B) — only the budget that governs it.

Success / closure condition

Closeable when the budget doc exists, every requirement this wave targets carries a budget + stopping rule, and the stopping rule resolves to disposition-plus-amendment with no carried-forward-todo escape.