feat(cosmology): add TODO items for FLRW background cosmology

[doxtor6]

Summary

Adds TODO items recording formalization targets for FLRW background cosmology, distilled from Chapter 2 of O. F. Piattella, Lecture Notes in Cosmology (arXiv:1803.00070). These are placeholder TODO items only — no definitions, lemmas, or sorrys are introduced. They give a roadmap that complements the existing Physlib/Cosmology/FLRW/Basic.lean (FLRW scaffolding, Friedmann equations, Hubble & deceleration parameters).

What's added

New TODO-only files under Physlib/Cosmology/FLRW/:

File	TODO topics
ConformalTime.lean	conformal time η, conformal Hubble factor ℋ = aH, conformal-time metric, conformal Friedmann/acceleration equations, cosmic↔conformal chain rule
Distances.lean	comoving/proper/transverse distance, Hubble–Lemaître law, Hubble radius, redshift, particle/event horizons, lookback time, luminosity & angular-diameter distance, Etherington duality, low-z expansions
MatterContent.lean	perfect-fluid stress–energy tensor, continuity equation (+ Friedmann redundancy), barotropic equation of state, density scaling ρ ∝ a⁻³⁽¹⁺ʷ⁾, standard components, Λ as a w = −1 fluid
DensityParameters.lean	critical density, density parameters Ω / Ω_K, closure relation, reduced Hubble function E(a), standard-model Friedmann equation, age of the universe, equality epochs
Dynamics.lean	energy conditions (NEC/WEC/SEC/DEC), acceleration ⇔ SEC violation, q₀ = ½ Σ Ω(1+3w), eternal expansion (K ≤ 0), Big-Bang singularity
Solutions.lean	de Sitter, radiation, Einstein–de Sitter, Milne, Einstein static universe

Modified files:

• Physlib/Cosmology/FLRW/Basic.lean — adds the Physlib.Meta.TODO.Basic import and four TODO items placed next to the relevant declarations: the concrete FLRW structure (to replace the sorry placeholder), and H₀ / H(z) / E(z) next to hubbleConstant.
• Physlib.lean — registers the six new modules (kept sorted).
• scripts/MetaPrograms/spellingWords.txt — adds the new cosmology terms appearing in module docstrings.

Reviewer map

1. Physlib/Cosmology/FLRW/Basic.lean — smallest diff (3 imports/TODOs); sets the level and conventions.
2. The six new TODO files — each is a module docstring + TODO items; skim for scope and wording.
3. Physlib.lean and scripts/MetaPrograms/spellingWords.txt — mechanical registration.

lake build Physlib passes.

🤖 Generated with Claude Code

[github-actions]

Thank you for this PR, which will now be reviewed.
If submitting to ./Physlib or ./QuantumInfo, please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process,
though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[jstoobysmith]

Approved - many thanks!