RenderedClaim
plain-language theorem explainer
A three-field record that packages one dimensionless claim for display: string identifier, human-readable statement, and a boolean proved flag. Verification exporters and claim lists cite it as the unit of rendered output. Pure data carrier with automatic Repr; no mathematical content is proved here.
Claim. A rendered claim is a triple $(\mathrm{id},\,\mathrm{statement},\,\mathrm{proved})$ where $\mathrm{id}$ and $\mathrm{statement}$ are strings and $\mathrm{proved}\in\{\mathrm{true},\mathrm{false}\}$ records whether the claim is established.
background
The Verification.Rendered module turns internal Recognition Science results into exportable, human-readable summaries. Dimensionless claims (ratios and pure numbers free of unit choice) are the natural objects to surface: gate equalities, minimal periods, and cover existence statements.
A rendered claim is only a presentation shell. The id field names the claim for lookup; statement holds prose or symbolic text; proved is a boolean status bit. Mathematical substance lives elsewhere in the monolith (cost algebra, eight-tick structure, Clifford bridge). Upstream edges that appear in the dependency graph are incidental name collisions on common identifiers such as identity maps and conjunction, not semantic inputs to this record.
proof idea
No proof. The declaration is a structure with three fields and deriving Repr. Lean generates the representation instance; there are no tactics, lemmas, or obligations.
why it matters
This record is the element type of dimlessClaimsRendered, the example list of exportable dimensionless claims. That list currently surfaces the kinetic gate equality, the lower bound that the minimal period is at least 8, and existence of a cover with period exactly 8. Those entries sit on the T7 eight-tick octave landmark in the forcing chain (period $2^3$). Without a uniform claim carrier, the verification layer cannot assemble a stable, machine-readable export of which dimensionless statements are marked proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.