pith. machine review for the scientific record. sign in
def definition def or abbrev

phi_cosmology_relations

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 167def phi_cosmology_relations : List String := [

proof body

Definition body.

 168  "H₀ may be φ-related to τ₀",
 169  "Critical density emerges from ledger capacity",
 170  "Ω = 1 is not tuned but derived",
 171  "Dark energy density also φ-constrained"
 172]
 173
 174/-! ## The Multiverse Alternative -/
 175
 176/-- Some physicists invoke the multiverse:
 177    "We observe Ω ≈ 1 because only such universes allow observers."
 178
 179    RS rejects this:
 180    - No need for anthropic selection
 181    - Ω = 1 is dynamically selected
 182    - The single universe has Ω = 1 necessarily -/

depends on (9)

Lean names referenced from this declaration's body.