canMakeSIPredictions
plain-language theorem explainer
Boolean gate: SI-unit predictions are policy-valid only when calibration is single-anchor mode. Dimensionless-only and placeholder modes return false. Anyone stating SI numerics from the φ-ladder cites this to stay honest about external scale. Proof is a one-clause match on the calibration inductive.
Claim. Given a calibration mode $m$, return $\mathsf{true}$ if and only if $m$ is single-anchor form (one fixed SI scale, e.g. $\hbar$ from CODATA); return $\mathsf{false}$ for dimensionless-only mode and for placeholder mode.
background
The Calibration Policy module separates two classes of RS claims. Dimensionless predictions are ratios, exponents, and φ-relations with no external input (φ = (1+√5)/2). SI-anchored predictions are absolute SI numbers and need at least one external scale fix.
CalibrationMode is the inductive that records how absolute scale is chosen: DimensionlessOnly (no SI claims), SingleAnchor carrying an SIAnchor (e.g. ℏ), or Placeholder (no anchor yet). The module notes that Constants.lean still uses placeholders (ħ=1, G=1, c=1), i.e. dimensionless-only practice.
This predicate is the mechanical answer to "may we emit SI numerics under the current mode?" It does not itself choose the anchor; it only reads the mode.
proof idea
Definition by exhaustive match on CalibrationMode. The SingleAnchor constructor (ignoring which concrete anchor) yields true; DimensionlessOnly and Placeholder yield false. No lemmas, no tactics: pure pattern dispatch.
why it matters
Keeps SI claims from leaking into dimensionless-only or placeholder runs. Downstream honest-claim scaffolding in the same module (dimensionlessOnlyClaim, singleAnchorClaim, CalibrationCompliance) is meant to consult this gate so the framework does not overclaim absolute scale.
In RS terms, φ-ladder mass and constant relations (c=1, ħ=φ^{-5}, G=φ^5/π, α^{-1} band) are dimensionless or ratio-level until one SI anchor is fixed. The module doc is explicit: SI predictions require either an external anchor (breaking pure zero-parameter status) or an internal scale-fixing mechanism not yet formalized. This def is the policy bit that enforces that distinction. No used_by edges yet; it is infrastructure for compliance checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.