AbsolutePack
plain-language theorem explainer
AbsolutePack bundles SI-unit values for c, hbar, G, Lambda and lists of masses and energies into a single carrier, parameterized by a Ledger and its Bridge. Researchers handling unit displays or SI-to-RS calibration would cite this packaging to separate absolute references from dimensionless packs. The declaration is a direct structure definition with no computational content or lemmas.
Claim. Let $L$ be a ledger and $B$ a bridge over $L$. An absolute pack consists of real numbers $c_{SI}$, $hbar_{SI}$, $G_{SI}$, $Lambda_{SI}$ together with lists of real numbers for masses and energies expressed in SI units.
background
RecogSpec.Core supplies the Ledger structure, a carrier type augmented with optional state and tick bookkeeping so downstream modules can project canonical states. Its sibling Bridge is a trivial wrapper over any Ledger. Upstream constants supply the external anchors: c_SI equals the exact 2019 SI value 299792458 m/s, hbar_SI the reduced Planck constant 1.054571817e-34 J s, and G_SI the CODATA 2022 gravitational constant 6.67430e-11 m^3 kg^-1 s^-2. The module distinguishes absolute SI packaging from dimensionless equivalents used elsewhere in recognition specifications.
proof idea
The declaration is a direct structure definition; no lemmas are applied and the proof body is empty.
why it matters
AbsolutePack supplies the SI reference format required by observable payloads and unit-equivalence relations in the recognition specification. It anchors the framework's handling of external constants against the exact SI definitions of c and hbar, keeping absolute displays separate from the phi-ladder and J-cost constructions used for dimensionless packs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.