SingleCalibration
plain-language theorem explainer
SingleCalibration encodes the proposition that a unique positive length scale determines all dimensionful constants once fixed. Researchers formalizing parameter-free derivations within Recognition Science would reference it when closing the absolute inevitability layer. The definition is supplied directly as an existential statement on the calibration length together with derivation relations.
Claim. There exists a unique positive real number $ℓ_0$ such that for all real numbers $τ_0$, $c$, $ℏ$, $G$ the relation $τ_0 = ℓ_0 / c$ holds and every other dimensionful constant is likewise derived from $ℓ_0$.
background
The InevitabilityEquivalence module bridges abstract inevitability slogans with concrete cost and CPM conditions. Single calibration realizes the absolute layer: once one length scale is fixed, all constants follow without free parameters. Upstream results include the explicit RS-native form of the gravitational constant $G = λ_{rec}^2 c^3 / (π ℏ)$ and structural bridges that pack models into traceable CPM structures.
proof idea
The declaration is a direct definition of the Prop. The body states unique existence of the positive length scale, then quantifies over the derived constants and records the example relation together with a placeholder for the remaining derivations.
why it matters
It supplies the INEV_ABSOLUTE component of the master equivalence Abstract Inevitability ⟺ Concrete Cost/CPM Conditions. By encoding the single calibration point it supports the claim that the framework admits no free parameters after one scale is set. This touches the open scaffolding question of discharging the full set of abstract-to-concrete equivalences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.