self_le_four_pow_self
plain-language theorem explainer
The inequality d ≤ 4^d holds for every natural number d. Embedding theorems for finite-dimensional linear dynamics into ququart-based coupled core spaces cite it to fix the index set size. The proof proceeds by induction on d, with the base case dispatched by norm_num and the successor step reduced to arithmetic bounds via the inductive hypothesis and a short calculation chain.
Claim. For every natural number $d$, $d ≤ 4^d$.
background
The CoupledRecognitionCores module equips ququart states with 4-dimensional complex vector structure, including basisKet, ququartX, ququartZ, and the associated add4/sub4 operations. This theorem supplies the elementary capacity bound that lets the index set of size d fit inside a space whose dimension is a power of 4. The local setting is the construction of exact linear embeddings of arbitrary maps on Fin d into CoupledCoreSpace d; the imported carrier definitions (5φ Hz) from the engineering modules are not invoked here.
proof idea
The proof is by induction on d. The d = 0 case is immediate by norm_num. In the successor case, set m := 4^d, apply the inductive hypothesis to obtain d ≤ m, establish 1 ≤ m by positivity of powers, then use omega to derive d + 1 ≤ 2m and 2m ≤ 4m; finally rewrite 4m as 4^(d+1) by pow_succ and ring.
why it matters
The bound is invoked inside finite_dimensional_exact_embedding to guarantee that the embedding map from Fin d vectors into the coupled-core space is well-defined for any d. It closes the dimension-counting step that lets arbitrary finite-dimensional linear dynamics be realized exactly inside the ququart carriers of the recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.