miniboone_lsnd_implies_flyby
plain-language theorem explainer
The theorem establishes that the MiniBooNE/LSND neutrino anomaly structure, when taken as following from the ledger, directly yields the flyby anomaly ledger condition. Experimental physicists studying neutrino oscillations or spacecraft trajectory discrepancies would cite this link to connect the two anomaly classes. The proof is a one-line term application of the hypothesis, which succeeds because the two propositions are definitionally identical.
Claim. If the MiniBooNE/LSND structure follows from the ledger, then the flyby anomaly follows from the ledger.
background
The Experimental.MiniBooNELSNDStructure module introduces propositions that embed specific experimental anomalies into the Recognition Science ledger. The upstream definition flyby_anomaly_from_ledger : Prop := atomki_x17_from_ledger supplies the base ledger-derived proposition for the flyby anomaly. The sibling definition miniboone_lsnd_from_ledger : Prop := flyby_anomaly_from_ledger then equates the MiniBooNE/LSND structure to that same proposition, creating a chain of structural implications between neutrino data and gravitational anomalies.
proof idea
The proof is a direct term-mode application of the hypothesis h : miniboone_lsnd_from_ledger. Because miniboone_lsnd_from_ledger is definitionally equal to flyby_anomaly_from_ledger, the implication holds by reflexivity of equality.
why it matters
This declaration supplies the explicit structural implication that ties the MiniBooNE/LSND neutrino anomaly to the flyby anomaly ledger input inside the experimental module. It advances the Recognition Science program of unifying disparate anomalies through ledger-derived propositions, even though no downstream theorems currently depend on it. The link remains open for integration into larger anomaly chains that might eventually connect to the core forcing chain or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.