def
definition
alphaInvValue
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 73.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
70/--- Compute α^{-1} ≈ 4π·11 − (f_gap + δ_κ) using rationals.
71 Use high-precision rationals: π ≈ 104348/33215 (|Δπ|≈3e−12), φ ≈ 161803399/100000000.
72 Let f_gap = w8 * ln φ with w8 ≈ 2.488254397846. ln φ via ln(1 + 1/φ) alternating series. -/
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,