Pith. sign in
module module moderate

IndisputableMonolith.Verification.CalibrationPolicy

show as:
view Lean formalization →

Defines the verification policy that separates pure φ-derived dimensionless predictions from SI-anchored ones. Authors of RS claim certificates cite it to state whether a result needs only the golden ratio or also a single laboratory anchor such as ħ. The module is definitional: prediction types, anchor records, calibration modes, and compliance predicates, with no deep proofs.

claimA dimensionless prediction is a real number obtained only from $\varphi$. An SI-anchored prediction pairs such a number with a single laboratory anchor (e.g. $\hbar$). Calibration modes record whether the stack is dimensionless-only or single-anchor; compliance predicates assert that listed modules obey the chosen mode.

background

Recognition Science works in RS-native units where $c=1$ and the fundamental tick is $\tau_0=1$, with $\hbar=\varphi^{-5}$ and $G=\varphi^5/\pi$ fixed by the forcing chain. Many derived quantities (mass ratios, $\alpha^{-1}$ band, rung gaps) are therefore pure functions of $\varphi$ and need no external scale.

Laboratory comparison still requires at least one SI anchor. This module, in the Verification domain, formalizes that distinction: DimensionlessPrediction for φ-only reals, SIAnchor / hbar_anchor for the chosen scale, and SIAnchoredPrediction for the pair. CalibrationMode and currentCalibrationMode record the active policy; canMakeSIPredictions gates unitful claims.

Upstream is only Constants (tick and φ-native constants). The policy does not re-derive those constants; it classifies how they may be used in certificates.

proof idea

This is a definition module, no proofs. It introduces inductive or structure types for dimensionless versus SI-anchored predictions, an enumeration of calibration modes, boolean gates such as canMakeSIPredictions, and Prop-level claims (dimensionlessOnlyClaim, singleAnchorClaim, CalibrationCompliance) that packages assert against a list of calibratedModules.

why it matters in Recognition Science

Without an explicit calibration policy, RS verification pages cannot tell a referee whether a displayed number is a pure φ consequence (T5–T6 J-uniqueness and self-similar fixed point) or silently assumes an SI unit. This module supplies that firewall for the Verification layer: dimensionless-only claims stay inside the forcing chain and the RCL; single-anchor claims may quote $\hbar=\varphi^{-5}$ once and then predict other SI values.

No downstream theorems are wired yet (used_by is empty), so the module is infrastructure for future certificate checkers and for CalibrationCompliance audits of named modules. It touches the open operational question of how many external anchors RS is allowed when confronting CODATA, while keeping the α-band and mass-ladder statements clearly marked as dimensionless when they are.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)