Pith. sign in
module module moderate

IndisputableMonolith.Verification.UnitsRescaledLawsCert

show as:
view Lean formalization →

Certification surface for Recognition Science laws under units rescaling with fixed light speed. Physicists checking that dimensionless RS predictions are anchor-independent cite this module. It packages the BridgeCore rescaling relation and K-gate observables into a single laws-certificate object for the verified surface.

claimThe module assembles a certificate that RS bridge laws (including the K-gate equality) remain invariant under units rescaling $U \sim U'$ that holds $c$ fixed, via the anchor-rescaling relation and bridge evaluation of observables from the verification core.

background

Recognition Science treats physical units through an anchor-rescaling relation that keeps $c$ fixed while other dimensionful anchors may change. BridgeCore supplies the minimal certified-surface infrastructure: the UnitsRescaled relation, the Observable/BridgeEval interface, and anchor_invariance, plus the canonical K-gate observables and the bridge-level equality $K_{\mathrm{gate}}$.

This module sits in the Verification domain. Its job is not to re-derive the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$), but to package the already-proved bridge invariances into a laws certificate that downstream RS-spec checks can import without reopening unit conventions.

In RS-native units one has $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$; dimensionless outputs (e.g. the $\alpha^{-1}$ band) must be stable under allowed rescalings. The certificate is the formal witness of that stability at the bridge layer.

proof idea

Definition and certificate packaging module rather than a deep proof development. It imports BridgeCore, exposes the units-rescaled laws certificate (sibling UnitsRescaledLawsCert), and wires the existing anchor-invariance and K-gate bridge equality into a single verification object. No independent forcing argument lives here; the logical content is assembly and re-export of bridge-level invariance facts.

why it matters in Recognition Science

The certified RS surface needs a single place that says: after units are rescaled with $c$ held fixed, the bridge laws still hold. This module is that place. It feeds the verification layer that checks band invariance and K-gate consistency without depending on a particular choice of anchors.

Upstream, BridgeCore already isolates UnitsRescaled, observables, and K_gate_bridge. Here those pieces become a laws certificate usable by higher verification targets. No downstream edges are recorded in the graph yet; the intended consumers are RS-spec and band-invariance checkers that refuse to treat unit choice as a free parameter.

Framework landmarks touched only indirectly: dimensionless constants (the $\alpha$ band, $\varphi$-ladder masses) are meaningful only if the bridge is units-stable. This module records that stability claim at the certificate boundary.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)