QuantumBlockEncoding/StoredHermiteRawCost.lean

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

def ordinary (cost : Cost) : ℕ := ∑ op : Op, cost op

/-- Eight-operation enumeration adapter; no producer or counter is altered. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “ordinary eq total”; the hypotheses and conclusion in the code panel fix its exact scope. Eight-operation enumeration adapter; no producer or counter is altered.

theorem ordinary_eq_total (cost : Cost) :
    ordinary cost = StoredRectangularGivens.total cost := by

commit-pinned source · Verso Blueprint panel

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

theorem ordinary_add (a b : Cost) : ordinary (a+b) = ordinary a + ordinary b := by

commit-pinned source · Verso Blueprint panel

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

theorem ordinary_zero : ordinary 0 = 0 := by simp [ordinary]

commit-pinned source · Verso Blueprint panel

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

theorem ordinary_tick (op : Op) : ordinary (tick op) = 1 := by simp [ordinary, tick]

commit-pinned source · Verso Blueprint panel

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

def stageBudget (k : ℕ) : ℕ :=
  40*(2*k+1)^3 + 84*(2*k+1)^2 + 64*(2*k+1) + 194 + 576*(2*k+6)^2

commit-pinned source · Verso Blueprint panel

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

theorem stage_total_cost_le {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
    (t : Fin (n+1)) : ordinary (stage cache t).run.cost ≤ stageBudget k := by

commit-pinned source · Verso Blueprint panel

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

theorem stage_exponentialCalls {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
    (t : Fin (n+1)) :
    (stage cache t).exponentialCalls = ∑ bit : Fin 2,
      if ((StoredHermiteStageInput.input cache t).run.value.children[bit.val]).leftFull
        then 1 else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “stage exponential calls le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem stage_exponentialCalls_le {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
    (t : Fin (n+1)) : (stage cache t).exponentialCalls ≤ 2 :=
  StoredHermiteStageFields.two_exponentialCalls_le _ _

commit-pinned source · Verso Blueprint panel

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

theorem stage_integerAdditions {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
    (t : Fin (n+1)) : (stage cache t).integerAdditions = 4 :=
  StoredHermiteStageInput.input_integerAdditions cache t

/-- The ledger table is materialized once. Its projection adds exactly three
reads and three writes per stage, including its initial stored record. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “collect stages cost”; the hypotheses and conclusion in the code panel fix its exact scope. The ledger table is materialized once.

theorem collectStages_cost {m : ℕ} (f : Fin m → StageRun α) (op : Op) :
    (collectStages f).run.cost op = (∑ i : Fin m, (f i).run.cost op) +
      m * (3*tick .read op + 3*tick .write op) := by

commit-pinned source · Verso Blueprint panel

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

theorem collectStages_total_cost {m : ℕ} (f : Fin m → StageRun α) :
    ordinary (collectStages f).run.cost =
      (∑ i : Fin m, ordinary (f i).run.cost) + 6*m := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “collect stages exponential calls”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem collectStages_exponentialCalls {m : ℕ} (f : Fin m → StageRun α) :
    (collectStages f).exponentialCalls = ∑ i : Fin m, (f i).exponentialCalls := by

commit-pinned source · Verso Blueprint panel

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

theorem collectStages_integerAdditions {m : ℕ} (f : Fin m → StageRun α) :
    (collectStages f).integerAdditions = ∑ i : Fin m, (f i).integerAdditions := by

commit-pinned source · Verso Blueprint panel

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

theorem tables_total_cost_le {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n) :
    ordinary (tables cache).run.cost ≤ (n+1)*(stageBudget k + 6) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “tables exponential calls le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem tables_exponentialCalls_le {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n) :
    (tables cache).exponentialCalls ≤ 2*(n+1) := by

commit-pinned source · Verso Blueprint panel

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

theorem tables_integerAdditions {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n) :
    (tables cache).integerAdditions = 4*(n+1) := by

commit-pinned source · Verso Blueprint panel

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

theorem boundaryInputs_cost {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n) (op : Op) :
    (boundaryInputs cache).cost op = 4*tick .read op := by

commit-pinned source · Verso Blueprint panel

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

theorem boundaries_total_cost {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n) :
    ordinary (boundaries cache).cost = 32*(2*k+6)+6 := by

commit-pinned source · Verso Blueprint panel

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

def rawBudget (k n : ℕ) : ℕ :=
  3200*(k+1)^2 + 256*(n+1)^2 +
    (n+1)*(40*(2*k+1)^3 + 84*(2*k+1)^2 + 64*(2*k+1) + 200 + 576*(2*k+6)^2) +
    20*(2*k+6)^2 + 62*(2*k+6) + 5*n^2 + 7*n + 37

/-- Every summand is a proved cost of a subrun actually used by raw. No
dimension-only or hypothetical source-entry budget is substituted. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “raw total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Every summand is a proved cost of a subrun actually used by raw.

theorem raw_total_cost_le (k n : ℕ) (L : ℝ) :
    ordinary (raw k n L).run.cost ≤ rawBudget k n := by

commit-pinned source · Verso Blueprint panel

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

theorem raw_stored_total_cost_le (k n : ℕ) (L : ℝ) :
    StoredRectangularGivens.total (raw k n L).run.cost ≤ rawBudget k n := by

commit-pinned source · Verso Blueprint panel

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

theorem raw_cost_le (k n : ℕ) (L : ℝ) (op : Op) :
    (raw k n L).run.cost op ≤ rawBudget k n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “raw exponential calls”; the hypotheses and conclusion in the code panel fix its exact scope. Exact exponential ledger: one coefficient call, n+1 cached tail calls, and the actual stage injection calls (zero on disabled Full guards).

theorem raw_exponentialCalls (k n : ℕ) (L : ℝ) :
    (raw k n L).exponentialCalls = n+2 + ∑ t : Fin (n+1),
      (stage (StoredHermiteSourceCache.compile k n L).run.value t).exponentialCalls := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “raw exponential calls le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem raw_exponentialCalls_le (k n : ℕ) (L : ℝ) :
    (raw k n L).exponentialCalls ≤ 3*(n+1)+1 := by

commit-pinned source · Verso Blueprint panel

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

theorem raw_quotientCalls (k n : ℕ) (L : ℝ) :
    (raw k n L).quotientCalls = (n+1)*(n+2) :=
  StoredHermiteSourceCache.compile_quotientCalls k n L

commit-pinned source · Verso Blueprint panel

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

theorem raw_remainderCalls (k n : ℕ) (L : ℝ) :
    (raw k n L).remainderCalls = (n+1)^2 :=
  StoredHermiteSourceCache.compile_remainderCalls k n L

commit-pinned source · Verso Blueprint panel

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

theorem raw_integerDoublings (k n : ℕ) (L : ℝ) :
    (raw k n L).integerDoublings = n :=
  StoredHermiteSourceCache.compile_integerDoublings k n L

commit-pinned source · Verso Blueprint panel

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

theorem raw_integerAdditions (k n : ℕ) (L : ℝ) :
    (raw k n L).integerAdditions = 4*(n+1) :=
  tables_integerAdditions _

/-- Sum of precisely the four named integer counters, not all integer work. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “raw selected integer total”; the hypotheses and conclusion in the code panel fix its exact scope. Sum of precisely the four named integer counters, not all integer work.

theorem raw_selected_integer_total (k n : ℕ) (L : ℝ) :
    (raw k n L).quotientCalls + (raw k n L).remainderCalls +
      (raw k n L).integerDoublings + (raw k n L).integerAdditions = 2*n^2+10*n+7 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “raw certified”; the hypotheses and conclusion in the code panel fix its exact scope. Same-run source equality, polynomial ordinary work, exponential cap, and the four accurately scoped integer counters.

theorem raw_certified (k n : ℕ) (L : ℝ) (hL : 0 < L) :
    let result := raw k n L
    denoteChain result.run.value = HermiteExplicitBond.rawSourceChain k n L ∧
    ordinary result.run.cost ≤ rawBudget k n ∧
    result.exponentialCalls ≤ 3*(n+1)+1 ∧
    result.quotientCalls = (n+1)*(n+2) ∧ result.remainderCalls = (n+1)^2 ∧
    result.integerDoublings = n ∧ result.integerAdditions = 4*(n+1) :=
  ⟨raw_value k n L hL, raw_total_cost_le k n L, raw_exponentialCalls_le k n L,
    raw_quotientCalls k n L, raw_remainderCalls k n L,
    raw_integerDoublings k n L, raw_integerAdditions k n L⟩

commit-pinned source · Verso Blueprint panel