module module

`IndisputableMonolith.Gap45.RecognitionBarrier`

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

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

IndisputableMonolith.Gap45.ShimmerFactor module_import
IndisputableMonolith.Superhuman.SafetyInterlock module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gap45 module_import
IndisputableMonolith.Gap45.SyncMinimization module_import

declarations in this module (14)

theorem coprime_barrier L37
theorem beat_diff L40
theorem beat_is_prime L43
theorem beat_fraction_irreducible L46
theorem window_insufficient L53
theorem minimal_resolution_window L58
theorem resolution_requires_full_period L62
theorem aliasing_ratio_lt_one L72
theorem time_dilation_factor L76
theorem phase_mismatch L85
structure BarrierCert L97
def barrier_cert L105
structure ConsciousnessHypothesis L126
def consciousness_hypothesis L135