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)
125def hack_exponent : ℝ :=
proof body
Definition body.
126 Real.log horton_length_ratio / Real.log horton_bifurcation_ratio
127
128/-- The headline identity: `h = 1/2` exactly. -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (4)
Lean names referenced from this declaration's body.
-
horton_bifurcation_ratio
in IndisputableMonolith.Climate.RiverNetworkFromSigmaConservation
decl_use
-
horton_length_ratio
in IndisputableMonolith.Climate.RiverNetworkFromSigmaConservation
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use