DimensionlessPrediction
plain-language theorem explainer
A record type for zero-parameter RS outputs: a real value, a human-readable formula string in terms of φ, and a Boolean saying whether Lean has checked it. Calibration and verification code cites it to list ratios and exponents that need no SI anchor. It is a plain structure definition with no proof obligations.
Claim. A dimensionless prediction is a triple $(v, f, b)$ where $v \in \mathbb{R}$ is a numerical value derived from $\varphi = (1+\sqrt{5})/2$ alone, $f$ is a string describing the $\varphi$-formula, and $b$ is a Boolean flag recording whether the value has been verified in Lean.
background
The CalibrationPolicy module separates two classes of RS claims. Dimensionless predictions are ratios, exponents, and algebraic relations fixed by $\varphi = (1+\sqrt{5})/2$ with no external scale. SI-anchored predictions need at least one laboratory constant (for example CODATA $\hbar$) to set units.
Current Constants placeholders ($c=1$, $\hbar=1$, $G=1$) put the codebase in dimensionless-only mode: ratios and ladder relations are fair game; absolute SI numerics are not. The structure packages one such zero-parameter output so lists and compliance checks can carry value, provenance string, and verification status together.
Upstream value extractors (certified analytic protocols, transformers, DeltaReal protocols) and ratio coordinates from CPT factorization supply the real numbers that fill the value field; this type does not itself compute them.
proof idea
No proof. The declaration is a three-field structure: a real value, a formula string, and a verified Boolean. Field doc-comments fix the intended meaning; inhabitants are built by structure literals elsewhere.
why it matters
This is the carrier type for the module's standard list dimensionlessPredictions, which records canonical RS outputs such as $\varphi$, $\varphi^2$, $\varphi^{-5}$ (coherence-to-reference energy), and a provisional $\alpha^{-1}$ entry. Downstream calibration modes (dimensionlessOnlyClaim, singleAnchorClaim, CalibrationCompliance) treat these records as the inventory of what may be claimed without an SI anchor.
In the broader framework the type marks the boundary between T5–T6 forced $\varphi$-structure (J-uniqueness and the golden fixed point) and any later SI scale fixing. It keeps the alpha-band and mass-ladder numerics honest: only entries with verified := true count as machine-checked dimensionless claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.