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)
72noncomputable def predict_mass_sdgt (sector : Anchor.Sector) (name : String) : ℝ :=
proof body
Definition body.
73 Anchor.yardstick sector *
74 Constants.phi ^ (rung_sdgt sector name + gap sector name - 8 + cross_sector_shift sector)
75
depends on (13)
Lean names referenced from this declaration's body.
-
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
gap
in IndisputableMonolith.Gap45.Derivation
decl_use
-
Sector
in IndisputableMonolith.Masses.Anchor
decl_use
-
yardstick
in IndisputableMonolith.Masses.Anchor
decl_use
-
cross_sector_shift
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
gap
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung_sdgt
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
yardstick
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
gap
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
Sector
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
Sector
in IndisputableMonolith.Masses.RungConstructor.Basic
decl_use
-
gap
in IndisputableMonolith.RSBridge.Anchor
decl_use
-
Sector
in IndisputableMonolith.RSBridge.Anchor
decl_use