T2_substrate_pos
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assign concrete Z-rung values to any qubit family.
- Does not derive the BIT frequency omega_BIT from first principles.
- Does not address measurement noise or statistical error bars on T2 data.
Lean usage
T2_pos := T2_substrate_pos T2_0 k hTformal statement (Lean)
78theorem T2_substrate_pos (T2_0 : ℝ) (k : ℕ) (hT : 0 < T2_0) :
79 0 < T2_substrate T2_0 k := by
proof body
Term-mode proof.
80 unfold T2_substrate
81 exact div_pos hT (pow_pos Constants.phi_pos k)
82
83/-- `T₂_substrate` is strictly decreasing in `k`. -/