SIAnchoredPrediction
plain-language theorem explainer
Records a numerical SI prediction that depends on one external scale anchor plus φ-derived relations. Verification and constants modules use it to separate zero-parameter dimensionless claims from values that need CODATA-style input. It is a plain data structure: name, anchor, real value, and a derivation-path string.
Claim. An SI-anchored prediction is a record $(n, A, v, d)$ where $n$ is the quantity name, $A$ is an external SI anchor (name, numerical value, source, unit), $v \in \mathbb{R}$ is the predicted SI value, and $d$ is a string describing the derivation from $\varphi$ together with $A$.
background
The CalibrationPolicy module separates two classes of RS claims. Dimensionless predictions (ratios, exponents, ladder relations) follow from $\varphi = (1+\sqrt{5})/2$ alone and need no external input. SI-anchored predictions are absolute numbers in SI units; they require at least one external scale fix.
An SI anchor is an externally supplied constant: name, numerical value, provenance (e.g. CODATA 2022), and unit string. The module notes that Constants currently uses placeholders ($\hbar=1$, $G=1$, $c=1$), i.e. dimensionless-only mode. Claiming true SI numerics either accepts an external anchor or needs an internal absolute-scale mechanism not yet formalized.
Upstream, cost-side Calibration axioms normalize curvature of the cost functional (second derivative at the log-origin equals 1) so the J-cost is unique up to that normalization; that is a different notion of calibration from the SI scale anchor packaged here.
proof idea
No proof: this is a structure declaration. Four fields package the data of an SI-level claim: quantity name, the chosen SIAnchor, the real predicted value, and a free-text derivation path. Downstream code is expected to construct inhabitants when a calibration mode permits SI claims.
why it matters
In the Recognition framework, absolute SI numbers are not zero-parameter outputs of the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$). Native units fix $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$; converting those to SI needs an external yardstick. This structure is the typed carrier for such converted claims under single-anchor policy, keeping them distinct from pure $\varphi$ predictions.
It supports the module's policy split (dimensionless-only vs single-anchor) and the compliance story around whether SI predictions are allowed. No downstream theorems currently depend on it in the graph; it is infrastructure for stating calibrated claims cleanly rather than a step in the forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.