rotation_180_control

formal source

 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
 190  global_only := global_only_policy
 191  ilg_beats_mond_mean := ilg_better_mean_than_mond
 192
 193end SPARCFalsifier