Verification Exclusivity Parameter Surface

Parameter surface

A parameter surface is the collection of adjustable numerical knobs that a physical framework carries. In classical physics, a theory with a coupling constant that can be set to any real value has a one-dimensional parameter surface: the real line. A theory with two such constants has a plane. A theory with none has a single point, since there is exactly one way to configure it. The concept matters because a claim that a framework has "zero free parameters" is only meaningful when the notion of a parameter is made precise.

The older definition of zero parameters identified it with having a countable state space. That definition was too weak. A framework could have a countable state space and still contain a free real-valued knob, such as a coupling constant that can be set to any number. The new approach introduces a parameter record, a type that captures the adjustable numerical knobs of a framework, together with a configuration map that says how each parameter value changes the evolution of the system. The configuration map is required to be injective: different parameter values must give genuinely different evolutions.

Within this formalization, a framework has zero free parameters when its parameter record is equivalent to the unit type, written PUnit, which has exactly one element. A framework has a free real knob when the real numbers embed into its parameter record, meaning there is an injective map from the reals into the set of configurations. The central theorem of the module proves that these two conditions are mutually exclusive: a framework cannot both have a unique configuration and admit a continuum of distinct real-valued settings.

The module demonstrates the definition on two toy examples. The first has a state space with a single element and a parameter record that is the unit type; it is proved to have zero parameters. The second has a state space of real numbers and a parameter record that is the real line, with the configuration map multiplying by the coupling; it is proved to have a free real knob and therefore not to have zero parameters. These examples show the definition separates the two cases cleanly.

In Recognition Science, the point of this formalization is to make the claim that the framework has no free parameters into a checkable statement rather than a slogan. The machine-checked library of formal theorems now contains a definition that distinguishes a genuinely parameter-free framework from one that merely has a countable state space. The definition does not by itself prove that any particular physical framework has zero parameters; it supplies the precise language in which such a claim can be stated and tested.

/-- A framework has zero free parameters if its parameter record is unique (PUnit). -/
def HasZeroParameters_Strong (F : PhysicsFramework) [HasParameterRecord F] : Prop :=
  Nonempty (ParameterRecord F ≃ PUnit.{1})

/-- A framework has at least one free ℝ knob if ℝ embeds into its parameter record. -/
def HasFreeRealKnob (F : PhysicsFramework) [HasParameterRecord F] : Prop :=
  ∃ (embed : ℝ → ParameterRecord F), Function.Injective embed

/-- Zero parameters and free knobs are mutually exclusive. -/
theorem zero_params_excludes_real_knob (F : PhysicsFramework) [HasParameterRecord F]
    (hZero : HasZeroParameters_Strong F)
    (hKnob : HasFreeRealKnob F) : False := by
  obtain ⟨eqv⟩ := hZero
  obtain ⟨embed, hInj⟩ := hKnob
  -- If ParameterRecord ≃ PUnit and ℝ ↪ ParameterRecord, then ℝ ↪ PUnit
  -- But PUnit has only one element, so ℝ cannot inject into it
  have h1 : ∀ x y : ℝ, eqv (embed x) = eqv (embed y) := fun _ _ => Subsingleton.elim _ _
  have h2 : ∀ x y : ℝ, embed x = embed y := fun x y => eqv.injective (h1 x y)
  -- Pick two different reals
  have hne : (0 : ℝ) ≠ 1 := by norm_num
  exact hne (hInj (h2 0 1))

/-- The toy framework genuinely has zero parameters. -/
theorem toy_has_zero_params : HasParameterRecord.HasZeroParameters_Strong toyZeroParamFramework :=
  ⟨Equiv.refl PUnit.{1}⟩

/-- The one-parameter framework has a free real knob. -/
theorem oneParam_has_knob : HasParameterRecord.HasFreeRealKnob oneParamFramework :=
  ⟨id, fun _ _ h => h⟩

/-- The one-parameter framework does NOT have zero parameters. -/
theorem oneParam_not_zero : ¬HasParameterRecord.HasZeroParameters_Strong oneParamFramework := by
  intro hZero
  exact HasParameterRecord.zero_params_excludes_real_knob oneParamFramework hZero oneParam_has_knob

What this page does not claim

No specific physical framework is proved to have zero free parameters in this module. The definition does not address parameters that are discrete rather than real-valued. The module does not show that the old countable-state-space definition is inconsistent, only that it is too weak.

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