A_amplitude
plain-language theorem explainer
The amplitude A for the spatial profile in RS gravity models is defined as one plus half the locked fine-structure constant. Galactic dynamics researchers cite this expression when fitting rotation-curve parameters to the predicted value near 1.096. The definition performs a direct substitution of the upstream alphaLock constant without further reduction.
Claim. The spatial profile amplitude satisfies $A = 1 + (1 - 1/φ)/4$, where the locked fine-structure constant is $(1 - 1/φ)/2$.
background
The GravityParameters module constructs seven phenomenological parameters for galactic gravity from Recognition Science. Among them, the amplitude A has an RS basis and is expressed using the locked fine-structure constant. The upstream definition states that this constant equals (1 minus 1 over phi) divided by 2, providing the algebraic bridge to phi-based quantities.
proof idea
This is a direct definition that inserts the value of the locked fine-structure constant into the arithmetic expression 1 plus that constant divided by 2. No lemmas or tactics are invoked; the body is a single equality.
why it matters
The definition supplies the concrete expression referenced by the downstream bounds theorem for the amplitude and the equality theorem for the amplitude. It occupies the HAS RS BASIS entry in the module's seven-parameter table, linking to the phi-derived constants. The construction aligns with the Recognition Science approach of obtaining gravity parameters from the forcing chain and the golden ratio fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.