`alpha_locked`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gravity.SPARCFalsifier on GitHub at line 73.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  70/-! ## RS Parameter Lock -/
  71
  72/-- The alpha parameter is locked to alphaLock ≈ 0.191. -/
  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 :=

papers checked against this theorem

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