Legitimacy · executed composition · offline artifact
Two approvals.
One collective effect.
Two supplied principals deliver harmless synthetic fragments. Local authorization permits each action. Their public deliveries can still compose into a forbidden result. Inspect the execution, then test a useful repair.
One fixed property throughout
Both distinct synthetic fragments must never reach the public channel.
Legitimacy.boolJointForbiddenList
A public exposure maps to A=true; B public exposure maps to B=false. Lean proves this principal-dependent encoding matches the existing conjunctive property.
Checking pinned fixture bytes…
What the host actually delivered
Event order is supplied by the sequential host. Actions come from its instrumented delivery boundary, never inferred from model prose.
Challenge the evidence
The missing obligation
Tracking the cross-agent conjunction is already present. The useful addition is to require each authorized delivery to preserve exclusion of the original collective property in the current exposure state.
Vault delivery and a public summary remain permitted. The same B fragment request is permitted before A's public release and denied afterward.
What the proof adds
Lean proves the executed-action refinement, safety for every finite guarded request list, and concrete useful alternatives. A full-context conventional checker reaches the same decisions. The contribution is the checked connection and repair, not superior detection.
Without scoped delegation, two observation-identical modeled requests require different decisions. Authentication alone cannot resolve that missing fact.
How much context must survive observation?
For exact next-request decisions, the monitor must distinguish these three reachable safe states. Lean proves one exposure-state bit cannot suffice; the two exposure bits are sufficient for every modeled request. A deny-all monitor is outside this selectivity requirement.
| Prior public exposure | Next A public fragment | Next B public fragment |
|---|
| Neither | Permit | Permit |
| A only | Permit | Deny |
| B only | Deny | Permit |
These answers assume authenticated, delegated requests. This finite bound concerns retained exposure context, not model capability or Shannon capacity.
Reproduce and inspect
./reproduce.sh
# Or: ./legitimacy-executed-composition check capture/bundle.json \
# --trust capture/trust-policy.json
The CLI reuses the existing typed Ed25519 replay authority boundary and checks concrete effects independently of this page. The browser checks pinned fixture bytes and recomputes finite semantics; it does not verify the signed replay receipt.
Trusted: the supplied host, principal slots, declared channels, host completion, action-to-effect implementation, and published public trust root. This is a sequential synthetic experiment. It proves no model alignment, production incident prevention, hidden-intent recovery, or unmodeled-channel discovery.