atomki_x17_structure
plain-language theorem explainer
The theorem proves the Atomki-X17 structural proposition holds by direct substitution of the xenon-excess structure result. Researchers tracing implication chains among experimental anomalies would cite this link to connect Atomki X17 data to xenon excess observations. The proof is a one-line term that applies the xenon excess theorem because the two propositions are definitionally identical.
Claim. The structural input for the Atomki-X17 anomaly holds because the xenon-excess structural input holds, as established by the xenon-excess structure theorem.
background
In this experimental module, structural inputs are propositions that encode ledger-derived constraints from specific observations. The Atomki-X17 from ledger proposition is defined to be identical to the xenon-excess from ledger proposition. Upstream, the xenon-excess structure theorem proves the xenon-excess from ledger proposition by appeal to the DAMA-modulation structure, forming an implication chain among anomaly data sets.
proof idea
This is a term-mode proof consisting of the single term xenon-excess structure. Because the target type is definitionally equal to the type of that theorem, the substitution is immediate and requires no further tactics or reductions.
why it matters
The declaration bridges Atomki-X17 structure to xenon-excess structure and supplies the input required by the flyby-anomaly structure theorem. It advances the experimental unification of multiple anomalies under a common ledger. Within the Recognition framework it supplies one link in the chain that tests consistency between observed signals and the forcing-chain derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.