pith. machine review for the scientific record. sign in
def definition def or abbrev

auditItems

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  76def auditItems : List AuditItem :=

proof body

Definition body.

  77  [ { name := "EightTickMinimality", category := "Timing", status := "Proven", usesExternalInput := false, value := some "1" }
  78  , { name := "Gap45_Delta_t_3_over_64", category := "Timing", status := "Proven", usesExternalInput := false, value := some "0.046875" }
  79  , { name := "UnitsInvariance", category := "Bridge", status := "Proven", usesExternalInput := false, value := some "1" }
  80  , { name := "KGate", category := "Bridge", status := "Proven", usesExternalInput := false, value := some "1" }
  81  , { name := "PlanckNormalization", category := "Identity", status := "Proven", usesExternalInput := false, value := some "0.31830988618" }
  82  , { name := "RSRealityMaster", category := "Bundle", status := "Proven", usesExternalInput := false, value := some "1" }
  83  , { name := "AlphaInvPrediction", category := "QED", status := "Proven", usesExternalInput := false, value := some alphaInvValue }
  84  -- EW/QCD scaffolding (placeholders; no numeric values yet)
  85  , { name := "Sin2ThetaW_at_MZ", category := "EW", status := "Planned", usesExternalInput := true }
  86  , { name := "MW_over_MZ", category := "EW", status := "Planned", usesExternalInput := true }
  87  , { name := "AlphaS_at_MZ", category := "QCD", status := "Planned", usesExternalInput := true }
  88  -- Flavor mixing (CKM): planned, external inputs for visibility
  89  , { name := "CKM_theta12_at_MZ", category := "CKM", status := "Planned", usesExternalInput := true }
  90  , { name := "CKM_theta23_at_MZ", category := "CKM", status := "Planned", usesExternalInput := true }
  91  , { name := "CKM_theta13_at_MZ", category := "CKM", status := "Planned", usesExternalInput := true }
  92  , { name := "CKM_deltaCP", category := "CKM", status := "Planned", usesExternalInput := true }
  93  , { name := "CKM_Jarlskog_J", category := "CKM", status := "Planned", usesExternalInput := true }
  94  -- Flavor mixing (PMNS): planned, external inputs for visibility
  95  , { name := "PMNS_theta12", category := "PMNS", status := "Planned", usesExternalInput := true }
  96  , { name := "PMNS_theta23", category := "PMNS", status := "Planned", usesExternalInput := true }
  97  , { name := "PMNS_theta13", category := "PMNS", status := "Planned", usesExternalInput := true }
  98  , { name := "PMNS_deltaCP", category := "PMNS", status := "Planned", usesExternalInput := true }
  99  , { name := "PMNS_Jarlskog_J", category := "PMNS", status := "Planned", usesExternalInput := true }
 100  -- Mass ratio family (explicit φ-powers). Example mapping from Source.txt RUNG_EXAMPLES
 101  , { name := "FamilyRatio_Leptons_e_over_mu", category := "MassRatios", status := "Scaffold", usesExternalInput := false,
 102      value := some (IndisputableMonolith.URCGenerators.Numeric.phiPowValueStr (-11) 12) }
 103  , { name := "FamilyRatio_Leptons_mu_over_tau", category := "MassRatios", status := "Scaffold", usesExternalInput := false,
 104      value := some (IndisputableMonolith.URCGenerators.Numeric.phiPowValueStr (-6) 12) }
 105  , { name := "ThetaBar_Bound", category := "QCD", status := "Proven", usesExternalInput := false, value := some "0" }
 106  , { name := "ElectronG2", category := "QED", status := "Scaffold", usesExternalInput := true, value := some "0.001159652181" }
 107  , { name := "MuonG2", category := "QED", status := "Scaffold", usesExternalInput := true, value := some "0.00116591810" }
 108  ]
 109

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.