flyby_anomaly_from_ledger
plain-language theorem explainer
Flyby anomaly from ledger equates the flyby structural input proposition to the Atomki X17 ledger input. Experimental modelers linking gravitational flyby data to nuclear excess observations cite this equivalence to chain assumptions across anomaly structures. The definition is realized as a direct alias to the upstream xenon excess proposition.
Claim. The flyby anomaly structural input is defined to be identical to the Atomki X17 structural input: $flyby_anomaly_from_ledger := atomki_x17_from_ledger$.
background
In the experimental structures layer, anomaly inputs are represented as propositions standing for ledger-derived assumptions rather than derived theorems. The upstream Atomki X17 ledger proposition is itself an alias to the xenon excess ledger proposition, allowing nuclear anomaly claims to propagate through the chain. The FlybyAnomalyStructure module imports AtomkiX17Structure to establish this link without invoking the core forcing chain or Recognition Composition Law.
proof idea
The definition is a one-line alias that directly substitutes the Atomki X17 ledger proposition.
why it matters
This definition supplies the structural input for the flyby anomaly theorem and for the MiniBooNE/LSND ledger proposition. It bridges the flyby anomaly to the Atomki X17 input, which traces to xenon excess observations. The placement keeps experimental anomaly claims modular while remaining downstream of the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.