AuditItem
plain-language theorem explainer
AuditItem defines a record type for cataloging individual invariants in the Recognition Science audit report, with fields for name, category, proof status, external dependency flag, and optional value. It is instantiated by auditItems and audit_json_report to produce deterministic JSON summaries of proven unitless results such as eight-tick minimality. The declaration is a plain structure that derives Repr for display and is used directly in list constructions downstream.
Claim. A record type with fields name : String, category : String, status : String (values such as ``Proven'', ``Scaffold'', or ``Planned''), usesExternalInput : Bool, and value : Option String (default none).
background
The Audit module supplies M1 scaffolding that emits a deterministic JSON summary of already-proven unitless invariants. Upstream constants include the status definition from RSNativeUnits, which records base units with tick and voxel normalized to 1, c = 1 voxel/tick, coherence quantum φ^{-5}, action quantum ħ = φ^{-5}, and the φ-ladder phiRung n = φ^n. Gap-weight functions f_gap from AlphaHigherOrder and GapWeight supply logarithmic corrections derived from the eight-tick projection. The structure is populated with concrete items such as EightTickMinimality (status Proven) and planned cosmology quantities that require external input.
proof idea
Plain structure definition that derives the Repr instance for representation.
why it matters
AuditItem supplies the data carrier for auditItems and audit_json_report, which together generate the machine-readable M1 summary. It directly catalogs core invariants that trace to the forcing chain steps establishing the eight-tick octave and three spatial dimensions, while marking cosmology entries as planned. The definition closes the immediate scaffolding surface for unitless invariants and leaves the numeric-value and external-input extensions for later milestones.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.