Trusted cost annotations

This module connects Lean-QuantumAlg theorem endpoints to a small trusted cost interface. A value of Timed α returns an object of type α and carries a trusted natural-number cost annotation.

The cost annotation is intentionally not derived from the Lean evaluator or from matrix dimensions. Correctness is proved on .ret, while .time records the selected model. In the current quantum algorithm bridge, one unit means one oracle query for the single-query Walsh-Hadamard algorithms, and one good/bad-plane iterate for amplitude amplification and Grover.

This is an operator-level bridge over the existing pure-state and gate semantics. Fuller quantum program logics, such as density-operator or Hoare-style semantics for quantum while programs, are future extensions rather than prerequisites for this TimeM layer.

structure QuantumAlg.Timed (α : Type u) : Type u

A computation result paired with a natural-number cost.

• ret : α

  The trusted return value.

• time : ℕ

  The trusted cost annotation.

def QuantumAlg.Timed.trusted {α : Type u} (cost : ℕ) (ret : α) : Timed α

Attach a trusted cost to a return value.

Equations

• QuantumAlg.Timed.trusted cost ret = { ret := ret, time := cost }

@[simp]

theorem QuantumAlg.Timed.trusted_ret {α : Type u} (cost : ℕ) (ret : α) : (trusted cost ret).ret = ret

@[simp]

theorem QuantumAlg.Timed.trusted_time {α : Type u} (cost : ℕ) (ret : α) : (trusted cost ret).time = cost

structure QuantumAlg.ResourceProfile : Type

A trusted resource profile for registered theorem endpoints.

The fields are intentionally lightweight counters. They record the resource model claimed beside a correctness theorem, not a derivation from Lean evaluation.

• oracleQueries : ℕ

  Number of oracle queries.

• hadamardGates : ℕ

  Number of Hadamard gates.

• elementaryGates : ℕ

  Number of non-oracle elementary gates.

• classicalOps : ℕ

  Number of trusted classical operations.

@[implicit_reducible]

instance QuantumAlg.instDecidableEqResourceProfile : DecidableEq ResourceProfile

Equations

• QuantumAlg.instDecidableEqResourceProfile = QuantumAlg.instDecidableEqResourceProfile.decEq

def QuantumAlg.instDecidableEqResourceProfile.decEq (x✝ x✝¹ : ResourceProfile) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def QuantumAlg.ResourceProfile.zero : ResourceProfile

The empty resource profile.

Equations

• QuantumAlg.ResourceProfile.zero = { oracleQueries := 0, hadamardGates := 0, elementaryGates := 0, classicalOps := 0 }

def QuantumAlg.ResourceProfile.sequential (left right : ResourceProfile) : ResourceProfile

Sequential composition adds every resource counter.

Equations

• One or more equations did not get rendered due to their size.

def QuantumAlg.ResourceProfile.tensor (left right : ResourceProfile) : ResourceProfile

Tensor/parallel circuit composition uses the same additive counters.

Equations

• left.tensor right = left.sequential right

def QuantumAlg.ResourceProfile.HasExactCounts (profile : ResourceProfile) (oracleQueries hadamardGates elementaryGates classicalOps : ℕ) : Prop

Exact counter claim used by supporting public theorem statements.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumAlg.ResourceProfile.sequential_oracleQueries (left right : ResourceProfile) : (left.sequential right).oracleQueries = left.oracleQueries + right.oracleQueries

@[simp]

theorem QuantumAlg.ResourceProfile.sequential_hadamardGates (left right : ResourceProfile) : (left.sequential right).hadamardGates = left.hadamardGates + right.hadamardGates

@[simp]

theorem QuantumAlg.ResourceProfile.sequential_elementaryGates (left right : ResourceProfile) : (left.sequential right).elementaryGates = left.elementaryGates + right.elementaryGates

@[simp]

theorem QuantumAlg.ResourceProfile.sequential_classicalOps (left right : ResourceProfile) : (left.sequential right).classicalOps = left.classicalOps + right.classicalOps

@[simp]

