proposition: Lemma Is_refining_M_depth_h:forall n mu alpha (H_r:Is_refining_M mu), let smodu:=semantic_modulus_h mu alpha H_r in n= projS1 smodu -> depth_h mu alpha (Is_refining_M_emits_h mu alpha H_r) = n.
proof: Proof. induction n; intros mu alpha H_r smodu Hn; set (d:=(proj1_sig (projT2 smodu))); assert (Hd':d=(proj1_sig (projT2 smodu))); trivial; destruct (proj2_sig (projT2 smodu)) as [H1 H3]. revert H1; rewrite <- Hd'; rewrite <- Hn; intros H1. case (Incl_M_dec_D mu LL); intros t_l. apply depth_h_L; trivial. case (Incl_M_dec_D mu RR); intros t_r. apply depth_h_R; trivial. case (Incl_M_dec_D mu MM); intros t_m. apply depth_h_M; trivial. destruct d; contradiction. generalize H1 (H3 O); clear H1 H3; rewrite <- Hd'; rewrite <- Hn; intros H1 H3. case (Incl_M_dec_D mu LL); intros t_l. rewrite depth_h_L; trivial; generalize (H3 LL (lt_O_Sn _)); simpl; intros H4; contradiction. case (Incl_M_dec_D mu RR); intros t_r. rewrite depth_h_R; trivial; generalize (H3 RR (lt_O_Sn _)); simpl; intros H4; contradiction. case (Incl_M_dec_D mu MM); intros t_m. rewrite depth_h_M; trivial; generalize (H3 MM (lt_O_Sn _)); simpl; intros H4; contradiction. set (smodu':=semantic_modulus_h (product mu (map_digits (hd alpha))) (tl alpha) (Is_refining_M_product_hd _ _ H_r)). generalize (semantic_modulus_h_S_product (S n) (projT1 smodu') _ alpha H_r (Is_refining_M_product_hd _ _ H_r)). intros H_Sn. rewrite (depth_h_absorbs _ _ (Is_refining_M_emits_h mu alpha H_r) t_l t_r t_m (Is_refining_M_emits_h _ (tl alpha) (Is_refining_M_product_hd mu alpha H_r))). apply eq_S. apply IHn. rewrite (eq_add_S _ _ (H_Sn (lt_O_Sn _) (refl_equal _) Hn)); trivial. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M