Pith. sign in
module module moderate

IndisputableMonolith.Physics.SuperconductingFluxQuantum

show as:
view Lean formalization →

Packages the Recognition Science account of the superconducting flux quantum: a domain cost on the flux variable, a canonical positive threshold, and an inhabited certificate bundling those facts. Condensed-matter and RS-constants workers cite it when tying flux quantization to the J-cost and the phi-scaled units. The module is mostly definitions plus elementary nonnegativity and positivity lemmas over Cost and Constants.

claimOn the superconducting flux domain one has a nonnegative cost $C$ (specialized from the RS $J$-cost), a canonical threshold $\theta>0$, and an inhabited certificate packing $C$, the identity $C$ at the reference point, nonnegativity of $C$, and positivity of $\theta$.

background

Recognition Science measures mismatch with the cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), imported here via the Cost module. Constants supplies the RS-native tick $\tau_0=1$ and the golden-ratio ladder that fixes units ($c=1$, $\hbar=\varphi^{-5}$, etc.).

Superconducting flux quantization is the statement that the enclosed flux sits on discrete levels set by $h/2e$ in SI units. This module rephrases that discreteness as a recognition threshold: a domain cost on the flux coordinate together with a canonical positive cutoff above which a flux quantum is registered.

Sibling definitions introduce domainCost (the restricted cost), its evaluation identity and nonnegativity, canonicalThreshold with a positivity lemma, and the bundle FluxQuantumCert witnessed by an inhabited cert.

proof idea

Definition-heavy module. Domain cost is specialized from the imported $J$-cost; nonnegativity is inherited from Cost. The canonical threshold is a positive constant built from Constants (phi-ladder / tick data); positivity is a short arithmetic lemma. The certificate is a structure packing those four facts, shown inhabited by assembling the preceding lemmas. No deep forcing-chain argument lives here.

why it matters in Recognition Science

Places flux quantization inside the same cost-and-threshold language used elsewhere in RS physics, so the superconducting quantum is not an extra SI postulate but a recognition event above a phi-consistent cutoff. Feeds any later condensed-matter or metrology development that needs a certified flux threshold in RS-native units. No downstream consumers are wired in the graph yet; the module stands as a physics-side leaf over Cost and Constants. Aligns with the broader program that discrete observables (eight-tick octave, rung masses, Berry threshold $\varphi^{-1}$) arise as cost crossings rather than independent axioms.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)