RealCertificate
plain-language theorem explainer
RealCertificate packages a real number with explicit lower and upper empirical bounds together with a proof that the number lies strictly inside those bounds. It supports numeric physical claims that must be certified against CODATA or PDG targets under the canon standard. The declaration is a direct structure definition with an accompanying Repr instance for formatted output.
Claim. A structure consisting of a real number $v$, real bounds $a < b$, and a proof that $a < v < b$.
background
The module sets the Standard of Truth for the Canon: every physical claim must be packaged as a PhysicalCertificate. That class requires an explicit name for the quantity, the derived value of the appropriate type, and a proof relying only on authorized axioms. RealCertificate supplies a concrete helper for the real-number case and depends on the PhysicalCertificate class, the phi-ladder lattice hypothesis structure, and the spin-statistics value definition.
proof idea
The declaration is a structure definition that introduces four fields (value, lower bound, upper bound, and the conjunction proof of the two strict inequalities) followed by a Repr instance that produces a formatted string. No lemmas or tactics are invoked; the construction is purely structural.
why it matters
The structure implements the packaging requirement stated in the PhysicalCertificate class so that real-valued predictions can be presented with explicit empirical targets. It therefore participates in the canon-level certification of quantities derived from the phi-ladder or from spin statistics, even though no downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.