structure
definition
StrongCPNumericalCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.StrongCP on GitHub at line 291.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
288
289/-- **STRONG CP NUMERICAL CERTIFICATE**.
290 Combines the structural (8-tick + J-min) and numerical (interval) statements. -/
291structure StrongCPNumericalCert where
292 predicted : theta_RS_predicted = 0
293 inside_experimental :
294 -theta_experimental_max < theta_RS_predicted ∧
295 theta_RS_predicted < theta_experimental_max
296 abs_lt : |theta_RS_predicted| < theta_experimental_max
297 gap_to_next : 1 - Real.cos (Real.pi / 4) > 0.29
298 J_cost_min : ∀ θ, thetaJCost 0 ≤ thetaJCost θ
299
300noncomputable def strongCPNumericalCert : StrongCPNumericalCert where
301 predicted := rfl
302 inside_experimental := theta_RS_inside_experimental
303 abs_lt := abs_theta_RS_lt_bound
304 gap_to_next := strong_cp_gap
305 J_cost_min := theta_zero_minimizes
306
307/-! ## Falsification Criteria -/
308
309/-- The derivation would be falsified if:
310 1. θ ≠ 0 is measured (even small nonzero)
311 2. 8-tick structure is disproven
312 3. Axion found with continuous θ relaxation -/
313structure StrongCPFalsifier where
314 theta_nonzero : Prop
315 eight_tick_wrong : Prop
316 continuous_axion : Prop
317 falsified : theta_nonzero → False
318
319end StrongCP
320end StandardModel
321end IndisputableMonolith