A_amplitude_eq
plain-language theorem explainer
The equality relating the spatial profile amplitude to the golden ratio holds by algebraic substitution of the locked fine-structure constant. Galaxy dynamics modelers in Recognition Science cite this to set the amplitude parameter A at approximately 1.096. The proof reduces directly to ring simplification after unfolding the definitions of A_amplitude and alphaLock.
Claim. The spatial profile amplitude satisfies $A = 1 + (1 - 1/φ)/4$.
background
This module derives galactic gravity parameters from Recognition Science using the golden ratio φ. The amplitude A is defined as 1 + α_lock / 2, where α_lock is the locked fine-structure constant (1 - 1/φ)/2. Upstream, alphaLock provides the canonical definition α_lock = (1 − 1/φ)/2, serving as a bridge identity for acceleration-parameterized exponents. The module table lists A under HAS RS BASIS with formula 1 + αLock/2 and 3% observational match.
proof idea
The proof unfolds the definitions of A_amplitude and alphaLock, then applies the ring tactic to perform the algebraic simplification showing equivalence to 1 + (1 - 1/φ)/4.
why it matters
This equality fixes the amplitude A in the gravity parameters table, where it is listed as having RS basis with predicted value 1 + αLock/2 ≈ 1.096 matching observations within 3%. It supports the derivation of phenomenological parameters from φ in the Gravity module, linking to the seven parameters including α, C_ξ, p, and Υ★ = φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.