cosmologyItems
plain-language theorem explainer
cosmologyItems constructs a fixed list of eight AuditItem records for the parameters Omega_b, Omega_c, Omega_Lambda, Omega_k, n_s, r, eta_B, and N_eff. Each record carries category Cosmology, status Planned, and usesExternalInput true. Researchers generating the framework's audit JSON summary cite this list to populate the cosmology section. The definition is a direct literal enumeration with no computation or lemmas.
Claim. The definition cosmologyItems yields the list of AuditItem records for the parameters $Omega_b$, $Omega_c$, $Omega_Lambda$, $Omega_k$, $n_s$, $r$, $eta_B$, $N_{rm eff}$, where each record has category ``Cosmology'', status ``Planned'', and usesExternalInput set to true.
background
AuditItem is the structure type with fields name (String), category (String), status (String, restricted to values such as Proven, Scaffold, or Planned), usesExternalInput (Bool), and optional value (Option String). The module implements audit scaffolding (M1) whose purpose is to emit a deterministic JSON summary of a minimal set of already-proven, unitless invariants; the surface is a placeholder to be extended with numeric values and scale-declared running quantities. Upstream, the list references the RS Native Units status (which records base units tick and voxel together with the phi-ladder) and the baryon asymmetry eta_B (defined as the observed value in the MatterAntimatter module).
proof idea
The definition is a direct literal list construction that enumerates the eight cosmology AuditItem structures by explicit record literals. No lemmas are applied and no tactics are used; the body is pure data.
why it matters
The definition supplies the cosmology segment of the JSON report produced by audit_json_report, which concatenates the cosmologyItems with the main auditItems list. It completes the M1 scaffolding milestone for cosmology invariants inside the Recognition Science framework and connects to the baryon asymmetry eta_B and the RS-native units status. The entry marks the current boundary before numeric values and scale-declared quantities are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.