SETH ⇒ OVC sparsification bundle 34: concrete word-RAM formalization

import Definitions.Def_WordRAMEquivalence_Foundation1
import Definitions.Def_WordRAM_Conjectures
import Definitions.Def_WordRAM_SETHOV_Reduction
import Definitions.Def_SETHOV_Sparsification_33

set_option autoImplicit true

/-! Construct both normalized child tables without losing the first result. -/
namespace WordRAM.Conjectures.Sparsification.BothChildren

def algorithm : Algorithm :=
  ⟨SourceChain.code (ChildAssembly.algorithm ChildAssembly.left).code
    (ChildAssembly.algorithm ChildAssembly.right).code, 1, by decide⟩

def cost (remaining petals : Nat) : Nat :=
  (remaining + 1) * (35 * (remaining + 1) + 55) +
    (remaining + petals) * (35 * (remaining + petals) + 55) + 80

/-- Source tables all precede the left raw buffer. The right raw buffer starts
after the entire left normalization workspace, preserving the left result. -/
structure Layout (w : Width) (a b remaining petals core leftRaw leftWork rightRaw rightWork : Nat) : Prop where
  remainingBase : 64 ≤ remaining
  petalsBase : 64 ≤ petals
  coreBase : 64 ≤ core
  remainingEnd : remaining + 3 * a ≤ leftRaw
  petalsEnd : petals + 3 * b ≤ leftRaw
  coreEnd : core + 3 ≤ leftRaw
  leftSpace : leftRaw + 3 * (a + 1) ≤ leftWork
  middle : leftWork + (a + 1) * (3 * (a + 2)) ≤ rightRaw
  rightSpace : rightRaw + 3 * (a + b) ≤ rightWork
  fits : rightWork + (a + b) * (3 * (a + b + 1)) < 2 ^ w.bits

