module module

`IndisputableMonolith.Constants.KDisplay`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Certificates.UnitsKGate module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.KDisplayCore module_import

declarations in this module (20)

lemma ell0_div_tau0_eq_c L16
lemma display_speed_eq_c_of_nonzero L24
lemma tau_rec_display_pos L35
lemma tau_rec_display_ne_zero L42
lemma display_speed_eq_c L45
theorem K_gate_units_invariant L53
theorem units_quotient_preserves_K L64
theorem single_inequality_audit L75
def K_gate_tolerance L81
def K_gate_check L89
theorem display_speed_positive L97
theorem display_ratio_scale_invariant L103
theorem display_rate_matches_structural_rate L114
theorem display_null_condition L131
def UnitsEquivalent L138
theorem displays_invariant_under_equivalence L168
structure KGateMeasurement L178
def validateKGate L193
def falsifier_K_gate_mismatch L198
theorem observable_factors_through_quotient L204