PhysicalCertificate
plain-language theorem explainer
PhysicalCertificate packages any physical claim as a named derived value paired with an empirical target and an axiom-compliance check. Physicists auditing mass or density predictions against CODATA would cite it to confirm that only authorized axioms appear in the derivation. The declaration is a direct class definition whose proof field is a True placeholder.
Claim. Let $α$ be a type with representation and decidable equality. A certificate consists of a string name, a derived value $val : α$, an empirical target $target : α$, an error bound $error_bound : α$, a proof term of type True, and a unit axiom check.
background
The Certificates.Standard module supplies the canonical packaging for every physical claim in the repository. Upstream, Mass is the abbreviation for the reals, NucleosynthesisTiers.of records nuclear densities on the φ-ladder, and LedgerFactorization.of calibrates the J-cost on the positive reals. The local setting requires that the derived value be explicit, the target drawn from CODATA or PDG, and the proof term rely only on the authorized axioms enforced by the CI auditor.
proof idea
The declaration is a class definition that directly introduces the six fields. The proof field is set to the placeholder True and the axiom_check field to Unit; no lemmas or tactics are invoked.
why it matters
This class supplies the interface that RealCertificate instantiates for numeric claims, thereby closing the packaging requirement for all downstream physical predictions. It implements the canon rule that every claim must expose its derived value, its empirical target, and its axiom footprint. In the Recognition framework it supports the mass formula on the φ-ladder and the eight-tick octave by providing the certification layer that feeds the RealCertificate structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.