This definition gives the library's named construction or computation for “gram”. Right Gram environment.
noncomputable def gram : {n l r : ℕ} → Chain n l r → _root_.Matrix (Fin l) (Fin l) ℝ
| _, _, _, .nil r => 1
| _, _, _, .cons A C =>
let E := gram C
∑ bit : Fin 2, slice A bit * E * (slice A bit).transpose
/-- Exact semantics of the small-matrix recursion, including every terminal
bond label. The full word sum appears only in the specification. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “gram eq sum”; the hypotheses and conclusion in the code panel fix its exact scope. Exact semantics of the small-matrix recursion, including every terminal bond label.
theorem gram_eq_sum {n l r : ℕ} (C : Chain n l r) :
gram C = ∑ x : Word n, contract C x * (contract C x).transpose := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “gram scalar”; the hypotheses and conclusion in the code panel fix its exact scope. A scalar-boundary train's environment entry is its complete squared norm.
theorem gram_scalar {n : ℕ} (C : Chain n 1 1) :
gram C 0 0 = ∑ x : Word n, (contract C x 0 0) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “gram scalar nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem gram_scalar_nonneg {n : ℕ} (C : Chain n 1 1) : 0 ≤ gram C 0 0 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “norm”. Local-core norm supplier; only one square root is performed after the Gram recursion.
noncomputable def norm {n : ℕ} (C : Chain n 1 1) : ℝ := Real.sqrt (gram C 0 0)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm eq”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem norm_eq {n : ℕ} (C : Chain n 1 1) :
norm C = Real.sqrt (∑ x : Word n, (contract C x 0 0) ^ 2) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm sq”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem norm_sq {n : ℕ} (C : Chain n 1 1) :
norm C ^ 2 = ∑ x : Word n, (contract C x 0 0) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm pos of nonzero”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem norm_pos_of_nonzero {n : ℕ} (C : Chain n 1 1)
(h : ∃ x, contract C x 0 0 ≠ 0) : 0 < norm C := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm eq of contract”; the hypotheses and conclusion in the code panel fix its exact scope. A reusable target adapter.
theorem norm_eq_of_contract {n : ℕ} {I : Type*} [Fintype I]
(C : Chain n 1 1) (e : Word n ≃ I) (target : I → ℝ)
(h : ∀ x, contract C x 0 0 = target (e x)) :
norm C = Real.sqrt (∑ i : I, target i ^ 2) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “environment scalars”. Storage if every intermediate environment is retained.
def environmentScalars : {n l r : ℕ} → Chain n l r → ℕ
| _, _, r, .nil _ => r ^ 2
| _, l, _, .cons _ C => l ^ 2 + environmentScalars C
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “environment scalars le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem environmentScalars_le {n l r : ℕ} (C : Chain n l r) (D : ℕ)
(hD : maxBond C ≤ D) : environmentScalars C ≤ (n + 1) * D ^ 2 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “update arithmetic budget”. A conservative count for direct dense real arithmetic at one update: two bits, products (l by m)*(m by m) and (l by m)*(m by l), charging one multiplication and at most one addition per inner-product term, then l^2 additions to combine the two bits.
def updateArithmeticBudget (l m : ℕ) : ℕ := 4 * (l * m * m + l * l * m) + l * l
/-- Syntactic real-operation budget of the stated local evaluation schedule.
This is not a cost semantics for an external runtime or finite-bit arithmetic. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “arithmetic budget”. Syntactic real-operation budget of the stated local evaluation schedule.
def arithmeticBudget : {n l r : ℕ} → Chain n l r → ℕ
| _, _, _, .nil _ => 0
| _, l, _, @Chain.cons _ _ m _ _ C => updateArithmeticBudget l m + arithmeticBudget C
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “update arithmetic budget le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem updateArithmeticBudget_le (l m D : ℕ) (hl : l ≤ D) (hm : m ≤ D) :
updateArithmeticBudget l m ≤ 9 * D ^ 3 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “arithmetic budget le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem arithmeticBudget_le {n l r : ℕ} (C : Chain n l r) (D : ℕ)
(hD : maxBond C ≤ D) : arithmeticBudget C ≤ 9 * n * D ^ 3 := by
commit-pinned source · Verso Blueprint panel