NicolasRouquette · Nov 14, 2026 · Nov 14, 2026
diff --git a/DOCS.md b/DOCS.md
@@ -52839,7 +52839,6 @@ P1 — P118's hypotheses hold at all 525 in-flow content steps (P115's count).
 **Review round 3 (PR #311).**  Finding: "Completed-pair detector misses reserved token slots — `saveSimpleKey` leaves `.placeholder` tokens between `:` and the value; `pairValueBefore` skips only properties, so the 0 pin cannot detect completed pairs."  Fair — a §7 green-signal error of the probe kind: the probe read `scanFiltered`'s output (placeholders filtered), while P119 walks the raw step states, where the slots are.  Both back-walks (`pairValueBefore`, `explicitKeyBefore`) now skip `.placeholder` with the properties, and the detector is pinned NON-vacuously: at every in-flow `,` / `]` / `}` step on a `.value` tail it must see the completed pair — 127 of 370 such steps are pairs (predicted ≈ 60, REFUTED upward: the corpus holds more flow pairs than the `?`/`:` estimate suggested), so a detector that missed them would move the pin.  The `:`-step classes are unchanged (implicit 113, explicit 13, after-a-pair 0 — the scanner refuses that `:`, so no step exists to detect).  Adversarial 62,182/62,182; test and docs only.
 
 **NEXT —** slice (4) PR 7 at the next free item number (494 or later — 492 is Row 19's births PR, 493 R12's (a) lemma; verify the open PRs before cutting and declare the gap), the pay of price (1): `KeyArm` in `StreamAccum` and `accum_step_block`'s conclusion carrying it at depth ≥ 1 (six constructors, the six sites; `FlowStackK.withArm`'s shape), with `keyArm_of_dispatch` reading the constructor off the dispatcher's split; Priority 119 is the grid (the arm by step as pinned); pins for a new typed production as item 484 recorded.  Then (2) the T step + fold (`receiveColonValue`, `accum_step_key_trace`, `accum_step_key_pairK`) and (3) `accum_step_flow_pairK`; then 2c (`scan_trace` over `scanLoop`).  (b) enters at the block re-walk's depth-0 node assembly, not before.  Item 481's NEXT (the census deletions, (C) split) stands behind the capstone lane.
