Structure before circuit tricks
Local Gram normalization
Can normalization be computed without summing exponentially many amplitudes?
\[E_i=\sum_{b=0}^1G_i[b]E_{i+1}G_i[b]^\top,\qquad Z=\ell^\top E_1\ell\]
What this technique preserves
Distribute the sum of squared contractions into local matrix products; compute the same finite norm from right to left.
Hypotheses and hidden contracts
- Real cores in this local Hermite route; use conjugate transpose for complex cores
- A nonzero raw state and compatible boundary dimensions
- Core construction and finite-bit arithmetic are separately charged
Mathematical proof mechanism
This is an authored reusable derivation guide, not a claim that the full family has been source-assimilated.
- Expand the squared scalar contraction.
- Exchange finite sums and collect the two values of the next bit.
- Inductively identify the Gram environment with the exact suffix norm and take the positive square root.
Exact Lean substrates
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm_eq_sampleNorm
Locate the same declaration in the Lean graph
Exact owning Lean module: QuantumBlockEncoding/HermiteFiniteNorm.lean
Whole module, including imports and scoped assumptions. The declaration link above focuses the generated statement.
import QuantumBlockEncoding.HermiteFiniteChain
import QuantumBlockEncoding.TensorTrainNormEnvironment
/-!
# A non-enumerating Hermite normalization supplier
The raw source chain contains no division by the full sample norm. Its small
Gram environments compute exactly that norm, with a polynomial syntactic
real-arithmetic budget. This does not charge construction of individual core
entries, canonicalization, angle evaluation or finite-bit arithmetic.
-/
namespace QuantumBlockEncoding.HermiteFiniteNorm
open TensorTrainCanonical TensorTrainWord HermiteBoundaryInjection HermiteFiniteChain
noncomputable def rawInitial (k n : Nat) (L : ℝ) : Fin (2 * k + 6) → ℝ :=
fun a => hermiteInitial k n L (bondEquiv k a)
/-- A scalar-boundary source representation without a precomputed normalizer. -/
noncomputable def rawSourceChain (k n : Nat) (L : ℝ) : Chain (n + 1) 1 1 :=
MatrixProductChain.ofKernel (kernel k n L) (rawInitial k n L) (terminal k) 0 n
theorem rawSourceChain_contract (k n : Nat) (L : ℝ) (hL : 0 < L)
(x : Word (n + 1)) :
contract (rawSourceChain k n L) x 0 0 =
HermiteStatePreparation.sampledAmplitude k (n + 1) L (sampleEquiv (n + 1) x) := by
rw [rawSourceChain, MatrixProductChain.ofKernel_contract]
simp_rw [kernel_readout k n L (n + 1) 0 (by omega), rawInitial]
have he : (∑ a, hermiteInitial k n L (bondEquiv k a) *
kernelContract (hermiteKernel k n L) (hermiteTerminal k) (toBits x) (bondEquiv k a)) =
kernelAmplitude (hermiteKernel k n L) (hermiteInitial k n L) (hermiteTerminal k) (toBits x) :=
(bondEquiv k).sum_comp (fun a => hermiteInitial k n L a *
kernelContract (hermiteKernel k n L) (hermiteTerminal k) (toBits x) a)
rw [he, hermiteKernel_eq_sample k n L hL (toBits x) (toBits_length x), wordSampleIndex_eq]
theorem rawSourceChain_maxBond (k n : Nat) (L : ℝ) :
maxBond (rawSourceChain k n L) ≤ 2 * k + 6 := by
have h := MatrixProductChain.ofKernel_maxBond (kernel k n L) (rawInitial k n L) (terminal k) 0 n
simpa [rawSourceChain, max_eq_left (show 1 ≤ 2 * k + 6 by omega)] using h
/-- Local matrix products followed by one real square root. -/
noncomputable def localSampleNorm (k n : Nat) (L : ℝ) : ℝ :=
TensorTrainNormEnvironment.norm (rawSourceChain k n L)
theorem localSampleNorm_eq_sampleNorm (k n : Nat) (L : ℝ) (hL : 0 < L) :
localSampleNorm k n L = HermiteStatePreparation.sampleNorm k (n + 1) L :=
TensorTrainNormEnvironment.norm_eq_of_contract (rawSourceChain k n L)
(sampleEquiv (n + 1)) (HermiteStatePreparation.sampledAmplitude k (n + 1) L)
(rawSourceChain_contract k n L hL)
theorem localSampleNorm_pos (k n : Nat) (L : ℝ) (hL : 0 < L) :
0 < localSampleNorm k n L := by
rw [localSampleNorm_eq_sampleNorm k n L hL]
exact HermiteStatePreparation.sampleNorm_pos k (n + 1) L
/-- The actual normalized source cores can use the local norm supplier. -/
theorem sourceChain_eq_local (k n : Nat) (L : ℝ) (hL : 0 < L) :
sourceChain k n L = MatrixProductChain.ofKernel (kernel k n L)
(fun a => rawInitial k n L a / localSampleNorm k n L) (terminal k) 0 n := by
rw [localSampleNorm_eq_sampleNorm k n L hL]
rfl
theorem rawSourceChain_storage (k n : Nat) (L : ℝ) :
MatrixProductChain.storedScalars (rawSourceChain k n L) ≤
2 * (n + 1) * (2 * k + 6) ^ 2 :=
MatrixProductChain.storedScalars_le _ _ (rawSourceChain_maxBond k n L)
theorem norm_environment_storage (k n : Nat) (L : ℝ) :
TensorTrainNormEnvironment.environmentScalars (rawSourceChain k n L) ≤
(n + 2) * (2 * k + 6) ^ 2 :=
TensorTrainNormEnvironment.environmentScalars_le _ _ (rawSourceChain_maxBond k n L)
/-- Addition/multiplication budget of the explicit Gram schedule, excluding
the final square root and the cost of supplying the raw core entries. -/
theorem norm_arithmetic_budget (k n : Nat) (L : ℝ) :
TensorTrainNormEnvironment.arithmeticBudget (rawSourceChain k n L) ≤
9 * (n + 1) * (2 * k + 6) ^ 3 :=
TensorTrainNormEnvironment.arithmeticBudget_le _ _ (rawSourceChain_maxBond k n L)
end QuantumBlockEncoding.HermiteFiniteNorm
QuantumBlockEncoding.HermiteFiniteNorm.norm_arithmetic_budget
Do not cross this boundary
An exact-real operation count is not a bit-complexity bound or a floating-point stability theorem.
Related transports
Normalize AND compile AND clean — curated-transport
Source and prior-art ledger
No external source is attached to this local mechanism note. It remains authored exposition, not a literature-priority claim.
Copy mathematical mechanism as LaTeX
% Authored mechanism lesson; not a new theorem certificate.
\section*{Local Gram normalization}
Can normalization be computed without summing exponentially many amplitudes?
\[
E_i=\sum_{b=0}^1G_i[b]E_{i+1}G_i[b]^\top,\qquad Z=\ell^\top E_1\ell
\]
Distribute the sum of squared contractions into local matrix products; compute the same finite norm from right to left.
\paragraph{Hypotheses and contracts.}
\begin{enumerate}
\item Real cores in this local Hermite route; use conjugate transpose for complex cores
\item A nonzero raw state and compatible boundary dimensions
\item Core construction and finite-bit arithmetic are separately charged
\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 Expand the squared scalar contraction.
\item Exchange finite sums and collect the two values of the next bit.
\item Inductively identify the Gram environment with the exact suffix norm and take the positive square root.
\end{enumerate}
\paragraph{Boundary.} An exact-real operation count is not a bit-complexity bound or a floating-point stability theorem.