def definition def or abbrev

`strongCPNumericalCert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 300noncomputable def strongCPNumericalCert : StrongCPNumericalCert where
 301  predicted := rfl

proof body

Definition body.

 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 -/

depends on (12)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
Axion in IndisputableMonolith.Cosmology.DarkMatter decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
abs_theta_RS_lt_bound in IndisputableMonolith.StandardModel.StrongCP decl_use
strong_cp_gap in IndisputableMonolith.StandardModel.StrongCP decl_use
StrongCPNumericalCert in IndisputableMonolith.StandardModel.StrongCP decl_use
theta_RS_inside_experimental in IndisputableMonolith.StandardModel.StrongCP decl_use
theta_zero_minimizes in IndisputableMonolith.StandardModel.StrongCP decl_use