A_amplitude_bounds
plain-language theorem explainer
The Recognition Science galactic gravity model requires the spatial profile amplitude A to satisfy 1 < A < 2. Galaxy rotation-curve fitters would cite this to anchor the RS-derived value A ≈ 1.096 against the observed 1.06 ± 0.04. The proof is a one-line wrapper that unfolds A = 1 + alphaLock/2, invokes the positivity and upper-bound lemmas on alphaLock, and closes both sides with linear arithmetic.
Claim. $1 < A < 2$ where $A := 1 + {alphaLock}/2$ and $alphaLock$ is the locked fine-structure parameter obeying $0 < alphaLock < 1$.
background
The GravityParameters module derives galactic gravity parameters from the golden ratio φ. A_amplitude is defined as 1 + alphaLock/2, where alphaLock is taken from the FineStructureConstant submodule and satisfies the strict bounds 0 < alphaLock < 1 by the lemmas alphaLock_pos and alphaLock_lt_one. The module classifies A as having an RS basis (formula 1 + alphaLock/2) with a 3% match to the paper's fitted value 1.06 ± 0.04, reducing the number of free parameters in the seven-parameter set.
proof idea
The proof unfolds the definition of A_amplitude, obtains the facts alphaLock_pos and alphaLock_lt_one, splits the conjunction via constructor, and discharges both inequalities with linarith.
why it matters
This bound confirms that the amplitude A in the galactic gravity profile lies in the open interval (1,2), supporting the module's claim that A has an RS basis via the alphaLock term. It contributes to the systematic reduction of phenomenological inputs in the GravityParameters module, consistent with the framework's derivation of constants from φ and the alpha band. No downstream uses are recorded, but the result underpins consistency checks for the linked parameters a0 and r0 via the memory timescale τ★.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.