module module high

`IndisputableMonolith.QuantumComputing.DecoherenceFromBIT`

The module defines the BIT carrier frequency at 5φ in RS-native units and introduces associated decoherence quantities for quantum computing substrates. Quantum information theorists working within Recognition Science would reference these definitions when modeling T2 times. The module consists of sequential definitions and elementary properties derived from the imported Constants and Cost modules.

claimThe BIT carrier frequency satisfies $ω_{BIT} = 5φ$ where $φ$ denotes the golden ratio in the Recognition Science framework.

background

The module operates in the Recognition Science setting where the fundamental time quantum is defined as τ₀ = 1 tick. It imports the Cost module to ground calculations in J-cost functions and introduces the BIT frequency as the carrier for decoherence analysis. Key definitions include omega_BIT and T2_substrate, which parameterize coherence times on the phi-ladder for platforms like transmons and trapped ions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the BIT frequency definition that underpins decoherence derivations in quantum computing applications of Recognition Science. It feeds into downstream calculations of T2 ratios and rung assignments for specific qubit technologies, aligning with the eight-tick octave and phi-based mass formulas from the framework.

scope and limits

Does not compute numerical decoherence rates for specific hardware.
Does not incorporate external noise sources beyond the BIT carrier.
Does not extend to multi-qubit entanglement effects.

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