`upsilon_locked`

definition

show as: view math explainer →

module: IndisputableMonolith.Gravity.SPARCFalsifier
domain: Gravity
line: 76 · 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 76.

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

  73noncomputable def alpha_locked : ℝ := alphaLock
  74
  75/-- The mass-to-light ratio is locked to phi ≈ 1.618. -/
  76noncomputable def upsilon_locked : ℝ := phi
  77
  78/-- The lag coupling is locked to phi^(-5) ≈ 0.090. -/
  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

papers checked against this theorem

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