QuantumBlockEncoding/StoredHermiteChildGeometry.lean

This record groups the data and proof fields needed for “flags”. A proposition-valued field is a requirement until a constructor supplies it.

structure Flags where
  full : Bool
  isPartial : Bool

/-- Four actual integer comparisons; `last` is the excluded integer endpoint. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “flags”. Four actual integer comparisons; 'last' is the excluded integer endpoint.

def flags (lower upper first last : ℕ) : Run Flags := do
  let lo ← charge .compare (decide (lower ≤ first))
  let hi ← charge .compare (decide (last ≤ upper))
  let below ← charge .compare (decide (last ≤ lower))
  let above ← charge .compare (decide (upper ≤ first))
  let full := lo && hi
  ⟨⟨full, !full && !(below || above)⟩, 2 • tick .write⟩

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “flags full”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem flags_full (lower upper first size : ℕ) :
    (flags lower upper first (first + size)).value.full = decide (Full lower upper first size) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “flags partial”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem flags_partial (lower upper first size : ℕ) :
    (flags lower upper first (first + size)).value.isPartial = decide (Partial lower upper first size) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “flags cost”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem flags_cost (lower upper first last : ℕ) (op : Op) :
    (flags lower upper first last).cost op = 4 * tick .compare op + 2 * tick .write op := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “child”. A proposition-valued field is a requirement until a constructor supplies it.

structure Child where
  first : ℕ
  lower : ℝ
  upper : ℝ
  leftFull : Bool
  leftPartial : Bool
  middleFull : Bool
  middlePartial : Bool

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “child run”. A proposition-valued field is a requirement until a constructor supplies it.

structure ChildRun (α : Type) where
  run : Run α
  integerAdditions : ℕ

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “child”.

noncomputable def child (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) (bit : Bool) : ChildRun Child :=
  let result : Run Child := do
    let parentFirst ← charge .read parent.first
    let parentLower ← charge .read parent.lower
    let width ← charge .read level.width
    let offset ← charge .compare (if bit then ((1 : ℝ), span) else (0, 0))
    let first := parentFirst + offset.2
    let last := first + span
    let shift ← StoredGivens.mul offset.1 width
    let lower ← StoredGivens.add parentLower shift

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “child first”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem child_first (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) (bit : Bool) :
    (child parent level span cut midpoint bit).run.value.first =
      parent.first + if bit then span else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “child lower”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem child_lower (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) (bit : Bool) :
    (child parent level span cut midpoint bit).run.value.lower =
      parent.lower + (if bit then 1 else 0) * level.width := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “child upper”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem child_upper (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) (bit : Bool) :
    (child parent level span cut midpoint bit).run.value.upper =
      (child parent level span cut midpoint bit).run.value.lower + level.width := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “child flags”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem child_flags (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) (bit : Bool) :
    let c := (child parent level span cut midpoint bit).run.value
    c.leftFull = decide (Full 0 cut c.first span) ∧
    c.leftPartial = decide (Partial 0 cut c.first span) ∧
    c.middleFull = decide (Full cut midpoint c.first span) ∧
    c.middlePartial = decide (Partial cut midpoint c.first span) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “child cost”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem child_cost (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) (bit : Bool) (op : Op) :
    (child parent level span cut midpoint bit).run.cost op =
      3 * tick .field op + 9 * tick .compare op +
        7 * tick .read op + 11 * tick .write op := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “child integer additions”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem child_integerAdditions (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) (bit : Bool) :
    (child parent level span cut midpoint bit).integerAdditions = 2 := rfl

/-- Value-only specification: all cached-data hypotheses are explicit. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “child refines”; the hypotheses and conclusion in the code panel fix its exact scope. Value-only specification: all cached-data hypotheses are explicit.

theorem child_refines (parent : Point) (level : TailLevel)
    (span cut midpoint n r : ℕ) (origin grid : ℝ) (bit : Bool)
    (hp : parent.first = boundarySchedule cut (r + 1))
    (hl : parent.lower = affinePoint origin grid parent.first)
    (hw : level.width = grid * (2 : ℝ)^r)
    (hs : span = 2^r) (hm : midpoint = 2^n) :
    let c := (child parent level span cut midpoint bit).run.value
    c.first = selectedChild (boundarySchedule cut) r bit ∧
    c.lower = affinePoint origin grid (selectedChild (boundarySchedule cut) r bit) ∧
    c.upper = affinePoint origin grid (selectedChild (boundarySchedule cut) r bit + 2^r) ∧
    c.leftFull = decide (Full 0 cut (selectedChild (boundarySchedule cut) r bit) (2^r)) ∧

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “children”. False/true children are computed once each, then stored in this order.

