contract(custody-schema): revision 12 — exact token comparison base case, split stale database-half boundary

sol r11 APPROVE minors:
- F19: strictly-less-than refusal made explicit; absent recorded token
  compares lower than every minted token, first acceptance creates the
  record; §7.10 virgin-locator control + delayed-first-grant race.
- F18 residual closed: §7.10 managed-deletion fault predicate restated
  as the exact §4.7 predicate (advance's epoch mint and token record
  permitted).
- F20: pre-advance linearization boundary distinguishes database
  halves — pair-conditioned step 2 for deletion/repair; terminated
  ordinary writer performs no pointer upsert, retry is a fresh
  acquisition; §7.10 control runs both branches.
- §8 item 16 revision-12 clause; preamble Revision 12 paragraph.

docs/requirements/custody-schema.md

@@ -247,6 +247,27 @@ pre-advance linearization control, and extends the fence-invariant
 static control with the token invariants; §7.16's static
 fenced-commit control carries the token (F16, F18).
 
+Revision 12 (sol r11 minors F18 residual, F19, F20): three
+exactness corrections to the revision-11 mechanism, no behavioral
+change. §3.7's token comparison is made exact at both ends:
+strictly less-than refuses (an already-recorded token re-presented
+by a swap-loop retry or a later mutation of the same acquisition is
+accepted), and an absent recorded token compares lower than every
+minted token, so a virgin locator's first advance is accepted and
+atomically creates the token record — with a §7.10 virgin-locator
+control and a delayed-first-grant race variant (F19). §7.10's
+remaining managed-deletion fault predicate ("both stores
+unchanged") is restated as the exact §4.7 predicate — content
+presence, content bytes, and database rows unchanged, the
+advance's epoch mint and token recording expressly permitted
+(F18 closed). The pre-advance-linearization outcome no longer
+assigns the (`id`, `generation`) pair to every stale operation:
+the §3.7 boundary text and the §7.10 control now distinguish the
+database halves — deletion's and repair's step 2 stays
+pair-conditioned, while a terminated ordinary writer performs no
+pointer upsert and can continue only through a fresh acquisition
+under a new token (F20).
+
 This contract binds the profile-category registry (§2), the custody
 placement rule (§3), the pointer schema (§4), the consent schema and its
 evaluation (§5), mode application (§6), witnesses (§7), and disclosed
@@ -529,6 +550,16 @@ with contract 6 (`mode-conversion.md`), identity with
    lock — the fence-advance below included — presents its holder's
    acquisition token, is REFUSED atomically when that token is
    less than the recorded value, and records it on acceptance.
+   The comparison is exact at both ends: it is strictly
+   less-than — re-presenting the already-recorded token, as a
+   swap-loop retry or a later mutation of the same acquisition
+   does, is accepted — and a locator with NO recorded token
+   compares as lower than every minted token, so a virgin
+   locator's first presented token is never refused by this
+   comparison and its acceptance atomically CREATES the token
+   record; an implementation whose absent-token comparison can
+   refuse or fail to record the first holder is nonconforming
+   (witness §7.10).
    **Fence-advance at
    acquisition:** immediately after acquiring the locator lock,
    before its first brain observation or mutation at the locator,
@@ -581,9 +612,16 @@ with contract 6 (`mode-conversion.md`), identity with
    advance — so the stale effect serializes entirely before
    anything the new holder relies on, indistinguishable from the
    same operation completing before the previous holder's lock
-   release, an outcome the protocol already defines as legal (its
+   release, an outcome the protocol already defines as legal. What
-   database half remains governed by the (`id`, `generation`)
+   the stale operation's DATABASE half may then do depends on its
-   pair, §4.5, §4.7). These are the only two outcomes: a stale
+   protocol: a managed deletion's or repair's step 2 remains
+   conditioned on the recorded (`id`, `generation`) pair (§4.5,
+   §4.7) and cannot unpoint any later row incarnation; an ordinary
+   write's terminated run performs NO pointer upsert — its
+   database session is dead, the committed-but-unpointed content
+   falls into the existing step-1-to-step-2 interruption window
+   repaired by §4.5, and any retry is a NEW lock acquisition under
+   a fresh token, never a continuation of the dead run. These are the only two outcomes: a stale
    operation either serializes wholly before the new holder's
    advance or is refused; it never applies after the advance, and
    it cannot remove or replace content committed by any later
@@ -1184,7 +1222,11 @@ declared profile table" means `profile_answers` (§3.5).
     the next triggered reconciliation deletes the pointer and writes
     no content anywhere in the database (§4.5). The §4.7 protocol is
     fault-injected at both interruption points: killed before the
-    brain commit, both stores are unchanged; killed between the brain
+    brain commit, content presence, content bytes, and every
+    database row are unchanged — the deleter's post-acquisition
+    fence-advance may already have minted an epoch and recorded an
+    acquisition token, the only brain change the protocol permits
+    before step 1; killed between the brain
     commit and the pointer delete, the dangling pointer is deleted by
     the next reconciliation — and at no point is content written to
     the database or restored to the brain. **Concurrent-rewrite
@@ -1327,7 +1369,20 @@ declared profile table" means `profile_answers` (§3.5).
     observes content absence, W1's late advance resumed before
     the DELETE is asserted refused and fenceless, and the DELETE
     completes under its recorded (`id`, `generation`) token with
-    no unpointed content resurrected. A **pre-advance
+    no unpointed content resurrected. A **virgin-locator token
+    control** exercises the §3.7 absent-token base case: the FIRST
+    lock grant ever issued for a locator (no recorded acquisition
+    token exists in the brain store) performs its mandatory
+    fence-advance and is asserted ACCEPTED — the advance mints the
+    locator's epoch and its acceptance atomically creates the
+    token record — and the holder's subsequent fenced mutation
+    succeeds; a delayed-first-grant race variant suspends that
+    first holder's advance before application, terminates the
+    session at the deadline, lets a second holder acquire the
+    lock (receiving a greater token) and complete its own advance,
+    then resumes the first holder's advance and asserts it REFUSED
+    by the token comparison — the base case never admits a
+    superseded first grant. A **pre-advance
     linearization control** exercises the §3.7 legal-outcome
     boundary: a terminated holder's stale content mutation is
     scheduled to linearize immediately BEFORE the next holder's
@@ -1337,9 +1392,17 @@ declared profile table" means `profile_answers` (§3.5).
     after it, the new holder's first relied-on observation
     reflects the committed stale effect, and the end state is
     consistent — equivalent to the stale operation having
-    completed before the previous holder's lock release — with
+    completed before the previous holder's lock release. The
-    the stale operation's database half still governed by the
+    control runs BOTH database-half branches: with the stale
-    (`id`, `generation`) pair. An **exceedance control** contrives a
+    mutation a managed deletion's step-1 brain half, its stale
+    step-2 DELETE remains conditioned on the recorded
+    (`id`, `generation`) pair and is asserted to match ZERO rows
+    against a later row incarnation; with the stale mutation an
+    ordinary §3.7 writer's step-1 content commit, the terminated
+    run is asserted to perform NO pointer upsert — the unpointed
+    content is repaired by §4.5 within one cycle, and a retry of
+    the write is asserted to run as a fresh lock acquisition
+    under a new token. An **exceedance control** contrives a
     cycle that cannot finish within its computed `M` (an injected
     sequence of deadline-length holders on a reserved locator) and
     asserts the cycle reports FAILURE — never completion —
@@ -1614,7 +1677,14 @@ UPDATE` as the first statement of its transaction, and the
     abort-release-surface transition, and a stale operation
     either serializes wholly before the new holder's advance —
     the defined legal pre-release-completion-equivalent outcome —
-    or is refused), so live interleavings
+    or is refused; per revision 12 the token comparison is exact
+    at both ends — strictly less-than refuses, an absent recorded
+    token compares lower than every minted token so a virgin
+    locator's first advance is accepted and creates the record —
+    and the pre-advance-linearization outcome distinguishes the
+    stale database halves: pair-conditioned step 2 for deletion
+    and repair, no pointer upsert ever for a terminated ordinary
+    writer), so live interleavings
     between any two mutators are excluded by one serialization
     protocol, and stale external tails are excluded by the fence
     (§3.7, §4.5, §4.7, §7.16).