proof(flow): item 497 — the strict-lead carry: FlowArm.openNest's ε lead carries trailingPropertyRun = [], accum_step_flow_trace's held-run nested-open disjunct folds into the first

DOCS.md

@@ -52929,6 +52929,22 @@ P1 — P118's hypotheses hold at all 525 in-flow content steps (P115's count).
 
 **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).
 
+### Item 497 (2026-11-14)
+
+**S3 slice (3) (a), the strict-lead carry — PAID: `FlowArm.openNest.h_lead`'s ε disjunct and `accum_step_flow`'s `h_tuple` open-lead conjunct carry `trailingPropertyRun sc.tokens = []`, so `accum_step_flow_trace`'s fourth disjunct (the held-run nested open `[&a [b]]`) is deleted and folds into the first: under a held run (`GapRead.props`' `h_held : ≠ []`) the lead is the strict separation `openNestSeqProps` / `openNestMapProps` ask, and the trace is `ev ++ ev_p`.  5 lines changed in `StreamAccum.lean` (one producer arm, the white one; the props arm already produced `Or.inl`), 18 in `TraceOf/FlowWalk.lean`.**  Taken by Row 19 at the coordinator's hand-off; flow-side, none of R12's producers.
+
+**The mandate** (item 474's NEXT, verbatim): "**NEXT —** S3 slice (3): (a) the fold — the ~10-line `StreamAccum` strict-lead carry above, to be scheduled with Row 19 (or taken by it): `FlowArm.openNest.h_lead`'s ε disjunct ∧ `trailingPropertyRun sc.tokens = []`, the `h_tuple` conjunct likewise, two producer sites; then `accum_step_flow_trace`'s fourth disjunct is deleted — its strict-lead hypothesis (review round 1) is discharged from the arm and the stack conclusion folds into the first disjunct; the `openNestSeqProps`/`openNestMapProps` call sites are already in place — Rule 2 rows already in P109 (iii)."  Taken as written; (b) IOU 1 and (c) stay S3's.
+
+**Predictions** (before the edit).  P1 the carry is ≤ 10 `StreamAccum` lines and touches no R12 producer.  P2 the two `openNest` producer sites (`accum_step_flow`'s `[` / `{` arms) build unchanged — the conjunct rides `h_lead_open` from `h_tuple`.  P3 only the white arm of `h_tuple` needs a new term (`trailingPropertyRun_eq_nil_of_sync h_sync`); the props arm already returns `Or.inl`.  P4 Rule 2 is P109 (iii) as it stands: the run is never glued to the bracket (glued 0).  P5 `accum_step_flow_trace` has no other consumer, so no caller moves; `GhostIndexCensus`' disjunct list moves on the one `openNest` row, the count stays 123.
+
+**The reading.**  The library build took one round (one elaboration fix in `FlowWalk`, an `And.intro` where `⟨…⟩` had no expected type); `accum_step_flow_trace`'s conclusion is now three disjuncts, the depth-0 open's `Or.inr (Or.inr …)` one level shallower.  P109 (iii) re-read on this tree: glued 0, spanning a line break 1 (adversarial 62181 / 62181).
+
+**Predictions, scored.**  P1 HELD (5 lines).  P2 HELD.  P3 HELD.  P4 HELD.  P5 HELD — `GhostIndexCensus` 123 → 123, one row's text.
+
+**Gates.**  Full `lake build` exit 0 (1564 jobs, 172 warnings) over two rounds; **pins moved**: `GhostIndexCensus` disjunct list — `FlowArm.openNest[14].h_lead`'s ε row gains `∧ trailingPropertyRun sc.tokens = []` (count 123 unchanged); `ValueLineOrigins` liteNodes 673507 → 674092 (term size of `accum_step_flow`'s white arm; no row moves).  `check-theorem-keyword` / `check-import-closure` / `check-reflection-index` / `check-closure-log` (11..498; 492 and 494 declared — #313, #316) / `check-serialization-proofs` / `check-gate-vocab` / `check-pack-births` / `check-scripts-lean` green; `check-hygiene` 11565 theorems / 0 sorries / 0 custom axioms; `run-all-tests` exit 0; suiterunner 869 / 0 / 151; eventscore 347 / 358; adversarial 62181 / 62181.  Axioms: `accum_step_flow` and `accum_step_flow_trace` the standard three, `FlowArm.openNest` `propext`.
+
+**NEXT —** S3's item 474 (b) and (c) stand (IOU 1, the depth-0 landing `sp_flow' = sp_open`; then slice (3) PR 2b-iii); Row 19 step (3) waits on R12's (d) (item 494's table).
+
 ### Item 498 (2026-11-14)
 
 **(ω-pay-births) (d) item (1) PAID — the landing lemma `markedCols_le_of_top` LANDED, `h_explUp_chainD`'s chain domain moved to the post-state `s'` at the three openers (9 relays paid), two of the seven `k ≤ n` `else`s paid at their no-survivor arms, six dead mark-step premises deleted; Rule 2 (P99) HELD.**  Items 492–497 were open PRs when this item was cut (491 = S3's #311, 493 = #312, 495 = #315 and 496 = #317 landed first and were dropped at the rebases; Row 19's #313 / #316 / #318, Row 12's #312 / #315 / #317) and are declared as gaps in `Scripts/Docs/ClosureLog.lean` until they land.

L4YAML/Proofs/Production/StreamAccum.lean

@@ -7127,7 +7127,8 @@ inductive FlowArm (sc s' : ScannerState) (c : Char) (sp_block sp_flow sp_scan :
       (gap : GapRead sc sp_flow sp_scan sp_flow₂)
       (h_depth : 1 ≤ sc.flowLevel) (h_c : c = if b then '[' else '{')
       (h_tail : ∀ kj, tailOf sc.tokens ≠ .value kj)
-      (h_lead : ∀ m, (SSeparateLines m sp_flow₂ sp_br ∨ (sp_br = sp_flow₂ ∧ (gapTail sc).leadFree = true)) ∨
+      (h_lead : ∀ m, (SSeparateLines m sp_flow₂ sp_br ∨
+          (sp_br = sp_flow₂ ∧ (gapTail sc).leadFree = true ∧ trailingPropertyRun sc.tokens = [])) ∨
         ¬ (m ≤ minContentIndentOf sc))
       (h_open : GLit c sp_br sp_open)
       (h_fl : s'.flowLevel = sc.flowLevel + 1) (h_ks : s'.flowStack = sc.flowStack.push b)
@@ -20051,7 +20052,8 @@ lemma accum_step_flow (sc : ScannerState)
           (∀ m, (SSeparateLines m sp_flow₂ sp_prep ∨ (sp_prep = sp_flow₂ ∧ tl₂.closeFree)) ∨
             ¬ (m ≤ minContentIndentOf sc)) ∧
           ((c = '[' ∨ c = '{') → ∀ m,
-            (SSeparateLines m sp_flow₂ sp_prep ∨ (sp_prep = sp_flow₂ ∧ tl₂.leadFree)) ∨
+            (SSeparateLines m sp_flow₂ sp_prep ∨
+              (sp_prep = sp_flow₂ ∧ tl₂.leadFree ∧ trailingPropertyRun sc.tokens = [])) ∨
             ¬ (m ≤ minContentIndentOf sc))) := by
       cases h_gap with
       | white h_ws h_sync h_colon_sc _ h_gate_w h_free_w =>
@@ -20079,13 +20081,16 @@ lemma accum_step_flow (sc : ScannerState)
               ¬ (m ≤ minContentIndentOf sc) :=
             fun m => (h_lead_at m).imp (fun h => h.imp id (fun h => ⟨h.1.trans h.2.symm, (h_fr h).1⟩)) id
           have h_lead_of_m : (c = '[' ∨ c = '{') → ∀ m,
-              (SSeparateLines m sp_flow sp_prep ∨ (sp_prep = sp_flow ∧ tl.leadFree)) ∨
+              (SSeparateLines m sp_flow sp_prep ∨
+                (sp_prep = sp_flow ∧ tl.leadFree ∧ trailingPropertyRun sc.tokens = [])) ∨
               ¬ (m ≤ minContentIndentOf sc) :=
             fun hc m => (h_lead_at m).imp (fun h => h.imp id (fun h => ⟨h.1.trans h.2.symm,
-              (h_fr h).2 (by rcases hc with rfl | rfl <;> decide)⟩)) id
+              (h_fr h).2 (by rcases hc with rfl | rfl <;> decide),
+              trailingPropertyRun_eq_nil_of_sync h_sync⟩)) id
           have h_lead_of : (c = '[' ∨ c = '{') →
               SSeparateLines nn sp_flow sp_prep ∨ (sp_prep = sp_flow ∧ tl.leadFree) :=
-            fun hc => (h_lead_of_m hc nn).resolve_right (fun hn => hn h_floorK)
+            fun hc => ((h_lead_of_m hc nn).resolve_right (fun hn => hn h_floorK)).imp id
+              (fun h => ⟨h.1, h.2.1⟩)
           have h_nil : trailingPropertyRun sc.tokens = [] := trailingPropertyRun_eq_nil_of_sync h_sync
           exact ⟨tl, sp_flow, h_fos, h_lead,
             (fun hc h_tail kj sp_ne h_c hj =>

L4YAML/Proofs/Serialization/TraceOf/FlowWalk.lean

@@ -1502,15 +1502,11 @@ lemma gapRead_onT {n d : Nat} {ks : Array Bool} {sc : L4YAML.Scanner.ScannerStat
     `accum_step_flow` reports.  Conclusion: the T stack at the post-state's indices with the trace
     grown by the gap's run (`ev ++ ev_g`), or the base close's hand-off (`[158]` content with that
     trace, the stack `nil`), or the depth-0 open's fresh frame (trace `[]`; its landing position is
-    `accum_flow_open_depth0`'s existential `sp_flow'`, so it is stated at the T side's `sp_open`), or
-    the one arm §7 has no twin for yet — a nested open AFTER a held run (`[&a [b]]`: the run wraps
-    the child, `inject`'s `propsContent`, not an empty node), returned with the run's T twin
-    (`TCNsProperties`, via `PropsRun.toT`), the bracket's `GLit`, and the pushed T stack through
-    `openNestSeqProps`/`openNestMapProps` UNDER the run's strict separation from the bracket — the
-    fact `accum_step_flow`'s proof holds (`h_sep0`) and `FlowArm.openNest.h_lead` does not state
-    (its ε disjunct reads `(gapTail sc).leadFree`, true after a run); carrying it is the
-    `StreamAccum` price item 474 records, after which this disjunct folds into the first.  `FlowArm` is a `Prop`, so that arm cannot be excluded by a premise on `arm` (§7: which
-    constructor fired is unobservable) — it is a disjunct of the conclusion instead.  The arm's
+    `accum_flow_open_depth0`'s existential `sp_flow'`, so it is stated at the T side's `sp_open`).
+    A nested open AFTER a held run (`[&a [b]]`: the run wraps the child, `inject`'s `propsContent`)
+    is in the first disjunct, `ev_g` the run's events: `FlowArm.openNest.h_lead`'s ε disjunct
+    carries `trailingPropertyRun sc.tokens = []` (item 497), so under the held run (`≠ []`) the
+    lead is the strict separation `openNestSeqProps`/`openNestMapProps` ask.  The arm's
     obligations are read at every floor; `hn` is the stack's floor (`FlowStackK`'s `n ≤ minContentIndentOf`). -/
 lemma accum_step_flow_trace {n : Nat} {sc s' : L4YAML.Scanner.ScannerState} {c : Char}
     {sp_block sp_flow sp_scan sp_block' sp_flow' : SurfPos} {ev : List Event}
@@ -1523,21 +1519,15 @@ lemma accum_step_flow_trace {n : Nat} {sc s' : L4YAML.Scanner.ScannerState} {c :
         ∃ sp_br sp_tok, TFlowContent n .flowOut sp_br sp_tok (ev ++ ev_g) ∧
           TFlowStackB n 0 #[] (tailOf s'.tokens) sp_block' sp_flow' []) ∨
       (sc.flowLevel = 0 ∧ ev = [] ∧ ev_g = [] ∧
-        ∃ sp_open, TFlowStackB n s'.flowLevel s'.flowStack (tailOf s'.tokens) sp_block' sp_open []) ∨
-      (1 ≤ sc.flowLevel ∧ (c = '[' ∨ c = '{') ∧ ev_g = [] ∧
-        ∃ sp_p ev_p, TCNsProperties n .flowIn sp_p sp_scan ev_p ∧
-          ∃ sp_br, GLit c sp_br sp_flow' ∧
-            (SSeparate n .flowIn sp_scan sp_br →
-              TFlowStackB n s'.flowLevel s'.flowStack (tailOf s'.tokens) sp_block' sp_flow'
-                (ev ++ ev_p))) := by
+        ∃ sp_open, TFlowStackB n s'.flowLevel s'.flowStack (tailOf s'.tokens) sp_block' sp_open []) := by
   generalize hks : sc.flowStack = ks at hT
   cases arm with
   | openBase b sp_br sp_open sp_block'' sp_flow'' h_depth h_c h_open h_fl h_ks h_tl =>
     rw [h_depth] at hT
     cases hT with
     | «open» _ _ _ _ _ _ h => cases h
     | nil =>
-      refine ⟨[], Or.inr (Or.inr (Or.inl ⟨h_depth, rfl, rfl, sp_open, ?_⟩))⟩
+      refine ⟨[], Or.inr (Or.inr ⟨h_depth, rfl, rfl, sp_open, ?_⟩)⟩
       rw [h_fl, h_ks, h_tl]
       cases b
       · have h_open' : GLit '{' sp_br sp_open := by subst h_c; simpa using h_open
@@ -1550,11 +1540,12 @@ lemma accum_step_flow_trace {n : Nat} {sc s' : L4YAML.Scanner.ScannerState} {c :
     cases hT with
     | «open» _ _ _ _ _ _ hTO =>
     cases gap with
-    | props ha ht sp_p h_tail₀ h_lead₀ h_run _ _ =>
+    | props ha ht sp_p h_tail₀ h_lead₀ h_run _ h_held =>
       obtain ⟨ev_p, hp⟩ := PropsRun.toT ((h_run n).resolve_right (fun h => h hn))
       have h_lead₀' := (h_lead₀ n).resolve_right (fun h => h hn)
-      refine ⟨[], Or.inr (Or.inr (Or.inr ⟨h_depth, by subst h_c; cases b <;> simp, rfl, sp_p, ev_p, hp,
-        sp_br, h_open, fun h_psep => ?_⟩))⟩
+      have h_psep : SSeparate n .flowIn sp_scan sp_br :=
+        ((h_lead n).resolve_right (fun h => h hn)).resolve_right (fun h => h_held h.2.2)
+      refine ⟨ev_p, Or.inl ?_⟩
       rw [h_fl, h_ks, h_tl, hd, hks]
       cases b
       · have h_open' : GLit '{' sp_br sp_flow' := by subst h_c; simpa using h_open
@@ -1566,6 +1557,7 @@ lemma accum_step_flow_trace {n : Nat} {sc s' : L4YAML.Scanner.ScannerState} {c :
     | white _ h_nil =>
       have h_lead' := (h_lead n).resolve_right (fun h => h hn)
       rw [gapTail_of_nil h_nil] at h_lead'
+      replace h_lead' := h_lead'.imp id (fun h => And.intro h.1 h.2.1)
       refine ⟨[], Or.inl ?_⟩
       rw [h_fl, h_ks, h_tl, hd, hks]
       cases b

Scripts/Docs/ClosureLog.lean

@@ -40,7 +40,7 @@ def declaredGaps : List (Nat × String) :=
    -- 492 = Row 19's #313, 494 = Row 19's #316, 497 = Row 19's #318: in flight when item 498 was cut
    -- (491 = S3's #311, 493 = #312, 495 = #315 and 496 = #317 landed first and were dropped at the
    -- rebases); dropped as they land.
-   (492, "item-498-2026-11-14"), (494, "item-498-2026-11-14"), (497, "item-498-2026-11-14")]
+   (492, "item-498-2026-11-14"), (494, "item-498-2026-11-14")]
 
 /-- One `### Item N[a] (DATE)` heading. -/
 structure Entry where

Tests/Guards/Proofs/GateVocabulary.lean

@@ -121,8 +121,10 @@ namespace L4YAML.Tests.Guards.GateVocabulary
 -- flow-value indent check the scanner refuses an under-indented continuation with, and the preprocess / block-indicator
 -- dispatch steps it re-derives the arm from (not spelled here: it would move `self`).
 -- 2026-11-14 (item 491): mentions 519 → 520 — P119's docstring and item 491 name the key/value dispatcher and its checks.
+-- 2026-11-14 (item 492's rebase): mentions 520 → 521 — item 493's Priority 97 rows (merged without the
+-- re-pin) name the preprocess step's scanner lemma once more; the base read 521 against this pin.
 def expectedGateVocab : String :=
-  "names=115 mentions=520 families=14 refuted=7 wrapped=4 self=2 unresolved=0"
+  "names=115 mentions=521 families=14 refuted=7 wrapped=4 self=2 unresolved=0"
 
 end L4YAML.Tests.Guards.GateVocabulary
 

Tests/Guards/Proofs/GhostIndexCensus.lean

@@ -463,7 +463,8 @@ def expectedDisjuncts : List String :=
    "ContentArm.blockScalar[5].h_c ∨ c = '>'",
    "ContentArm.blockScalar[6].h_bs ∨ SCLFolded 0 sp sp'",
    "FlowArm.openNest[14].h_lead ∨ ¬m ≤ PreprocessIndentStable.minContentIndentOf sc",
-   "FlowArm.openNest[14].h_lead ∨ sp_br = sp_flow₂ ∧ (gapTail sc).leadFree = true",
+   -- 2026-11-14 (item 497): the ε lead also carries `trailingPropertyRun sc.tokens = []` (the strict-lead carry).
+   "FlowArm.openNest[14].h_lead ∨ sp_br = sp_flow₂ ∧ (gapTail sc).leadFree = true ∧ trailingPropertyRun sc.tokens = []",
    "FlowArm.comma[13].h_lead ∨ ¬m ≤ PreprocessIndentStable.minContentIndentOf sc",
    "FlowArm.comma[13].h_lead ∨ sp_prep = sp_flow₂ ∧ (gapTail sc).closeFree = true",
    "FlowArm.closeNested[14].h_lead ∨ ¬m ≤ PreprocessIndentStable.minContentIndentOf sc",

Tests/Guards/Proofs/ValueLineOrigins.lean

@@ -1213,6 +1213,7 @@ def expectedUnborn : List String := []
 -- 2026-11-09 (item 469): lets 716 → 718, lapps 895 → 900, alts 5652 → 5478, nodes 14418 → 14437, liteNodes 681093 → 664267 —
 -- the flow pack sites build arm-first through `FlowStackKA.ofPack`/`ofK`; the body is now the one `FlowStackKBody` abbrev, so the
 -- walk reads fewer alternatives and lite nodes while the (sharing-insensitive) node count grows by the wrappers.
+-- 2026-11-14 (item 497's rebase onto item 498): term sizes only — the strict-lead conjunct on item 498's tree.
 def expectedLine : String :=
   -- 2026-10-25 (item 359): punt 12 → 11, stamp 39 → 40 — the `noPending` value-park face pays `PackAlt.ofRefused (h_noek …)`;
   -- lapps 806 → 807, liteNodes 607398 → 607407 — that one application and its term.
@@ -1233,7 +1234,7 @@ def expectedLine : String :=
   -- relays across the `≤` park faces and `closeThenBlock`'s `ResumeFrames.strict` read; no origin row moved.
 -- 2026-11-10 (item 473, option (A)): term-size tallies only (lapps 908 → 905, alts 5575 → 5576, liteNodes 673520 → 673507):
 -- the `≤` faces drop `Nat.le_of_lt` wrappers and the positional `ResumeWidths` reshapes `resumeAt`; positions/rows unchanged.
-  "positions=52 packaged=7 packConsts=[ImplicitKeyPack,PropsKeyPack] rows=197 ctorRows=104 paramRows=93 packagedRows=29 punt=4 stamp=42 built=151 origins=67 originRows=32 route=12 frames=29 tail=14 other=0 concl=8 invariant=4 heldOrigins=14 allHeld=2 someHeld=37 noneHeld=98 unbornRows=0 relayedPunt=0 relayedStamp=10 relayedAbsurd=4 relayedFact=0 deadRows=0 unbornPos=0 rounds=4 follows=410 lets=740 lapps=910 alts=5596 nodes=14489 liteNodes=677574"
+  "positions=52 packaged=7 packConsts=[ImplicitKeyPack,PropsKeyPack] rows=197 ctorRows=104 paramRows=93 packagedRows=29 punt=4 stamp=42 built=151 origins=67 originRows=32 route=12 frames=29 tail=14 other=0 concl=8 invariant=4 heldOrigins=14 allHeld=2 someHeld=37 noneHeld=98 unbornRows=0 relayedPunt=0 relayedStamp=10 relayedAbsurd=4 relayedFact=0 deadRows=0 unbornPos=0 rounds=4 follows=410 lets=740 lapps=910 alts=5596 nodes=14489 liteNodes=678159"
 
 /-! ## §4 The reading -/