/-- Both descriptors survive in cells 43/44 and 45/46. The metadata cells
34–42 describe source tables and the two disjoint construction workspaces;
48 contains the singleton-core table's count, one. -/
theorem builds (remaining petals : CNF n) (core : Clause n) (s : State w)
    (remainingAddress petalAddress coreAddress leftRaw leftWork rightRaw rightWork : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits)
    (layout : Layout w remaining.length petals.length remainingAddress petalAddress coreAddress leftRaw leftWork rightRaw rightWork)
    (rptr : s.mem 34 = BitVec.ofNat w.bits remainingAddress)
    (pptr : s.mem 35 = BitVec.ofNat w.bits petalAddress)
    (rcount : s.mem 36 = BitVec.ofNat w.bits remaining.length)
    (pcount : s.mem 37 = BitVec.ofNat w.bits petals.length)
    (cptr : s.mem 38 = BitVec.ofNat w.bits coreAddress)
    (lrptr : s.mem 39 = BitVec.ofNat w.bits leftRaw)
    (lwptr : s.mem 40 = BitVec.ofNat w.bits leftWork)
    (rrptr : s.mem 41 = BitVec.ofNat w.bits rightRaw)
    (rwptr : s.mem 42 = BitVec.ofNat w.bits rightWork)
    (one : s.mem 48 = 1#w.bits)
    (remainingInput : VectorBuilder.Stored s.mem remainingAddress (RecordTable.words w remaining))
    (petalInput : VectorBuilder.Stored s.mem petalAddress (RecordTable.words w petals))
    (coreInput : VectorBuilder.Stored s.mem coreAddress (RecordTable.words w [core])) :
    ∃ time final leftAddress rightAddress,
      time ≤ cost remaining.length petals.length ∧ Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem leftAddress (RecordTable.words w (Normalize.normalize (remaining ++ [core]))) ∧
      VectorBuilder.Stored final.mem rightAddress (RecordTable.words w (Normalize.normalize (remaining ++ petals))) ∧
      final.mem 43 = BitVec.ofNat w.bits leftAddress ∧
      final.mem 44 = BitVec.ofNat w.bits (Normalize.normalize (remaining ++ [core])).length ∧
      final.mem 45 = BitVec.ofNat w.bits rightAddress ∧
      final.mem 46 = BitVec.ofNat w.bits (Normalize.normalize (remaining ++ petals)).length ∧
      leftRaw ≤ leftAddress ∧ leftAddress + 3 * (Normalize.normalize (remaining ++ [core])).length ≤ rightRaw ∧
      rightRaw ≤ rightAddress ∧ rightAddress + 3 * (Normalize.normalize (remaining ++ petals)).length ≤
        rightWork + (remaining.length + petals.length) * (3 * (remaining.length + petals.length + 1)) ∧
      (∀ a, 32 ≤ a → a ≠ 43 → a ≠ 44 → a ≠ 45 → a ≠ 46 →
        (a < leftRaw ∨ rightWork + (remaining.length + petals.length) * (3 * (remaining.length + petals.length + 1)) ≤ a) →
        final.mem a = s.mem a) := by
  have rb := layout.remainingBase
  have pb := layout.petalsBase
  have cb := layout.coreBase
  have re := layout.remainingEnd
  have pe := layout.petalsEnd
  have ce := layout.coreEnd
  have ls := layout.leftSpace
  have mid := layout.middle
  have rs := layout.rightSpace
  have fits := layout.fits
  have leftEnd : leftWork + (remaining.length + 1) * (3 * (remaining.length + 1 + 1)) ≤ rightRaw := by
    simpa only [Nat.add_assoc] using mid
  obtain ⟨lt, leftState, la, lb, ltrace, lh, ltable, lp, lc, lower, upper, lf⟩ :=
    ChildAssembly.assembles ChildAssembly.left ChildAssembly.left_valid remaining [core] s
      remainingAddress coreAddress leftRaw leftWork pc live rb cb re (by simpa using ce)
      (by simpa using ls) (by simp only [List.length_cons, List.length_nil, Nat.zero_add]; omega)
      variablesFit rptr cptr lrptr rcount one lwptr remainingInput coreInput
  simp only [List.length_cons, List.length_nil, Nat.zero_add] at lb lower upper lf
  have saved : ∀ a, 32 ≤ a → a < 64 → a ≠ 43 → a ≠ 44 → leftState.mem a = s.mem a := by
    intro a ha hb h43 h44
    exact lf a ha h43 h44 (Or.inl (by omega)) (Or.inl (by omega))
  have remainingPreserved : VectorBuilder.Stored leftState.mem remainingAddress (RecordTable.words w remaining) := by
    apply MemoryCopy.stored_frame _ _ remainingInput
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact lf a (by omega) (by simp [ChildAssembly.left]; omega) (by simp [ChildAssembly.left]; omega)
      (Or.inl (by omega)) (Or.inl (by omega))
  have petalsPreserved : VectorBuilder.Stored leftState.mem petalAddress (RecordTable.words w petals) := by
    apply MemoryCopy.stored_frame _ _ petalInput
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact lf a (by omega) (by simp [ChildAssembly.left]; omega) (by simp [ChildAssembly.left]; omega)
      (Or.inl (by omega)) (Or.inl (by omega))
  obtain ⟨rt, out, ra, rbound, rtrace, rh, rtable, rp, rc, rlower, rupper, rf⟩ :=
    ChildAssembly.assembles ChildAssembly.right ChildAssembly.right_valid remaining petals (SourceChain.resume leftState)
      remainingAddress petalAddress rightRaw rightWork rfl rfl rb pb (by omega) (by omega) rs fits variablesFit
      ((saved 34 (by decide) (by decide) (by decide) (by decide)).trans rptr)
      ((saved 35 (by decide) (by decide) (by decide) (by decide)).trans pptr)
      ((saved 41 (by decide) (by decide) (by decide) (by decide)).trans rrptr)
      ((saved 36 (by decide) (by decide) (by decide) (by decide)).trans rcount)
      ((saved 37 (by decide) (by decide) (by decide) (by decide)).trans pcount)
      ((saved 42 (by decide) (by decide) (by decide) (by decide)).trans rwptr)
      remainingPreserved petalsPreserved
  have full := SourceChain.traces (ChildAssembly.algorithm ChildAssembly.left).code
    (ChildAssembly.algorithm ChildAssembly.right).code s leftState out lt rt live lh ltrace rtrace
  refine ⟨lt + rt, out.relocate (ChildAssembly.algorithm ChildAssembly.left).code.length, la, ra,
    by unfold cost; omega, full, rh, ?_, rtable, ?_, ?_, rp, rc, by omega, by omega, by omega, rupper, ?_⟩
  · apply MemoryCopy.stored_frame _ _ ltable
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact rf a (by omega) (by simp [ChildAssembly.right]; omega) (by simp [ChildAssembly.right]; omega)
      (Or.inl (by omega)) (Or.inl (by omega))
  · exact (rf 43 (by decide) (by decide) (by decide) (Or.inl (by omega)) (Or.inl (by omega))).trans lp
  · exact (rf 44 (by decide) (by decide) (by decide) (Or.inl (by omega)) (Or.inl (by omega))).trans lc
  · intro a ha h43 h44 h45 h46 outside
    exact (rf a ha h45 h46 (by omega) (by omega)).trans
      (lf a ha h43 h44 (by omega) (by omega))

end WordRAM.Conjectures.Sparsification.BothChildren

/-! Complete construction of two normalized children from a partition. -/
namespace WordRAM.Conjectures.Sparsification.BuildChildren

private def reg (i : Nat) : SourceOperand := .memory (.direct i)

def prepare : Algorithm :=
  ⟨[.copy (.direct 20) (reg 32), .copy (.direct 21) (reg 33),
    .copy (.direct 31) (reg 38), .copy (.direct 48) (.immediate 1), .halt], 1, by decide⟩

def algorithm : Algorithm :=
  ⟨SourceChain.code prepare.code (SourceChain.code CoreRecord.algorithm.code BothChildren.algorithm.code), 1, by decide⟩

theorem prepares (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (prepare.program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧ t.mem 20 = s.mem 32 ∧ t.mem 21 = s.mem 33 ∧
      t.mem 31 = s.mem 38 ∧ t.mem 48 = 1#w.bits ∧
      (∀ a, 32 ≤ a → a ≠ 48 → t.mem a = s.mem a) := by
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a ha h48
  have h : a ≠ 20 ∧ a ≠ 21 ∧ a ≠ 31 := by omega
  simp [h, h48]

private theorem trace_of_ticks (program : Program w .multiplication 1) (s : State w) (fuel : Nat)
    (cost : (run widthConstant program fuel s).ticks = s.ticks + fuel) :
    Runs widthConstant program fuel s (run widthConstant program fuel s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant program fuel s
  have ticks := runs_cost trace
  have eq : time = fuel := by omega
  subst time; exact trace

/-- Materialize the core and construct both normalized children. Every memory
operation and control transfer belongs to the given uniform source program. -/
theorem builds (remaining petals : CNF n) (core : Clause n) (s : State w)
    (remainingAddress petalAddress coreAddress leftRaw leftWork rightRaw rightWork : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits)
    (layout : BothChildren.Layout w remaining.length petals.length remainingAddress petalAddress coreAddress leftRaw leftWork rightRaw rightWork)
    (remainingBeforeCore : remainingAddress + 3 * remaining.length ≤ coreAddress)
    (petalsBeforeCore : petalAddress + 3 * petals.length ≤ coreAddress)
    (qp : s.mem 32 = Masks.encode w core true) (qn : s.mem 33 = Masks.encode w core false)
    (rptr : s.mem 34 = BitVec.ofNat w.bits remainingAddress)
    (pptr : s.mem 35 = BitVec.ofNat w.bits petalAddress)
    (rcount : s.mem 36 = BitVec.ofNat w.bits remaining.length)
    (pcount : s.mem 37 = BitVec.ofNat w.bits petals.length)
    (cptr : s.mem 38 = BitVec.ofNat w.bits coreAddress)
    (lrptr : s.mem 39 = BitVec.ofNat w.bits leftRaw)
    (lwptr : s.mem 40 = BitVec.ofNat w.bits leftWork)
    (rrptr : s.mem 41 = BitVec.ofNat w.bits rightRaw)
    (rwptr : s.mem 42 = BitVec.ofNat w.bits rightWork)
    (remainingInput : VectorBuilder.Stored s.mem remainingAddress (RecordTable.words w remaining))
    (petalInput : VectorBuilder.Stored s.mem petalAddress (RecordTable.words w petals)) :
    ∃ time final leftAddress rightAddress,
      time ≤ 12 * w.bits + 33 + BothChildren.cost remaining.length petals.length ∧
      Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem leftAddress (RecordTable.words w (Normalize.normalize (remaining ++ [core]))) ∧
      VectorBuilder.Stored final.mem rightAddress (RecordTable.words w (Normalize.normalize (remaining ++ petals))) ∧
      final.mem 43 = BitVec.ofNat w.bits leftAddress ∧
      final.mem 44 = BitVec.ofNat w.bits (Normalize.normalize (remaining ++ [core])).length ∧
      final.mem 45 = BitVec.ofNat w.bits rightAddress ∧
      final.mem 46 = BitVec.ofNat w.bits (Normalize.normalize (remaining ++ petals)).length ∧
      leftRaw ≤ leftAddress ∧ leftAddress + 3 * (Normalize.normalize (remaining ++ [core])).length ≤ rightRaw ∧
      rightRaw ≤ rightAddress ∧ rightAddress + 3 * (Normalize.normalize (remaining ++ petals)).length ≤
        rightWork + (remaining.length + petals.length) * (3 * (remaining.length + petals.length + 1)) ∧
      (∀ a, 32 ≤ a → a ≠ 43 → a ≠ 44 → a ≠ 45 → a ≠ 46 → a ≠ 48 →
        (a < coreAddress ∨ rightWork + (remaining.length + petals.length) * (3 * (remaining.length + petals.length + 1)) ≤ a) →
        final.mem a = s.mem a) := by
  have rb := layout.remainingBase
  have pb := layout.petalsBase
  have cb := layout.coreBase
  have ce := layout.coreEnd
  have ls := layout.leftSpace
  have mid := layout.middle
  have rs := layout.rightSpace
  have fits := layout.fits
  let prepared := run widthConstant (prepare.program w) 5 s
  obtain ⟨ph, pt, pp, pn, pcptr, one, pf⟩ := prepares s pc live
  obtain ⟨coreState, ct, ch, coreTable, cf⟩ := CoreRecord.builds core (SourceChain.resume prepared) coreAddress
    rfl rfl variablesFit (by omega) (by omega) (pp.trans qp) (pn.trans qn) (pcptr.trans cptr)
  have saved : ∀ a, 32 ≤ a → a < 64 → a ≠ 48 → coreState.mem a = s.mem a := by
    intro a ha hb h48
    exact (cf a (by omega) (Or.inl (by omega))).trans (pf a ha h48)
  have remainingPreserved : VectorBuilder.Stored coreState.mem remainingAddress (RecordTable.words w remaining) := by
    apply MemoryCopy.stored_frame _ _ remainingInput
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact (cf a (by omega) (Or.inl (by omega))).trans (pf a (by omega) (by omega))
  have petalsPreserved : VectorBuilder.Stored coreState.mem petalAddress (RecordTable.words w petals) := by
    apply MemoryCopy.stored_frame _ _ petalInput
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact (cf a (by omega) (Or.inl (by omega))).trans (pf a (by omega) (by omega))
  obtain ⟨time, out, la, ra, bound, trace, halted, leftTable, rightTable, lp, lc, rp, rc, ll, lu, rl, ru, frame⟩ :=
    BothChildren.builds remaining petals core (SourceChain.resume coreState)
      remainingAddress petalAddress coreAddress leftRaw leftWork rightRaw rightWork rfl rfl variablesFit layout
      ((saved 34 (by decide) (by decide) (by decide)).trans rptr)
      ((saved 35 (by decide) (by decide) (by decide)).trans pptr)
      ((saved 36 (by decide) (by decide) (by decide)).trans rcount)
      ((saved 37 (by decide) (by decide) (by decide)).trans pcount)
      ((saved 38 (by decide) (by decide) (by decide)).trans cptr)
      ((saved 39 (by decide) (by decide) (by decide)).trans lrptr)
      ((saved 40 (by decide) (by decide) (by decide)).trans lwptr)
      ((saved 41 (by decide) (by decide) (by decide)).trans rrptr)
      ((saved 42 (by decide) (by decide) (by decide)).trans rwptr)
      ((cf 48 (by decide) (Or.inl (by omega))).trans one) remainingPreserved petalsPreserved coreTable
  have tail := SourceChain.traces CoreRecord.algorithm.code BothChildren.algorithm.code (SourceChain.resume prepared)
    coreState out (12 * w.bits + 28) time rfl ch ct trace
  have full := SourceChain.traces prepare.code (SourceChain.code CoreRecord.algorithm.code BothChildren.algorithm.code)
    s prepared _ 5 ((12 * w.bits + 28) + time) live ph (trace_of_ticks _ s 5 pt) tail
  refine ⟨5 + ((12 * w.bits + 28) + time), (out.relocate CoreRecord.algorithm.code.length).relocate prepare.code.length,
    la, ra, by omega, full, halted, leftTable, rightTable, lp, lc, rp, rc, ll, lu, rl, ru, ?_⟩
  intro a ha h43 h44 h45 h46 h48 outside
  exact (frame a ha h43 h44 h45 h46 (by omega)).trans
    ((cf a (by omega) (by omega)).trans (pf a ha h48))

end WordRAM.Conjectures.Sparsification.BuildChildren

/-! Actual wordRAM realization of the two mathematical sparsification branches. -/
namespace WordRAM.Conjectures.Sparsification.BranchMachine

private def reg (i : Nat) : SourceOperand := .memory (.direct i)

def prepare : Algorithm :=
  ⟨[.copy (.direct 32) (reg 20), .copy (.direct 33) (reg 21),
    .copy (.direct 34) (reg 18), .copy (.direct 35) (reg 19), .halt], 1, by decide⟩

def bridge : Algorithm :=
  ⟨[.copy (.direct 36) (reg 16), .copy (.direct 37) (reg 17), .halt], 1, by decide⟩

def algorithm : Algorithm :=
  ⟨SourceChain.code prepare.code (SourceChain.code BranchPartition.algorithm.code
    (SourceChain.code bridge.code BuildChildren.algorithm.code)), 1, by decide⟩

theorem prepares (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (prepare.program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧ t.mem 32 = s.mem 20 ∧ t.mem 33 = s.mem 21 ∧
      t.mem 34 = s.mem 18 ∧ t.mem 35 = s.mem 19 ∧
      (∀ a, a ≠ 32 → a ≠ 33 → a ≠ 34 → a ≠ 35 → t.mem a = s.mem a) := by
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h32 h33 h34 h35; simp [h32, h33, h34, h35]

theorem bridges (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (bridge.program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 36 = s.mem 16 ∧ t.mem 37 = s.mem 17 ∧
      (∀ a, a ≠ 36 → a ≠ 37 → t.mem a = s.mem a) := by
  simp [bridge, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h36 h37; simp [h36, h37]

private theorem trace_of_ticks (program : Program w .multiplication 1) (s : State w) (fuel : Nat)
    (cost : (run widthConstant program fuel s).ticks = s.ticks + fuel) :
    Runs widthConstant program fuel s (run widthConstant program fuel s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant program fuel s
  have ticks := runs_cost trace
  have eq : time = fuel := by omega
  subst time; exact trace

set_option maxRecDepth 4096 in
/-- From a selected core and an input clause table, construct exactly the two
normalized formulas in `Branch.left` and `Branch.right`, with both descriptors
saved and the original input preserved. -/
theorem branches (formula : CNF n) (core : Clause n) (size : Nat) (s : State w)
    (source remainingAddress petalAddress coreAddress leftRaw leftWork rightRaw rightWork : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits)
    (nodup : ∀ clause ∈ formula, clause.Nodup) (sourceBase : 64 ≤ source)
    (partitionLayout : PartitionInvariant.Layout w formula.length source remainingAddress petalAddress)
    (childLayout : BothChildren.Layout w (Branch.remaining formula core size).length
      (BranchTables.petals formula core size).length remainingAddress petalAddress coreAddress leftRaw leftWork rightRaw rightWork)
    (petalsBeforeCore : petalAddress + 3 * formula.length ≤ coreAddress)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula))
    (count : s.mem 24 = BitVec.ofNat w.bits formula.length)
    (pointer : s.mem 23 = BitVec.ofNat w.bits source)
    (remainingPointer : s.mem 18 = BitVec.ofNat w.bits remainingAddress)
    (petalPointer : s.mem 19 = BitVec.ofNat w.bits petalAddress)
    (qp : s.mem 20 = Masks.encode w core true) (qn : s.mem 21 = Masks.encode w core false)
    (target : s.mem 22 = BitVec.ofNat w.bits size)
    (cptr : s.mem 38 = BitVec.ofNat w.bits coreAddress)
    (lrptr : s.mem 39 = BitVec.ofNat w.bits leftRaw)
    (lwptr : s.mem 40 = BitVec.ofNat w.bits leftWork)
    (rrptr : s.mem 41 = BitVec.ofNat w.bits rightRaw)
    (rwptr : s.mem 42 = BitVec.ofNat w.bits rightWork) :
    ∃ time final leftAddress rightAddress,
      time ≤ formula.length * (12 * w.bits + 86) + 12 * w.bits + 50 +
        BothChildren.cost (Branch.remaining formula core size).length (BranchTables.petals formula core size).length ∧
      Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem leftAddress (RecordTable.words w (Branch.left formula core size)) ∧
      VectorBuilder.Stored final.mem rightAddress (RecordTable.words w (Branch.right formula core size)) ∧
      final.mem 43 = BitVec.ofNat w.bits leftAddress ∧ final.mem 44 = BitVec.ofNat w.bits (Branch.left formula core size).length ∧
      final.mem 45 = BitVec.ofNat w.bits rightAddress ∧ final.mem 46 = BitVec.ofNat w.bits (Branch.right formula core size).length ∧
      leftRaw ≤ leftAddress ∧ leftAddress + 3 * (Branch.left formula core size).length ≤ rightRaw ∧
      rightRaw ≤ rightAddress ∧ rightAddress + 3 * (Branch.right formula core size).length ≤
        rightWork + ((Branch.remaining formula core size).length + (BranchTables.petals formula core size).length) *
          (3 * ((Branch.remaining formula core size).length + (BranchTables.petals formula core size).length + 1)) ∧
      VectorBuilder.Stored final.mem source (RecordTable.words w formula) ∧
      (∀ a, 49 ≤ a → (a < remainingAddress ∨
        rightWork + ((Branch.remaining formula core size).length + (BranchTables.petals formula core size).length) *
          (3 * ((Branch.remaining formula core size).length + (BranchTables.petals formula core size).length + 1)) ≤ a) →
        final.mem a = s.mem a) := by
  have remainingBase := childLayout.remainingBase
  have petalsBase := childLayout.petalsBase
  have sourceEnd := partitionLayout.sourceEnd
  have partitionEnd := partitionLayout.leftEnd
  have coreBase := childLayout.coreBase
  have coreEnd := childLayout.coreEnd
  have leftSpace := childLayout.leftSpace
  have middleSpace := childLayout.middle
  have rightSpace := childLayout.rightSpace
  let prepared := run widthConstant (prepare.program w) 5 s
  obtain ⟨ph, pt, pos, neg, remp, petp, pf⟩ := prepares s pc live
  have preparedInput : VectorBuilder.Stored prepared.mem source (RecordTable.words w formula) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a ha _; exact pf a (by omega) (by omega) (by omega) (by omega)
  obtain ⟨time, partitioned, bound, trace, halted, remainingTable, petalTable, remainingCount, petalCount,
      _, _, _, _, _, _, _, frame⟩ := PartitionMachine.partitions formula core size source remainingAddress petalAddress
      (SourceChain.resume prepared) rfl rfl partitionLayout variablesFit width sizeFits nodup preparedInput
      ((pf 24 (by decide) (by decide) (by decide) (by decide)).trans count)
      ((pf 23 (by decide) (by decide) (by decide) (by decide)).trans pointer)
      ((pf 18 (by decide) (by decide) (by decide) (by decide)).trans remainingPointer)
      ((pf 19 (by decide) (by decide) (by decide) (by decide)).trans petalPointer)
      ((pf 20 (by decide) (by decide) (by decide) (by decide)).trans qp)
      ((pf 21 (by decide) (by decide) (by decide) (by decide)).trans qn)
      ((pf 22 (by decide) (by decide) (by decide) (by decide)).trans target)
  have metadata : ∀ a, 32 ≤ a → a < 64 → partitioned.mem a = prepared.mem a := by
    intro a ha hb
    exact frame a ⟨ha, Or.inl (by omega), Or.inl (by omega)⟩
  let middle := run widthConstant (bridge.program w) 3 (SourceChain.resume partitioned)
  obtain ⟨mh, mt, mc, mp, mf⟩ := bridges (SourceChain.resume partitioned) rfl rfl
  have saved : ∀ a, 38 ≤ a → a < 64 → middle.mem a = s.mem a := by
    intro a ha hb
    exact (mf a (by omega) (by omega)).trans ((metadata a (by omega) hb).trans
      (pf a (by omega) (by omega) (by omega) (by omega)))
  have remainingInput : VectorBuilder.Stored middle.mem remainingAddress
      (RecordTable.words w (Branch.remaining formula core size)) := by
    apply MemoryCopy.stored_frame _ _ remainingTable
    intro a ha _; exact mf a (by omega) (by omega)
  have petalsInput : VectorBuilder.Stored middle.mem petalAddress
      (RecordTable.words w (BranchTables.petals formula core size)) := by
    apply MemoryCopy.stored_frame _ _ petalTable
    intro a ha _; exact mf a (by omega) (by omega)
  have rl := BranchTables.remaining_length formula core size
  have pl := BranchTables.petals_length formula core size
  obtain ⟨buildTime, out, la, ra, buildBound, buildTrace, buildHalt, leftTable, rightTable, lp, lc, rp, rc,
      ll, lu, rlo, ru, bf⟩ := BuildChildren.builds (Branch.remaining formula core size) (BranchTables.petals formula core size)
      core (SourceChain.resume middle) remainingAddress petalAddress coreAddress leftRaw leftWork rightRaw rightWork
      rfl rfl variablesFit childLayout (by omega) (by omega)
      ((mf 32 (by decide) (by decide)).trans ((metadata 32 (by decide) (by decide)).trans (pos.trans qp)))
      ((mf 33 (by decide) (by decide)).trans ((metadata 33 (by decide) (by decide)).trans (neg.trans qn)))
      ((mf 34 (by decide) (by decide)).trans ((metadata 34 (by decide) (by decide)).trans (remp.trans remainingPointer)))
      ((mf 35 (by decide) (by decide)).trans ((metadata 35 (by decide) (by decide)).trans (petp.trans petalPointer)))
      (mc.trans remainingCount) (mp.trans petalCount)
      ((saved 38 (by decide) (by decide)).trans cptr) ((saved 39 (by decide) (by decide)).trans lrptr)
      ((saved 40 (by decide) (by decide)).trans lwptr) ((saved 41 (by decide) (by decide)).trans rrptr)
      ((saved 42 (by decide) (by decide)).trans rwptr) remainingInput petalsInput
  have tail := SourceChain.traces bridge.code BuildChildren.algorithm.code (SourceChain.resume partitioned)
    middle out 3 buildTime rfl mh (trace_of_ticks _ _ 3 mt) buildTrace
  have midTrace := SourceChain.traces BranchPartition.algorithm.code (SourceChain.code bridge.code BuildChildren.algorithm.code)
    (SourceChain.resume prepared) partitioned _ time (3 + buildTime) rfl halted trace tail
  have full := SourceChain.traces prepare.code (SourceChain.code BranchPartition.algorithm.code
      (SourceChain.code bridge.code BuildChildren.algorithm.code)) s prepared _ 5 (time + (3 + buildTime)) live ph
    (trace_of_ticks _ s 5 pt) midTrace
  refine ⟨5 + (time + (3 + buildTime)),
    ((out.relocate bridge.code.length).relocate BranchPartition.algorithm.code.length).relocate prepare.code.length,
    la, ra, by omega, full, buildHalt, leftTable, rightTable, lp, lc, rp, rc, ll, lu, rlo, ru, ?_, ?_⟩
  · apply MemoryCopy.stored_frame _ _ input
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact (bf a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (Or.inl (by omega))).trans
      ((mf a (by omega) (by omega)).trans ((frame a ⟨by omega, Or.inl (by omega), Or.inl (by omega)⟩).trans
        (pf a (by omega) (by omega) (by omega) (by omega))))
  · intro a ha outside
    exact (bf a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)).trans
      ((mf a (by omega) (by omega)).trans ((frame a ⟨by omega, by omega, by omega⟩).trans
        (pf a (by omega) (by omega) (by omega) (by omega))))

end WordRAM.Conjectures.Sparsification.BranchMachine