circuitModes_8
plain-language theorem explainer
The equality between the circuit mode count and eight follows from defining that count as two to the third power. Modelers of Josephson-junction circuits in Recognition Science cite the result to fix the eight Fourier modes that arise from the 8-tick octave. The proof is a one-line decision procedure that evaluates the arithmetic identity directly.
Claim. The number of Fourier modes in the superconducting circuit model equals eight, where eight is obtained as $2^3$.
background
The module treats superconducting qubits as Josephson-junction circuits whose five canonical elements (Josephson junction, SQUID, transmon, fluxonium, CPB) realize configDim equal to five. Circuit resonance is analyzed with 8-tick DFT modes, and the local definition sets the mode count to two raised to three. This construction rests on the eight-tick octave of the forcing chain, in which a period of $2^3$ supplies exactly eight modes for the recognition phase variable.
proof idea
The proof is a one-line wrapper that applies the decide tactic to reduce the arithmetic equality $2^3 = 8$ to a decidable proposition.
why it matters
The result populates the eight_modes field of the scCircuitCert certificate, anchoring the 8-tick structure for the five circuit elements. It instantiates the T7 eight-tick octave landmark and the relation $8 = 2^D$ with $D = 3$, thereby connecting the recognition phase at equilibrium to circuit resonances. No open scaffolding questions are closed by this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.