canonical2025Q4
plain-language theorem explainer
Canonical Q4-2025 renormalization-group transport policy identity: an immutable Lean record of the external certificate name, path, generator, UTC stamp, SHA-256, and summary. Anyone comparing RS masses to PDG via a fixed SM RG scheme cites this anchor. It is a pure structure instance filling six string fields; no proof obligations.
Claim. The canonical Q4-2025 RG transport policy identity is the immutable record with policy name $\mathrm{RS\_CANONICAL\_2025\_Q4}$, certificate path $\texttt{data/certificates/rg\_transport/canonical\_2025\_q4.json}$, generator $\texttt{tools/rg\_transport\_certify.py}$, generation time $2026$-$02$-$16\,T04{:}39{:}34Z$, SHA-256 digest $558450033973f51d\ldots981bafd7$, and a nonempty summary stating that the artifact is the declared SM RG convention (scheme, loops, thresholds, integrator) used only for transport/PDG comparison, not model-layer fitting.
background
The module binds an external RG-transport certificate policy to immutable Lean metadata (name, artifact hash, path, summary). It does not run RG numerics in Lean; it supplies an auditable identity so downstream certificates can pin an exact policy artifact rather than bare transported numbers.
The carrier type is a six-field structure: policy name, certificate path, UTC generation stamp, generator script path, SHA-256 of the JSON artifact, and a human-readable policy summary. Equality and printing are derived. The doc-comment states that this definition mirrors data/certificates/rg_transport/canonical_2025_q4.json and that the stored hash is the SHA-256 of that file.
In the broader RS stack, mass comparisons to PDG data require a fixed SM running convention. This record is the Lean-side name for that convention in the 2025 Q4 canonical cut.
proof idea
Definitional structure instance, not a theorem. Each field is a string literal: policy name, relative certificate path, UTC timestamp, generator script path, the 64-hex SHA-256 of the mirrored JSON, and a two-sentence summary built by string concatenation. No tactics, no lemmas, no sorry. Downstream matchers reduce by simp or rfl against these literals.
why it matters
Gives verification certificates a single named policy object instead of ad-hoc strings. Immediate consumers are the in-module checks that the identity matches the expected name and hash, that the certificate path is the canonical JSON path, and that the summary is nonempty. Those facts let later RG-transport or mass-comparison certificates refuse silent policy drift.
Framework role is infrastructural rather than dynamical: RS mass formulas live on the phi-ladder and need a declared SM transport scheme when confronting PDG values. This definition freezes that scheme for the 2025 Q4 cut (scheme, loop order, thresholds, integrator) and records that it is for transport comparison only, not for fitting model-layer parameters. It does not itself force T5–T8 or the RCL; it anchors the external numerics those comparisons rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.