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

GlobalOnlyPolicy

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)

 140structure GlobalOnlyPolicy where
 141  alpha_from_phi : alpha_locked = (1 - 1/phi) / 2
 142  upsilon_from_phi : upsilon_locked = phi
 143  clag_from_phi : clag_locked = phi ^ (-(5 : ℝ))
 144  per_galaxy_params : per_galaxy_free_parameters = 0
 145

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.