global_only_policy

formal source

 143  clag_from_phi : clag_locked = phi ^ (-(5 : ℝ))
 144  per_galaxy_params : per_galaxy_free_parameters = 0
 145
 146theorem global_only_policy : GlobalOnlyPolicy where
 147  alpha_from_phi := parameters_from_phi.1
 148  upsilon_from_phi := parameters_from_phi.2.1
 149  clag_from_phi := parameters_from_phi.2.2
 150  per_galaxy_params := zero_free_params
 151
 152/-! ## Negative Control Tests -/
 153
 154/-- Negative control: velocity permutation (shuffle v_obs across radii).
 155    Must inflate chi2 well above the ILG median. -/
 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 -/