6.7. QuantumBlockEncoding/PrimitiveRefinement.lean🔗

5 explicit public declarations, in source order.

Definition6.7.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “primitive program refinement”. A proposition-valued field is a requirement until a constructor supplies it. Exact refinement for a primitive program, including its declared global phase.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Exact refinement for a primitive program, including its declared global phase. This is the acceptance record used by phase-sensitive macro compilers.

Declaration kind. structure.

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

Lean code for Definition6.7.1●1 definition

structure(3 fields)defined in QuantumBlockEncoding/PrimitiveRefinement.lean

complete

structure QuantumBlockEncoding.PrimitiveProgramRefinement (qubits : ℕ) : Type

structure QuantumBlockEncoding.PrimitiveProgramRefinement
  (qubits : ℕ) : Type

Exact refinement for a primitive program, including its declared global
phase. This is the acceptance record used by phase-sensitive macro compilers.

Fields

program : QuantumBlockEncoding.PrimitiveProgram qubits

target : Matrix (QuantumBlockEncoding.PrimitiveBasis qubits) (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

exact : QuantumBlockEncoding.evalPrimitiveProgram self.program = self.target

Definition6.7.2

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/PrimitiveRefinement.lean:20. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.7.2●1 definition

defdefined in QuantumBlockEncoding/PrimitiveRefinement.lean

complete

def QuantumBlockEncoding.PrimitiveProgramRefinement.resource {qubits : ℕ}
  (refinement :
    QuantumBlockEncoding.PrimitiveProgramRefinement qubits) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.PrimitiveProgramRefinement.resource
  {qubits : ℕ}
  (refinement :
    QuantumBlockEncoding.PrimitiveProgramRefinement
      qubits) :
  QuantumBlockEncoding.Resource

Theorem6.7.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “oracle calls eq zero”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/PrimitiveRefinement.lean:24. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.7.3●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRefinement.lean

complete

theorem QuantumBlockEncoding.PrimitiveProgramRefinement.oracleCalls_eq_zero
  {qubits : ℕ}
  (refinement :
    QuantumBlockEncoding.PrimitiveProgramRefinement qubits) :
  refinement.resource.oracleCalls = 0

theorem QuantumBlockEncoding.PrimitiveProgramRefinement.oracleCalls_eq_zero
  {qubits : ℕ}
  (refinement :
    QuantumBlockEncoding.PrimitiveProgramRefinement
      qubits) :
  refinement.resource.oracleCalls = 0

Definition6.7.4

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/PrimitiveRefinement.lean:29. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.7.4●1 definition

defdefined in QuantumBlockEncoding/PrimitiveRefinement.lean

complete

def QuantumBlockEncoding.PrimitiveRefinement.resource {qubits : ℕ}
  (refinement : QuantumBlockEncoding.PrimitiveRefinement qubits) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.PrimitiveRefinement.resource
  {qubits : ℕ}
  (refinement :
    QuantumBlockEncoding.PrimitiveRefinement
      qubits) :
  QuantumBlockEncoding.Resource

Theorem6.7.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “oracle calls eq zero”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/PrimitiveRefinement.lean:33. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.7.5●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveRefinement.lean

complete

theorem QuantumBlockEncoding.PrimitiveRefinement.oracleCalls_eq_zero
  {qubits : ℕ}
  (refinement : QuantumBlockEncoding.PrimitiveRefinement qubits) :
  refinement.resource.oracleCalls = 0

theorem QuantumBlockEncoding.PrimitiveRefinement.oracleCalls_eq_zero
  {qubits : ℕ}
  (refinement :
    QuantumBlockEncoding.PrimitiveRefinement
      qubits) :
  refinement.resource.oracleCalls = 0