phi_2_6
plain-language theorem explainer
The declaration defines φ^{2.6} as the real obtained by raising the golden ratio to the power 2.6. Kaon mass modelers in Recognition Science cite it to approximate the observed m_K/m_π ratio near 3.54. The construction is a direct real exponentiation with no auxiliary lemmas or tactics.
Claim. Let φ denote the golden ratio fixed point. Define φ^{2.6} as the real number φ raised to the power 2.6, serving as an approximation to the kaon-pion mass ratio m_K/m_π.
background
In the Kaon Masses module the kaons sit on a higher rung of the phi-ladder than the pions because of the strange-quark content. The module states that the mass ratio follows phi-patterns and records the explicit numerical claim m_K/m_π ≈ 3.54 ≈ φ^{2.6}. Upstream results supply the general ledger and forcing structures that keep all mass assignments collision-free and algebraically consistent with the Recognition Composition Law.
proof idea
The definition is a direct real exponentiation phi ^ (2.6 : ℝ). No lemmas are invoked and no tactics are used beyond the built-in real power operation.
why it matters
The definition supplies the numerical handle used inside the P-014 kaon-mass derivation. It instantiates the phi-ladder placement required by the forcing chain at T6, where phi is the self-similar fixed point. The construction remains open to refinement once electromagnetic corrections and exact rung-gap assignments are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.