Verification Bridge Core

The bridge core

Verification bridge core is the part of Recognition Science that makes a promise precise: the numbers the framework reports do not change when you rescale your units. In physics, a measurement like a speed depends on whether you use meters or feet. The framework's core numbers are meant to be like ratios, which stay the same under such a change. The framework defines a rescaling relation, UnitsRescaled, which says that two unit systems are related when you multiply both the time and length anchors by the same positive number, leaving the speed of light fixed. It then proves, as a theorem, that any observable built to be dimensionless under this relation gives the same value in either system.

The classical idea here is dimensional analysis, the practice of checking that an equation's units balance. The framework's contribution is to make that check formal. It defines an Observable as a function from unit systems to real numbers that is invariant under rescaling, and a BridgeEval as the act of evaluating such an observable at a particular unit system. The theorem anchor_invariance states that this evaluation does not depend on which rescaled anchors you pick. In plain language: if two people use different but related unit systems, they compute the same number for any observable the framework recognizes.

The framework then applies this to a specific constant, the K-gate. It defines two observables, K_A_obs and K_B_obs, each of which simply returns the framework's constant K regardless of units. The theorem K_gate_bridge proves that these two observables agree identically: for every unit system, evaluating the first gives the same number as evaluating the second. This is the bridge-level equality, and it is what the larger verification infrastructure builds on. The framework is deliberately small, containing only this minimal bridge-invariance machinery, so that the certified import-closure stays small and free of unrelated scaffolding.

What this establishes, in the framework's own account, is that the K-gate constant is not an artifact of a particular choice of units. The framework models the constant as a genuine feature of its recognition ledger, a discrete record of events, rather than a convention-dependent display. The machine-checked library of formal theorems guarantees that the invariance proof is complete and axiom-clean. The consequence is that when the framework reports a number, it comes with a certificate: the number is the same under any allowed rescaling, and two independent routes to it agree exactly.

/-- Anchor-invariance (Q): evaluation does not depend on rescaled anchors. -/
theorem anchor_invariance (O : Observable) {U U'}
  (hUU' : UnitsRescaled U U') : BridgeEval O U = BridgeEval O U' := O.dimless hUU'

/-- The two route displays agree identically as observables (bridge-level K-gate). -/
theorem K_gate_bridge : ∀ U, BridgeEval K_A_obs U = BridgeEval K_B_obs U := by
  intro U; simp [BridgeEval, K_A_obs, K_B_obs]

/-- Anchor rescaling relation: scale time and length anchors together by s>0, keep c fixed. -/
structure UnitsRescaled (U U' : RSUnits) where
  s    : ℝ
  hs   : 0 < s
  tau0 : U'.tau0 = s * U.tau0
  ell0 : U'.ell0 = s * U.ell0
  cfix : U'.c = U.c

What this page does not claim

This framework does not prove that the K-gate constant has any particular numerical value. The bridge core does not establish that all framework numbers are dimensionless, only those built as Observables. No claim is made here about how the bridge core relates to the physical recognition-to-linking bridge, which remains open.

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/BridgeCore.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: