Approval binds the action actually consumed¶
GA-SYN-001 · Edition 2026.10.8 · Synthetic technical investigation
Proposition and operational question¶
An approval for the blue message permits at most one execution, and every permitted execution is blue, over all three-submission histories drawn from blue and green.
This matters when a continuing task reuses an earlier decision or representation. A final success label can conceal a different failure earlier in the trace. The proposition therefore identifies the exact observation that would refute it.
Definitions, trust and failure model¶
A ticket is a single available permission. A submission is an opaque message label. Equality of labels stands for equality of the complete approved object; it is an assumption about identity, not a hash implementation. The execution list is the observation. The consumer atomically checks equality and consumes the ticket. The requester controls submission order and may change its proposal after approval. It cannot alter the consumer or mint another ticket.
Worked synthetic trace¶
Consider green, blue, blue. Initially the ticket is unused and the execution list is empty. Green fails the equality check, leaving the ticket available. Blue then consumes it and appends blue. The third submission is refused because the ticket is spent. The final list is [blue]. Over all eight length-three histories the list is either empty or [blue]. This is stronger than checking that a ticket was consumed: it checks the identity that was actually executed.
Negative control¶
Remove the equality condition while retaining one-use accounting. The history green, blue, blue now executes green first and spends the ticket. The one-use condition still holds, so that condition alone would miss the error. The mutant command returns a nonzero exit and prints the offending history. No real action endpoint is present.
Three evidence records and separate axes¶
| Record | Method and evidence | Scope and status |
|---|---|---|
| Research | Authored finite argument and explicit counterexample, 12 October 2026 | Analytical; limited to the definitions above |
| Reference | My execution, with AI assistance, of the independently designed public teaching case approval, 12 October 2026 |
Fault-tested; externally reproducible with the commands below; no independent reproduction claimed |
| Production | None for this proposition | No product conformance inferred |
Engineering maturity: reference_implemented, referring only to the disclosed teaching case. Assurance: analytical, fault_tested, externally_reproducible, each restricted to its evidence record. These labels are independent dimensions, not a score or a global verification flag. The exact machine-readable record is in the public evidence catalog. My own runs do not count as independent review.
Limitations and open obligations¶
Identity equality must include every consequential parameter in a real system; an omitted target or changed interpretation can invalidate the abstraction. Atomic check-and-consume, durable state across crashes, authority revocation, multiple approvers and concurrent consumers are unmodeled. The reference has one ticket, not a distributed approval service. A receipt about consumption does not establish an external effect.
Prior art and contribution limit¶
Complete mediation and separation of privilege are established protection principles. This case adds no new authorization theorem. Its contribution is an inspectable distinction between one-use accounting and payload binding, which the AD8 investigation must preserve through any implementation. See the primary reference and the comparison guide. No priority or superiority claim follows from this example.
Reproduction and falsification¶
From the successor public source package, use CPython 3.12.14 and no external packages:
python examples/investigations/check.py --case approval
python examples/investigations/check.py --case approval --mutant
The first command must exit zero, with no positive violations and at least one negative violation. The second intentionally exits one and prints an actual violated case. It is a deliberate fault result, not an installation failure. Source and reproduction contract identify the exact population and scope.
Submit a counterexample, a missing assumption or a prior-art correction through the review guide. Include GA-SYN-001, edition 2026.10.8, the command, input and output, and whether the objection concerns the model, implementation or proposed product relationship. Do not send credentials or confidential customer material.
For the wider architecture, see the AD8 paper, architecture synthesis, claim register, and AD8 investigation overview. Native reference results and open constructions have separate scope; these examples do not implement them.