feat(Cosmology): comoving distance, redshift, Hubble-Lemaitre law, transverse distance and horizons - #1639

Open

KevorkianPhilippe wants to merge 58 commits into

leanprover-community:masterfrom

KevorkianPhilippe:flrw-distances-8

Commits on Sep 10, 2026

feat(Cosmology): de Sitter solution of the Friedmann equations

Philippe Kevorkian
and
claude
committed
d2ddfe3
feat(Cosmology): flat power-law solutions of the Friedmann equations

Philippe Kevorkian
and
claude
committed
b8a0b43
feat(Cosmology): Milne solution and Einstein static universe relations

Philippe Kevorkian
and
claude
committed
0be812c
feat(Cosmology): continuity equation of the cosmic fluid from the Friedmann equations

Philippe Kevorkian
and
claude
committed
9a7000f
feat(Cosmology): barotropic equation of state, density scaling laws, cosmological constant as a fluid

Philippe Kevorkian
and
claude
committed
d5f24a5
feat(Cosmology): density parameters, closure relation, reduced Hubble function and age

Philippe Kevorkian
and
claude
committed
d5ea2bb
feat(Cosmology): energy conditions, acceleration criterion, deceleration parameter, eternal expansion and Big-Bang bound

Philippe Kevorkian
and
claude
committed
e180863
feat(Cosmology): comoving distance, redshift, Hubble-Lemaitre law, transverse distance and horizons

Philippe Kevorkian
and
claude
committed
616e823

Commits on Sep 11, 2026

chore(Cosmology): order authors alphabetically by last name

Philippe Kevorkian
and
claude
committed
4c6ea7f
chore(Cosmology): order authors alphabetically by last name

Philippe Kevorkian
and
claude
committed
7ec56a8
chore(Cosmology): order authors alphabetically by last name

Philippe Kevorkian
and
claude
committed
6b52a4e
chore(Cosmology): order authors alphabetically by last name

Philippe Kevorkian
and
claude
committed
0ed56f1
chore(Cosmology): order authors alphabetically by last name

Philippe Kevorkian
and
claude
committed
eb6a6ea
chore(Cosmology): order authors alphabetically by last name

Philippe Kevorkian
and
claude
committed
c6492fb
chore(Cosmology): order authors alphabetically by last name

Philippe Kevorkian
and
claude
committed
9d0eb90
style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition

Philippe Kevorkian
and
claude
committed
171e458
style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition

Philippe Kevorkian
and
claude
committed
78428d2
style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition

Philippe Kevorkian
and
claude
committed
6f82dc0
style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition

Philippe Kevorkian
and
claude
committed
3a83e2c
style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition

Philippe Kevorkian
and
claude
committed
d70fe93
style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition

Philippe Kevorkian
and
claude
committed
b88bfc5
style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition

