From eec5f907f72a307af5d5d873e60146ef968671ed Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 14 Nov 2026 20:31:13 +0000 Subject: [PATCH] =?UTF-8?q?docs(row=2012):=20item=20496=20=E2=80=94=20(?= =?UTF-8?q?=CF=89-pay-births)=20(d)=20PRICED=20as=20one=20composite=20spec?= =?UTF-8?q?=20(scripts/flips/item496=5Fd=5Fcomposite.json:=20item=20471's?= =?UTF-8?q?=20premise=20+=20the=20chain=20domain=20on=20the=20post-state?= =?UTF-8?q?=20+=20Row=2019's=20item=20494=20h=5Fres=5Fland=20clause):=2010?= =?UTF-8?q?0=20sites=20/=2017=20declarations=20at=20the=20StreamAccum=20fi?= =?UTF-8?q?xpoint,=20additive=2078=20+=209=20+=2013,=20no=20class=20STARVE?= =?UTF-8?q?D;=20the=20two=20closeThenBlock=20=E2=9F=A8[],=20=E2=80=A6?= =?UTF-8?q?=E2=9F=A9=20births=20named=20by=20hand;=20source=20restored;=20?= =?UTF-8?q?no=20library=20change;=20gaps=20491=E2=80=93495=20declared?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Nicolas Rouquette --- DOCS.md | 33 +++- Scripts/Docs/ClosureLog.lean | 7 +- scripts/flips/item496_d_composite.json | 167 +++++++++++++++++++ scripts/flips/item496_post_state_domain.json | 50 ++++++ 4 files changed, 253 insertions(+), 4 deletions(-) create mode 100644 scripts/flips/item496_d_composite.json create mode 100644 scripts/flips/item496_post_state_domain.json diff --git a/DOCS.md b/DOCS.md index 877fd7a76..1b5955d10 100644 --- 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 index 4f5e57bb8..1a9b470dc 100644 --- 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 diff --git a/scripts/flips/item496_d_composite.json b/scripts/flips/item496_d_composite.json new file mode 100644 index 000000000..f382f6079 --- /dev/null +++ b/scripts/flips/item496_d_composite.json @@ -0,0 +1,167 @@ +{ + "item": 496, + "tag": "PRICE-496-D-COMPOSITE", + "rev": "8e06fe35", + "target": "L4YAML", + "msgWidth": 110, + "rounds": 6, + "report": "bodies", + "log": "scratch/price496_d.log", + "files": [ + { + "file": "L4YAML/Proofs/Production/StreamAccum.lean", + "patches": [ + { + "name": "L1226.ImplicitKeyPack.chain", + "line": 1167, + "old": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_w) ∨ PackAlt sc) ∧" + ], + "new": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_w)) ∧" + ], + "count": 1 + }, + { + "name": "L1906.PropsKeyPack.chain", + "line": 1817, + "old": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_w) ∨ PackAlt sc) ∧" + ], + "new": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_w)) ∧" + ], + "count": 1 + }, + { + "name": "L34640.entryKeyPack.h_nodeV", + "line": 34277, + "old": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v) ∨ PackAlt sc)" + ], + "new": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v))" + ], + "count": 1 + }, + { + "name": "L34660.h_cp_chain", + "line": 34297, + "old": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v) ∨ PackAlt sc)) ∨ True)" + ], + "new": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v))) ∨ True)" + ], + "count": 1 + }, + { + "name": "L34681.h_cp_chain", + "line": 34318, + "old": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v) ∨ PackAlt sc)))" + ], + "new": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v))))" + ], + "count": 1 + }, + { + "name": "L35351.entryPropsKeyPack.h_nodeV", + "line": 34988, + "old": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v) ∨ PackAlt sc)" + ], + "new": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v))" + ], + "count": 1 + }, + { + "name": "L35364.h_cp_chain", + "line": 35001, + "old": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v) ∨ PackAlt sc)) ∨ True)" + ], + "new": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v))) ∨ True)" + ], + "count": 1 + }, + { + "name": "L35452.h_cp_chain", + "line": 35089, + "old": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v) ∨ PackAlt sc)))" + ], + "new": [ + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_v))))" + ], + "count": 1 + }, + { + "name": "L35937.content_dispatch_routed.h_chainUp", + "line": 35574, + "old": [ + " (h_alt : PackAlt s_prep)" + ], + "new": [ + " (h_alt : PackAlt s_prep)", + " (h_chainUp : ∃ ns : List Nat, RegisterWitness.MarkedColsIn s_prep ns ∧ ∀ nv ∈ ns,", + " ∀ sp_i sp_c : SurfPos, SIndent nv sp_prep sp_i → GLit ':' sp_i sp_c →", + " ∀ sp_w : SurfPos, SBlockIndented nv .blockOut sp_c sp_w →", + " ResumeFrames (SLYamlStream sp_start) [FrameLevel.map nv] sp_w)" + ], + "count": 1 + }, + { + "name": "L24301.colon_open_map.h_explUp_chainD", + "line": 24301, + "old": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn sc ns ∧ ∀ nv ∈ ns," + ], + "new": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn s' ns ∧ ∀ nv ∈ ns," + ], + "count": 1 + }, + { + "name": "L24612.question_open_map.h_explUp_chainD", + "line": 24612, + "old": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn sc ns ∧ ∀ nv ∈ ns," + ], + "new": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn s' ns ∧ ∀ nv ∈ ns," + ], + "count": 1 + }, + { + "name": "L25541.indicator_open_map.h_explUp_chainD", + "line": 25541, + "old": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn sc ns ∧ ∀ nv ∈ ns," + ], + "new": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn s' ns ∧ ∀ nv ∈ ns," + ], + "count": 1 + }, + { + "name": "RES_LAND_NO_DECLINE", + "old": [ + " (h_res_land : (∃ ks : List FrameLevel, (∀ fr ∈ ks, fr.width ≤ k) ∧", + " ∀ sp_end : SurfPos, SCompactMapTail k sp_land sp_end →", + " ResumeFrames (SLYamlStream sp_start) ks sp_end) ∨ True)" + ], + "new": [ + " (h_res_land : (∃ ks : List FrameLevel, (∀ fr ∈ ks, fr.width ≤ k) ∧", + " ∀ sp_end : SurfPos, SCompactMapTail k sp_land sp_end →", + " ResumeFrames (SLYamlStream sp_start) ks sp_end) ∨ False)" + ], + "count": 3 + } + ] + } + ] +} \ No newline at end of file diff --git a/scripts/flips/item496_post_state_domain.json b/scripts/flips/item496_post_state_domain.json new file mode 100644 index 000000000..ea57aa941 --- /dev/null +++ b/scripts/flips/item496_post_state_domain.json @@ -0,0 +1,50 @@ +{ + "item": 496, + "tag": "PRICE-496-POST-STATE-DOMAIN", + "rev": "8e06fe35", + "target": "L4YAML", + "msgWidth": 110, + "rounds": 6, + "report": "bodies", + "log": "scratch/price496_a.log", + "files": [ + { + "file": "L4YAML/Proofs/Production/StreamAccum.lean", + "patches": [ + { + "name": "L24301.colon_open_map.h_explUp_chainD", + "line": 24301, + "old": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn sc ns ∧ ∀ nv ∈ ns," + ], + "new": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn s' ns ∧ ∀ nv ∈ ns," + ], + "count": 1 + }, + { + "name": "L24612.question_open_map.h_explUp_chainD", + "line": 24612, + "old": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn sc ns ∧ ∀ nv ∈ ns," + ], + "new": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn s' ns ∧ ∀ nv ∈ ns," + ], + "count": 1 + }, + { + "name": "L25541.indicator_open_map.h_explUp_chainD", + "line": 25541, + "old": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn sc ns ∧ ∀ nv ∈ ns," + ], + "new": [ + " (h_explUp_chainD : (∃ ns : List Nat, RegisterWitness.MarkedColsIn s' ns ∧ ∀ nv ∈ ns," + ], + "count": 1 + } + ] + } + ] +} \ No newline at end of file