circuitModes_2cubeD
plain-language theorem explainer
The declaration sets the number of modes in the superconducting circuit model to exactly eight. Researchers deriving qubit spectra from Josephson junctions under Recognition Science would cite this count when applying eight-tick Fourier analysis to resonance. The proof is a one-line reflexivity that matches the explicit definition of the mode count to 2 raised to the third power.
Claim. The number of modes supported by the superconducting circuit equals $2^3$.
background
The module treats superconducting qubits as Josephson junction circuits whose five canonical elements (Josephson junction, SQUID, transmon, fluxonium, CPB) realize configDim D = 5. Circuit resonance is analyzed with 8-tick DFT modes whose count is fixed by the eight-tick octave. The upstream definition in the same module sets the mode count to exactly 2 raised to the third power, reflecting the period-8 structure of the recognition phase variable at equilibrium.
proof idea
The proof is a one-line wrapper that applies reflexivity to the upstream definition of the mode count.
why it matters
This equality supplies the concrete mode count required by the superconducting-circuit derivations and directly instantiates the eight-tick octave (period 2^3) from the forcing chain. It anchors the application of the Recognition Composition Law to circuit elements and supports downstream counting of Fourier modes for qubit spectra. The module records zero sorry, confirming the direct embedding of the 2^D structure into the physics model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.