b_meson_anomalies_from_ledger
plain-language theorem explainer
The definition identifies the B-meson anomalies proposition with the muon g-2 ledger condition, which holds when the golden ratio exceeds zero. Experimental physicists studying flavor anomalies would cite this equivalence to connect B-meson decay data with the muon magnetic moment under a shared ledger input. It is implemented as a direct abbreviation of the upstream muon g-2 proposition.
Claim. Let $phi$ denote the golden ratio fixed point. The proposition that B-meson anomalies arise from the ledger is defined to be the assertion that $0 < phi$.
background
This definition appears in the Experimental.BMesonAnomaliesStructure module, which imports MuonGMinusTwoStructure to share structural inputs across lepton and meson anomalies. The upstream muon_g_minus_two_from_ledger is the proposition $0 < phi$, with phi the self-similar fixed point forced as the T6 step in the unified forcing chain. Recognition Science uses this phi to generate constants such as $hbar = phi^{-5}$ and the alpha inverse band, supplying the common ledger basis for both muon g-2 and B-meson structures.
proof idea
The definition is a one-line abbreviation that directly equates the B-meson anomalies from ledger proposition to the muon g-2 from ledger proposition.
why it matters
This supplies the shared proposition for the theorem asserting B-meson anomaly structure and the theorem recovering the muon g-2 input from it. It integrates B-meson anomalies into the Recognition Science framework by linking them to the phi-based ledger, consistent with J-uniqueness and the eight-tick octave. No open questions are resolved by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.