module module

`IndisputableMonolith.RecogSpec.Bands`

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 (4)

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

IndisputableMonolith.RecogSpec.Spec module_import
IndisputableMonolith.Verification.BandsInvariantCert module_import
IndisputableMonolith.Verification.DimensionCRT module_import
IndisputableMonolith.Verification.Gap45DimensionCert module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.BridgeCore module_import

declarations in this module (25)

structure Band L7
abbrev Bands L13
def wideBand L33
lemma wideBand_width L35
lemma wideBand_width_nonneg L39
lemma wideBand_contains_center L45
lemma wideBand_valid L56
lemma wideBand_contains_lo L60
lemma wideBand_contains_hi L64
def sampleBandsFor L68
lemma sampleBandsFor_nonempty L70
lemma sampleBandsFor_singleton L73
def evalBandsAt L76
def meetsBandsChecker_gen L78
def meetsBandsChecker L82
def evalToBands_c L86
lemma evalToBands_c_invariant L90
lemma evalToBands_c_wideBand_center L106
lemma evalToBands_c_sampleBandsFor L113
lemma meetsBandsChecker_gen_nil L119
lemma meetsBandsChecker_nil L124
lemma meetsBandsChecker_gen_nilBands L129
lemma center_in_sampleBandsFor L134
lemma center_in_each_sample L141
theorem lcm_pow2_45_eq_iff L152