`C_is_complement_of_Jphi`

proved

show as: view math explainer →

module: IndisputableMonolith.Gravity.ILGSpatialKernel
domain: Gravity
line: 170 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.ILGSpatialKernel on GitHub at line 170.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 167  linarith
 168
 169/-- `C` is the complement of `J(φ)` within the half-rung budget. -/
 170theorem C_is_complement_of_Jphi :
 171    C_kernel = 1 / 2 - Jphi_penalty := by
 172  have h := half_rung_budget
 173  linarith
 174
 175/-- Numerical: `J(φ) + C ≈ 1/2`, with both individually positive. -/
 176theorem half_rung_components_band :
 177    (0.110 : ℝ) < Jphi_penalty ∧ Jphi_penalty < (0.120 : ℝ) ∧
 178    (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ) := by
 179  refine ⟨?_, ?_, C_kernel_band.1, C_kernel_band.2⟩
 180  · unfold Jphi_penalty
 181    have h := phi_gt_onePointSixOne
 182    linarith
 183  · unfold Jphi_penalty
 184    have h := phi_lt_onePointSixTwo
 185    linarith
 186
 187/-! ## §5. Discrimination from the competing hypothesis `C = φ⁻³ᐟ²`
 188
 189The competing value `C' = φ⁻³ᐟ² ≈ 0.486` from
 190`Gravity_From_Recognition` does NOT satisfy the half-rung budget
 191identity. We show this discrepancy formally.
 192-/
 193
 194/-- The competing amplitude `C' = φ⁻³ᐟ²`. -/
 195def C_kernel_competing : ℝ := phi ^ (-(3 / 2 : ℝ))
 196
 197/-- `C'` is positive. -/
 198theorem C_kernel_competing_pos : 0 < C_kernel_competing := by
 199  unfold C_kernel_competing
 200  exact Real.rpow_pos_of_pos phi_pos _

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.