theorem proved term proof

`C_kernel_lt_half`

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

formal statement (Lean)

 121theorem C_kernel_lt_half : C_kernel < 1 / 2 := by

proof body

Term-mode proof.

 122  rw [C_kernel_eq_two_minus_phi]
 123  have h := phi_gt_onePointFive
 124  linarith
 125
 126/-! ## §3. Numerical band -/
 127
 128/-- **THEOREM.** Numerical band: `0.380 < C < 0.390` from
 129    `1.61 < φ < 1.62` via the `2 - φ` closed form. -/

depends on (6)

Lean names referenced from this declaration's body.

phi_gt_onePointFive in IndisputableMonolith.Constants decl_use
via in IndisputableMonolith.Derivations.MassToLight decl_use
band in IndisputableMonolith.Foundation.PreLogicalCost decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
C_kernel in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
C_kernel_eq_two_minus_phi in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use