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

auditItems

show as:
view Lean formalization →

The auditItems definition assembles a fixed list of 20 AuditItem records that enumerate proven invariants from the forcing chain together with planned electroweak and flavor entries. An auditor of the monolith would cite the list to verify coverage of eight-tick minimality, phi-ladder mass ratios, and unitless predictions such as alpha inverse. The body is a direct literal construction that hard-codes each record's name, category, status flag, external-input marker, and optional value string.

claimLet $L$ be the list of audit records where each record is a 5-tuple (name, category, status, usesExternalInput, value) with status in {Proven, Scaffold, Planned}. The list begins with (EightTickMinimality, Timing, Proven, false, 1), includes (AlphaInvPrediction, QED, Proven, false, alpha inverse value), and ends with (MuonG2, QED, Scaffold, true, 0.00116591810), together with planned electroweak and CKM/PMNS entries and two explicit phi-power mass-ratio scaffolds.

background

AuditItem is the structure with fields name : String, category : String, status : String (Proven | Scaffold | Planned), usesExternalInput : Bool, and value : Option String. The module documentation states that this definition supplies audit scaffolding (M1) for a deterministic JSON summary of already-proven, unitless invariants that will later be extended with numeric values and scale-declared running quantities. Upstream results include the status definition in RSNativeUnits that records base units tick and voxel with c = 1 and the phi-ladder, the Identity proposition in LogicAsFunctionalEquation that formalizes zero-cost self-comparison, and the Mass abbrev that supplies the real-valued mass type used in the phi-power entries.

proof idea

The definition is realized by a direct list literal of 20 AuditItem constructors. No lemmas or tactics are invoked; the construction simply enumerates each record with its category drawn from Timing, Bridge, Identity, QED, EW, CKM, PMNS, and MassRatios, together with the explicit phiPowValueStr calls for the two lepton mass-ratio scaffolds.

why it matters in Recognition Science

This definition supplies the data source consumed by the downstream audit_json_report function that produces the concatenated JSON string. It fills the M1 milestone by listing invariants tied to the eight-tick octave (T7) and phi-ladder mass formulas, with placeholders for future numeric predictions inside the alpha band (137.030, 137.039). The list includes both proven entries such as AlphaInvPrediction and scaffolded mass ratios that reference the phi-power yardstick formula.

scope and limits

Lean usage

def exampleReport : String := audit_json_report

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.