pith. machine review for the scientific record. sign in
theorem proved term proof

C_kernel_band

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)

 130theorem C_kernel_band :
 131    (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ) := by

proof body

Term-mode proof.

 132  rw [C_kernel_eq_two_minus_phi]
 133  have h_lo : 1.61 < phi := phi_gt_onePointSixOne
 134  have h_hi : phi < 1.62 := phi_lt_onePointSixTwo
 135  refine ⟨?_, ?_⟩ <;> linarith
 136
 137/-! ## §4. The half-rung budget identity
 138
 139The crown identity: `J(φ) + C = 1/2`. The penalty for one rung crossing
 140plus the kernel-amplitude saving fills exactly the half-rung budget.
 141-/
 142
 143/-- The first-rung J-cost penalty has closed form `φ - 3/2`. -/

used by (3)

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

depends on (26)

Lean names referenced from this declaration's body.