dama_implies_anita
plain-language theorem explainer
The declaration shows that the DAMA modulation structure derived from the ledger directly supplies the ANITA upgoing structural input. Experimental physicists correlating annual modulation signals with upgoing neutrino-like events would cite this link when unifying DAMA and ANITA anomalies under a shared ledger. The proof succeeds by direct return of the hypothesis, as the two propositions are definitionally identical.
Claim. If the DAMA modulation structure follows from the ledger, then the ANITA upgoing events follow from the ledger.
background
In the Experimental.DAMAModulationStructure module the proposition dama_modulation_from_ledger is defined to equal anita_upgoing_from_ledger. The upstream definition anita_upgoing_from_ledger itself equals gallium_anomaly_from_ledger, so both statements encode the same ledger-derived structural input for the respective anomalies. The local setting is an experimental bridge inside Recognition Science that treats DAMA and ANITA signals as consequences of a common ledger rather than independent observations.
proof idea
The proof is a one-line term that returns the hypothesis h. Because dama_modulation_from_ledger is definitionally equal to anita_upgoing_from_ledger, the implication holds by reflexivity with no further lemmas required.
why it matters
The theorem supplies the direct implication between the two experimental propositions inside the Recognition Science ledger framework. It completes the structural connection between DAMA modulation and ANITA upgoing events that the module doc-comment identifies, even though no downstream theorems currently depend on it. The result therefore closes a small but explicit link in the experimental implications of the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.