Pith. sign in
module module moderate

IndisputableMonolith.Verification.BridgeCore

show as:
view Lean formalization →

Defines the anchor-rescaling relation used by Recognition verification bridges: time and length anchors scale by the same factor s>0 while c stays fixed. Introduces dimensionless observables, bridge evaluation, and the K-gate observables that sit on top of that relation. Downstream certificates and RecogSpec bands import it to treat unit choice as an equivalence rather than a free parameter. Mostly definitional scaffolding with invariance lemmas.

claimThe module fixes an anchor-rescaling relation on RS units packs: scale the time and length anchors by a common factor $s>0$, hold $c$ fixed, and treat two packs as equivalent when one is obtained from the other this way. It packages dimensionless observables, bridge evaluation maps, anchor-invariance statements, and the $K_A$, $K_B$, $K_{\mathrm{gate}}$ bridge observables built on that relation.

background

Recognition Science works in native units with a fundamental time quantum $\tau_0$ equal to one tick (from Constants). Physical predictions that matter for certificates are dimensionless or ratio-like, so absolute choice of time and length anchors should drop out once $c$ is held fixed.

This module sits in the Verification layer. It introduces the relation that identifies units packs related by a common positive scale $s$ on the time and length anchors, together with the supporting notions of dimensionless quantities, observables, and bridge evaluation. The local convention is that $c$ is invariant under the rescaling, so light-cone structure is not deformed.

Sibling names in the module (UnitsRescaled, Dimensionless, Observable, BridgeEval, anchor_invariance, and the $K$-gate observables) are the vocabulary later certificates use when they say a law is units-invariant.

proof idea

This is primarily a definition module: it declares the anchor-rescaling relation, the dimensionless and observable wrappers, bridge evaluation, and the named $K_A$, $K_B$, $K_{\mathrm{gate}}$ bridge observables. Supporting lemmas (notably anchor invariance) are short structural facts about that relation rather than a long derivation chain. Heavier algebraic closure (reflexivity, symmetry, transitivity of rescaling) is certified downstream, not proved in bulk here.

why it matters in Recognition Science

Verification certificates must not depend on an arbitrary choice of RS anchors. This module supplies the equivalence relation and the observable layer that make that claim checkable. It is imported by RecogSpec.Bands and RecogSpec.Spec, so recognition-band statements can be stated in units-invariant form, and by Verification.UnitsRescaledLawsCert, whose doc-comment records closure properties of UnitsRescaled: reflexivity, symmetry, and transitivity of anchor rescaling. Without this core, units-rescaled law certificates and dimensionless bridge gates have no shared carrier.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)