T2_substrate_pos
plain-language theorem explainer
The declaration shows that the substrate decoherence time T2_substrate remains positive for any natural-number rung index whenever the base time T2_0 is positive. Qubit modelers working inside the Recognition Science BIT-coupling framework cite it to guarantee sign consistency before invoking the phi-power ratio theorems. The proof is a one-line term that unfolds the definition and applies the library facts on positivity of division and of phi to a positive power.
Claim. Let $T_{2,0} > 0$ be real and let $k$ be a natural number. Then the substrate decoherence time defined by $T_2(k) := T_{2,0} / phi^k$ satisfies $T_2(k) > 0$, where $phi$ is the positive golden-ratio constant supplied by the framework Constants bundle.
background
The DecoherenceFromBIT module defines the structural decoherence time by T2_substrate(T2_0, k) = T2_0 / phi^k. This encodes stronger BIT coupling at higher substrate Z-rung and therefore faster decoherence. The module works under the Bosonic Identity Theorem, treats per-class Z-rung assignments as hypotheses, and proves only the algebraic ratio structure T2(class_a)/T2(class_b) = phi^k for integer k determined by rung difference.
proof idea
The proof unfolds the definition of T2_substrate and applies the library lemma div_pos to the hypothesis 0 < T2_0 together with the positivity of phi raised to the natural number k.
why it matters
This positivity result supplies one of the four fields required to inhabit the master certificate decoherenceFromBITCert. It closes the sign requirement for the downstream theorem T2_ratio_is_phi_power that forces T2 ratios between qubit classes to be integer powers of phi. The construction sits inside the phi-ladder and eight-tick octave of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.