Verification Exclusivity Dimensionless Forcing

Dimensionless forcing

In physics, a dimensionful quantity carries units: meters, seconds, kilograms. A dimensionless quantity is a pure number, like a ratio or a count. The classical lesson is that units are conventions, so any theory built from a fixed set of dimensionful constants can often be rescaled. That rescaling freedom is a kind of knob: turn it and the theory changes.

Recognition Science formalizes this intuition. Its machine-checked library of formal theorems defines a framework as a system with states, observables, and a measurement map. A dimension system assigns a dimension to each observable and marks some as dimensionless. The key definition is strong zero-parameter posture: a framework with no free real-valued knobs at all. The library then proves a forcing theorem: if a framework has strong zero-parameter posture, and if any dimensionful observable would create a free real knob, then every observable in the framework is dimensionless.

The proof is a short contradiction. Suppose some observable has a dimension. By the premise, that dimensionful observable induces a genuine real-valued knob. But strong zero-parameter posture says no such knob exists. Therefore no dimensionful observable can exist, so all observables are dimensionless. The theorem is named zero_params_forces_dimensionless and it is fully checked by the machine, with no gaps.

The module goes one step further. It defines single-channel conservation: a framework with exactly one independent conserved quantity, positive in every state. From that conserved quantity one can extract a ratio by dividing by its value in a reference state. The library proves bridge B3: strong zero parameters plus single-channel conservation force a dimensionless positive ratio interface. In plain language, if the ledger has no knobs and conserves exactly one positive quantity, then all observable behavior factors through a single positive dimensionless ratio. Two states that yield the same ratio are indistinguishable by measurement.

This result matters because it shows how a parameter-free starting point constrains what a theory can look like. It is not a claim about any specific physical system. It is a structural theorem: given the right postulates, dimensionless ratios are not a choice but a consequence. The framework's library proves this consequence, and the proof is machine-checked.

/-- Strong zero-parameter posture forces dimensionless observables.

    The proof uses the non-vacuous parameter-record formalization:
    if a dimensionful observable existed, it would induce a genuine real-valued
    knob in the framework. That contradicts the theorem
    `zero_params_excludes_real_knob`. -/
theorem zero_params_forces_dimensionless (F : PhysicsFramework)
    [HasParameterRecord F]
    (hZero : HasZeroParameters_Strong F)
    (D : DimensionSystem F)
    (h_dimensionful_forces_knob :
      ∀ o, ¬ D.is_dimensionless o → HasFreeRealKnob F) :
    HasDimensionlessObservables F D := by
  intro o
  by_contra h
  exact zero_params_excludes_real_knob F hZero (h_dimensionful_forces_knob o h)

/-- Bridge B3: strong zero parameters plus single-channel conservation force a
    dimensionless positive ratio interface.

    The observable interface factors through r : S → R₊ when:
    1. The framework has no free real knobs (dimensionless observables)
    2. The ledger conserves a single quantity (one-dimensional ratio) -/
theorem bridge_B3_single_channel_forces_ratio (F : PhysicsFramework)
    [HasParameterRecord F]
    (hZero : HasZeroParameters_Strong F)
    (D : DimensionSystem F)
    (h_dimensionful_forces_knob :
      ∀ o, ¬ D.is_dimensionless o → HasFreeRealKnob F)
    (C : SingleChannelConservation F)
    (h_all_pos : ∀ s, 0 < C.conserved_quantity s)
    (h_obs_determined : ∀ s₁ s₂,
      ratio_from_conservation C s₁ = ratio_from_conservation C s₂ →
      F.measure s₁ = F.measure s₂) :
    HasDimensionlessObservables F D ∧
      ∃ (r : F.StateSpace → ℝ),
        (∀ s, 0 < r s) ∧
        (∀ s₁ s₂, r s₁ = r s₂ → F.measure s₁ = F.measure s₂) := by
  refine ⟨zero_params_forces_dimensionless F hZero D h_dimensionful_forces_knob, ?_⟩
  exact ⟨ratio_from_conservation C,
    ratio_pos_of_conservation C h_all_pos,
    h_obs_determined⟩

What this page does not claim

No claim that any specific physical theory is parameter-free. No claim that dimensionful observables are impossible in all frameworks. No claim about the empirical content of the ratio interface.

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/Exclusivity/DimensionlessForcing.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: