Pith. sign in
module module moderate

IndisputableMonolith.Verification.Exclusivity.DimensionlessForcing

show as:
view Lean formalization →

Formalizes dimension systems on framework observables and proves that a zero-parameter surface forces all observables to be dimensionless. Also packages single-channel conservation into positive ratios and the B3 bridge that single-channel bookkeeping yields a unique ratio. Cited by exclusivity and necessity arguments that eliminate free dimensional knobs. Argument is definitional setup plus short algebraic lemmas on conservation and ratios.

claimA dimension system assigns a dimension to each framework observable. If the parameter surface has zero free parameters, every observable is dimensionless. Under single-channel conservation one obtains a positive ratio of conserved quantities; the B3 bridge states that single-channel conservation forces that ratio uniquely.

background

This module sits in the Verification/Exclusivity layer. The shared Framework import supplies the core physics-framework types used by both NoAlternatives and the necessity proofs, deliberately thin so circular imports are avoided. ParameterSurface supplies a non-trivial reading of "zero free parameters": not merely a countable state space, but the absence of adjustable numerical knobs in the physics sense.

A dimension system is the assignment of dimensions to those framework observables. Dimensionless observables are the ones whose assigned dimension is trivial. Single-channel conservation is the bookkeeping hypothesis that a single conserved channel relates two positive quantities; from it one extracts a ratio and proves positivity. These pieces connect the abstract zero-parameter claim to concrete, scale-free predictions.

proof idea

Definition module with a short forcing chain, not a single deep proof. It introduces DimensionSystem and the predicate that observables are dimensionless, then records that a zero-parameter surface forces that predicate. Separately it defines single-channel conservation, derives the associated ratio and its positivity, and packages the B3 bridge: single-channel conservation forces the ratio. The steps are algebraic identities and predicate unfolding on top of Framework and ParameterSurface; no heavy analysis.

why it matters in Recognition Science

Exclusivity arguments need a precise link from "no free parameters" to "no free dimensional scales." This module supplies that link: zero parameters force dimensionless observables, so predicted numbers are pure ratios rather than dimensionful knobs. The single-channel conservation package and B3 bridge feed the same exclusivity narrative by showing that conservation in one channel pins a unique positive ratio. In the broader Recognition chain this supports the claim that the framework does not smuggle adjustable units once the parameter surface is empty, aligning with the zero-parameter and forcing-chain story used downstream in necessity proofs.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)