T2_substrate_pos
plain-language theorem explainer
Positivity of the substrate decoherence time T2(k) = T2_0 / phi^k holds whenever the base time T2_0 is positive. Researchers modeling qubit decoherence under the Bosonic Identity Theorem in Recognition Science cite this to maintain physical consistency across Z-rungs. The proof is a one-line wrapper that unfolds the definition and applies the division positivity lemma together with phi positivity.
Claim. If $T_{2,0} > 0$ and $k$ is a natural number, then the substrate decoherence time $T_2(k) := T_{2,0} / phi^k > 0$.
background
The Decoherence from BIT module develops the structural consequences of coupling a qubit substrate to the BIT carrier at frequency omega_BIT = 5 phi. The definition T2_substrate sets the decoherence time at Z-rung k to T2_0 / phi^k, with higher rung corresponding to stronger coupling and shorter lifetime. Constants supplies the positive real phi used in the denominator. The module distinguishes theorem-grade algebraic facts about phi-power ratios from hypothesis-grade assignments of specific qubit families to Z-rungs.
proof idea
Unfold T2_substrate to expose the quotient T2_0 / phi^k, then apply div_pos to the hypothesis 0 < T2_0 and the fact pow_pos Constants.phi_pos k.
why it matters
The result supplies the T2_pos field required by the master certificate decoherenceFromBITCert. It completes one algebraic prerequisite for the claim that T2 ratios between qubit classes equal phi to an integer power under the BIT model. The module thereby discharges the structural half of Track F1 in Completion Plan v4 while leaving Z-rung assignments as open hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.