IndisputableMonolith.Unification.RecognitionBandwidth

declarations in this module (20)

• def eightTickCadence L48
• theorem eightTickCadence_pos L50
• theorem eightTickCadence_eq L54
• def bandwidth L74
• theorem planckArea_pos L78
• theorem bandwidth_denom_pos L83
• theorem bandwidth_pos L93
• theorem bandwidth_pos' L97
• theorem bandwidth_monotone L101
• theorem bandwidth_linear L107
• def holographicBits L115
• theorem bandwidth_eq_bits_over_cost L119
• theorem bandwidth_times_cost_eq_rate L126
• theorem Clag_eq_phi_neg5 L136
• theorem alpha_locked_in_unit L141
• def demandedRate L154
• theorem demandedRate_pos L157
• def IsSaturated L167
• def IsSubSaturated L171
• theorem saturated_or_sub L175