theorem QuantumAlg.ResourceProfile.tensor_oracleQueries (left right : ResourceProfile) : (left.tensor right).oracleQueries = left.oracleQueries + right.oracleQueries

@[simp]

theorem QuantumAlg.ResourceProfile.tensor_hadamardGates (left right : ResourceProfile) : (left.tensor right).hadamardGates = left.hadamardGates + right.hadamardGates

@[simp]

theorem QuantumAlg.ResourceProfile.tensor_elementaryGates (left right : ResourceProfile) : (left.tensor right).elementaryGates = left.elementaryGates + right.elementaryGates

@[simp]

theorem QuantumAlg.ResourceProfile.tensor_classicalOps (left right : ResourceProfile) : (left.tensor right).classicalOps = left.classicalOps + right.classicalOps

structure QuantumAlg.CircuitGateProfile : Type

Gate counts for fixed circuit statements with named gate families.

• hadamardGates : ℕ

  Number of Hadamard gates.

• controlledPhaseGates : ℕ

  Number of controlled phase gates.

• swapGates : ℕ

  Number of swap gates.

def QuantumAlg.instDecidableEqCircuitGateProfile.decEq (x✝ x✝¹ : CircuitGateProfile) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance QuantumAlg.instDecidableEqCircuitGateProfile : DecidableEq CircuitGateProfile

Equations

• QuantumAlg.instDecidableEqCircuitGateProfile = QuantumAlg.instDecidableEqCircuitGateProfile.decEq

def QuantumAlg.CircuitGateProfile.HasExactCounts (profile : CircuitGateProfile) (hadamardGates controlledPhaseGates swapGates : ℕ) : Prop

Exact fixed-circuit gate-count claim.

Equations

• One or more equations did not get rendered due to their size.

structure QuantumAlg.Profiled (α : Type u) : Type u

A return value paired with a trusted resource profile.

• ret : α

  The returned value.

• resources : ResourceProfile

  Trusted resource accounting attached to the value.

def QuantumAlg.Profiled.trusted {α : Type u} (resources : ResourceProfile) (ret : α) : Profiled α

Attach a trusted resource profile to a return value.

Equations

• QuantumAlg.Profiled.trusted resources ret = { ret := ret, resources := resources }

@[simp]

theorem QuantumAlg.Profiled.trusted_ret {α : Type u} (resources : ResourceProfile) (ret : α) : (trusted resources ret).ret = ret

@[simp]

theorem QuantumAlg.Profiled.trusted_resources {α : Type u} (resources : ResourceProfile) (ret : α) : (trusted resources ret).resources = resources

structure QuantumAlg.CommunicationProfile : Type

Communication resources for protocol statements.

• classicalBits : ℕ

  Number of classical bits communicated.

• transmittedQubits : ℕ

  Number of qubits transmitted.

• bellPairs : ℕ

  Number of Bell pairs consumed.

@[implicit_reducible]

instance QuantumAlg.instDecidableEqCommunicationProfile : DecidableEq CommunicationProfile

Equations

• QuantumAlg.instDecidableEqCommunicationProfile = QuantumAlg.instDecidableEqCommunicationProfile.decEq

def QuantumAlg.instDecidableEqCommunicationProfile.decEq (x✝ x✝¹ : CommunicationProfile) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def QuantumAlg.CommunicationProfile.HasExactCounts (profile : CommunicationProfile) (classicalBits transmittedQubits bellPairs : ℕ) : Prop

Exact communication-resource claim for protocol supporting theorems.

Equations

• profile.HasExactCounts classicalBits transmittedQubits bellPairs = (profile.classicalBits = classicalBits ∧ profile.transmittedQubits = transmittedQubits ∧ profile.bellPairs = bellPairs)

@[simp]

theorem QuantumAlg.CommunicationProfile.hasExactCounts_mk (classicalBits transmittedQubits bellPairs : ℕ) : { classicalBits := classicalBits, transmittedQubits := transmittedQubits, bellPairs := bellPairs }.HasExactCounts classicalBits transmittedQubits bellPairs