anita_upgoing_structure
plain-language theorem explainer
The ANITA upgoing structure theorem asserts that the ledger condition required for ANITA upgoing events holds because it coincides with the gallium anomaly from ledger. Experimental physicists chaining neutrino and dark matter anomaly datasets would cite this link to propagate structural constraints across independent observations. The proof is a direct term application of the gallium anomaly structure theorem.
Claim. The proposition that ANITA upgoing events satisfy the ledger condition (equivalent to the gallium anomaly from ledger) holds, as established by the gallium anomaly structure theorem which reduces it to positivity of phi.
background
In the Experimental module, anomaly structures are propositions that tie observed signals to a shared ledger condition in Recognition Science. The ANITA upgoing from ledger is defined exactly as the gallium anomaly from ledger. The gallium anomaly structure theorem proves this ledger condition by reduction to phi positivity, per its doc-comment stating that the gallium anomaly structure implies positivity of phi.
proof idea
The proof is a one-line wrapper that applies the gallium anomaly structure theorem to discharge the target proposition.
why it matters
This theorem acts as the direct bridge from ANITA upgoing events to the gallium anomaly ledger, supplying the input used by the downstream DAMA modulation structure theorem. It aligns the experimental chain with Recognition Science landmarks including the phi fixed point and the forcing chain steps that enforce phi positivity. No open scaffolding remains as the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.