noncomputable def children (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) : ChildRun (Vector Child 2) :=
  let left := child parent level span cut midpoint false
  let right := child parent level span cut midpoint true
  let stored := collect fun i : Fin 2 => do
    let selectRight ← charge .compare (decide (i.val = 1))
    pure (if selectRight then right.run.value else left.run.value)
  ⟨⟨stored.value, left.run.cost + right.run.cost + stored.cost⟩,
    left.integerAdditions + right.integerAdditions⟩

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “children value”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem children_value (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) (bit : Bool) :
    (children parent level span cut midpoint).run.value[if bit then 1 else 0]'(by cases bit <;> decide) =
      (child parent level span cut midpoint bit).run.value := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “children cost”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem children_cost (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) (op : Op) :
    (children parent level span cut midpoint).run.cost op =
      6 * tick .field op + 20 * tick .compare op +
        18 * tick .read op + 26 * tick .write op := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “children integer additions”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem children_integerAdditions (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) :
    (children parent level span cut midpoint).integerAdditions = 4 := rfl

/-- Fixed charged work for both children; integer additions remain separate. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “children total cost”; the hypotheses and conclusion in the code panel fix its exact scope. Fixed charged work for both children; integer additions remain separate.

theorem children_total_cost (parent : Point) (level : TailLevel)
    (span cut midpoint : ℕ) :
    (∑ op : Op, (children parent level span cut midpoint).run.cost op) = 70 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “refines”.

def Refines (c : Child) (cut n r : ℕ) (origin grid : ℝ) (bit : Bool) : Prop :=
  c.first = selectedChild (boundarySchedule cut) r bit ∧
  c.lower = affinePoint origin grid (selectedChild (boundarySchedule cut) r bit) ∧
  c.upper = affinePoint origin grid (selectedChild (boundarySchedule cut) r bit + 2^r) ∧
  c.leftFull = decide (Full 0 cut (selectedChild (boundarySchedule cut) r bit) (2^r)) ∧
  c.leftPartial = decide (Partial 0 cut (selectedChild (boundarySchedule cut) r bit) (2^r)) ∧
  c.middleFull = decide (Full cut (2^n) (selectedChild (boundarySchedule cut) r bit) (2^r)) ∧
  c.middlePartial = decide (Partial cut (2^n) (selectedChild (boundarySchedule cut) r bit) (2^r))

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “children refines”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem children_refines (parent : Point) (level : TailLevel)
    (span cut midpoint n r : ℕ) (origin grid : ℝ) (bit : Bool)
    (hp : parent.first = boundarySchedule cut (r + 1))
    (hl : parent.lower = affinePoint origin grid parent.first)
    (hw : level.width = grid * (2 : ℝ)^r)
    (hs : span = 2^r) (hm : midpoint = 2^n) :
    Refines ((children parent level span cut midpoint).run.value[
      if bit then 1 else 0]'(by cases bit <;> decide)) cut n r origin grid bit := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “children certified”; the hypotheses and conclusion in the code panel fix its exact scope. Refinement and charged work belong to the same pair-producing run.

theorem children_certified (parent : Point) (level : TailLevel)
    (span cut midpoint n r : ℕ) (origin grid : ℝ)
    (hp : parent.first = boundarySchedule cut (r + 1))
    (hl : parent.lower = affinePoint origin grid parent.first)
    (hw : level.width = grid * (2 : ℝ)^r)
    (hs : span = 2^r) (hm : midpoint = 2^n) :
    let result := children parent level span cut midpoint
    (∀ bit : Bool, Refines (result.run.value[
      if bit then 1 else 0]'(by cases bit <;> decide)) cut n r origin grid bit) ∧
    (∑ op : Op, result.run.cost op) = 70 ∧ result.integerAdditions = 4 :=
  ⟨fun bit => children_refines parent level span cut midpoint n r origin grid bit hp hl hw hs hm,

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “child index word bound”; the hypotheses and conclusion in the code panel fix its exact scope. With legal source indices, every generated endpoint fits in n+2 bits.

theorem child_index_word_bound (parent : Point) (level : TailLevel)
    (span cut midpoint n r : ℕ) (bit : Bool)
    (hp : parent.first = boundarySchedule cut (r + 1))
    (hs : span = 2^r) (hc : cut ≤ 2^n) (hr : r ≤ n) :
    (child parent level span cut midpoint bit).run.value.first + span < 2^(n + 2) := by

commit-pinned source · Verso Blueprint panel