`parameters_from_phi`

proved

show as: view math explainer →

module: IndisputableMonolith.Gravity.SPARCFalsifier
domain: Gravity
line: 82 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.SPARCFalsifier on GitHub at line 82.

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

used by

formal source

  79noncomputable def clag_locked : ℝ := cLagLock
  80
  81/-- All three parameters are derived from phi (zero free parameters). -/
  82theorem parameters_from_phi :
  83    alpha_locked = (1 - 1/phi) / 2 ∧
  84    upsilon_locked = phi ∧
  85    clag_locked = phi ^ (-(5 : ℝ)) := by
  86  unfold alpha_locked upsilon_locked clag_locked alphaLock cLagLock
  87  exact ⟨rfl, rfl, rfl⟩
  88
  89/-- The number of per-galaxy free parameters is exactly zero. -/
  90def per_galaxy_free_parameters : ℕ := 0
  91
  92theorem zero_free_params : per_galaxy_free_parameters = 0 := rfl
  93
  94/-! ## SPARC Benchmark Values
  95
  96The theory document (line ~3304) gives benchmark chi2 values.
  97These are encoded as hypotheses (to be discharged by the Python script). -/
  98
  99/-- RS-predicted median chi2/dof across SPARC. -/
 100def predicted_median : ℝ := 2.75
 101
 102/-- The RS prediction: median chi2/dof ≈ 2.75 (within 1.0). -/
 103def H_SPARC_median : Prop :=
 104  ∃ median_obs : ℝ, abs (median_obs - predicted_median) < 1.0 ∧
 105    ILG_passes median_obs
 106
 107/-! ## Paper II Benchmark Values (Rotation-curves-Paper2-Sept-26.tex) -/
 108
 109/-- Paper II reports ILG median chi2/N = 2.75 on SPARC Q=1 subset. -/
 110def paper2_median_chi2 : ℝ := 2.75
 111
 112/-- Paper II reports ILG mean chi2/N = 4.23 on SPARC Q=1 subset. -/

papers checked against this theorem

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