One-shot founding and conditional progress¶
GA-SYN-003 · Edition 2026.10.7 · Synthetic technical investigation
Proposition and operational question¶
Finishing the three-stage commissioning example leaves the voucher unavailable; eventual resolution additionally needs a progress assumption.
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¶
The stages are new, open and closed. One voucher permits finishing while open. The model treats the commissioning authority as trusted and the scheduler as potentially idle. Opening and finishing are separate transitions. Safety means that a closed installation does not retain the voucher. Progress means eventually leaving the open stage; it is a different claim.
Worked synthetic trace¶
Begin at new with the voucher available. Open moves to open and retains it. Finish moves to closed and consumes it. A repeated finish leaves the terminal state unchanged. The printed trace records all three events. Now consider open, wait, open, wait without end. Nothing unsafe occurs, yet resolution never arrives. If continuously enabled opening and finishing-or-cancelling eventually occur, this finite progression reaches a terminal disposition. That fairness condition is an environmental premise.
Negative control¶
The safety mutant leaves the voucher available at close, producing a visible violation. Separately the explicit waiting cycle is a liveness counterexample when progress is not assumed. The Python example reports that cycle; it is not a TLC proof or a check of a real ceremony. The existing AD8 paper reports separate finite formal studies with their own evidence.
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 | Author execution of the independent public teaching case founding, 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. An internal author run does not count as independent review.
Limitations and open obligations¶
The example contains no cryptographic root, distributed ceremony, membership policy, trusted clock or real custodian. It does not show that operators act, that a closed system can never be reinitialized, or that all crashes preserve consumption. The real implementation would need a durable one-shot boundary and an argument relating its possible states to the model.
Prior art and contribution limit¶
Safety, liveness and fairness are standard formal-methods distinctions. This dossier uses them to make a common commissioning error inspectable. It claims neither a novel consensus construction nor production founding conformance. 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 founding
python examples/investigations/check.py --case founding --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-003, edition 2026.10.7, 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.