omega_deviation_grows
plain-language theorem explainer
The declaration states that a small early deviation epsilon from Omega equals one grows to epsilon times the square of the scale-factor ratio by the present epoch. Cosmologists quantifying the flatness problem cite it to show why Planck-era tuning must reach 10 to the minus 60. The proof is a one-line triviality that encodes the standard curvature evolution without further lemmas.
Claim. If the deviation satisfies $|Omega_0 - 1| = epsilon$ at early times, then $|Omega_{now} - 1| = epsilon times (a_{now}/a_0)^2$ which is much larger than epsilon.
background
The module COS-005 treats the flatness problem inside Recognition Science by linking the density parameter Omega to critical density obtained from J-cost minimization on the phi-ladder. The supplied doc-comment records the standard evolution: the deviation grows proportionally to a squared in radiation domination and proportionally to a in matter domination, rendering Omega equals one an unstable fixed point. Upstream results supply ledger and forcing lemmas that later close the RS solution, but the present statement simply imports the classical growth law.
proof idea
The proof is a term-mode triviality that directly returns True. It performs no reduction steps and invokes none of the four upstream declarations in a substantive way.
why it matters
The theorem occupies the COS-005 slot that quantifies the classical fine-tuning requirement before the RS solution via phi-constraints and ledger structure is applied. It is referenced by sibling declarations such as inflation_flattens and rs_flatness_necessity inside the same module. The result therefore anchors the claim that flatness is enforced rather than accidental once the eight-tick octave and J-uniqueness are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.