QuantumBlockEncoding/HermiteBoundaryInjection.lean

This definition gives the library's named construction or computation for “word value”. The first list entry is the most significant digit.

def wordValue : List Bool → ℕ
  | [] => 0
  | bit :: bits => (if bit then 2 ^ bits.length else 0) + wordValue bits

commit-pinned source · Verso Blueprint panel

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

theorem wordValue_lt (bits : List Bool) : wordValue bits < 2 ^ bits.length := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “path coordinate eq word value”; the hypotheses and conclusion in the code panel fix its exact scope. Reconciles the polynomial's real path coordinate with integer bit order.

theorem pathCoordinate_eq_wordValue (bits : List Bool) :
    pathCoordinate bits 0 = (wordValue bits : ℝ) / 2 ^ bits.length := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “full”. A dyadic node lies entirely in the half-open target interval.

def Full (lower upper first size : ℕ) : Prop :=
  lower ≤ first ∧ first + size ≤ upper

/-- A dyadic node is disjoint from the half-open target interval. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “outside”. A dyadic node is disjoint from the half-open target interval.

def Outside (lower upper first size : ℕ) : Prop :=
  first + size ≤ lower ∨ upper ≤ first

instance (lower upper first size : ℕ) : Decidable (Full lower upper first size) :=
  inferInstanceAs (Decidable (_ ∧ _))

instance (lower upper first size : ℕ) : Decidable (Outside lower upper first size) :=
  inferInstanceAs (Decidable (_ ∨ _))

/-- A genuinely unresolved interval, not a wholly included or outside node. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “partial”. A genuinely unresolved interval, not a wholly included or outside node.

def Partial (lower upper first size : ℕ) : Prop :=
  ¬ Full lower upper first size ∧ ¬ Outside lower upper first size

instance (lower upper first size : ℕ) : Decidable (Partial lower upper first size) :=
  inferInstanceAs (Decidable (_ ∧ _))

/-- At an upper-aligned cut there is only one possible unresolved prefix.
The quotient is computed directly; no list of prefixes is constructed. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “partial prefix eq”; the hypotheses and conclusion in the code panel fix its exact scope. At an upper-aligned cut there is only one possible unresolved prefix.

theorem partial_prefix_eq (lower M B x : ℕ) (hM : 0 < M)
    (hp : Partial lower (M * B) (M * x) M) : x = lower / M := by

commit-pinned source · Verso Blueprint panel

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

theorem partial_prefix_unique (lower M B x y : ℕ) (hM : 0 < M)
    (hx : Partial lower (M * B) (M * x) M)
    (hy : Partial lower (M * B) (M * y) M) : x = y := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “not partial unit”; the hypotheses and conclusion in the code panel fix its exact scope. The integer endpoint prevents an unresolved state at the last bit.

theorem not_partial_unit (lower upper first : ℕ) :
    ¬ Partial lower upper first 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “partial middle prefix unique”; the hypotheses and conclusion in the code panel fix its exact scope. Every cut after the first consumed bit in an 'n+1'-bit middle interval has an upper endpoint aligned with the remaining dyadic block size.

theorem partial_middle_prefix_unique (lower pWidth sWidth x y : ℕ)
    (hx : Partial lower (2 ^ (pWidth + sWidth)) (2 ^ sWidth * x) (2 ^ sWidth))
    (hy : Partial lower (2 ^ (pWidth + sWidth)) (2 ^ sWidth * y) (2 ^ sWidth)) :
    x = y := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “middle root not full”; the hypotheses and conclusion in the code panel fix its exact scope. The initial whole-grid node cannot inject directly: its upper child is outside the middle component.

