pith. sign in
module module moderate

IndisputableMonolith.Physics.SuperconductingCircuitsFromRS

show as:
view Lean formalization →

This module constructs superconducting circuit models from Recognition Science primitives by defining circuit elements, mode counts, and validity certifications. It maps the J-cost function and phi-ladder to circuit parameters in RS-native units. Quantum circuit researchers and condensed matter theorists would cite it for framework-native derivations of mode structures. The module is entirely definitional, establishing the core objects without theorems or external hypotheses.

claimThe module defines the objects $SCCircuitElement$, $scCircuitCount$, $circuitModes$, $circuitModes_8$, $circuitModes_2cubeD$, and $SCCircuitCert$ that represent superconducting circuit elements, their mode enumerations, and certification predicates in terms of the Recognition Science J-function and phi-ladder.

background

Recognition Science starts from the single functional equation whose solutions yield the J-cost $J(x) = (x + x^{-1})/2 - 1$ together with the self-similar fixed point phi. The module applies these to superconducting circuits by introducing typed elements whose parameters sit on the phi-ladder with rung and gap(Z) offsets. It inherits the eight-tick octave (T7) and three-dimensional spatial structure (T8) from the upstream UnifiedForcingChain, using Mathlib only for basic type and function infrastructure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the interface that lets Recognition Science address superconducting circuits, feeding downstream applications that link circuit modes to the Berry creation threshold phi^{-1} and the alpha^{-1} band. It closes the definitional gap between the abstract forcing chain and concrete circuit constructions, preparing the ground for later mode-counting lemmas that inherit the RCL identity.

scope and limits

declarations in this module (7)