RS5B-CLOSEOUT-PATCH2 02 — Complete RBP Oracle, PASS Condition & Explicit I6 Predicate — 2026-06-21
RS5B-CLOSEOUT-PATCH2 02 — Complete RBP Oracle, PASS Condition & Explicit I6 Predicate — 2026-06-21
Scope: close Codex blockers B1 (PASS formula omits ¬RBP1) and B2 (I6 has no complete reject predicate). Define the closed reject set, the complete PASS condition, and the explicit I6 predicate ROLLBACK_FORWARD_FAIL_CLOSED_VIOLATED.
Gate: REGISTRATION_HOLD · REGISTRATION_CAN_PROCEED = NO · 0 mutations (design-only). The oracle classifies a proposed rollback plan; classifying it authorizes no rollback execution (invariant I10). ROLLBACK_CONTRACT_VALID_FOR_REVIEW is necessary-not-sufficient.
Supersession: PATCH1-04 §1 reject-set numbering, §2 precedence, and §3 PASS formula (PASS ⇔ ¬RBP0 ∧ ¬RBP2 ∧ … ∧ ¬RBP9, "RBP-1 not a conjunct") are SUPERSEDED_BY_RS5B_CLOSEOUT_PATCH2 (file 08 M11/M12). I1–I10 (PATCH1-02 §2) are retained, not weakened.
1. The closed reject set (RBP-0 .. RBP-10 + RBP-PASS)
The oracle returns exactly one code from this closed set. Each RBP-k (k ≥ 2) is the negation of one rollback invariant (PATCH1-02 §2); RBP-0 enforces I10 at design/review time; RBP-1 is the absence of the object the invariants test.
RBP-0 runtime mutation observed (DDL/DML/PG/Directus/handler write during design/review)
⇒ RUNTIME_MUTATION_REJECTED (enforces I10)
RBP-1 rollback plan absent entirely
⇒ ROLLBACK_PLAN_ABSENT (no plan object to test)
RBP-2 rollback deletes a stable identity referenced by C2 / audit / prior decision
⇒ ROLLBACK_DELETES_REFERENCED_IDENTITY (¬I1 stable identity)
RBP-3 rollback orphans a dependency edge (a reference becomes dangling / unresolvable)
⇒ ROLLBACK_ORPHANS_DEPENDENCY (¬I3 reference integrity)
RBP-4 rollback erases historical evidence while reference/identity may still exist
⇒ ROLLBACK_ERASES_HISTORY (¬I2 historical evidence)
RBP-5 rollback changes the semantics of a prior envelope / schema version
⇒ ROLLBACK_CHANGES_HISTORICAL_SEMANTICS (¬I4 semantic immutability)
RBP-6 rollback weakens a prior OR forward authority requirement
⇒ ROLLBACK_WEAKENS_AUTHORITY (¬I5 authority non-weakening)
RBP-7 rollback lacks a successor / supersession / compatibility rule
⇒ ROLLBACK_SUCCESSOR_RULE_ABSENT (¬I7 versioned/compensating)
RBP-8 a successor rule EXISTS but the retired/superseded value remains valid for new use
⇒ ROLLBACK_FORWARD_FAIL_CLOSED_VIOLATED (¬I6 forward fail-closed) ← NEW (B2)
RBP-9 rollback cannot be audited (no rollback_ref / no audit entry)
⇒ ROLLBACK_AUDIT_TRAIL_ABSENT (¬I8 auditability)
RBP-10 rollback requires silent mutation of another carrier
⇒ ROLLBACK_NOT_LOCAL (¬I9 locality)
RBP-PASS no reject predicate matches
⇒ ROLLBACK_CONTRACT_VALID_FOR_REVIEW (I1–I10 all hold; review-only)
Change vs PATCH1: PATCH1 had ten reject predicates (RBP-0, RBP-2..RBP-9, RBP-1) and folded I6 into "RBP-7 plus per-carrier postconditions." PATCH2 adds RBP-8 ROLLBACK_FORWARD_FAIL_CLOSED_VIOLATED as the dedicated I6 predicate, and renumbers audit → RBP-9 and locality → RBP-10. The reject set is now eleven predicates with a 1:1 invariant mapping (§4).
2. The complete PASS condition (closes B1)
ROLLBACK_CONTRACT_VALID_FOR_REVIEW is emitted iff no reject predicate matches. Stated as the controlling conjunction over every reject predicate, including ¬RBP1:
ROLLBACK_CONTRACT_VALID_FOR_REVIEW ⇔
¬RBP0 ∧ ¬RBP1 ∧ ¬RBP2 ∧ ¬RBP3 ∧ ¬RBP4 ∧
¬RBP5 ∧ ¬RBP6 ∧ ¬RBP7 ∧ ¬RBP8 ∧ ¬RBP9 ∧ ¬RBP10
Equivalently: PASS ⇔ ¬(RBP0 ∨ RBP1 ∨ … ∨ RBP10). Plan presence is a conjunct of PASS (¬RBP1), not an external assumption. The PATCH1 sentence "RBP-1 is not a conjunct of PASS" is superseded and deleted from the controlling reading.
2.1 Mandatory PASS-impossibility proofs
P-B1 — ROLLBACK_PLAN_ABSENT ⇒ PASS impossible. If RBP-1 matches, then ¬RBP1 is false, so the conjunction is false, so ROLLBACK_CONTRACT_VALID_FOR_REVIEW cannot be emitted. A missing plan can never be a valid plan. ∎
P-B2 — successor exists but retired value remains valid for new use ⇒ PASS impossible. Such an input matches RBP-8 (ROLLBACK_FORWARD_FAIL_CLOSED_VIOLATED), so ¬RBP8 is false, so the conjunction is false. The presence of a successor rule negates only RBP-7, not RBP-8; the two are disjoint by the predicate Q below. Therefore "has a successor rule" no longer buys a path to PASS. ∎
P-destructive — any destructive/orphan/history/semantic/authority/non-local match ⇒ PASS impossible. If any of RBP-2..RBP-6, RBP-9, RBP-10 matches, its negation is false and the conjunction is false. A plan that deletes a referenced identity (RBP-2), orphans a dependency (RBP-3), erases history (RBP-4), changes prior semantics (RBP-5), weakens prior or forward authority (RBP-6), is unauditable (RBP-9), or is non-local (RBP-10) cannot reach PASS — regardless of how many other invariants it satisfies. ∎
Corollary (implementation-independent). PASS is the conjunction of all eleven invariant checks; it is therefore independent of evaluation order. The precedence (file 03 §1) decides which single code is reported when several reject predicates match, but it never makes PASS reachable for an input that matches any reject predicate.
3. The explicit I6 predicate ROLLBACK_FORWARD_FAIL_CLOSED_VIOLATED (closes B2)
I6 (PATCH1-02 §2) requires: new use of a retired/superseded carrier value must fail unless an explicit successor transition exists. PATCH1 enforced I6 "jointly by RBP-7 and per-carrier postconditions." Codex §6.2 proved that insufficient: a plan can have a successor rule and still admit the retired value for new acts, while satisfying every other invariant — and reach PASS.
PATCH2 gives I6 its own reject predicate.
3.1 RBP-8 definition
RBP-8 fires when a rollback plan has a successor / supersession / compatibility rule (so RBP-7 does not fire) and the retired / superseded value remains admissible for a new act — i.e. the forward path is not fail-closed against the retired value. ⇒
ROLLBACK_FORWARD_FAIL_CLOSED_VIOLATED.
3.2 Disjointness of RBP-7 vs RBP-8 (predicate Q)
Let Q = (a successor / supersession / compatibility rule is present in the plan).
| Q | retired value admissible for new use? | Code |
|---|---|---|
| ¬Q | — (no successor rule at all) | RBP-7 ROLLBACK_SUCCESSOR_RULE_ABSENT |
| Q | yes (new act may still use the retired value) | RBP-8 ROLLBACK_FORWARD_FAIL_CLOSED_VIOLATED |
| Q | no (new use of the retired value is fail-closed; only the successor is accepted) | neither — continue to RBP-9/RBP-10/PASS |
RBP-7 and RBP-8 are mutually exclusive on Q: RBP-7 requires ¬Q, RBP-8 requires Q. No input satisfies both. RBP-7 (rank 7) precedes RBP-8 (rank 8): a plan with no successor rule at all is reported as ROLLBACK_SUCCESSOR_RULE_ABSENT (the more basic defect) before the forward-fail-closed test is even reached. This is the same two-layer disjoint-by-discriminator construction used for BI-E6 → BI-E1 in Job A (discriminator P); here the discriminator is Q.
3.3 Why RBP-8 was necessary
Without RBP-8, the input "retire value v, define successor v′, but keep accepting v for new effects" satisfies: I1 (v resolvable), I2 (history readable), I3 (edges intact), I4 (no semantic change), I5 (no authority change), I7 (a successor rule exists ⇒ ¬RBP7), I8 (audited), I9 (local). Under PATCH1 it reached ROLLBACK_CONTRACT_VALID_FOR_REVIEW while violating I6. Under PATCH2 it matches RBP-8 ⇒ ¬RBP8 false ⇒ PASS impossible (proof P-B2). Fixture XBI-26 (file 04) is the executable witness.
4. Invariant ↔ predicate mapping (1:1, complete)
| Invariant (PATCH1-02 §2) | Reject predicate | Code |
|---|---|---|
| I1 stable identity | RBP-2 | ROLLBACK_DELETES_REFERENCED_IDENTITY |
| I2 historical evidence | RBP-4 | ROLLBACK_ERASES_HISTORY |
| I3 reference integrity | RBP-3 | ROLLBACK_ORPHANS_DEPENDENCY |
| I4 semantic immutability | RBP-5 | ROLLBACK_CHANGES_HISTORICAL_SEMANTICS |
| I5 authority non-weakening (prior and forward) | RBP-6 | ROLLBACK_WEAKENS_AUTHORITY |
| I6 forward fail-closed | RBP-8 | ROLLBACK_FORWARD_FAIL_CLOSED_VIOLATED ← NEW |
| I7 versioned / compensating | RBP-7 | ROLLBACK_SUCCESSOR_RULE_ABSENT |
| I8 auditability | RBP-9 | ROLLBACK_AUDIT_TRAIL_ABSENT |
| I9 locality | RBP-10 | ROLLBACK_NOT_LOCAL |
| I10 no runtime permission | RBP-0 (design/review-time) | RUNTIME_MUTATION_REJECTED |
| (precondition: a plan object exists) | RBP-1 | ROLLBACK_PLAN_ABSENT |
Every invariant now has a dedicated reject predicate. The earlier "I6 enforced jointly by RBP-7 + postconditions" is superseded: I6 ↔ RBP-8 exclusively (postconditions remain corroborating evidence, not the sole enforcement).
5. Necessary-not-sufficient restatement
ROLLBACK_CONTRACT_VALID_FOR_REVIEW means only: this rollback plan is dependency-safe enough to be reviewed. It is not runtime permission, not permission to execute the rollback, not P2 authorization, not registration/activation. Executing a rollback is a separate, separately-authorized act (Gate B / a later P3-grade gate) under item-13 Chairman authorization, and the global RUNTIME_MUTATION_REJECTED short-circuit (RBP-0) applies to any rollback write observed in design/review. Same posture as BINDING_CHECK_PASS in Job A.
6. Boundary attestation
This file changes no runtime state, creates no carrier, executes no rollback, opens no P2, and clears no blocker. It defines the oracle's PASS condition and the I6 predicate at design level only. REGISTRATION_HOLD retained; REGISTRATION_CAN_PROCEED = NO; I1–I10 not weakened; Job A not reopened.