Philippe Kevorkian
and
claude
committed
c640e70
Merge master into flrw-solutions-2 (after the merge of #1632, on which this branch is stacked)
Philippe Kevorkian
committed
8843171
Merge master into flrw-solutions-3 (after the merge of #1632, on which this branch is stacked)
Philippe Kevorkian
committed
15146dd
Merge master into flrw-matter-4 (after the merge of #1632, on which this branch is stacked)
Philippe Kevorkian
committed
296bf90
Merge master into flrw-matter-5 (after the merge of #1632, on which this branch is stacked)
Philippe Kevorkian
committed
5ac158e
Merge master into flrw-dynamics-6 (after the merge of #1632, on which this branch is stacked)
Philippe Kevorkian
committed
1b25624
Merge master into flrw-dynamics-7 (after the merge of #1632, on which this branch is stacked)
Philippe Kevorkian
committed
e484546
Merge master into flrw-distances-8 (after the merge of #1632, on which this branch is stacked)
Philippe Kevorkian
committed
9302040

Commits on Sep 12, 2026

Merge remote-tracking branch 'origin/master' into flrw-solutions-2
Philippe Kevorkian
committed
782c6d0
refactor(Cosmology): inline the power-law scaffolding of the flat solutions

Philippe Kevorkian
and
claude
committed
8580455
refactor(Cosmology): the normalisation epoch of the power-law solutions is a Time

Philippe Kevorkian
and
claude
committed
1a2cb0d
Merge branch 'flrw-solutions-2' into flrw-solutions-3
Philippe Kevorkian
committed
9cbd5cf
docs(Cosmology): the Milne scale factor puts the Big Bang at the origin of the time chart

Philippe Kevorkian
and
claude
committed
076b0e5
refactor(Cosmology): state the Einstein static density directly

Philippe Kevorkian
and
claude
committed
9e97b70
Merge branch 'flrw-solutions-3' into flrw-matter-4
Philippe Kevorkian
committed
444ec0b
Merge branch 'flrw-matter-4' into flrw-matter-5
Philippe Kevorkian
committed
311fa03
Merge branch 'flrw-matter-5' into flrw-dynamics-6
Philippe Kevorkian
committed
9c25cd4
Merge branch 'flrw-dynamics-6' into flrw-dynamics-7
Philippe Kevorkian
committed
f939500
Merge branch 'flrw-dynamics-7' into flrw-distances-8
Philippe Kevorkian
committed
8812447
refactor(Cosmology): adapt the Einstein-de Sitter particle horizon to t0 : Time

Philippe Kevorkian
and
claude
committed
f677dff

Commits on Sep 16, 2026

Merge master (#1633 merged) into flrw-solutions-3
Philippe Kevorkian
committed
657d813
Merge flrw-solutions-3 (master with #1633) into flrw-matter-4
Philippe Kevorkian
committed
8422b0d
Merge flrw-matter-4 (master with #1633) into flrw-matter-5
Philippe Kevorkian
committed
dc13d13
Merge flrw-matter-5 (master with #1633) into flrw-dynamics-6
Philippe Kevorkian
committed
ee71f8c
Merge flrw-dynamics-6 (master with #1633) into flrw-dynamics-7
Philippe Kevorkian
committed
1c1ee22
Merge flrw-dynamics-7 (master with #1633) into flrw-distances-8
Philippe Kevorkian
committed
2639b98

Commits on Sep 17, 2026

Merge master (#1634 merged) into flrw-matter-4
Philippe Kevorkian
committed
bd8402a
refactor(Time, Cosmology): state the HasDerivAt bridge and deriv_firstOrderFriedmann at t : Time

Philippe Kevorkian
and
claude
committed
e29b83e
doc(Cosmology/FLRW): TODOs for the Bianchi identity and the fluid energy equation, API map

Philippe Kevorkian
and
claude
committed
0235ed4
Merge flrw-matter-4 (review of #1635, master with #1634) into flrw-matter-5
Philippe Kevorkian
committed
5ac4fc9
refactor(Cosmology/FLRW): inline the one-off HasDerivAt helper of density_scaling, API map

Philippe Kevorkian
and
claude
committed
c68ff5e
Merge flrw-matter-5 (review of #1635, master with #1634) into flrw-dynamics-6
Philippe Kevorkian
committed
0d1214d
doc(Cosmology/FLRW): API map for the density parameters and the standard model

Philippe Kevorkian
and
claude
committed
8ede452
Merge flrw-dynamics-6 (review of #1635, master with #1634) into flrw-dynamics-7
Philippe Kevorkian
committed
9d85390
doc(Cosmology/FLRW): API map for the energy conditions and the Big-Bang bound

Philippe Kevorkian
and
claude
committed
99bfe7a
Merge flrw-dynamics-7 (review of #1635, master with #1634) into flrw-distances-8
Philippe Kevorkian
committed
a22d426
doc(Cosmology/FLRW): API map for the comoving, proper and transverse distances and the horizons

Philippe Kevorkian
and
claude
committed
fc93b4b