flyby_implies_atomki_x17
plain-language theorem explainer
The theorem shows that the flyby anomaly ledger condition directly yields the Atomki X17 ledger condition. Experimental researchers linking spacecraft trajectory data to nuclear decay anomalies in Recognition Science would cite this link. The proof is a one-line term that returns the hypothesis unchanged because the two ledger propositions are definitionally identical.
Claim. If the flyby anomaly ledger condition holds, then the Atomki X17 ledger condition holds.
background
In the Experimental module, ledger conditions serve as structural inputs drawn from observations. The Atomki X17 from ledger is defined as the xenon excess from ledger. The flyby anomaly from ledger is defined as the Atomki X17 from ledger, thereby equating the two propositions at the definitional level.
proof idea
The proof is a term-mode one-liner that returns the hypothesis h directly. It relies on the definitional equality between flyby_anomaly_from_ledger and atomki_x17_from_ledger supplied by the upstream definitions.
why it matters
This declaration supplies the direct implication step that lets flyby anomaly data feed into Atomki X17 structural claims inside the experimental layer. It sits downstream of the two ledger definitions and upstream of any future unification of anomalies under the phi-ladder or J-cost structures, though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.