T2_substrate_strictly_decreasing
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.