module module

`IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom`

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.Mathematics.RamanujanBridge module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (42)

structure is L63
abbrev Window8 L89
def IsBalanced L92
def balanceDebt L96
theorem balanced_has_zero_debt L100
structure MockModularDefect L111
structure PhantomBalance L124
theorem balanced_phantom_zero L139
theorem nonzero_accumulation_forces_phantom L144
structure MockThetaPhantomCorrespondence L161
theorem phantom_completes_to_balanced L181
theorem mock_orders_coprime_to_8 L202
theorem mock_orders_are_odd_primes_lt_8 L211
theorem coprime_order_forces_mock_defect L226
structure TwoTimeBoundaryCondition L249
theorem two_time_unique L258
structure MockThetaPhantomFalsifier L265
theorem odd_prime_lt_8_in_mock_orders L284
theorem mock_orders_are_complete L297
theorem mock_orders_exactly_odd_primes_lt_8 L308
def min_windows_to_close L335
theorem order3_requires_3_windows L338
theorem order5_requires_5_windows L341
theorem order7_requires_7_windows L344
theorem mock_orders_require_multiple_windows L348
theorem coprime_requires_k_windows L359
def closes_in_one_window L376
theorem divisors_close L379
theorem mock_orders_dont_close L387
theorem prime_closes_iff_two L394
theorem order3_closure_eq_Q3_directed_flux L421
theorem mock_closure_periods L425
theorem mock_closure_periods_div_8 L430
theorem mock_and_congruence_primes_overlap L437
theorem full_mock_sync_period L442
theorem balanced_iff_zero_debt L453
theorem shadow_is_unique L460
theorem shadow_eq_neg_accumulated L464
theorem phantom_shadow_uniqueness L468
theorem balanced_completion_unique L475
theorem debt_is_running_negation L481
theorem debt_forces_unique_future L488