Structure before circuit tricks
Can a bounded-rank description be turned into an actual primitive list?
Canonicalize without changing the contraction, absorb the signed scalar boundary, complete each local isometry, compile its actual orthogonal matrix and assemble physical wires.
This is an authored reusable derivation guide, not a claim that the full family has been source-assimilated.
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_spec
Locate the same declaration in the Lean graph
Whole module, including imports and scoped assumptions. The declaration link above focuses the generated statement.
import QuantumBlockEncoding.ConstructiveTensorTrain
import QuantumBlockEncoding.ConstructiveIsometryLocal
import QuantumBlockEncoding.TensorTrainPrimitivePreparation
import QuantumBlockEncoding.TensorTrainWord
import QuantumBlockEncoding.PrimitiveDepthBound
/-!+# An actual primitive compiler for normalized real tensor trains
Canonicalization, signed boundary absorption, local SO completion, Gray/Givens
compilation, and physical-wire assembly are all named data producers. No chain,
matrix, or circuit is selected from an existence theorem. Quantum resource
bounds count the actual final list; classical preprocessing costs remain a
separate refinement obligation.
-/
namespace QuantumBlockEncoding.ConstructiveTensorTrainCompiler
open scoped BigOperators
open TensorTrainCanonical TensorTrainSchedule
open TensorTrainPrimitivePreparation
/-- Absorb the signed residual boundary into the actual first core. -/
noncomputable def absorbBoundary {n l r : ℕ} (u : Fin l → ℝ) :
Chain (n + 1) l r → Chain (n + 1) 1 r
| .cons A tail => .cons (boundaryRow u * A) tail
theorem absorbBoundary_canonical {n l r : ℕ} (u : Fin l → ℝ) (hu : mass u = 1)
(D : Chain (n + 1) l r) (hD : RightCanonical D) :
RightCanonical (absorbBoundary u D) := by
cases D with
| cons A tail => exact ⟨boundaryCore_isometry u hu A hD.1, hD.2⟩
theorem absorbBoundary_contract {n l r : ℕ} (u : Fin l → ℝ)
(D : Chain (n + 1) l r) (x : Word (n + 1)) :
contract (absorbBoundary u D) x = boundaryRow u * contract D x := by
cases D with
| cons A tail => exact boundaryCore_contract u A tail x
theorem absorbBoundary_maxBond {n l r : ℕ} (u : Fin l → ℝ)
(D : Chain (n + 1) l r) : maxBond (absorbBoundary u D) ≤ max 1 (maxBond D) := by
cases D with
| cons A tail => simp only [absorbBoundary, maxBond]; omega
/-- Concrete scalar-boundary canonical train, with no separate initialization circuit. -/
noncomputable def unitBoundary {n : ℕ} (C : Chain (n + 1) 1 1) : Chain (n + 1) 1 1 :=
absorbBoundary (ConstructiveTensorTrain.stateBoundary C)
(ConstructiveTensorTrain.canonicalize C).canonical
theorem unitBoundary_canonical {n : ℕ} (C : Chain (n + 1) 1 1)
(hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1) :
RightCanonical (unitBoundary C) :=
absorbBoundary_canonical _ (ConstructiveTensorTrain.stateBoundary_normalized C hNorm)
_ (ConstructiveTensorTrain.canonicalize_rightCanonical C)
theorem unitBoundary_contract {n : ℕ} (C : Chain (n + 1) 1 1) (x : Word (n + 1)) :
contract (unitBoundary C) x 0 0 = contract C x 0 0 := by
rw [unitBoundary, absorbBoundary_contract]
simpa [boundaryRow, _root_.Matrix.mul_apply] using
(ConstructiveTensorTrain.stateBoundary_action C x).symm
theorem unitBoundary_maxBond_le {n : ℕ} (C : Chain (n + 1) 1 1) :
maxBond (unitBoundary C) ≤ maxBond C := by
have hOne : 1 ≤ maxBond C := by
have h := rankAt_le_maxBond C 0
simpa only [rankAt_zero] using h
exact (absorbBoundary_maxBond _ _).trans
(max_le hOne (ConstructiveTensorTrain.canonicalize_maxBond_le C))
/-- Every local primitive list is computed from its actual completed SO matrix. -/
noncomputable def stage {n l r q : ℕ} (D : Chain n l r)
(hB : maxBond D ≤ 2 ^ q) (t : ℕ) : PrimitiveCircuit (q + 1) :=
GrayGivensCompiler.compileSO (ConstructiveIsometryLocal.completeStage D hB t)
theorem stage_gateCount {n l r q : ℕ} (D : Chain n l r)
(hB : maxBond D ≤ 2 ^ q) (t : ℕ) :
(stage D hB t).gateCount ≤ 6 * (2 ^ q) ^ 3 :=
(GrayGivensCompiler.compileSO_cubic_bound _).1
theorem stage_columns {n l r q : ℕ} (D : Chain n l r)
(hD : RightCanonical D) (hB : maxBond D ≤ 2 ^ q) (t : ℕ) (ht : t < n)
(bit : Fin 2) (b a : PrimitiveBasis q)
(ha : (primitiveBasisLEEquiv q a).val < rankAt D t) :
evalPrimitiveCircuit (stage D hB t) (Fin.snoc b bit) (Fin.snoc a 0) =
paddedAt D t (bit, primitiveBasisLEEquiv q b) (primitiveBasisLEEquiv q a) := by
obtain ⟨ho, hd, hc⟩ := ConstructiveIsometryLocal.completeStage_spec D hD hB t ht
rw [stage, GrayGivensCompiler.compileSO_eval _ ho hd]
exact hc bit b a ha
/-- Final physical circuit: data occupy the low wires, and the clean bond the high wires. -/
noncomputable def compile {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q) : PrimitiveCircuit ((n + 1) + q) :=
SequentialPrimitiveAssembly.publicCircuit []
(stage (unitBoundary C) ((unitBoundary_maxBond_le C).trans hB)) (n + 1)
theorem compile_gateCount {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q) :
(compile C hB).gateCount ≤ (n + 1) * (6 * (2 ^ q) ^ 3) :=
publicCircuit_gateCount_bound _ _ _ (fun t _ => stage_gateCount _ _ t)
theorem compile_depth {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q) :
(compile C hB).resource.depth ≤ (n + 1) * (6 * (2 ^ q) ^ 3) :=
(compile C hB).resource_depth_le_gateCount.trans (compile_gateCount C hB)
theorem compile_unitary {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q) :
evalPrimitiveCircuit (compile C hB) ∈
_root_.Matrix.unitaryGroup (PrimitiveBasis ((n + 1) + q)) ℂ :=
evalPrimitiveCircuit_unitary _
/-- All data words and all bond sectors, including every non-clean output. -/
theorem compile_columns {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q)
(hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1)
(x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis q) :
evalPrimitiveCircuit (compile C hB) (Fin.append x b) (fun _ => 0) =
if b = (fun _ => 0) then
(contract C (wordOfBasis (fun i => x i.rev)) 0 0 : ℂ) else 0 := by
rw [compile, publicCircuit_clean (unitBoundary C) ((unitBoundary_maxBond_le C).trans hB) _
(fun t ht bit b a ha => stage_columns _ (unitBoundary_canonical C hNorm) _ t ht bit b a ha),
unitBoundary_contract]
theorem compile_word {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q)
(hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1)
(x : Word (n + 1)) (b : PrimitiveBasis q) :
evalPrimitiveCircuit (compile C hB)
(Fin.append (fun i => TensorTrainWord.toBasis x i.rev) b) (fun _ => 0) =
if b = (fun _ => 0) then (contract C x 0 0 : ℂ) else 0 := by
simpa only [Fin.rev_rev, TensorTrainWord.wordOfBasis_toBasis] using
compile_columns C hB hNorm (fun i => TensorTrainWord.toBasis x i.rev) b
/-- Complete quantum correctness and resource certificate for the actual producer. -/
theorem compile_spec {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q)
(hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1) :
(compile C hB).gateCount ≤ (n + 1) * (6 * (2 ^ q) ^ 3) ∧
(compile C hB).resource.depth ≤ (n + 1) * (6 * (2 ^ q) ^ 3) ∧
(compile C hB).resource.oracleCalls = 0 ∧
evalPrimitiveCircuit (compile C hB) ∈
_root_.Matrix.unitaryGroup (PrimitiveBasis ((n + 1) + q)) ℂ ∧
∀ (x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis q),
evalPrimitiveCircuit (compile C hB) (Fin.append x b) (fun _ => 0) =
if b = (fun _ => 0) then
(contract C (wordOfBasis (fun i => x i.rev)) 0 0 : ℂ) else 0 :=
⟨compile_gateCount C hB, compile_depth C hB, rfl, compile_unitary C hB,
compile_columns C hB hNorm⟩
end QuantumBlockEncoding.ConstructiveTensorTrainCompiler
QuantumBlockEncoding.ConstructiveHermitePreparation.prepare_spec
Locate the same declaration in the Lean graph
Whole module, including imports and scoped assumptions. The declaration link above focuses the generated statement.
import QuantumBlockEncoding.ConstructiveTensorTrainCompiler
import QuantumBlockEncoding.HermiteFiniteNorm
/-!+# An actual exact-real Hermite preparation circuit
The source uses the existing literal Hermite kernel and the local Gram-based
norm supplier. It is fed through deterministic tensor-train canonicalization,
SO completion, and primitive compilation. This closes the data-producing
quantum construction, not its whole classical evaluation-cost obligation.
-/
namespace QuantumBlockEncoding.ConstructiveHermitePreparation
open scoped BigOperators
open TensorTrainCanonical TensorTrainWord HermiteFiniteChain HermiteFiniteNorm
/-- Normalize the formula-derived cores using the local norm, not a full sample sum. -/
noncomputable def normalizedSource (k n : ℕ) (L : ℝ) : Chain (n + 1) 1 1 :=
MatrixProductChain.ofKernel (kernel k n L)
(fun a => rawInitial k n L a / localSampleNorm k n L) (terminal k) 0 n
theorem normalizedSource_eq_source (k n : ℕ) (L : ℝ) (hL : 0 < L) :
normalizedSource k n L = sourceChain k n L :=
(sourceChain_eq_local k n L hL).symm
theorem normalizedSource_maxBond (k n : ℕ) (L : ℝ) :
maxBond (normalizedSource k n L) ≤ 2 * k + 6 := by
have h := MatrixProductChain.ofKernel_maxBond (kernel k n L)
(fun a => rawInitial k n L a / localSampleNorm k n L) (terminal k) 0 n
simpa [normalizedSource, max_eq_left (show 1 ≤ 2 * k + 6 by omega)] using h
theorem normalizedSource_normalized (k n : ℕ) (L : ℝ) (hL : 0 < L) :
(∑ x : Word (n + 1), (contract (normalizedSource k n L) x 0 0) ^ 2) = 1 := by
rw [normalizedSource_eq_source k n L hL]
exact sourceChain_normalized k n L hL
theorem normalizedSource_contract (k n : ℕ) (L : ℝ) (hL : 0 < L)
(x : Word (n + 1)) :
contract (normalizedSource k n L) x 0 0 =
HermiteStatePreparation.sampledAmplitude k (n + 1) L (sampleEquiv (n + 1) x) /
HermiteStatePreparation.sampleNorm k (n + 1) L := by
rw [normalizedSource_eq_source k n L hL, sourceChain_contract k n L hL]
/-- The actual finite primitive list; no circuit witness is selected. -/
noncomputable def prepare (k n : ℕ) (L : ℝ) : PrimitiveCircuit ((n + 1) + bondQubits k) :=
ConstructiveTensorTrainCompiler.compile (normalizedSource k n L)
((normalizedSource_maxBond k n L).trans (bond_fits k))
theorem prepare_gateCount (k n : ℕ) (L : ℝ) :
(prepare k n L).gateCount ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 := by
apply (ConstructiveTensorTrainCompiler.compile_gateCount (normalizedSource k n L)
((normalizedSource_maxBond k n L).trans (bond_fits k))).trans
simpa only [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using cubic_stage_budget k n
theorem prepare_depth (k n : ℕ) (L : ℝ) :
(prepare k n L).resource.depth ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 :=
(prepare k n L).resource_depth_le_gateCount.trans (prepare_gateCount k n L)
theorem prepare_columns (k n : ℕ) (L : ℝ) (hL : 0 < L)
(x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis (bondQubits k)) :
evalPrimitiveCircuit (prepare k n L) (Fin.append x b) (fun _ => 0) =
if b = (fun _ => 0) then
HermiteStatePreparation.normalizedAmplitude k (n + 1) L
(primitiveBasisLEEquiv (n + 1) x) else 0 := by
rw [prepare, ConstructiveTensorTrainCompiler.compile_columns _ _
(normalizedSource_normalized k n L hL), normalizedSource_contract k n L hL,
sampleEquiv_public]
rfl
/-- Literal source semantics, all clean/non-clean output sectors, full unitary,
and gate/depth bounds for this particular constructed circuit. -/
theorem prepare_spec (k n : ℕ) (L : ℝ) (hL : 0 < L) :
(prepare k n L).gateCount ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 ∧
(prepare k n L).resource.depth ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 ∧
(prepare k n L).resource.oracleCalls = 0 ∧
evalPrimitiveCircuit (prepare k n L) ∈
_root_.Matrix.unitaryGroup (PrimitiveBasis ((n + 1) + bondQubits k)) ℂ ∧
∀ (x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis (bondQubits k)),
evalPrimitiveCircuit (prepare k n L) (Fin.append x b) (fun _ => 0) =
if b = (fun _ => 0) then
HermiteStatePreparation.normalizedAmplitude k (n + 1) L
(primitiveBasisLEEquiv (n + 1) x) else 0 :=
⟨prepare_gateCount k n L, prepare_depth k n L, rfl,
evalPrimitiveCircuit_unitary _, prepare_columns k n L hL⟩
end QuantumBlockEncoding.ConstructiveHermitePreparation
The current symbolic resource theorem does not include a full stable finite-precision T-gate compiler.
Normalize AND compile AND clean — curated-transport
primary-metadata-checked Abstract: explicit function to MPS to circuit; requested v1 HTML was unavailable in this audit
Prior art for function-to-MPS preparation. The ASPBE Hermite specialization must not be credited with inventing polynomial-to-MPS or sequential MPS preparation.
% Authored mechanism lesson; not a new theorem certificate.
\section*{Canonicalization, completion and local compilation}
Can a bounded-rank description be turned into an actual primitive list?
\[
V_i^\dagger V_i=I\quad\Longrightarrow\quad U_i(|a\rangle|0\rangle)=\sum_{b,a'}(V_i)_{b,a',a}|a'\rangle|b\rangle
\]
Canonicalize without changing the contraction, absorb the signed scalar boundary, complete each local isometry, compile its actual orthogonal matrix and assemble physical wires.
\paragraph{Hypotheses and contracts.}
\begin{enumerate}
\item Normalized scalar-boundary real TT
\item Rank-deficient factors and signed boundary cases are handled
\item All non-clean output sectors vanish at the final stage
\end{enumerate}
\paragraph{Mathematical proof mechanism.}
This is a reusable derivation guide; exact certified scope is given by the linked Lean signatures.
\begin{enumerate}
\item Factor local cores and pass the residual factor to the neighboring core.
\item Prove preservation of every contracted amplitude and the local isometry identity.
\item Complete to an orthogonal matrix, decompose into plane rotations and compile to RY/CX.
\item Compose the stages and prove both clean output and primitive resource bounds.
\end{enumerate}
\paragraph{Boundary.} The current symbolic resource theorem does not include a full stable finite-precision T-gate compiler.