10.60. QuantumBlockEncoding/StoredHermiteChildGeometry.lean🔗

24 explicit public declarations, in source order.

Definition10.60.1

uses 0used by 0✓L∃∀N

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

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. structure.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:19. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.60.1●1 definition

structure(2 fields)defined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

structure QuantumBlockEncoding.StoredHermiteChildGeometry.Flags : Type

structure QuantumBlockEncoding.StoredHermiteChildGeometry.Flags :
  Type

Fields

full : Bool

isPartial : Bool

Definition10.60.2

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Four actual integer comparisons; 'last' is the excluded integer endpoint.

Declaration kind. def.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:24. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.60.2●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

def QuantumBlockEncoding.StoredHermiteChildGeometry.flags
  (lower upper first last : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    QuantumBlockEncoding.StoredHermiteChildGeometry.Flags

def QuantumBlockEncoding.StoredHermiteChildGeometry.flags
  (lower upper first last : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    QuantumBlockEncoding.StoredHermiteChildGeometry.Flags

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

Theorem10.60.3

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:32. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

Theorem10.60.4

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:36. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.4●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

Theorem10.60.5

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:42. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.5●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

Definition10.60.6

uses 0used by 0✓L∃∀N

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

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. structure.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:47. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.60.6●1 definition

structure(7 fields)defined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

structure QuantumBlockEncoding.StoredHermiteChildGeometry.Child : Type

structure QuantumBlockEncoding.StoredHermiteChildGeometry.Child :
  Type

Fields

first : ℕ

lower : ℝ

upper : ℝ

leftFull : Bool

leftPartial : Bool

middleFull : Bool

middlePartial : Bool

Definition10.60.7

uses 0used by 0✓L∃∀N

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

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. structure.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:56. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.60.7●1 definition

structure(2 fields)defined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

structure QuantumBlockEncoding.StoredHermiteChildGeometry.ChildRun (α : Type) :
  Type

structure QuantumBlockEncoding.StoredHermiteChildGeometry.ChildRun
  (α : Type) : Type

Fields

run : QuantumBlockEncoding.StoredGivens.Run α

integerAdditions : ℕ

Definition10.60.8

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:60. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.60.8●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

def QuantumBlockEncoding.StoredHermiteChildGeometry.child
  (parent : QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) (bit : Bool) :
  QuantumBlockEncoding.StoredHermiteChildGeometry.ChildRun
    QuantumBlockEncoding.StoredHermiteChildGeometry.Child

def QuantumBlockEncoding.StoredHermiteChildGeometry.child
  (parent :
    QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) (bit : Bool) :
  QuantumBlockEncoding.StoredHermiteChildGeometry.ChildRun
    QuantumBlockEncoding.StoredHermiteChildGeometry.Child

Theorem10.60.9

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:81. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

Theorem10.60.10

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:87. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

Theorem10.60.11

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:93. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

Theorem10.60.12

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:98. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.child_flags
  (parent : QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) (bit : Bool) :
  have c :=
    (QuantumBlockEncoding.StoredHermiteChildGeometry.child parent level
          span cut midpoint bit).run.value;
  c.leftFull =
      decide
        (QuantumBlockEncoding.HermiteBoundaryInjection.Full 0 cut
          c.first span) ∧
    c.leftPartial =
        decide
          (QuantumBlockEncoding.HermiteBoundaryInjection.Partial 0 cut
            c.first span) ∧
      c.middleFull =
          decide
            (QuantumBlockEncoding.HermiteBoundaryInjection.Full cut
              midpoint c.first span) ∧
        c.middlePartial =
          decide
            (QuantumBlockEncoding.HermiteBoundaryInjection.Partial cut
              midpoint c.first span)

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.child_flags
  (parent :
    QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) (bit : Bool) :
  have c :=
    (QuantumBlockEncoding.StoredHermiteChildGeometry.child
          parent level span cut midpoint
          bit).run.value;
  c.leftFull =
      decide
        (QuantumBlockEncoding.HermiteBoundaryInjection.Full
          0 cut c.first span) ∧
    c.leftPartial =
        decide
          (QuantumBlockEncoding.HermiteBoundaryInjection.Partial
            0 cut c.first span) ∧
      c.middleFull =
          decide
            (QuantumBlockEncoding.HermiteBoundaryInjection.Full
              cut midpoint c.first span) ∧
        c.middlePartial =
          decide
            (QuantumBlockEncoding.HermiteBoundaryInjection.Partial
              cut midpoint c.first span)

Theorem10.60.13

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:109. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

Theorem10.60.14

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:117. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.14●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

Theorem10.60.15

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Value-only specification: all cached-data hypotheses are explicit.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:122. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

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

Definition10.60.16

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. False/true children are computed once each, then stored in this order.

Declaration kind. def.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:157. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.60.16●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

def QuantumBlockEncoding.StoredHermiteChildGeometry.children
  (parent : QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) :
  QuantumBlockEncoding.StoredHermiteChildGeometry.ChildRun
    (Vector QuantumBlockEncoding.StoredHermiteChildGeometry.Child 2)

def QuantumBlockEncoding.StoredHermiteChildGeometry.children
  (parent :
    QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) :
  QuantumBlockEncoding.StoredHermiteChildGeometry.ChildRun
    (Vector
      QuantumBlockEncoding.StoredHermiteChildGeometry.Child
      2)

False/true children are computed once each, then stored in this order.

Theorem10.60.17

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:167. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.17●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_value
  (parent : QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) (bit : Bool) :
  (QuantumBlockEncoding.StoredHermiteChildGeometry.children parent level
            span cut midpoint).run.value[if bit = true then 1 else 0] =
    (QuantumBlockEncoding.StoredHermiteChildGeometry.child parent level
          span cut midpoint bit).run.value

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_value
  (parent :
    QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) (bit : Bool) :
  (QuantumBlockEncoding.StoredHermiteChildGeometry.children
            parent level span cut
            midpoint).run.value[if
          bit = true then 1
      else 0] =
    (QuantumBlockEncoding.StoredHermiteChildGeometry.child
          parent level span cut midpoint
          bit).run.value

Theorem10.60.18

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:173. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.18●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

Theorem10.60.19

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:181. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.19●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_integerAdditions
  (parent : QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) :
  (QuantumBlockEncoding.StoredHermiteChildGeometry.children parent level
        span cut midpoint).integerAdditions =
    4

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_integerAdditions
  (parent :
    QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) :
  (QuantumBlockEncoding.StoredHermiteChildGeometry.children
        parent level span cut
        midpoint).integerAdditions =
    4

Theorem10.60.20

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Fixed charged work for both children; integer additions remain separate.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:186. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.20●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_total_cost
  (parent : QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) :
  ∑ op,
      (QuantumBlockEncoding.StoredHermiteChildGeometry.children parent
              level span cut midpoint).run.cost
        op =
    70

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_total_cost
  (parent :
    QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint : ℕ) :
  ∑ op,
      (QuantumBlockEncoding.StoredHermiteChildGeometry.children
              parent level span cut
              midpoint).run.cost
        op =
    70

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

Definition10.60.21

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:194. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.60.21●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

def QuantumBlockEncoding.StoredHermiteChildGeometry.Refines
  (c : QuantumBlockEncoding.StoredHermiteChildGeometry.Child)
  (cut n r : ℕ) (origin grid : ℝ) (bit : Bool) : Prop

def QuantumBlockEncoding.StoredHermiteChildGeometry.Refines
  (c :
    QuantumBlockEncoding.StoredHermiteChildGeometry.Child)
  (cut n r : ℕ) (origin grid : ℝ)
  (bit : Bool) : Prop

Theorem10.60.22

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:203. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.22●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_refines
  (parent : QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint n r : ℕ) (origin grid : ℝ) (bit : Bool)
  (hp :
    parent.first =
      QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule cut
        (r + 1))
  (hl :
    parent.lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        grid parent.first)
  (hw : level.width = grid * 2 ^ r) (hs : span = 2 ^ r)
  (hm : midpoint = 2 ^ n) :
  QuantumBlockEncoding.StoredHermiteChildGeometry.Refines
    (QuantumBlockEncoding.StoredHermiteChildGeometry.children parent
            level span cut
            midpoint).run.value[if bit = true then 1 else 0]
    cut n r origin grid bit

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_refines
  (parent :
    QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint n r : ℕ)
  (origin grid : ℝ) (bit : Bool)
  (hp :
    parent.first =
      QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        cut (r + 1))
  (hl :
    parent.lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin grid parent.first)
  (hw : level.width = grid * 2 ^ r)
  (hs : span = 2 ^ r)
  (hm : midpoint = 2 ^ n) :
  QuantumBlockEncoding.StoredHermiteChildGeometry.Refines
    (QuantumBlockEncoding.StoredHermiteChildGeometry.children
            parent level span cut
            midpoint).run.value[if
          bit = true then 1
      else 0]
    cut n r origin grid bit

Theorem10.60.23

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Refinement and charged work belong to the same pair-producing run.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:215. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.23●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_certified
  (parent : QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint n r : ℕ) (origin grid : ℝ)
  (hp :
    parent.first =
      QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule cut
        (r + 1))
  (hl :
    parent.lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        grid parent.first)
  (hw : level.width = grid * 2 ^ r) (hs : span = 2 ^ r)
  (hm : midpoint = 2 ^ n) :
  have result :=
    QuantumBlockEncoding.StoredHermiteChildGeometry.children parent
      level span cut midpoint;
  (∀ (bit : Bool),
      QuantumBlockEncoding.StoredHermiteChildGeometry.Refines
        result.run.value[if bit = true then 1 else 0] cut n r origin
        grid bit) ∧
    ∑ op, result.run.cost op = 70 ∧ result.integerAdditions = 4

theorem QuantumBlockEncoding.StoredHermiteChildGeometry.children_certified
  (parent :
    QuantumBlockEncoding.StoredBinaryCoordinates.Point)
  (level :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (span cut midpoint n r : ℕ)
  (origin grid : ℝ)
  (hp :
    parent.first =
      QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        cut (r + 1))
  (hl :
    parent.lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin grid parent.first)
  (hw : level.width = grid * 2 ^ r)
  (hs : span = 2 ^ r)
  (hm : midpoint = 2 ^ n) :
  have result :=
    QuantumBlockEncoding.StoredHermiteChildGeometry.children
      parent level span cut midpoint;
  (∀ (bit : Bool),
      QuantumBlockEncoding.StoredHermiteChildGeometry.Refines
        result.run.value[if
              bit = true then 1
          else 0]
        cut n r origin grid bit) ∧
    ∑ op, result.run.cost op = 70 ∧
      result.integerAdditions = 4

Refinement and charged work belong to the same pair-producing run.

Theorem10.60.24

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. With legal source indices, every generated endpoint fits in n+2 bits. This states a word-size requirement, not the cost of implementing word arithmetic.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteChildGeometry.lean:230. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.60.24●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteChildGeometry.lean

complete

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

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

With legal source indices, every generated endpoint fits in n+2 bits.
This states a word-size requirement, not the cost of implementing word arithmetic.