audit_json_report
plain-language theorem explainer
This definition assembles a JSON string that packages a fixed collection of proven unitless invariants together with a list of planned cosmology parameters. Researchers auditing core Recognition Science claims would invoke the downstream printer to obtain this deterministic report for external checks. The construction proceeds by direct string concatenation after mapping each list entry through its JSON serializer.
Claim. A string definition that returns the JSON object containing an array of serialized audit entries (each with name, category, status, external-input flag, and optional value) drawn from the timing-bridge-identity list, followed by a second array of planned cosmological parameters.
background
AuditItem is the structure holding name, category, status (Proven/Scaffold/Planned), usesExternalInput flag, and optional value string. The auditItems definition supplies the concrete list: EightTickMinimality (Timing, Proven, value 1), Gap45_Delta_t_3_over_64 (Timing, Proven), UnitsInvariance (Bridge, Proven), KGate (Bridge, Proven), and PlanckNormalization (Identity, Proven). cosmologyItems supplies the five planned entries Omega_b, Omega_c, Omega_Lambda, Omega_k, and n_s, each marked Planned and requiring external input.
proof idea
One-line wrapper that builds two comma-separated strings via String.intercalate applied to the mapped auditItems and cosmologyItems lists, then concatenates them inside the fixed JSON skeleton with keys items and cosmology.
why it matters
Supplies the concrete output consumed by runAudit, which simply prints the report. It implements the Audit scaffolding (M1) placeholder whose module documentation states it emits a deterministic JSON summary of already-proven unitless invariants and will later incorporate numeric values and scale-declared quantities. The listed items reference framework elements such as the eight-tick minimality and units invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.