theorem proved term proof

`half_rung_budget`

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

formal statement (Lean)

 159theorem half_rung_budget : Jphi_penalty + C_kernel = 1 / 2 := by

Term-mode proof.

 160  rw [Jphi_penalty_eq_phi_minus_three_halves, C_kernel_eq_two_minus_phi]
 161  ring
 162
 163/-- Equivalent form: `2 J(φ) + 2 C = 1`. -/

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

C_competing_violates_budget in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
C_is_complement_of_Jphi in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
half_rung_budget_doubled in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
ilgSpatialKernelCert in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
ilg_spatial_kernel_one_statement in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use

Lean names referenced from this declaration's body.

C_kernel in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
C_kernel_eq_two_minus_phi in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
Jphi_penalty in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
Jphi_penalty_eq_phi_minus_three_halves in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use