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)
83theorem born_weight_pos (C_I : ℝ) : 0 < born_weight C_I := Real.exp_pos _
proof body
Term-mode proof.
84
85/-- For the C = 2A case: born_weight = sin²(θ_s).
86 This follows from exp(-2A) = exp(2 ln sin θ) = sin²θ. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (5)
Lean names referenced from this declaration's body.
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
born_weight
in IndisputableMonolith.Gravity.CoherenceCollapse
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use