-||||||| parent of b040f343 (docs(row 12): item 493 — (ω-pay-births) step (a) REFUTED before the proof: the three non-strict `nv ≤ k` guards are slot survival, not a scanner fact — Rule 2 (P97) reaches their `else` on-path at 12 dedent-`-` pauses (10 parsing); the lemma holds of the post-step marks (0 violations) and is (d)'s dedent clause; the 3 re-priced into the 'closed by this step' class; test exe built, no library change; gap 492 (Row 19) declared; 491 (#311) landed first)
 
 ### Item 493 (2026-11-14)
 
@@ -52869,3 +52868,35 @@ P1 — P118's hypotheses hold at all 525 in-flow content steps (P115's count).
 **Gates.**  Full `lake build` green on the #310 base plus this test (1564 jobs, 177 warnings — the base's); `check-theorem-keyword`, `check-import-closure`, `check-reflection-index`, `check-closure-log` (11..493 ascending, dates non-decreasing, 4 gaps: 18, 442, 491, 492), `check-serialization-proofs`, `check-gate-vocab`, `check-pack-births` (9+5 / 9+5 / 23+0 unchanged — no producer touched), `check-scripts-lean`, `run-all-tests`, `suiterunner` 869 / 0 / 151, `eventscore`; `lake exe adversarialinstantiation` 62182 / 62182 (+1 claim, P97).  No pin moved: no library module changed, no census count moved; capstone-path ON 7 / 269 unchanged.  Axiom census: no declaration touched.
 
 **NEXT —** (ω-pay-births) resumes with the plan corrected: (b′) `sameLevelChainMap` as item 462 priced it, with its "by refutation" clause now NAMED and owed as the lemma above (`∀ m ∈ markedCols s', m ≤ k` at a `-` landing; its `:`/`?` twin at the opener arm) — one PR; then (c) `h_mapTail` (item 471's spec); then (d), whose spec grows one clause: `PackAlt`'s content for the 7 "closed by this step" `else`s is `nv ∉ markedCols s'` (post-state), to be flip-priced on the item 442 anchor before the pay — STOP-price if the restatement starves.  No further read item on (a): its question is closed.
+
+### Item 496 (2026-11-14)
+
+**(ω-pay-births) (d) PRICED as ONE composite spec, `scripts/flips/item496_d_composite.json`: item 471's producers' premise (9 anchors) + the chain premise's domain moved to the POST-state (`scripts/flips/item496_post_state_domain.json`, 3 anchors — the honest content of items 493 / 495's seven "closed by this step" `else`s) + Row 19's item 494 `h_res_land` clause (3 anchors): 100 sites in 17 declarations at the StreamAccum fixpoint (two rounds; +2 capstone `sorryAx` propagation sites outside the flip's scope), exactly additive — 78 (item 471) + 9 (the domain) + 13 (item 494), no site shared; no class STARVED; the two `closeThenBlock` `⟨[], …⟩` births over `SCompactSeqTail` do not surface (they type-check) and are named by hand. Source restored; no build; no library change.**  Gaps 492 (Row 19's #313), 494 (Row 19's #316) and 495 (#315) are declared until they land.
+
+**The mandate.**  Item 490's NEXT (the latest merged) is S3's lane — quoted at item 493 / 495 and unchanged.  This lane's mandate is item 495's NEXT (#315, open): "(ω-pay-births) is (d) alone, spec first — item 471's producers' premise re-anchored and grown by the post-state clause, the two landing lemmas, (c)'s `h_mapTail` as the dedent-sibling clause, and Row 19's `h_res_land` resume-fact clause (item 494) — Rule 2 (P99) over every ON position before any pay; STOP-price if it starves" — and the owner's ruling (relayed 2026-11-14): "(d)'s scope now includes, in the same producers (`closeThenBlock` / `pendingBlockContent` / `pendingBlock`): (i) the openers' `h_res_land` resume fact at the 12 declines — 6 relays of upstream `∨ True` carriers (cover / `h_closeF_old` / `h_mt`), 3 frameless-chain, 3 sequence-top — payable from the `[map k]` frame item 492 supplies (no class STARVED per P120); (ii) the two `closeThenBlock` births still `⟨[], …⟩` over `SCompactSeqTail` … Read #316 and fold both into the (d) flip-price on 442's anchor before paying."  Departure, stated: the "post-state clause" is NOT a restatement of `PackAlt` at item 442's anchor (`abbrev PackAlt sc`) — `PackAlt sc` has no `s'` to speak of — but the DOMAIN of the chain premise `h_explUp_chainD` moved from `MarkedColsIn sc ns` to `MarkedColsIn s' ns` at its three holders (`colon_open_map` L24301, `question_open_map` L24612, `indicator_open_map` L25541): the consumers already read the chain on `s'`'s marks (`h_mstep` / `h_mcstep`, items 412 / 417), so the restatement puts the obligation where it is consumed, and a mark the step closes is no longer owed.  `h_mapTail` ((c)) is not in the composite: item 471's spec for it prices a field on `pendingMapValue`'s lane (14 / 6) and is additive by the same argument; it is folded at the pay.
+
+**Predictions first** (ledger `496/notes.md`, before each flip ran).  Spec (a), the domain: Pa1 round 1 ≈ 4 sites in 3 declarations (the holders' internal relays); Pa2 fixpoint 7–12 sites in 3–4 producers, ≤ 20 / ≤ 6; Pa3 no STARVED class — every site is paid by the step premise already in scope (`h_mstep` / `h_mcstep` / `h_mcstep_ne`) or the landing lemma; Pa4 restored, no pin.  Composite (d): Pd1 fixpoint ≤ 110 sites / ≤ 14 declarations (471 alone 78 / 11; 494 13 / 4 one round; (a) ≤ 20 / 6, overlapping in `closeThenBlock` / `pendingBlock*`); Pd2 item 494's 13 sites reappear inside the composite's `closeThenBlock` / `pendingBlockContent` / `pendingBlock` / `noPending` rows; Pd3 no class STARVED — every site is one of {chain hand-off through the step premise, landing lemma, `[map k]` frame from item 492's births, upstream-carrier relay, producer write from the premise}; Pd4 the two `closeThenBlock` `⟨[], …⟩` births do NOT surface (they type-check as they stand); Pd5 source restored, no pin moved.
+
+**The reading, (a)** (`scratch/price496_a.log`): round 1 **9 sites / 4 declarations**, round 2 +2 in `L4YAML/Capstones.lean` (`parse_strict_proof depends on sorryAx` — the flip's sorries propagating; outside scope), fixpoint 11 / 5; restored `identical=true`, rebuilt exit 0.  By site: `colon_open_map` 24417 (`h_mstep ns hdom` — the relay is the identity once the domain is on `s'`); `question_open_map` 24743 / 24780 / 24867 / 24876 (`h_mcstep nsU hdomU` → a cons on `s'`'s domain, `MarkedColsIn.mono`); `accum_block_on_closeThenBlock` 28318 (`hdomU : MarkedColsIn sc (nv :: nsU)` where `s'` is expected — the `k > n` hand-off, paid by the step premise `h_mcstep` / `h_mcstep_ne`); `accum_block_on_pendingBlock` 30330 / 30333 / 30337 (`MarkedColsIn.self sc` / `union_left` on `sc` — the same step premise).  All nine are relays of a fact already in scope: the domain restatement costs nothing new in the `k > n` lanes; its value is at the `k ≤ n` `else`s, where `ns` becomes the SURVIVORS, the closed marks drop by the landing lemma (`∀ m ∈ markedCols s', m ≤ k`), and what remains is the survivors' chain — the ancestors' one-frame line per mark, which is exactly the producers' premise (d) hands in.
+
+**The reading, (d) composite** (`scratch/price496_d.out`; 13 patches / 15 anchors, `--dry` 13 / 13 on `8e06fe35`): round 1 **100 sites / 17 declarations**, round 2 +2 (`Capstones.lean`, as above), `INCOMPLETE` only in that sense; restored `identical=true`, rebuilt exit 0.  By declaration: `accum_content_on_pendingBlock_indented` 27, `accum_content_pending` 15, `entryKeyPack_of_dispatch` 11, `entryPropsKeyPack_of_dispatch` 11, `accum_block_on_pendingBlock` 9, `accum_block_on_pendingBlockContent` 5, `question_open_map` 4, `accum_content_on_pendingMapValue_indented` 3, `flowKeyPack_of_close` 2, `accum_block_on_closeThenBlock` 2, `colon_fires_props_key` 2, `colon_fires_implicit_key` 2, `content_dispatch_routed` 2, `accum_content_on_noPending` 2, `colon_open_map` 1, `accum_block_on_noPending` 1, `content_dispatch_after_close` 1.  By kind: 30 `∨ PackAlt` declines that lose their arm (`Or.inr h_alt` / `.imp … PackAlt.*`), 19 destructurings of the pack's chain field (`⟨…⟩` over `List Nat`), 13 type mismatches at the pack's construction, 11 `Or.inr trivial` declines (the `h_res_land` relays: `pendingBlock` 5, `pendingBlockContent` 5, `noPending` 1), 9 domain relays ((a)'s nine, verbatim), 8 `h_chainUp` hand-offs at `content_dispatch_routed`'s callers, 8 argument mismatches, 2 `Function expected`.  **Additivity:** item 471's 78 = `entryKeyPack` 11 + `entryPropsKeyPack` 11 + `content_dispatch_routed` 2 + its 54 caller hand-offs (`pendingBlock_indented` 27, `content_pending` 15, `pendingMapValue_indented` 3, `content_on_noPending` 2, `flowKeyPack_of_close` 2, `colon_fires_*` 4, `after_close` 1); (a)'s 9 as listed; item 494's 13 = the 11 `Or.inr trivial` + `closeThenBlock`'s `deeperLandingResume` relay + `pendingBlock`'s `Or.inr h_tr` (30255) — 78 + 9 + 13 = 100, and no line is in two classes.  **STARVED?**  None: the 30 + 13 + 19 + 8 of item 471's class are paid by the premise `h_chainUp` the spec itself adds to `content_dispatch_routed` and by the park fields' hand-offs (item 460: the fields are full-domain); the 9 by the step premises; the 13 of item 494's class by the `[map k]` frame item 492's births supply (P120, no class short of a scanner fact) or by the upstream carrier (cover / `h_closeF_old` / `h_mt`) at the 6 relays.  **The two births** (`closeThenBlock`'s `⟨[], …⟩` over `SCompactSeqTail`, the owner's (ii)) are not errors of any flip — `[]` type-checks — so they are owed by name: the enclosing LEVEL (`seq` / the chain), to be supplied by the same premise at the pay.
+
+**Predictions, scored.**
+
+| P | said | result | verdict |
+|---|---|---|---|
+| Pa1 | round 1 ≈ 4 / 3 | 9 / 4 | REFUTED on the count (the holders relay the domain at 5 sites, not 2; the two producers' hand-offs surface in round 1, not 2) — shape held: all relays |
+| Pa2 | fixpoint 7–12 sites in 3–4 producers, ≤ 20 / ≤ 6 | 11 / 5 (9 in StreamAccum + 2 capstone propagation) | HELD |
+| Pa3 | no STARVED | every site a step-premise relay | HELD |
+| Pa4 | restored, no pin | `identical=true` | HELD |
+| Pd1 | ≤ 110 sites / ≤ 14 decls | 100 / 17 (+1 module) | sites HELD, declarations REFUTED — 471's 54 hand-offs sit in 9 callers, more than the 3–4 producers the overlap assumed |
+| Pd2 | 494's sites reappear in CTB / PBC / PB / noPending | 5 + 5 + 1 + CTB 1 + PB `h_tr` 1 = 13 | HELD |
+| Pd3 | no STARVED | none (reading above) | HELD |
+| Pd4 | the two `⟨[], …⟩` births do not surface | CTB has exactly 2 sites, neither a birth | HELD |
+| Pd5 | restored, no pin | `identical=true`; no pin touched | HELD |
+
+**What it teaches.**  §9: the composite is three readings taken at once, and it agrees with the three taken apart (78, 9, 13) to the site — the overlap Pd1 assumed between the classes was not there because each class is a different FACT (the pack, its domain, the resume) at a different position of the same producers.  The instrument note: `scripts-flip` writes its build log to the spec's `log` path; redirecting stdout to the same file loses round 1's site list (the first composite run did; `scratch/price496_d.out` is the re-run).
+
+**Gates.**  No build (docs + two flip specs; the specs restore the source).  `check-closure-log` 11..496 ascending, dates non-decreasing, 5 gaps (18, 442, 492, 494, 495; 491 (#311) and 493 (#312) landed under this item and were dropped at the rebase); `check-gate-vocab`; `check-scripts-lean` (specs are JSON, no Python).  Adversarial exe unchanged from the base (62181 / 62181 without #312 / #315's rows).  No pin moved; no declaration touched.
+
+**NEXT —** (ω-pay-births) (d) the PAY, in this order, each a build-changing item off the merged base (rebased over #313 / #316 as they land; #313 shifts the openers by +18 lines, no anchor text touched): (1) the two landing lemmas in `RegisterWitness` / `StreamAccum` (`∀ m ∈ markedCols s', m ≤ k` at the `-` landing, P97(v); at the `:`/`?` opener, P95(ii)) and the domain restatement (a) — 9 sites, all step-premise relays, the seven `k ≤ n` `else`s rewritten to the survivors' chain where the ancestors' lines come from the park fields' hand-offs (STOP-price if a survivor's line is not in scope: that is the (d)-proper premise and it moves to (2)); (2) item 471's premise `h_chainUp` at `content_dispatch_routed` + the 11 producer writes + 54 hand-offs + 13 destructurings, with `h_mapTail` as the dedent-sibling clause; (3) item 494's 13 with the `[map k]` frame and the two `⟨[], …⟩` births from the enclosing level.  Rule 2 before (1): P99 — at every ON position, `markedCols s' ⊆ {m | m ≤ k}` and, for each survivor `nv < k` at an own / dedent landing, the ancestor's `: v` after the landing's whole entry parses (P95(iii)'s 41 / 41 generalized to the `-` landings).
diff --git a/Scripts/Docs/ClosureLog.lean b/Scripts/Docs/ClosureLog.lean
@@ -38,9 +38,10 @@ def declaredGaps : List (Nat × String) :=
    -- 442: the slot two concurrent lanes both took on 2026-11-06 — Row 19's entry became 443 and
    -- Row 12's (the (ω-negative) item) became 444; nothing was written as 442.
    (442, "item-445-2026-11-06"),
-   -- 491 = S3's slice (4) PR 6 (#311), 492 = Row 19's births PR: both assigned and in flight
-   -- when Row 12's item 493 was cut off the #310 base; dropped as they land.
-   (492, "item-493-2026-11-14")]
+   -- 492 = Row 19's #313, 494 = Row 19's #316, 495 = Row 12's #315: all in flight when item 496
+   -- was cut off the #310 base (491 = S3's #311 and 493 = Row 12's #312 landed first and were
+   -- dropped at the rebase); dropped as they land.
+   (492, "item-496-2026-11-14"), (494, "item-496-2026-11-14"), (495, "item-496-2026-11-14")]
 
 /-- One `### Item N[a] (DATE)` heading. -/
 structure Entry where