muon_g_minus_two_from_ledger
plain-language theorem explainer
The definition sets the muon g-2 ledger structure equal to the statement that phi is positive. Particle physicists examining lepton anomalies would cite it when mapping g-2 data onto Recognition Science constants. It is a direct one-line abbreviation with no proof obligations or lemmas.
Claim. The muon g-2 structure from the ledger is the proposition $0 < phi$, where $phi$ is the self-similar fixed point of the Recognition Composition Law.
background
Recognition Science forces phi at step T6 of the UnifiedForcingChain as the unique positive solution to the fixed-point equation arising from the J-cost function and the Recognition Composition Law. The module Experimental.MuonGMinusTwoStructure introduces ledger-based propositions that tie experimental anomalies to this constant. The definition uses the upstream positivity result phi_pos from the Constants module.
proof idea
This is a one-line definition that directly assigns the inequality 0 < phi to the identifier muon_g_minus_two_from_ledger.
why it matters
The definition supplies the structural premise for b_meson_anomalies_from_ledger and for the theorems muon_g_minus_two_implies_phi_pos and muon_g_minus_two_structure. It connects the experimental muon g-2 discrepancy to the positivity of phi required by the eight-tick octave (T7) and D = 3. It closes the interface between ledger assumptions and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.