def
definition
auditItems
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.URCAdapters.Audit on GitHub at line 76.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
73def alphaInvValue : String :=
74 IndisputableMonolith.URCGenerators.Numeric.alphaInvValueStr
75
76def auditItems : List AuditItem :=
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" }