05 - Uniform End-State Proof Scope

The principle

Under Option Beta every in-scope object converges to one uniform authority-neutralized end-state. The recheck-3 fix makes the scope of each proof obligation type-exact, so each obligation runs over a set whose members can actually satisfy it:

obligation	runs over	shape	guard	blueprint ref
owner isolated (OWNER TO qt001_cp_owner)	U_legacy_object only	PG object identity	G-U-LEGACY-OPTION-BETA-UNIFORM-ENDSTATE, G-OWNER-UNREACHABLE	doc 02 §H.3(1), doc 04 S15.1
body/definition unchanged	U_legacy_object only	object definition hash	G-U-LEGACY-OPTION-BETA-UNIFORM-ENDSTATE	doc 02 §H.3(2), doc 04 S15
effective privileges == sealed #21	U_legacy_object × U_effective_privilege_principal	privilege tuple	G-NOLEGACY-POST, G-PRINCIPAL-SET-SEPARATE	doc 02 §H.3(3)/§H.4.B, doc 04 S15.2/S15.3
object exact-set both-EXCEPT	U_legacy_object vs object denominator	PG object identity	G-LEGACY-TARGET-CLOSED-DENOMINATOR, G-U-LEGACY-OBJECT-ONLY	doc 02 §H.4.A
bypass coverage	U_entry_vector → object reachability	entry vector → object	G-ENTRY-VECTOR-SEPARATE	doc 02 §H.4.C

Why this resolves the recheck-3 blocker

The owner/body/#21 object proof now applies only to U_legacy_object. A principal or an entry vector — which cannot own, have a body, or carry object state — is never asked to satisfy an object predicate. The privilege obligation is correctly expressed as a property of (object, principal) pairs (the tuple join), and the bypass obligation as (vector → object) reachability. Each both-EXCEPT compares like with like.

Establishment order (doc 02 §H.5)

1. S00 candidate discovery (diagnostic only).
2. Object membership: U_legacy_object via the #11/#22 object closure ONLY.
3. Object exact-set proof (§H.4.A).
4. Privilege evaluation: build U_effective_privilege_principal, join, reconcile to #21 (§H.4.B).
5. Entry-vector coverage: build U_entry_vector, prove coverage (§H.4.C).
6. Seal only after 3+4+5 pass.

Effective-privilege and entry-vector facts are downstream evaluations over the already-fixed object set — not membership criteria. This removes the type-mixing at its root.

Self-check

PASS. Owner/body/#21 object proof applies only to U_legacy_object; privilege is the object × principal tuple reconciliation; bypass is entry-vector → object coverage; every both-EXCEPT is type-identical.