fiveLayerBound
plain-language theorem explainer
The inequality 2^5 ≥ 25 shows that the 25 states from five molecular energy levels crossed with five gate types remain reachable inside a five-layer quantum circuit. Cross-domain researchers cite it to certify the cardinality bound for molecular substrates in Recognition Science. The proof is a direct decision that evaluates 32 ≥ 25.
Claim. $2^{5} ≥ 25$, hence $⌈log_{2} 25⌉ ≤ 5$.
background
The CrossDomain.QuantumMolecularBound module models the reachable states as the product MolecularEnergyLevel × QuantumGateType, each of size 5, producing a state space of cardinality 25. This space is bounded by the 32 configurations of a five-layer two-qubit circuit. The module's setting is the structural claim that molecular targets are reachable in at most five gate layers, one per cube dimension plus overhead, as part of the Recognition Science cross-domain analysis.
proof idea
The proof is a one-line term that invokes decide to confirm the numerical inequality 32 ≥ 25 by exhaustive evaluation.
why it matters
The theorem supplies the five_layer component of the QuantumMolecularBoundCert definition. It closes the cardinality step in the C4 quantum-molecular bound, confirming that the 5 × 5 product fits inside the five-tick overhead permitted by the framework's eight-tick octave. The result is sharp; any requirement for more than five layers would indicate an error in the RS decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.