RealCertificate
RealCertificate bundles a real number with explicit lower and upper bounds together with a direct proof that the number lies strictly inside those bounds. It supplies the numeric specialization of the PhysicalCertificate requirement for claims that must be checked against CODATA or PDG intervals. The definition is a four-field structure whose only additional content is a Repr instance that formats the value and bounds for display.
claimA real certificate consists of a real number $v$, bounds $m < M$, and a proof that $m < v < M$.
background
The module states that every physical claim must be packaged as a PhysicalCertificate so that the derived value, the empirical target from CODATA or PDG, and the proof from authorized axioms are all explicit. RealCertificate is the concrete helper that realizes this packaging when the quantity is a real number. Upstream, PhysicalCertificate is declared as a class requiring a name string, a value of the carrier type, and supporting Repr and DecidableEq instances; the RealCertificate structure supplies the corresponding numeric case without the name field.
proof idea
The declaration is a plain structure definition whose four fields directly encode the value, the two bounds, and the inequality proof. The only additional content is a one-line Repr instance that concatenates the value and the interval into a readable string.
why it matters in Recognition Science
It implements the numeric case of the module's packaging rule, allowing derived real quantities (for example from the phi-ladder or spin-statistics definitions) to be presented with explicit empirical intervals. The structure therefore sits inside the Standard of Truth mechanism that enforces explicit targets and axiom-only proofs for all physical claims.
scope and limits
- Does not include a name field for the physical quantity.
- Does not record the provenance of the bounds or the derivation of the value.
- Does not enforce that the bounds come from CODATA or PDG.
- Does not discharge the proof obligation; the proof must be supplied at construction time.
formal statement (Lean)
39structure RealCertificate where
40 val : ℝ
41 target_min : ℝ
42 target_max : ℝ
43 /-- Proof that the value lies within the empirical bounds. -/
44 proof : target_min < val ∧ val < target_max
45
46instance : Repr RealCertificate where
47 reprPrec c _ :=
proof body
Definition body.
48 "PhysicalCertificate(val=" ++ repr c.val ++
49 ", bounds=[" ++ repr c.target_min ++ ", " ++ repr c.target_max ++ "])"
50
51end IndisputableMonolith