def
definition
largeScaleStructureCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cosmology.LargeScaleStructureFromRS on GitHub at line 44.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
41 phi_ratio : ∀ k, scale (k + 1) / scale k = phi
42 scale_always_pos : ∀ k, 0 < scale k
43
44noncomputable def largeScaleStructureCert : LargeScaleStructureCert where
45 five_regimes := lssRegime_count
46 phi_ratio := scale_ratio
47 scale_always_pos := scale_pos
48
49end IndisputableMonolith.Cosmology.LargeScaleStructureFromRS