SCCircuitCert
plain-language theorem explainer
The SCCircuitCert structure certifies that superconducting circuits in the Recognition Science model contain exactly five canonical elements and eight Fourier modes. Circuit modelers aligning Josephson phase with the recognition variable would cite it to confirm the match to configDim five and the eight-tick octave. The definition is a direct packaging of the Fintype cardinality of the element inductive type together with the constant circuitModes equal to two cubed.
Claim. A certificate asserting that the set of superconducting circuit elements has cardinality five and that the number of circuit modes equals eight.
background
In the module on superconducting circuits from Recognition Science the five elements are the Josephson junction, SQUID, transmon, fluxonium and CPB; these realize configDim equal to five. Circuit modes are defined as two raised to the third power, reproducing the eight-tick DFT octave. The local theoretical setting is RS_PAT_043 at S6 depth, where the Josephson junction phase variable is identified with the recognition phase at equilibrium where the J-cost analogue vanishes.
proof idea
The declaration is a structure definition that directly records the two equalities. It draws the cardinality five from the inductive type having five constructors and the mode count eight from the upstream definition of circuit modes as two cubed.
why it matters
The certificate is instantiated by the downstream scCircuitCert construction in the same module. It supplies the numerical match required by RS_PAT_043 / S6 Depth and thereby connects the T7 eight-tick octave and T8 three spatial dimensions to the modeling of Josephson-junction qubits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.