module module high

`IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom`

This module defines the 8-tick window and associated balance structures for mock theta phantoms in Recognition Science. Researchers formalizing the Ramanujan bridge would cite it to anchor signal values at the eight positions. The module supplies definitions and balance lemmas that establish zero-debt conditions without deeper analytic proofs.

claimAn 8-tick window is a map $W: [0,7] → ℝ$ assigning signal values to each position, equipped with the balance predicate IsBalanced($W$) that enforces zero net debt via the cost function.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants and the cost machinery from Cost. It introduces the 8-tick window as the basic object carrying signal values at each of the eight positions, together with the IsBalanced predicate and the MockThetaPhantom type that records phantom accumulation. These sit inside the larger RamanujanBridge effort that links Ramanujan’s structures to the Recognition Science forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete 8-tick objects required by the parent RamanujanBridge module, which states that Ramanujan’s deepest structures find natural expression inside Recognition Science. It closes the mock-theta phantom fragment of that bridge and prepares the ground for the full correspondence lemmas listed among its siblings.

scope and limits

Does not derive Ramanujan’s full mock theta series identities.
Does not embed the window into the phi-ladder or mass formula.
Does not prove uniqueness of the phantom balance beyond the zero-debt condition.
Does not address physical constants outside the 8-tick structure.

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