Window8
plain-language theorem explainer
The declaration introduces the type of an 8-tick window as a function from the eight discrete positions to integer signal values. Researchers analyzing the Ramanujan mock theta correspondence in Recognition Science cite this when treating unclosed windows as sources of phantom balance debt. The definition is introduced directly as a type abbreviation of the function space.
Claim. An 8-tick window is a function $w : {0,1,2,3,4,5,6,7} to Z$ assigning an integer signal to each position in the window.
background
The module develops a bridge between Ramanujan's mock theta functions and the Recognition Science ledger by modeling them as unclosed 8-tick windows. In this setting, a true modular form corresponds to a window whose signals sum to zero, while a mock theta function encodes a partial window with remaining balance debt. The upstream LedgerAlgebra supplies the full structure of windows over ledger events, which this mock version simplifies to integer signals for the phantom light analysis. The eight-tick structure originates from the forcing chain step T7, establishing the octave period that underlies balanced ledgers.
proof idea
The declaration is a direct type abbreviation. It requires no proof steps or lemma applications and simply names the function type from the eight ticks to integers for use in balance calculations.
why it matters
This type underpins the neutral window construction and balance debt function in the same module and in LedgerAlgebra. It realizes the eight-tick window required for the RS interpretation of mock theta functions as systems resolving phase debt, with the shadow term corresponding to phantom light. The declaration closes the scaffolding for the correspondence between unclosed windows and the mock modular defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.