scCircuitCount
plain-language theorem explainer
The Recognition Science framework enumerates exactly five canonical superconducting circuit elements for Josephson junction based qubits. Circuit physicists would cite this cardinality when fixing configDim D equals five for qubit architectures. The proof is a one-line decision procedure that counts the constructors of the inductive type.
Claim. The set consisting of the Josephson junction, SQUID, transmon, fluxonium, and Cooper pair box has cardinality five.
background
In the Superconducting Circuits from RS module, superconducting qubits are identified with Josephson junction circuits. The five canonical elements are defined inductively as Josephson junction, SQUID, transmon, fluxonium, and CPB, which set configDim D = 5. The Josephson junction phase serves as the recognition phase variable, equilibrating at phase zero in analogy to the J-cost being zero. Eight-tick DFT modes govern the circuit resonance, matching the eight equals 2^D Fourier modes.
proof idea
The theorem is a one-line wrapper that applies the decide tactic to the Fintype.card computation, using the DecidableEq, Repr, BEq, and Fintype instances derived from the inductive definition of the five-element type.
why it matters
This cardinality supplies the five_elements field in the scCircuitCert definition, which certifies the superconducting circuit model together with the eight modes. It fills the RS_PAT_043 / S6 Depth proposition by establishing the five-element basis for Josephson-based qubits. The result connects to the eight-tick octave in the forcing chain, where period 2^3 governs the circuit mode count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.