Pith. sign in
module module moderate

IndisputableMonolith.Verification.CalibrationPolicy

show as:
view Lean formalization →

Policy layer that separates pure φ-derived dimensionless predictions from SI-unit claims that need an explicit anchor (for example ħ). Verification authors cite it to state whether a module is dimensionless-only, single-anchor, or fully calibrated. The module is definitional: structures, mode flags, and compliance predicates, not deep proofs.

claimA dimensionless prediction is a real number obtained only from $\varphi$. An SI-anchored prediction pairs such a number with a fixed SI anchor (e.g. $\hbar$). Calibration mode is dimensionless-only, single-anchor, or calibrated; compliance records which modules may emit SI claims under the active mode.

background

Recognition Science works in native units where $c=1$, $\hbar=\varphi^{-5}$, and $G=\varphi^5/\pi$, with masses on the $\varphi$-ladder. Dimensionless ratios (fine-structure band, mass ratios, tick counts) are therefore pure functions of $\varphi$ and need no laboratory scale. Converting a prediction into SI units requires at least one external anchor so that the native yardstick is fixed against experiment.

This module sits in the Verification domain and imports only Mathlib and Constants (including the RS time quantum $\tau_0=1$ tick). It introduces the vocabulary that later certificates use: dimensionless predictions, SI anchors such as the $\hbar$ anchor, SI-anchored predictions, and a small calibration-mode enum with a current mode and a predicate for whether SI predictions are allowed.

proof idea

This is a definition module, no substantive proofs. It declares structures for dimensionless and SI-anchored predictions, an anchor for $\hbar$, a calibration-mode type with a current mode, boolean gates such as whether SI predictions are permitted, named claims (dimensionless-only and single-anchor), a list of calibrated modules, and a compliance record tying those pieces together.

why it matters in Recognition Science

Without an explicit calibration policy, a verifier could silently treat a pure $\varphi$ number as an SI quantity or hide an extra fitted constant. This module forces every downstream certificate to declare its mode: dimensionless-only (safe for $\alpha^{-1}$ band checks and ladder ratios), single-anchor (one SI scale fixed), or calibrated. Parent consumers are verification and certificate layers that import CalibrationPolicy; the sibling claims and Compliance structure are the hooks those layers read. It does not itself prove a forcing-chain step (T5–T8) or the RCL identity; it polices how constants from that chain are reported against experiment.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)