Quantum-kernel learning advantage (Liu, Arunachalam, Temme 2021)

A genuine conditional separation over the discrete-log concept class: under the hardness of the discrete-logarithm problem, a support-vector machine with quantum-kernel estimation provably separates a concept class that no efficient classical learner can. The classical accuracy ceiling is derived (not assumed) by a contrapositive that consumes the proved secret-homogeneity acc_shift (in LeanPool.LeanQuantumAlg.Primitives.QKernel.DiscreteLogConcept); the deep crypto/learning facts (DLP hardness, the efficient reduction, the SVM-QKE margin floor) are named hypothesis fields citing Liu, NOT axioms.

The expressivity (density-matrix EQK realization) half lives in LeanPool.LeanQuantumAlg.Primitives.QKernel.Expressivity; the fidelity-kernel PSD foundation is in LeanPool.LeanQuantumAlg.Primitives.QKernel.Fidelity.

Source: Liu, Arunachalam, Temme (2021), A rigorous and robust quantum speed-up in supervised machine learning.

structure QuantumAlg.QuantumKernelAdvantage (G : Type u_1) [Group G] [Fintype G] [IsCyclic G] : Type u_1

Provable quantum-kernel learning advantage (Liu, Arunachalam, Temme 2021), as a genuine conditional separation over the discrete-log concept class on a finite cyclic group G. The classical ceiling is derived (not assumed) by a contrapositive that consumes the proved secret-homogeneity acc_shift: a learner beating 1/2 + ε, transported to the fixed concept f_1, would solve the discrete-log problem.

The genuinely deep crypto/learning facts are named hypothesis fields citing Liu (NOT axioms): ClassicalSolvesDLP/dlpHard (DLP hardness — equivalent to a P≠ statement, unprovable in principle), singleConceptReduction (the efficient reduction; its algebraic step is the proved dlogConcept_reduction), and quantumFloor (the SVM-QKE margin generalization).

• g : G

  A generator of the cyclic group.

• hg (x : G) : x ∈ Subgroup.zpowers self.g

  g generates G.

• ε : ℝ

  The classical advantage gap above chance that is provably unreachable.

• hε : 0 < self.ε

  The gap is positive.

• hε_lt : 1 / 2 + self.ε < 99 / 100

  The chance ceiling stays strictly below the quantum floor.

• ClassicalSolvesDLP : Prop

  An opaque proposition standing for "the discrete-log problem is classically easy".

• dlpHard : ¬self.ClassicalSolvesDLP

  DLP hardness (Liu Thm 1 assumption): no efficient classical DLP solver.

• classicalPredictor : G → Bool

  The classical learner under scrutiny.

• classicalSecret : ZMod (Nat.card G)

  The secret labelling the learner targets.

• classicalAcc : ℝ

  The learner's (uniform) test accuracy.

• classicalAcc_def : self.classicalAcc = acc self.g ⋯ self.classicalPredictor self.classicalSecret

  The accuracy is the uniform agreement with the concept f_{classicalSecret}.

• singleConceptReduction : 1 / 2 + self.ε < acc self.g ⋯ (fun (y : G) => self.classicalPredictor (y * gpow self.g ⋯ (self.classicalSecret - 1))) 1 → self.ClassicalSolvesDLP

  The reduction (Liu Thm 1): an above-chance learner for the fixed concept f_1 yields an efficient DLP solver. Its algebraic step is dlogConcept_reduction.

• quantumAcc : ℝ

  The quantum-kernel SVM's accuracy.

• quantumFloor : 99 / 100 ≤ self.quantumAcc

  Quantum floor (Liu Thm 2): the SVM with quantum-kernel estimation is highly accurate (margin generalization).

theorem QuantumAlg.QuantumKernelAdvantage.classical_ceiling {G : Type u_1} [Group G] [Fintype G] [IsCyclic G] (M : QuantumKernelAdvantage G) : M.classicalAcc ≤ 1 / 2 + M.ε

Genuine classical accuracy ceiling: under DLP hardness, the classical learner cannot beat 1/2 + ε. The proof transports the learner to the fixed concept via acc_shift and applies the reduction, contradicting hardness.

theorem QuantumAlg.QuantumKernelAdvantage.separation {G : Type u_1} [Group G] [Fintype G] [IsCyclic G] (M : QuantumKernelAdvantage G) : M.classicalAcc < M.quantumAcc

The quantum-kernel learner strictly outperforms every classical learner.

theorem QuantumAlg.qka_nonempty : Nonempty (QuantumKernelAdvantage (Multiplicative (ZMod 2)))

The conditional-separation hypotheses are jointly satisfiable (not vacuous): a concrete QuantumKernelAdvantage on the order-2 cyclic group, with an always-wrong classical predictor (acc = 0), so the reduction's premise is false and the bundle is consistent with dlpHard.