proposition: Lemma semantic_modulus_q: forall xi alpha beta, Is_refining_T xi -> {n:nat & { d | Incl_T (product_init_zip xi alpha beta n) d /\ (forall m d', (m<n)%nat ->~Incl_T (product_init_zip xi alpha beta m) d') } }.
proof: Proof. intros xi alpha beta H_r. apply LNP_sigS_nat_Digit. intros n d; apply Incl_T_dec_D. apply thesis_5_6_10'; assumption. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M