dama_modulation_from_ledger
plain-language theorem explainer
Equates the proposition for DAMA modulation structure from the ledger to the ANITA upgoing structure proposition. Experimental physicists studying annual modulation in direct-detection data or upgoing events would cite the link to chain anomaly inputs. The definition is a one-line alias that reduces directly to the gallium anomaly proposition.
Claim. Let $P$ be the proposition that the DAMA modulation signal follows from the ledger structure. Let $Q$ be the proposition that ANITA upgoing events follow from the ledger structure. Then $P$ is defined to be identical to $Q$.
background
The declaration sits in the Experimental.DAMAModulationStructure module, which assembles propositions that tie observed signals to the Recognition Science ledger. The sole upstream dependency defines the ANITA upgoing proposition as identical to the gallium anomaly proposition, thereby extending a chain from neutrino data through ANITA to DAMA modulation. No further hypotheses or parameters are introduced at this step.
proof idea
One-line definition that directly aliases the DAMA modulation proposition to the ANITA upgoing proposition.
why it matters
The definition supplies the hypothesis for the dama_implies_anita theorem and the dama_modulation_structure theorem. It also serves as the structural input for the xenon excess propositions in the sibling module. The construction therefore closes one link in the experimental chain that connects DAMA annual modulation, ANITA upgoing events, and the gallium anomaly under a common ledger structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.