T2_substrate_strictly_decreasing
The declaration proves that the substrate decoherence time T₂(k) = T₂₀ / φ^k is strictly decreasing in the natural number k whenever T₂₀ is positive. Researchers modeling qubit coherence times under the Bosonic Identity Theorem would cite it to establish the required ordering across substrate classes. The proof unfolds the definition and chains positivity of powers of φ, the fact that φ exceeds 1, and a division inequality.
claimLet $T_{2,0} > 0$ and $k ∈ ℕ$. Then $T_2(k+1) < T_2(k)$, where $T_2(k) := T_{2,0} / φ^k$.
background
The module treats decoherence arising from coupling to the BIT carrier at frequency 5φ. The sibling definition T2_substrate sets the structural decoherence time at Z-rung k to T₂₀ divided by φ^k, with higher rungs producing stronger coupling and therefore shorter T₂. This algebraic structure is proved inside the Recognition Science framework where quantities occupy discrete φ-tiers and ratios between classes are forced to exact φ-powers.
proof idea
The tactic proof first unfolds T2_substrate. It obtains 0 < φ^k and 0 < φ^{k+1} from pow_pos applied to Constants.phi_pos. It invokes one_lt_phi, rewrites with pow_succ, and applies nlinarith to establish φ^k < φ^{k+1}. It then finishes with div_lt_div_of_pos_left using the hypothesis 0 < T2_0.
why it matters in Recognition Science
The result is assembled directly into the master certificate decoherenceFromBITCert and into the one-statement theorem that collects the ω_BIT band, T₂ positivity, strict decrease, and φ-power ratios. It supplies the monotonicity required by the phi-ladder so that higher Z-rungs yield shorter coherence times under BIT coupling. The module treats rung assignments to specific qubit families as separate hypotheses while proving this ordering unconditionally.
scope and limits
- Does not assign specific Z-rungs to qubit classes such as transmon or fluxonium.
- Does not derive the BIT frequency from more primitive axioms.
- Does not predict absolute numerical values of T₂ without an empirical T2_0.
- Does not address decoherence channels outside the BIT-coupling model.
formal statement (Lean)
84theorem T2_substrate_strictly_decreasing (T2_0 : ℝ) (k : ℕ) (hT : 0 < T2_0) :
85 T2_substrate T2_0 (k + 1) < T2_substrate T2_0 k := by
proof body
Tactic-mode proof.
86 unfold T2_substrate
87 have h_pow_pos : 0 < Constants.phi ^ k := pow_pos Constants.phi_pos k
88 have h_pow_succ_pos : 0 < Constants.phi ^ (k + 1) := pow_pos Constants.phi_pos (k + 1)
89 have h_phi := Constants.one_lt_phi
90 have h_lt : Constants.phi ^ k < Constants.phi ^ (k + 1) := by
91 rw [pow_succ]
92 nlinarith [h_pow_pos, h_phi]
93 exact div_lt_div_of_pos_left hT h_pow_pos h_lt
94
95/-! ## §3. The cross-class ratio is a φ-power -/
96
97/-- **STRUCTURAL THEOREM (F1)**: the ratio of decoherence times
98 between two substrate classes at Z-rungs `k_a` and `k_b` is
99 `φ^(k_b - k_a)` (treating the integer subtraction as `k_b - k_a`
100 when `k_b ≥ k_a`).
101
102 Stated here with `k_b ≥ k_a` for non-negativity. -/