SCCircuitElement
plain-language theorem explainer
The inductive type enumerates the five canonical superconducting circuit elements treated as recognition phase configurations in the RS framework. Circuit physicists mapping Josephson junctions to equilibrium phase zero would cite this enumeration to fix the configuration dimension at five. The declaration is a direct inductive definition that derives decidable equality and the Fintype instance for immediate cardinality use.
Claim. Let $E$ be the finite set whose elements are the Josephson junction, SQUID, transmon, fluxonium, and CPB. Then $|E|=5$, and $E$ carries decidable equality together with a canonical finite-type structure.
background
The module treats superconducting qubits as Josephson-junction circuits whose phase variable is identified with the recognition phase. Equilibrium corresponds to phase zero, the analogue of vanishing J-cost. Five elements are declared to realize configuration dimension five, while eight-tick DFT modes are attached to circuit resonances via the relation eight equals two to the configuration dimension.
proof idea
The declaration is an inductive definition with five constructors that automatically derives DecidableEq, Repr, BEq, and Fintype from Mathlib.
why it matters
The type supplies the finite set required by the downstream certification structure SCCircuitCert, which records both five elements and eight modes, and by the theorem scCircuitCount that computes the cardinality by decision. It implements the direct link from hardware elements to the eight-tick octave (T7) and the recognition phase variable without axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.