pith. sign in
module module high

IndisputableMonolith.Experimental.DAMAModulationStructure

show as:
view Lean formalization →

This module establishes that DAMA modulation structure implies ANITA-upgoing structural input in the Recognition Science experimental layer. Physicists modeling annual modulation signals alongside neutrino anomalies would cite the implication to connect DAMA/LIBRA data with ANITA events. The module consists of sibling definitions for ledger-derived modulation and the core implication theorem, structured as a thin wrapper over the imported ANITAUpgoingStructure.

claimDAMA modulation structure (defined via ledger and phi-ladder) implies ANITA upgoing structural input.

background

Recognition Science derives experimental structures from the J-cost function and phi-ladder in the UnifiedForcingChain (T0-T8). This module sits in the Experimental domain and imports ANITAUpgoingStructure to supply the upgoing-event definitions. It introduces local objects dama_modulation_from_ledger and dama_modulation_structure that encode annual modulation patterns consistent with the Recognition Composition Law.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the DAMA-ANITA link required by the downstream XenonExcessStructure. It fills the experimental-implication step that follows the eight-tick octave and D=3 spatial dimensions in the forcing chain, allowing anomaly data to constrain the phi-ladder mass formula.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)