Foundation Inevitability Equivalence No Free Parameters

What no free parameters means

The phrase "no free parameters" usually signals a hope, not a result. In Recognition Science it names a proved statement. The framework's machine-checked library of formal theorems contains a declaration, noFreeParameters, which proves that a cost function, a rule that assigns a price to each possible state, is uniquely determined by its basic axioms. The theorem states that any cost function which satisfies five conditions, normalization, reciprocal symmetry, non-negativity, smoothness, and a calibration condition, must equal the specific function J(x) = (x + 1/x)/2 - 1. This is not a claim that the universe has no adjustable dials; it is a claim that within this framework, the cost function has no alternatives.

The five conditions are plain. Normalization says the cost of the identity state is zero. Reciprocal symmetry says the cost of a state and its inverse are the same. Non-negativity says no cost is negative. Smoothness says the function changes gradually. Calibration fixes the scale of curvature at one point. The theorem, named noFreeParameters, proves that any cost function meeting all five must be J. The proof chains through a series of lemmas, including the uniqueness of the golden ratio as the positive solution to x² = x + 1, and the fact that the only state with zero cost is the identity.

What the declaration does not claim is just as important. It does not claim that the five conditions are true of the physical world; that is a separate modeling choice. It does not claim that every constant in physics is derived, only that the cost function itself has no free parameters once the axioms are accepted. The theorem is a piece of mathematics, not a statement about which axioms nature obeys. The framework's library proves the implication, not the premises.

The consequence is a sharpened sense of what "no alternatives" can mean. Within the framework, any rival cost function must either violate one of the five conditions or add a parameter. This is a precise, checkable statement. It turns a vague slogan into a formal result, and it leaves the question of whether the axioms match experiment entirely open.

/-- NoFreeParameters holds: J is uniquely determined by the axiom bundle. -/
theorem noFreeParameters : NoFreeParameters := inevitability_chain
  (fun x hx => concrete_inevitability.defect_char x hx)
  concrete_inevitability.nothing_infinite
  concrete_inevitability.phi_unique

/-- φ is the unique positive solution to x² = x + 1. -/
theorem phi_unique_pos : ∃! x : ℝ, x > 0 ∧ x^2 = x + 1 := by
  use (1 + sqrt 5) / 2
  constructor
  · constructor
    · -- x > 0
      have h5 : sqrt 5 > 0 := sqrt_pos.mpr (by norm_num)
      linarith
    · -- x^2 = x + 1
      have h5 : sqrt 5 ^ 2 = 5 := sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
      ring_nf
      rw [h5]
      ring
  · -- uniqueness
    intro y ⟨hy_pos, hy_eq⟩
    have h5 : sqrt 5 ^ 2 = 5 := sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
    nlinarith [sq_nonneg (y - (1 + sqrt 5) / 2), sq_nonneg (y - (1 - sqrt 5) / 2),
               sq_nonneg y, h5, sq_nonneg (sqrt 5 - 2), sqrt_nonneg 5]

/-- The concrete inevitability conditions are satisfied. -/
noncomputable def concrete_inevitability : ConcreteInevitability := {
  phi_unique := phi_unique_pos
  defect_char := fun x hx => defect_zero_iff_one hx
  nothing_infinite := nothing_cannot_exist
}

What this page does not claim

The five axioms are true of the physical world. All physical constants are derived within the framework. The theorem proves that no alternative framework with different axioms could exist.

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/Foundation/InevitabilityEquivalence.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: