def definition def or abbrev

`Jphi_penalty`

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

formal statement (Lean)

  92def Jphi_penalty : ℝ := phi - 3 / 2

proof body

Definition body.

  93
  94/-! ## §2. The closed-form identity `C = 2 - φ` -/
  95
  96/-- **THEOREM.** `C = φ⁻² = 2 - φ`. Proof: `φ⁻² = 1/φ² = 1/(φ+1)`, and
  97    `(φ+1)(2-φ) = 2φ+2-φ²-φ = φ+2-(φ+1) = 1`, so `(φ+1)⁻¹ = 2-φ`. -/

used by (9)

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 in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
half_rung_budget_doubled in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
half_rung_components_band in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
ILGSpatialKernelCert in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
ilg_spatial_kernel_one_statement in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
Jphi_penalty_eq_Jcost_phi in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
Jphi_penalty_eq_phi_minus_three_halves in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use

depends on (3)

Lean names referenced from this declaration's body.

identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use