IndisputableMonolith.Foundation.DeltaSpine.MassRatioBindingReal

declarations in this module (19)

• def muEWindow L69
• lemma muE_scale_pos L72
• lemma muE_lo_div_pos L74
• theorem muEWindow_pos L78
• theorem muE_window_between_rungs L84
• theorem muE_sq_between L95
• theorem muE_pow63_gt L118
• theorem muE_pow88_lt L130
• lemma logb_lift_lower L144
• lemma logb_lift_upper L153
• theorem muE_logb_window L164
• theorem muE_logb_halfstep L176
• theorem muE_nearest_rung_unique L189
• theorem muE_epsilon_bracket L207
• theorem epsilon_upper_lt_inv_four_pi L223
• theorem muE_deviation_refutes_inv4pi L231
• theorem muE_equal_Z L238
• theorem muE_anchor_prediction L243
• theorem muE_rung_gap_certified L267