docs/veto-necessity.md
Necessity of veto — re-derived over execution semantics
Application of the frozen framework (foundation.md, category 2). Discharges
the re-derivation recorded as pending in §7.3.
Supersedes the earlier state-based derivation. Two of its claims are retracted below; the conclusion survives and is stronger, because it is no longer agent-relative.
1. Execution semantics
An execution is a finite sequence e = ⟨(α₁,p₁), …, (αₙ,pₙ)⟩ of acts paired with the principal who performed them.
- config(e) = ⟨C, L, D⟩ — the constitutional configuration after e: constitutional text, ledger, decision received. A function of e.
- G(e, α, p) — the guard: may principal p perform α after execution e.
- Permitted(e) = { (α,p) : G(e,α,p) }
- Lawful(e) — every step of e was permitted given its own prefix.
The move from states to executions is forced by Article IX, whose guard depends on what happened earlier rather than on what is currently true. Everything else transfers unchanged.
1.1 The current execution is not lawful, and this does not matter
e₀ — the actual history — contains two edits to constitution/amendments.json
performed while the gate was blocking. So ¬Lawful(e₀).
Under Article 0.2, violations "are violations of this constitution, not challenges to it. Fix them immediately." An unlawful step therefore creates a repair obligation; it does not nullify the system or void subsequent guards. Permitted(e₀) is well-defined.
Worth recording because the state-based model could not see this at all: it examined only config(e₀) and had no way to represent that the history reaching it was defective.
2. Exhaustiveness transfers
config(e) remains ⟨C, L, D⟩, and its mutators remain fixed: Article VIII enumerates three files for C and L; X.1.1 fixes two strings for D. So the next act still partitions by which component it changes, or none:
| Partition | Acts | Verdict under Φ |
|---|---|---|
| ΔC | write CONSTITUTION.md / world/constitution.ts |
blocked |
| ΔL | write the ledger, incl. appending a superseding entry | blocked (conflicts with XII.1, the recorded deadlock) |
| ΔD | the two decision strings | permitted to U only |
| none | non-constitutional writes; deploy; merge; workaround; reinterpretation; inaction | mixed, per Φ's five closed bullets |
The decomposition argument is unchanged; it now ranges over Permitted(e₀) rather than over a state.
3. Lemma A′ — approval admits no continuation
Let e₁ = e₀ · (approve, U). Φ lifts. Let α_write be "write the merged Article
XIII into CONSTITUTION.md".
3.1 Disposing of the naive IX.3 reading
IX.3's ordered test contains "Does it touch a constitutional file (VIII)? → amendment". Read literally, enacting any approved amendment would itself require a fresh amendment — an infinite regress, and refuted by fact: AMD-0001 was enacted and Articles XI and XII exist in the document.
IX.3 therefore governs whether Article X must be invoked. Where X has already been invoked and approval given, faithful enactment falls within that protocol rather than constituting a fresh classification event.
That reading has a precise boundary. Enactment is faithful only insofar as the approval determines it. Choices the approval does not settle are fresh constitutional questions, and Article IX bites on those.
3.2 Retraction 1 — Article IX is not independent of SA6′
Previously claimed: the theorem survives SA6′'s failure because Article IX blocks α_write independently. False.
IX's bite is conditional on the rendering containing unsettled choices — which is exactly SA6′'s content. If SA6′ is false, meaning the approval determines a unique article text, then there is no unsettled question for IX to classify and IX does not bite either. X.1.2 and IX key on the same condition. They are one argument, not two.
3.3 Retraction 2 — the theorem is not agent-relative
Previously claimed: APPROVE is progressing when U is the implementer, because Article IX is scoped to "The AI"; hence the result depends on SA8, "the implementer is the AI." False, and the error is locatable.
Article IX is principal-scoped — that observation stands. But it is not the binding constraint. X.1.2 reads:
"Approval is scoped to the single proposal as written. It does not authorise related changes, follow-on edits, or a broader reading."
Its grammatical subject is Approval, not the actor. It constrains what the approval authorises, full stop. Under SA6′ the approval authorises no rendering by anyone; U is as unauthorised as A.
The adversarial pass identified a real asymmetry in IX and then mislocated the binding constraint. SA8 is withdrawn as unnecessary.
3.4 Lemma A′
Under SA6′, for every principal p, (α_write, p) ∉ Permitted(e₁). ∎
Corollary (independent, non-load-bearing). Even were α_write permitted, VII.1 would be violated on ratification: Article XIII obligates three identity-bearing vocabularies and one is probed.
4. Theorem
From e₀:
- Permitted(e₀) ⊇ { (non-constitutional write, A), (inaction, A), (approve, U), (veto, U), (any other utterance, U) }
- Resolving — changing AMD-0003's status: { (approve, U), (veto, U) }
- Under SA6′, e₀·(approve, U) admits no continuation completing ratification, for any principal (Lemma A′)
- e₀·(veto, U) lifts Φ, after which every recorded repair becomes permitted
∴ VETO is the unique progressing transition, agent-independently.
Necessity is conditional on SA6′ alone: approval authorises rendering only when the proposal determines a unique article text. AMD-0003 fails determinacy — its operative content is a base clause plus three corrections that were never merged, and merging requires choices the proposal does not settle.
SA6′ remains checkable and repairable: merge the corrections into one canonical clause and determinacy holds. The theorem thus identifies the single edit that would change its own answer.
5. Status
| Necessity theorem | REFUTED — see §6 |
| Exhaustiveness | transfers by the same decomposition |
| SA8 (implementer is the AI) | withdrawn — unnecessary |
| "IX independent of SA6′" | retracted — same condition |
| Agent-relativity | retracted — X.1.2 is principal-neutral |
| Engineering recommendation | unchanged, but now a preference, not a proven necessity — stated with criteria in amd-0003-decision.md |
6. Refutation
The theorem in §4 is unsound. Found on review of the derivation itself rather than of the surrounding model.
6.1 Fatal — Lemma A′ cannot carry the bullet resting on it
Lemma A′ establishes a one-step claim: (α_write, p) ∉ Permitted(e₁). The third bullet of §4 asserts a claim over all continuations: that e₀·(approve,U) admits no continuation completing ratification. The inference from the first to the second is invalid.
A counterexample exists. Post-approval Φ is lifted, so a further proposal is lawful:
e₁ · propose(AMD-0004: Article XIII with determinate text)
· (decide, U) · enact · α_write
AMD-0004 supplies the determinacy AMD-0003 lacks, so by SA6′ itself α_write becomes permitted. e₁ therefore does complete ratification. The bullet is false and the theorem fails with it.
6.2 The other half was never proven
"e₀·(veto,U) lifts Φ, after which every recorded repair becomes permitted" is asserted with no supporting lemma, and is not self-evident: every repair touches a constitutional file, so by IX.3 each is an amendment requiring its own Article X cycle, with Φ re-engaging on each proposal.
A uniqueness claim requires proving one branch dead and the other alive. One branch was proven (incorrectly) and the other assumed.
6.3 Smaller defects, all real
- ⊇ versus =. Permitted(e₀) is given as a superset, then Resolving is given as a closed set. That step requires equality. §2 argues exhaustiveness, so the ⊇ should be =; as written, §4 does not license its own second bullet.
- SA6′'s applicability is asserted, not exhibited. The claim that merging requires unsettled choices is stated without a witness. One exists — does correction (B) replace or supplement the base clause's "stops it being emitted"? — but it was never written into the proof.
- Quantification. "For any principal" ranges over SA3's two-principal set, which this document does not restate.
- Ratification ⟹ α_write is used but never argued.
6.4 Corrected result
Both APPROVE and VETO are progressing. They differ in cost:
| Cost | |
|---|---|
| APPROVE | an extra amendment cycle, plus an approved-but-never-enacted AMD-0003 left permanently in the ledger |
| VETO | one re-proposal with determinate text |
Necessity fails. VETO CONSTITUTION CHANGE survives as a preference on
grounds of cost and ledger hygiene, not as a proven consequence.
6.5 Pattern worth recording
This is the third time a necessity claim has been advanced and withdrawn in this line of work — first as "the only lawful exit", then as "unique progressing, agent-relative", now as "unique progressing, agent-independent". Each retraction was correct on its own terms, but the recurrence is the signal: the honest claim available from this material has consistently been cheaper and cleaner, and "necessary" has been reached for three times and earned zero.
Future derivations in this area should treat a uniqueness claim as suspect until both branches are proven — the dead one and the live one.