Pith. sign in
module module low

IndisputableMonolith.Verification.UniqueCalibrationCert

show as:
view Lean formalization →

Verification module that packages a certificate for uniqueness of the RS calibration choice (the single scale fixing that pins units to the phi-ladder and J-cost). Auditors cite it when checking that no alternate calibration satisfies the same RecogSpec constraints. The module is thin: it imports the recognition specification and exposes one named certificate object rather than a long proof development.

claimA verification certificate asserting that the Recognition Science calibration is unique: among admissible scale fixings compatible with the recognition specification, only one choice is consistent with the $J$-cost, the self-similar fixed point $\varphi$, and the unit conventions ($c=1$, $\hbar=\varphi^{-5}$, etc.).

background

Recognition Science fixes physical units by a single calibration against the cost functional $J$ and the golden-ratio fixed point $\varphi$ forced by the self-similarity step of the forcing chain. The recognition specification (RecogSpec.Spec) states the admissible constraints those units must satisfy.

This module lives in the Verification layer. Its job is not to re-derive $J$ or $\varphi$, but to expose a named certificate that the calibration solving those constraints is unique. Downstream checkers can then treat "unique calibration" as a single audited fact rather than re-opening the scale choice.

Notation follows RS-native units: $c=1$, $\hbar=\varphi^{-5}$, and related constants tied to the phi-ladder. The certificate is the module's main surface object.

proof idea

Definition and certificate packaging module, not a multi-lemma proof development. It imports RecogSpec.Spec and Mathlib, then exposes the UniqueCalibrationCert object as the audited handle for uniqueness of the calibration. Any substantive uniqueness argument is expected to sit upstream in the specification or forcing-chain layers; this file is the verification wrapper.

why it matters in Recognition Science

Unique calibration is a gate for the rest of the RS unit system: masses on the phi-ladder, the alpha band, and the constants $c$, $\hbar$, $G$ only make sense once the scale choice is fixed and shown unique. This module gives Verification a single named certificate for that claim.

No downstream used_by edges are recorded in the graph snapshot, so it currently functions as a leaf certificate for external or top-level audits rather than an intermediate lemma inside a larger proved chain. It sits beside other Verification certificates that discharge specification obligations without reopening Foundation forcing steps (T5–T8).

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)