module module high

`IndisputableMonolith.QuantumComputing.DecoherenceFromBIT`

This module defines the BIT carrier frequency ω_BIT = 5φ in RS-native units and derives T2 decoherence times for quantum substrates from the Recognition Science cost function. Researchers modeling quantum hardware decoherence via RS principles would cite these definitions. The module consists of sequential definitions establishing positivity, band constraints, and phi-power ratios for the frequency and substrate T2 values.

claimThe BIT carrier frequency satisfies $\omega_{\rm BIT} = 5\phi$ in RS-native units. Derived T2 times for substrates obey $T2_{\rm substrate} = \tau_0 \cdot \phi^{r}$ with rung $r$ specific to transmon, fluxonium, NV center, and trapped-ion systems.

background

The module sits in the QuantumComputing domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants together with the cost function from Cost. It introduces the BIT frequency and T2_substrate quantities that rest on the J-cost and phi-ladder structures of the parent framework. Sibling declarations establish positivity of $\omega_{\rm BIT}$, its placement inside the allowed band, and the strictly decreasing character of T2_substrate.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the BIT frequency and substrate T2 definitions that support downstream quantum-computing calculations in Recognition Science. It supplies the carrier-frequency step required for decoherence estimates on transmon, fluxonium, NV, and trapped-ion platforms.

scope and limits

Does not convert T2 values to SI units or experimental frequencies.
Does not model entanglement or multi-qubit decoherence channels.
Does not incorporate external bath spectral densities beyond the BIT carrier.
Does not address finite-temperature corrections to the T2 expressions.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (16)

def omega_BIT L53
theorem omega_BIT_pos L56
theorem omega_BIT_band L62
def T2_substrate L75
theorem T2_substrate_pos L78
theorem T2_substrate_strictly_decreasing L84
theorem T2_ratio_is_phi_power L103
def z_rung_transmon L125
def z_rung_fluxonium L128
def z_rung_NV L131
def z_rung_trapped_ion L134
theorem T2_transmon_to_fluxonium_ratio L137
theorem T2_transmon_to_trapped_ion_ratio L145
structure DecoherenceFromBITCert L162
def decoherenceFromBITCert L174
theorem decoherence_from_BIT_one_statement L189