def
definition
velocity_permutation_control
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.SPARCFalsifier on GitHub at line 159.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
156def NegativeControl := ℝ → Prop
157
158/-- Velocity permutation: randomly reassign v_obs to different radii. -/
159def velocity_permutation_control (chi2_perm : ℝ) : Prop :=
160 paper2_median_chi2 < chi2_perm
161
162/-- 180-degree rotation: reverse the radial profile. -/
163def rotation_180_control (chi2_rot : ℝ) : Prop :=
164 paper2_median_chi2 < chi2_rot
165
166/-- Gas-stars swap: interchange v_gas and v_disk. -/
167def gas_stars_swap_control (chi2_swap : ℝ) : Prop :=
168 paper2_median_chi2 < chi2_swap
169
170/-- All negative controls must inflate chi2 above the ILG result. -/
171def all_controls_inflated (chi2_perm chi2_rot chi2_swap : ℝ) : Prop :=
172 velocity_permutation_control chi2_perm ∧
173 rotation_180_control chi2_rot ∧
174 gas_stars_swap_control chi2_swap
175
176/-! ## Certificate -/
177
178structure SPARCFalsifierCert where
179 zero_params : per_galaxy_free_parameters = 0
180 params_from_phi : alpha_locked = (1 - 1/phi) / 2 ∧ upsilon_locked = phi ∧
181 clag_locked = phi ^ (-(5 : ℝ))
182 criterion_decidable : ∀ x : ℝ, ILG_falsified x ∨ ILG_passes x
183 global_only : GlobalOnlyPolicy
184 ilg_beats_mond_mean : paper2_mean_chi2 < mond_mean_chi2
185
186theorem sparc_falsifier_cert : SPARCFalsifierCert where
187 zero_params := zero_free_params
188 params_from_phi := parameters_from_phi
189 criterion_decidable := falsification_decidable