Pith. sign in
inductive

CalibrationMode

definition
show as:
module
IndisputableMonolith.Verification.CalibrationPolicy
domain
Verification
line
102 · github
papers citing
none yet

plain-language theorem explainer

Enumeration of how absolute scale is fixed in Recognition Science: dimensionless-only (φ alone), single external SI anchor, or placeholder. Verification and constants modules cite it to gate SI claims. Pure inductive definition with three constructors; no proof content.

Claim. A calibration mode is one of: (i) dimensionless-only, allowing only $\varphi$-derived ratios and relations with no SI claims; (ii) single-anchor, where one external SI value (name, numerical value, source, unit) fixes absolute scale; (iii) placeholder, when no anchor has been chosen yet.

background

The Calibration Policy module separates zero-parameter Recognition Science from SI numerics. Dimensionless predictions are ratios, exponents, and relations forced by $\varphi=(1+\sqrt{5})/2$ alone. SI-anchored predictions need at least one external scale-setting constant (e.g. CODATA $\hbar$).

An SI anchor is a record: constant name, real SI value, provenance string, and unit string. The framework currently keeps placeholder constants ($\hbar=1$, $G=1$, $c=1$), which is dimensionless-only practice: ratios are meaningful, absolute SI numbers are not.

Policy choice is explicit so that SI claims cannot be smuggled in without stating the external input. Single-anchor mode is the minimal honest bridge: fix one constant, derive the rest via $\varphi$-ladder relations.

proof idea

No proof: this is an inductive type. Three constructors encode the policy states. DimensionlessOnly and Placeholder are nullary; SingleAnchor carries an SIAnchor payload. Downstream defs pattern-match on the constructors.

why it matters

Gates honesty about what the framework may claim in SI units. currentCalibrationMode is set to Placeholder, recording that absolute scale is not yet fixed. canMakeSIPredictions returns true only on SingleAnchor, false otherwise, so SI numerics are blocked unless an external anchor is declared.

This sits under the verification domain and implements the module's core distinction: $\varphi$-only content versus calibrated SI values. It does not resolve the open question of an internal absolute-scale mechanism; it only makes the policy states machine-checkable so that "no external input" claims stay consistent with the constants file.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.