theorem middle_root_not_full (lower n : ℕ) : ¬ Full lower (2 ^ n) 0 (2 ^ (n + 1)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “affine point”. Affine source coordinate, also meaningful at a block's excluded endpoint.

def affinePoint (origin step : ℝ) (j : ℕ) : ℝ := origin + step * j

/-- Literal restricted Bernstein row readout for a fully included dyadic node. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “injected readout”. Literal restricted Bernstein row readout for a fully included dyadic node.

def injectedReadout (k : ℕ) (origin step : ℝ) (first : ℕ) (bits : List Bool) : ℝ :=
  subdivisionPath (2 * k + 1)
    (restrictCoefficients (2 * k + 1)
      (1 + affinePoint origin step first)
      (1 + affinePoint origin step (first + 2 ^ bits.length))
      (sourceBernsteinCoefficient k)) bits 0

commit-pinned source · Verso Blueprint panel

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

theorem injectedReadout_eq (k : ℕ) (origin step : ℝ) (first : ℕ)
    (bits : List Bool) (hfirst : affinePoint origin step first ≠ 0) :
    injectedReadout k origin step first bits =
      (HermitePolynomial.sourceInterpolant k).eval
        (affinePoint origin step (first + wordValue bits)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “unit coefficient”. A finite coefficient basis vector, extended by zero to the existing Bernstein coefficient API.

def unitCoefficient (d : ℕ) (i : Fin (d + 1)) : ℕ → ℝ :=
  fun j => if j = i.val then 1 else 0

/-- The actual finite row-update matrix: input coefficient `i`, output `j`.
It is the transpose of the usual coefficient-column subdivision matrix. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “shared core”. The actual finite row-update matrix: input coefficient 'i', output 'j'.

def sharedCore (d : ℕ) (bit : Bool) :
    _root_.Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ :=
  fun i j => halfSubdivision d bit (unitCoefficient d i) j.val

/-- The prototype's lower triangular subdivision, transposed for row updates. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “shared core false”; the hypotheses and conclusion in the code panel fix its exact scope. The prototype's lower triangular subdivision, transposed for row updates.

theorem sharedCore_false (d : ℕ) (i j : Fin (d + 1)) :
    sharedCore d false i j =
      if i.val ≤ j.val then (j.val.choose i.val : ℝ) / 2 ^ j.val else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “shared core true”; the hypotheses and conclusion in the code panel fix its exact scope. The prototype's upper triangular subdivision, in the same row orientation.

theorem sharedCore_true (d : ℕ) (i j : Fin (d + 1)) :
    sharedCore d true i j =
      if j.val ≤ i.val then ((d - j.val).choose (i.val - j.val) : ℝ) /
        2 ^ (d - j.val) else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “shared core basis”; the hypotheses and conclusion in the code panel fix its exact scope. One finite core has the Bernstein basis pullback dictated by its bit.

theorem sharedCore_basis (d : ℕ) (bit : Bool) (i : Fin (d + 1)) (t : ℝ) :
    (∑ j : Fin (d + 1), sharedCore d bit i j * basis d j.val t) =
      basis d i.val (childCoordinate bit t) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “shared contract”. Backward finite-matrix contraction with the terminal coefficient-zero selector.

def sharedContract (d : ℕ) : List Bool → Fin (d + 1) → ℝ
  | [], i => if i.val = 0 then 1 else 0
  | bit :: bits, i => ∑ j : Fin (d + 1), sharedCore d bit i j * sharedContract d bits j

/-- All finite shared-core products, with arbitrary MSB-first suffix length. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “shared contract eq basis”; the hypotheses and conclusion in the code panel fix its exact scope. All finite shared-core products, with arbitrary MSB-first suffix length.

theorem sharedContract_eq_basis (d : ℕ) (bits : List Bool) (i : Fin (d + 1)) :
    sharedContract d bits i = basis d i.val (pathCoordinate bits 0) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “injected finite readout”. The restricted coefficient row contracted with the finite core matrices.

def injectedFiniteReadout (k : ℕ) (origin step : ℝ) (first : ℕ)
    (bits : List Bool) : ℝ :=
  ∑ i : Fin (2 * k + 1 + 1),
    restrictCoefficients (2 * k + 1)
      (1 + affinePoint origin step first)
      (1 + affinePoint origin step (first + 2 ^ bits.length))
      (sourceBernsteinCoefficient k) i.val * sharedContract (2 * k + 1) bits i

/-- Matrix-level finite restriction/suffix adapter, not an assumed contract. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “injected finite readout eq injected readout”; the hypotheses and conclusion in the code panel fix its exact scope. Matrix-level finite restriction/suffix adapter, not an assumed contract.

theorem injectedFiniteReadout_eq_injectedReadout (k : ℕ) (origin step : ℝ)
    (first : ℕ) (bits : List Bool) :
    injectedFiniteReadout k origin step first bits =
      injectedReadout k origin step first bits := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “injected finite readout eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem injectedFiniteReadout_eq (k : ℕ) (origin step : ℝ) (first : ℕ)
    (bits : List Bool) (hfirst : affinePoint origin step first ≠ 0) :
    injectedFiniteReadout k origin step first bits =
      (HermitePolynomial.sourceInterpolant k).eval
        (affinePoint origin step (first + wordValue bits)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary readout”. Follow one query path.

def boundaryReadout (k : ℕ) (origin step : ℝ) (lower upper first : ℕ)
    (bits : List Bool) : ℝ :=
  if Full lower upper first (2 ^ bits.length) then
    injectedReadout k origin step first bits
  else if Outside lower upper first (2 ^ bits.length) then 0
  else match bits with
    | [] => 0
    | bit :: rest => boundaryReadout k origin step lower upper
        (first + if bit then 2 ^ rest.length else 0) rest
termination_by bits.length

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary readout eq”; the hypotheses and conclusion in the code panel fix its exact scope. Exact traversal semantics.

theorem boundaryReadout_eq (k : ℕ) (origin step : ℝ) (lower upper : ℕ)
    (hvalid : ∀ j, lower ≤ j → j < upper → affinePoint origin step j ≠ 0)
    (first : ℕ) (bits : List Bool) :
    boundaryReadout k origin step lower upper first bits =
      if lower ≤ first + wordValue bits ∧ first + wordValue bits < upper then
        (HermitePolynomial.sourceInterpolant k).eval
          (affinePoint origin step (first + wordValue bits)) else 0 := by

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “injection bond”. One unresolved boundary scalar and one shared degree-sized coefficient row.

abbrev InjectionBond (k : ℕ) := Option (Fin (2 * k + 1 + 1))

/-- First integer index of the selected child; `r` is its remaining width. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “selected child”. First integer index of the selected child; 'r' is its remaining width.

def selectedChild (schedule : ℕ → ℕ) (r : ℕ) (bit : Bool) : ℕ :=
  schedule (r + 1) + if bit then 2 ^ r else 0

/-- Full-block injection parameters are exactly `u=1+origin+step*first` and
`v=1+origin+step*(first+2^r)`. This row has only `2*k+2` entries. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “block injection row”. Full-block injection parameters are exactly 'u=1+origin+step*first' and 'v=1+origin+step*(first+2^r)'.

def blockInjectionRow (k : ℕ) (origin step : ℝ) (first r : ℕ) :
    Fin (2 * k + 1 + 1) → ℝ :=
  fun i => restrictCoefficients (2 * k + 1)
    (1 + affinePoint origin step first)
    (1 + affinePoint origin step (first + 2 ^ r))
    (sourceBernsteinCoefficient k) i.val

/-- Actual finite core, with one shared boundary state at every level.
Rows are input states; columns are output states. No prefix-indexed space occurs. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “injection core”. Actual finite core, with one shared boundary state at every level.

def injectionCore (k : ℕ) (origin step : ℝ) (lower upper : ℕ)
    (schedule : ℕ → ℕ) (r : ℕ) (bit : Bool) :
    _root_.Matrix (InjectionBond k) (InjectionBond k) ℝ
  | none, none => if Partial lower upper (selectedChild schedule r bit) (2 ^ r) then 1 else 0
  | none, some j => if Full lower upper (selectedChild schedule r bit) (2 ^ r) then
      blockInjectionRow k origin step (selectedChild schedule r bit) r j else 0
  | some _, none => 0
  | some i, some j => sharedCore (2 * k + 1) bit i j

/-- Finite matrix contraction, terminating with the coefficient-zero selector.
The level is read from the suffix length, so every word shares one core sequence. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “injection contract”. Finite matrix contraction, terminating with the coefficient-zero selector.

def injectionContract (k : ℕ) (origin step : ℝ) (lower upper : ℕ)
    (schedule : ℕ → ℕ) : List Bool → InjectionBond k → ℝ
  | [], none => 0
  | [], some i => if i.val = 0 then 1 else 0
  | bit :: bits, i => ∑ j : InjectionBond k,
      injectionCore k origin step lower upper schedule bits.length bit i j *
        injectionContract k origin step lower upper schedule bits j

/-- After injection, the finite contraction never re-enters the boundary state. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “injection contract shared”; the hypotheses and conclusion in the code panel fix its exact scope. After injection, the finite contraction never re-enters the boundary state.

theorem injectionContract_shared (k : ℕ) (origin step : ℝ) (lower upper : ℕ)
    (schedule : ℕ → ℕ) (bits : List Bool) (i : Fin (2 * k + 1 + 1)) :
    injectionContract k origin step lower upper schedule bits (some i) =
      sharedContract (2 * k + 1) bits i := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “schedule valid”. The schedule obligation is purely integer control flow: any partial child must be the unique boundary node used by the next finite matrix.

def ScheduleValid (lower upper : ℕ) (schedule : ℕ → ℕ) (width : ℕ) : Prop :=
  ∀ r, r < width → ∀ bit,
    Partial lower upper (selectedChild schedule r bit) (2 ^ r) →
      schedule r = selectedChild schedule r bit

/-- Finite Option(Fin) contraction equals the verified tree traversal whenever
the current node is genuinely partial. There is no assumed source/core equality. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “injection contract boundary”; the hypotheses and conclusion in the code panel fix its exact scope. Finite Option(Fin) contraction equals the verified tree traversal whenever the current node is genuinely partial.

theorem injectionContract_boundary (k : ℕ) (origin step : ℝ) (lower upper : ℕ)
    (schedule : ℕ → ℕ) (bits : List Bool)
    (hnext : ScheduleValid lower upper schedule bits.length)
    (hp : Partial lower upper (schedule bits.length) (2 ^ bits.length)) :
    injectionContract k origin step lower upper schedule bits none =
      boundaryReadout k origin step lower upper (schedule bits.length) bits := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary schedule”. Closed-form boundary schedule, computed by a single integer quotient per level.

def boundarySchedule (lower r : ℕ) : ℕ := 2 ^ r * (lower / 2 ^ r)

commit-pinned source · Verso Blueprint panel

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

theorem boundarySchedule_child (lower r : ℕ) (bit : Bool) :
    selectedChild (boundarySchedule lower) r bit =
      2 ^ r * (2 * (lower / 2 ^ (r + 1)) + if bit then 1 else 0) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary schedule valid”; the hypotheses and conclusion in the code panel fix its exact scope. The upper-half interval makes the quotient schedule valid at every level.

theorem boundarySchedule_valid (lower n : ℕ) :
    ScheduleValid lower (2 ^ n) (boundarySchedule lower) (n + 1) := by

commit-pinned source · Verso Blueprint panel

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

theorem boundarySchedule_root (lower n : ℕ) (hl : lower ≤ 2 ^ n) :
    boundarySchedule lower (n + 1) = 0 := by

commit-pinned source · Verso Blueprint panel

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

theorem middle_root_partial (lower n : ℕ) (hl : lower < 2 ^ n) :
    Partial lower (2 ^ n) 0 (2 ^ (n + 1)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “partial left prefix eq”; the hypotheses and conclusion in the code panel fix its exact scope. A prefix interval '[0,upper)' has one unresolved aligned block as well.

theorem partial_left_prefix_eq (upper M x : ℕ) (hM : 0 < M)
    (hp : Partial 0 upper (M * x) M) : x = upper / M := by

commit-pinned source · Verso Blueprint panel

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

theorem boundarySchedule_left_valid (upper width : ℕ) :
    ScheduleValid 0 upper (boundarySchedule upper) width := by

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “scalar bond”. A scalar free branch needs only the boundary state and one shared state.

abbrev ScalarBond := Option Unit

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “scalar free contract”.

def scalarFreeContract (free : ℕ → Bool → ℝ) : List Bool → ℝ
  | [] => 1
  | bit :: bits => free bits.length bit * scalarFreeContract free bits

commit-pinned source · Verso Blueprint panel

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

def scalarCore (lower upper : ℕ) (schedule : ℕ → ℕ)
    (inject : ℕ → ℕ → ℝ) (free : ℕ → Bool → ℝ) (r : ℕ) (bit : Bool) :
    _root_.Matrix ScalarBond ScalarBond ℝ
  | none, none => if Partial lower upper (selectedChild schedule r bit) (2 ^ r) then 1 else 0
  | none, some _ => if Full lower upper (selectedChild schedule r bit) (2 ^ r) then
      inject (selectedChild schedule r bit) r else 0
  | some _, none => 0
  | some _, some _ => free r bit

commit-pinned source · Verso Blueprint panel

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

def scalarContract (lower upper : ℕ) (schedule : ℕ → ℕ)
    (inject : ℕ → ℕ → ℝ) (free : ℕ → Bool → ℝ) : List Bool → ScalarBond → ℝ
  | [], none => 0
  | [], some _ => 1
  | bit :: bits, i => ∑ j : ScalarBond,
      scalarCore lower upper schedule inject free bits.length bit i j *
        scalarContract lower upper schedule inject free bits j

commit-pinned source · Verso Blueprint panel

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

theorem scalarContract_shared (lower upper : ℕ) (schedule : ℕ → ℕ)
    (inject : ℕ → ℕ → ℝ) (free : ℕ → Bool → ℝ) (bits : List Bool) :
    scalarContract lower upper schedule inject free bits (some ()) =
      scalarFreeContract free bits := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “scalar boundary readout”.

def scalarBoundaryReadout (lower upper : ℕ) (inject : ℕ → ℕ → ℝ)
    (free : ℕ → Bool → ℝ) (first : ℕ) (bits : List Bool) : ℝ :=
  if Full lower upper first (2 ^ bits.length) then
    inject first bits.length * scalarFreeContract free bits
  else if Outside lower upper first (2 ^ bits.length) then 0
  else match bits with
    | [] => 0
    | bit :: rest => scalarBoundaryReadout lower upper inject free
        (first + if bit then 2 ^ rest.length else 0) rest
termination_by bits.length

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar boundary readout eq”; the hypotheses and conclusion in the code panel fix its exact scope. A generic scalar source bridge, consumed below with a proved exponential suffix identity.

theorem scalarBoundaryReadout_eq (lower upper : ℕ) (inject : ℕ → ℕ → ℝ)
    (free : ℕ → Bool → ℝ) (target : ℕ → ℝ)
    (hinject : ∀ first bits, inject first bits.length * scalarFreeContract free bits =
      target (first + wordValue bits)) (first : ℕ) (bits : List Bool) :
    scalarBoundaryReadout lower upper inject free first bits =
      if lower ≤ first + wordValue bits ∧ first + wordValue bits < upper then
        target (first + wordValue bits) else 0 := by

commit-pinned source · Verso Blueprint panel

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

theorem scalarContract_boundary (lower upper : ℕ) (schedule : ℕ → ℕ)
    (inject : ℕ → ℕ → ℝ) (free : ℕ → Bool → ℝ) (bits : List Bool)
    (hnext : ScheduleValid lower upper schedule bits.length)
    (hp : Partial lower upper (schedule bits.length) (2 ^ bits.length)) :
    scalarContract lower upper schedule inject free bits none =
      scalarBoundaryReadout lower upper inject free (schedule bits.length) bits := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “left free”. Stable left-tail factors use only nonpositive exponential arguments for positive step.

def leftFree (step : ℝ) (r : ℕ) (bit : Bool) : ℝ :=
  if bit then 1 else Real.exp (-step * 2 ^ r)

commit-pinned source · Verso Blueprint panel

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

def leftInject (origin step : ℝ) (first r : ℕ) : ℝ :=
  Real.exp (affinePoint origin step first + step * (2 ^ r - 1))

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left free contract eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem leftFreeContract_eq (step : ℝ) (bits : List Bool) :
    scalarFreeContract (leftFree step) bits =
      Real.exp (-step * (2 ^ bits.length - 1 - (wordValue bits : ℝ))) := by

commit-pinned source · Verso Blueprint panel

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

theorem leftInject_readout (origin step : ℝ) (first : ℕ) (bits : List Bool) :
    leftInject origin step first bits.length * scalarFreeContract (leftFree step) bits =
      Real.exp (affinePoint origin step (first + wordValue bits)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left inject eq last”; the hypotheses and conclusion in the code panel fix its exact scope. Exact correspondence with the prototype's last included block index.

theorem leftInject_eq_last (origin step : ℝ) (first r : ℕ) :
    leftInject origin step first r =
      Real.exp (affinePoint origin step (first + 2 ^ r - 1)) := by

commit-pinned source · Verso Blueprint panel

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

theorem leftFree_bounds (step : ℝ) (hs : 0 ≤ step) (r : ℕ) (bit : Bool) :
    0 ≤ leftFree step r bit ∧ leftFree step r bit ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “grid step”. The exact grid step on 'n+1' qubits; 'n' may be zero.

def gridStep (n : ℕ) (L : ℝ) : ℝ :=
  2 * Real.pi * L / (gridSize (n + 1) : ℝ)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “grid point nat”.

def gridPointNat (n : ℕ) (L : ℝ) (j : ℕ) : ℝ :=
  affinePoint (-Real.pi * L) (gridStep n L) j

commit-pinned source · Verso Blueprint panel

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

theorem gridStep_pos (n : ℕ) (L : ℝ) (hL : 0 < L) : 0 < gridStep n L := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid point nat eq grid point”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem gridPointNat_eq_gridPoint (n : ℕ) (L : ℝ) (j : Fin (gridSize (n + 1))) :
    gridPointNat n L j = HermiteStatePreparation.gridPoint (n + 1) L j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid point nat midpoint”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem gridPointNat_midpoint (n : ℕ) (L : ℝ) :
    gridPointNat n L (2 ^ n) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid point nat strict mono”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem gridPointNat_strictMono (n : ℕ) (L : ℝ) (hL : 0 < L) :
    StrictMono (gridPointNat n L) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid point nat lt zero iff”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem gridPointNat_lt_zero_iff (n : ℕ) (L : ℝ) (hL : 0 < L) (j : ℕ) :
    gridPointNat n L j < 0 ↔ j < 2 ^ n := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cut index”. Natural ceiling implements the lower clamp at zero.

def cutIndex (n : ℕ) (L : ℝ) : ℕ :=
  Nat.ceil ((-1 - (-Real.pi * L)) / gridStep n L)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid point nat lt neg one iff”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem gridPointNat_lt_neg_one_iff (n : ℕ) (L : ℝ) (hL : 0 < L) (j : ℕ) :
    gridPointNat n L j < -1 ↔ j < cutIndex n L :=
  HermiteCutRank.affine_lt_cut (-Real.pi * L) (gridStep n L) (-1)
    (gridStep_pos n L hL) j

commit-pinned source · Verso Blueprint panel

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

theorem cutIndex_le_midpoint (n : ℕ) (L : ℝ) (hL : 0 < L) :
    cutIndex n L ≤ 2 ^ n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cut index eq clamped”; the hypotheses and conclusion in the code panel fix its exact scope. This is the candidate's exact clamped ceiling, before any rounding of pi.

theorem cutIndex_eq_clamped (n : ℕ) (L : ℝ) (hL : 0 < L) :
    cutIndex n L = min
      (Nat.ceil ((2 ^ n : ℕ) - (gridSize (n + 1) : ℝ) / (2 * Real.pi * L)))
      (2 ^ n) := by

commit-pinned source · Verso Blueprint panel

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

theorem middle_membership_iff (n : ℕ) (L : ℝ) (hL : 0 < L) (j : ℕ) :
    (cutIndex n L ≤ j ∧ j < 2 ^ n) ↔
      (-1 ≤ gridPointNat n L j ∧ gridPointNat n L j < 0) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “injection domain”; the hypotheses and conclusion in the code panel fix its exact scope. Every actual injected dyadic block has valid de Casteljau parameters, including a block whose excluded endpoint is the zero-coordinate midpoint.

theorem injection_domain (n : ℕ) (L : ℝ) (hL : 0 < L) (first size : ℕ)
    (hs : 0 < size) (hf : Full (cutIndex n L) (2 ^ n) first size) :
    0 ≤ 1 + gridPointNat n L first ∧
      1 + gridPointNat n L first < 1 + gridPointNat n L (first + size) ∧
      1 + gridPointNat n L (first + size) ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “middle readout”. The middle component uses the same one-boundary traversal as the prototype.

def middleReadout (k n : ℕ) (L : ℝ) (bits : List Bool) : ℝ :=
  boundaryReadout k (-Real.pi * L) (gridStep n L) (cutIndex n L) (2 ^ n) 0 bits

commit-pinned source · Verso Blueprint panel

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

theorem middleReadout_eq (k n : ℕ) (L : ℝ) (hL : 0 < L) (bits : List Bool) :
    middleReadout k n L bits =
      if -1 ≤ gridPointNat n L (wordValue bits) ∧
          gridPointNat n L (wordValue bits) < 0 then
        (HermitePolynomial.sourceInterpolant k).eval
          (gridPointNat n L (wordValue bits)) else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “middle readout empty”; the hypotheses and conclusion in the code panel fix its exact scope. A cutoff at the midpoint gives the prototype's zero middle component.

theorem middleReadout_empty (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (hcut : cutIndex n L = 2 ^ n) (bits : List Bool) :
    middleReadout k n L bits = 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “word sample index”. Word-to-public-grid adapter, with explicit width equality.

def wordSampleIndex (n : ℕ) (bits : List Bool) (hbits : bits.length = n + 1) :
    Fin (gridSize (n + 1)) :=
  ⟨wordValue bits, by simpa only [gridSize, ← hbits] using wordValue_lt bits⟩

/-- All-bit exact source readout on the actual public sample API. The center
belongs to the right tail, while the sample at `p=-1` belongs to this component. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “middle readout eq masked sample”; the hypotheses and conclusion in the code panel fix its exact scope. All-bit exact source readout on the actual public sample API.

theorem middleReadout_eq_masked_sample (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (bits : List Bool) (hbits : bits.length = n + 1) :
    middleReadout k n L bits =
      if cutIndex n L ≤ wordValue bits ∧ wordValue bits < 2 ^ n then
        HermiteStatePreparation.sampledAmplitude k (n + 1) L
          (wordSampleIndex n bits hbits) else 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “middle finite readout”. The exact finite middle TT, including the prototype's empty-interval fast path.

def middleFiniteReadout (k n : ℕ) (L : ℝ) (bits : List Bool) : ℝ :=
  if cutIndex n L = 2 ^ n then 0 else
    injectionContract k (-Real.pi * L) (gridStep n L) (cutIndex n L) (2 ^ n)
      (boundarySchedule (cutIndex n L)) bits none

/-- Source-derived one-boundary finite TT equals the verified interval traversal. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “middle finite readout eq middle readout”; the hypotheses and conclusion in the code panel fix its exact scope. Source-derived one-boundary finite TT equals the verified interval traversal.

theorem middleFiniteReadout_eq_middleReadout (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (bits : List Bool) (hbits : bits.length = n + 1) :
    middleFiniteReadout k n L bits = middleReadout k n L bits := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “middle finite readout eq masked sample”; the hypotheses and conclusion in the code panel fix its exact scope. Complete all-bit, actual-grid semantics of the finite middle TT.

theorem middleFiniteReadout_eq_masked_sample (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (bits : List Bool) (hbits : bits.length = n + 1) :
    middleFiniteReadout k n L bits =
      if cutIndex n L ≤ wordValue bits ∧ wordValue bits < 2 ^ n then
        HermiteStatePreparation.sampledAmplitude k (n + 1) L
          (wordSampleIndex n bits hbits) else 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “left finite readout”.

def leftFiniteReadout (n : ℕ) (L : ℝ) (bits : List Bool) : ℝ :=
  if cutIndex n L = 0 then 0 else
    scalarContract 0 (cutIndex n L) (boundarySchedule (cutIndex n L))
      (leftInject (-Real.pi * L) (gridStep n L)) (leftFree (gridStep n L)) bits none

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left finite readout eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem leftFiniteReadout_eq (n : ℕ) (L : ℝ) (hL : 0 < L)
    (bits : List Bool) (hbits : bits.length = n + 1) :
    leftFiniteReadout n L bits = if wordValue bits < cutIndex n L then
      Real.exp (gridPointNat n L (wordValue bits)) else 0 := by

commit-pinned source · Verso Blueprint panel

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

theorem leftInject_bounds (n : ℕ) (L : ℝ) (hL : 0 < L) (first r : ℕ)
    (hf : Full 0 (cutIndex n L) first (2 ^ r)) :
    0 ≤ leftInject (-Real.pi * L) (gridStep n L) first r ∧
      leftInject (-Real.pi * L) (gridStep n L) first r ≤ 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left finite readout eq masked sample”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem leftFiniteReadout_eq_masked_sample (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (bits : List Bool) (hbits : bits.length = n + 1) :
    leftFiniteReadout n L bits = if wordValue bits < cutIndex n L then
      HermiteStatePreparation.sampledAmplitude k (n + 1) L
        (wordSampleIndex n bits hbits) else 0 := by

commit-pinned source · Verso Blueprint panel

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

def rightFree (step : ℝ) (r : ℕ) (bit : Bool) : ℝ :=
  if bit then Real.exp (-step * 2 ^ r) else 1

commit-pinned source · Verso Blueprint panel

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

theorem rightFree_bounds (step : ℝ) (hs : 0 ≤ step) (r : ℕ) (bit : Bool) :
    0 ≤ rightFree step r bit ∧ rightFree step r bit ≤ 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “right free contract eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rightFreeContract_eq (step : ℝ) (bits : List Bool) :
    scalarFreeContract (rightFree step) bits =
      Real.exp (-step * (wordValue bits : ℝ)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “right core”. Rank-one right component: the first MSB selects the right half; subsequent bits use bounded negative exponential factors.

def rightCore (n : ℕ) (step : ℝ) (r : ℕ) (bit : Bool) : ℝ :=
  if r = n then (if bit then 1 else 0) else rightFree step r bit

commit-pinned source · Verso Blueprint panel

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

theorem rightCore_suffix (n : ℕ) (step : ℝ) (bits : List Bool)
    (hlen : bits.length ≤ n) :
    scalarFreeContract (rightCore n step) bits =
      scalarFreeContract (rightFree step) bits := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “right finite readout”.

def rightFiniteReadout (n : ℕ) (L : ℝ) (bits : List Bool) : ℝ :=
  scalarFreeContract (rightCore n (gridStep n L)) bits

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “right finite readout eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rightFiniteReadout_eq (n : ℕ) (L : ℝ) (bits : List Bool)
    (hbits : bits.length = n + 1) :
    rightFiniteReadout n L bits = if wordValue bits < 2 ^ n then 0 else
      Real.exp (-gridPointNat n L (wordValue bits)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “right finite readout eq masked sample”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rightFiniteReadout_eq_masked_sample (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (bits : List Bool) (hbits : bits.length = n + 1) :
    rightFiniteReadout n L bits = if wordValue bits < 2 ^ n then 0 else
      HermiteStatePreparation.sampledAmplitude k (n + 1) L
        (wordSampleIndex n bits hbits) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “three branch readout eq sample”; the hypotheses and conclusion in the code panel fix its exact scope. Exact three-component source action.

theorem threeBranchReadout_eq_sample (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (bits : List Bool) (hbits : bits.length = n + 1) :
    leftFiniteReadout n L bits + middleFiniteReadout k n L bits +
      rightFiniteReadout n L bits =
        HermiteStatePreparation.sampledAmplitude k (n + 1) L
          (wordSampleIndex n bits hbits) := by

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “kernel”. A common fixed-bond kernel interface.

abbrev Kernel (B : Type*) := ℕ → Bool → _root_.Matrix B B ℝ

commit-pinned source · Verso Blueprint panel

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

def kernelContract {B : Type*} [Fintype B] (K : Kernel B) (right : B → ℝ) :
    List Bool → B → ℝ
  | [], i => right i
  | bit :: bits, i => ∑ j : B, K bits.length bit i j * kernelContract K right bits j

commit-pinned source · Verso Blueprint panel

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

def kernelAmplitude {B : Type*} [Fintype B] (K : Kernel B) (left right : B → ℝ)
    (bits : List Bool) : ℝ := ∑ i : B, left i * kernelContract K right bits i

commit-pinned source · Verso Blueprint panel

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

def sumKernel {B C : Type*} (K : Kernel B) (H : Kernel C) : Kernel (Sum B C) :=
  fun r bit i j => match i, j with
    | .inl a, .inl b => K r bit a b
    | .inr a, .inr b => H r bit a b
    | _, _ => 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “kernel contract sum inl”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem kernelContract_sum_inl {B C : Type*} [Fintype B] [Fintype C]
    (K : Kernel B) (H : Kernel C) (right : B → ℝ) (last : C → ℝ)
    (bits : List Bool) (i : B) :
    kernelContract (sumKernel K H) (Sum.elim right last) bits (.inl i) =
      kernelContract K right bits i := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “kernel contract sum inr”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem kernelContract_sum_inr {B C : Type*} [Fintype B] [Fintype C]
    (K : Kernel B) (H : Kernel C) (right : B → ℝ) (last : C → ℝ)
    (bits : List Bool) (i : C) :
    kernelContract (sumKernel K H) (Sum.elim right last) bits (.inr i) =
      kernelContract H last bits i := by

commit-pinned source · Verso Blueprint panel

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

theorem kernelAmplitude_sum {B C : Type*} [Fintype B] [Fintype C]
    (K : Kernel B) (H : Kernel C) (left right : B → ℝ) (first last : C → ℝ)
    (bits : List Bool) :
    kernelAmplitude (sumKernel K H) (Sum.elim left first) (Sum.elim right last) bits =
      kernelAmplitude K left right bits + kernelAmplitude H first last bits := by

commit-pinned source · Verso Blueprint panel

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

def injectionTerminal (k : ℕ) : InjectionBond k → ℝ
  | none => 0
  | some i => if i.val = 0 then 1 else 0

commit-pinned source · Verso Blueprint panel

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

def scalarTerminal : ScalarBond → ℝ
  | none => 0
  | some _ => 1

commit-pinned source · Verso Blueprint panel

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

theorem kernelContract_injection (k : ℕ) (origin step : ℝ) (lower upper : ℕ)
    (schedule : ℕ → ℕ) (bits : List Bool) (i : InjectionBond k) :
    kernelContract (injectionCore k origin step lower upper schedule)
      (injectionTerminal k) bits i =
        injectionContract k origin step lower upper schedule bits i := by

commit-pinned source · Verso Blueprint panel

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

theorem kernelContract_scalar (lower upper : ℕ) (schedule : ℕ → ℕ)
    (inject : ℕ → ℕ → ℝ) (free : ℕ → Bool → ℝ) (bits : List Bool) (i : ScalarBond) :
    kernelContract (scalarCore lower upper schedule inject free) scalarTerminal bits i =
      scalarContract lower upper schedule inject free bits i := by

commit-pinned source · Verso Blueprint panel

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

theorem kernelContract_unit (free : ℕ → Bool → ℝ) (bits : List Bool) (i : Unit) :
    kernelContract (fun r bit (_ _ : Unit) => free r bit) (fun _ => 1) bits i =
      scalarFreeContract free bits := by

commit-pinned source · Verso Blueprint panel

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

def leftKernel (n : ℕ) (L : ℝ) : Kernel ScalarBond :=
  scalarCore 0 (cutIndex n L) (boundarySchedule (cutIndex n L))
    (leftInject (-Real.pi * L) (gridStep n L)) (leftFree (gridStep n L))

commit-pinned source · Verso Blueprint panel

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

def middleKernel (k n : ℕ) (L : ℝ) : Kernel (InjectionBond k) :=
  injectionCore k (-Real.pi * L) (gridStep n L) (cutIndex n L) (2 ^ n)
    (boundarySchedule (cutIndex n L))

commit-pinned source · Verso Blueprint panel

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

def rightKernel (n : ℕ) (L : ℝ) : Kernel Unit :=
  fun r bit _ _ => rightCore n (gridStep n L) r bit

commit-pinned source · Verso Blueprint panel

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

def leftInitial (n : ℕ) (L : ℝ) : ScalarBond → ℝ
  | none => if cutIndex n L = 0 then 0 else 1
  | some _ => 0

commit-pinned source · Verso Blueprint panel

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

def middleInitial (k n : ℕ) (L : ℝ) : InjectionBond k → ℝ
  | none => if cutIndex n L = 2 ^ n then 0 else 1
  | some _ => 0

commit-pinned source · Verso Blueprint panel

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

theorem kernelAmplitude_left (n : ℕ) (L : ℝ) (bits : List Bool) :
    kernelAmplitude (leftKernel n L) (leftInitial n L) scalarTerminal bits =
      leftFiniteReadout n L bits := by

commit-pinned source · Verso Blueprint panel

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

theorem kernelAmplitude_middle (k n : ℕ) (L : ℝ) (bits : List Bool) :
    kernelAmplitude (middleKernel k n L) (middleInitial k n L) (injectionTerminal k) bits =
      middleFiniteReadout k n L bits := by

commit-pinned source · Verso Blueprint panel

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

theorem kernelAmplitude_right (n : ℕ) (L : ℝ) (bits : List Bool) :
    kernelAmplitude (rightKernel n L) (fun _ => 1) (fun _ => 1) bits =
      rightFiniteReadout n L bits := by

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “hermite finite bond”. One fixed direct-sum bond, with no state allocated per dyadic prefix.

abbrev HermiteFiniteBond (k : ℕ) := Sum ScalarBond (Sum (InjectionBond k) Unit)

commit-pinned source · Verso Blueprint panel

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

def hermiteKernel (k n : ℕ) (L : ℝ) : Kernel (HermiteFiniteBond k) :=
  sumKernel (leftKernel n L) (sumKernel (middleKernel k n L) (rightKernel n L))

commit-pinned source · Verso Blueprint panel

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

def hermiteInitial (k n : ℕ) (L : ℝ) : HermiteFiniteBond k → ℝ :=
  Sum.elim (leftInitial n L) (Sum.elim (middleInitial k n L) (fun _ => 1))

commit-pinned source · Verso Blueprint panel

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

def hermiteTerminal (k : ℕ) : HermiteFiniteBond k → ℝ :=
  Sum.elim scalarTerminal (Sum.elim (injectionTerminal k) (fun _ => 1))

/-- Main exact real-algebra root: one formula-derived fixed-width kernel family
and explicit left/right boundaries produce every literal Hermite sample. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hermite kernel eq sample”; the hypotheses and conclusion in the code panel fix its exact scope. Main exact real-algebra root: one formula-derived fixed-width kernel family and explicit left/right boundaries produce every literal Hermite sample.

theorem hermiteKernel_eq_sample (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (bits : List Bool) (hbits : bits.length = n + 1) :
    kernelAmplitude (hermiteKernel k n L) (hermiteInitial k n L) (hermiteTerminal k) bits =
      HermiteStatePreparation.sampledAmplitude k (n + 1) L
        (wordSampleIndex n bits hbits) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hermite finite bond card”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hermiteFiniteBond_card (k : ℕ) :
    Fintype.card (HermiteFiniteBond k) = 2 * k + 6 := by

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “hermite core address”. Address space of the actual two-slice cores on 'n+1' qubits.

abbrev HermiteCoreAddress (k n : ℕ) :=
  Fin (n + 1) × Bool × HermiteFiniteBond k × HermiteFiniteBond k

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hermite core entry”.

def hermiteCoreEntry (k n : ℕ) (L : ℝ) (a : HermiteCoreAddress k n) : ℝ :=
  hermiteKernel k n L (n - a.1.val) a.2.1 a.2.2.1 a.2.2.2

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hermite core address card”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hermiteCoreAddress_card (k n : ℕ) :
    Fintype.card (HermiteCoreAddress k n) = 2 * (n + 1) * (2 * k + 6) ^ 2 := by

commit-pinned source · Verso Blueprint panel

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

theorem injectionBond_card (k : ℕ) : Fintype.card (InjectionBond k) = 2 * k + 3 := by

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “middle bond”. Candidate middle register: one boundary scalar plus the shared coefficients.

abbrev MiddleBond (k : ℕ) := Option (Fin (2 * k + 2))

commit-pinned source · Verso Blueprint panel

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

theorem middleBond_card (k : ℕ) : Fintype.card (MiddleBond k) = 2 * k + 3 := by

commit-pinned source · Verso Blueprint panel