log25_eq_5
plain-language theorem explainer
The equality establishes that the ceiling of log base 2 of 25 equals 5. Researchers bounding quantum circuit depth for 25-state molecular systems cite it to confirm five gate layers suffice. The proof proceeds by direct evaluation using Lean's decide tactic on the decidable equality.
Claim. $⌈log₂ 25⌉ = 5$
background
The CrossDomain.QuantumMolecularBound module models the reachable state space of a quantum circuit on a molecular substrate as the product MolecularEnergyLevel × QuantumGateType, each of size 5, for a total of 25 states. It requires that 25 ≤ 2^5 = 32, so every state is reachable in at most five two-qubit gate layers. This uses the upstream log2 definition from Information.Compression, given as noncomputable def log2 (x : ℝ) : ℝ := Real.logb 2 x.
proof idea
One-line wrapper that applies the decide tactic to verify the equality by computation.
why it matters
The result is referenced inside quantumMolecularBoundCert to certify the five-layer bound on the 5 × 5 state space. It supports the module's structural claim that the RS decomposition yields a sharp gate-layer limit for molecular targets. The declaration closes the verification for this specific cardinality without axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.