auditItems
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.