amplitude_derivation
plain-language theorem explainer
The declaration asserts that the observed scalar amplitude of approximately 2 times 10 to the minus 9 arises from inflationary dynamics combined with quantum fluctuations in the Recognition Science framework. Cosmologists deriving CMB spectra from J-cost fluctuations would cite this step when linking energy-scale ratios to observed A_s. The proof reduces immediately to the trivial proposition as a placeholder.
Claim. The scalar amplitude of primordial fluctuations satisfies $A_s approx 2 times 10^{-9}$, obtained from the ratio of the inflationary Hubble scale to the Planck mass with additional quantum corrections from the phi-ladder.
background
The Cosmology.PrimordialSpectrum module targets derivation of the CMB power spectrum from J-cost quantum fluctuations during inflation, as stated in the module doc. The power function computes the spectrum value at wavenumber k by scaling the amplitude by (k over pivot_scale) to the power of (spectral_index minus 1). Upstream results supply the amplitude definition from S-matrix unitarity, which extracts the matrix element for state transitions, and the double-slit amplitude, which sums complex phases along paths.
proof idea
The proof is a term-mode reduction that directly applies the trivial proposition to discharge the claim.
why it matters
This theorem fills the COS-009 target for the primordial spectrum amplitude within the Recognition Science framework, connecting to the J-uniqueness fixed point and phi-ladder tilt from the forcing chain. The doc-comment notes that pure energy-scale ratios yield too small a value, requiring quantum effects to reach the observed 10^{-9} level. No downstream uses are recorded yet, leaving the link to spectral index and tensor-to-scalar bounds open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.