Verification Calibration Policy

The calibration policy

Verification calibration policy is the rule that decides which predictions a scientific framework may call its own and which ones it must borrow a number from the outside world to make. In Recognition Science, the framework derives its structure from a single source, the golden ratio φ = (1 + √5)/2, which emerges from a proved cost function. The policy asks a sharp question of every prediction: does it follow from φ alone, or does it need an external anchor, such as a measured constant, to set the scale?

The policy defines two modes. In dimensionless-only mode, the framework claims only ratios, exponents, and relations that follow from φ with no external input. These are zero-parameter predictions: they stand or fall on the framework's own logic. In single-anchor mode, the framework fixes exactly one SI constant, for example the reduced Planck constant ℏ from CODATA 2022, and then derives all other SI values from φ-based relations applied to that anchor. The policy is explicit that the current formalization runs in a placeholder mode: it can derive ratios and relations, but it does not claim to produce SI numerics internally.

The module that formalizes this policy, CalibrationPolicy.lean, establishes the vocabulary and the boundaries. It defines what counts as a dimensionless prediction, what counts as an SI anchor, and what counts as an SI-anchored prediction. It also records which physics modules carry a seam note, a flag that says the module uses SI units and therefore depends on an external anchor. The electron mass, quark masses, and neutrino sector all carry such notes. The policy's central declaration is that no SI constant is claimed to be derived internally in the current formalization.

One consequence follows immediately. The inverse fine-structure constant, α⁻¹, is the exception by theorem: the framework proves that its forced sector cannot pin it down, so α⁻¹ is treated as a boundary datum, not a derived ratio. This is not a failure of the framework; it is the policy working as designed. By marking which numbers are derived and which are borrowed, the policy lets a reader see exactly what the framework claims to explain and what it takes as given.

For a reader, the policy is a promise of legibility. It means that every numerical claim in the framework carries a label: derived from φ alone, or anchored to an external measurement. That label is what lets a claim be checked, and a claim that can be checked is a claim that can be trusted or rejected on its merits.

/-- The honest claim about constants in dimensionless-only mode.

    α⁻¹ is NOT in the derived list: the no-go of 2026-06-26
    (`Constants/AlphaGenesis/KappaGammaIrreducibility.lean`; canonical
    `Constants/AlphaGenesis/AlphaStatus.lean`) proves the forced sector cannot
    pin the electromagnetic coupling, so it is a boundary datum. An earlier
    version of this string named α⁻¹ among the derived ratios, which is the
    sentence the library forbids. -/
def dimensionlessOnlyClaim : String :=
  "RS derives dimensionless ratios (mass ratios and the like) from φ alone. " ++
  "The inverse fine-structure constant is the exception by theorem: RS proves " ++
  "the forced sector cannot pin it, so α⁻¹ is a boundary datum, not a derived ratio. " ++
  "SI numerical values require an external anchor (e.g., CODATA ℏ). " ++
  "No SI constants are claimed to be 'derived internally' in the current formalization."

/-- The honest claim about constants in single-anchor mode. -/
def singleAnchorClaim (anchor : SIAnchor) : String :=
  "RS derives all SI constants from φ plus one external anchor: " ++ anchor.name ++
  " (" ++ anchor.source ++ "). " ++
  "All other SI values follow from φ-based relations applied to this anchor."

/-- The current calibration mode for the framework. -/
def currentCalibrationMode : CalibrationMode :=
  CalibrationMode.Placeholder

/-- The honest claim about constants in dimensionless-only mode.

    α⁻¹ is NOT in the derived list: the no-go of 2026-06-26
    (`Constants/AlphaGenesis/KappaGammaIrreducibility.lean`; canonical
    `Constants/AlphaGenesis/AlphaStatus.lean`) proves the forced sector cannot
    pin the electromagnetic coupling, so it is a boundary datum. An earlier
    version of this string named α⁻¹ among the derived ratios, which is the
    sentence the library forbids. -/
def dimensionlessOnlyClaim : String :=
  "RS derives dimensionless ratios (mass ratios and the like) from φ alone. " ++
  "The inverse fine-structure constant is the exception by theorem: RS proves " ++
  "the forced sector cannot pin it, so α⁻¹ is a boundary datum, not a derived ratio. " ++
  "SI numerical values require an external anchor (e.g., CODATA ℏ). " ++
  "No SI constants are claimed to be 'derived internally' in the current formalization."

What this page does not claim

The policy does not claim that any SI constant is derived internally in the current formalization. The policy does not claim that the framework derives the fine-structure constant from φ alone.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/CalibrationPolicy.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: