Constants Alpha Genesis Calibration Forcing Step Nonneg

The step is positive

A survival fraction is a number between zero and one: the share of something that remains after a load is applied. In the Recognition Science framework, the framework models a physical response as such a fraction, a function g of a nonnegative load t. The declaration step_nonneg is a proved theorem about this function at the single point t = 1, the first full step of load. It states that the survival fraction at that step is never negative: 0 ≤ g(1).

The proof is short and structural. The framework's ledger premise, factorization over independent loads, says that the survival fraction for a total load is the product of the fractions for its parts. Splitting the unit load into two halves gives g(1) = g(1/2)². A square of a real number is always nonnegative, so the step is nonnegative. This is the entire content of step_nonneg: a positivity fact derived from a multiplication rule, with no assumption about the size of the step.

The theorem does not stand alone. Its companion step_ne_zero shows the step cannot be zero, because g(1) = 0 would contradict the self-similar balance equation g(1) = 1/(1 + g(1)). Together, nonnegativity and nonzero force strict positivity: g(1) > 0. That strict positivity is what lets the balance equation select a unique root. The reciprocal of the step satisfies r² = r + 1, the defining equation of the golden ratio, so the step is forced to be φ⁻¹. This is the calibration forcing result: the step value is derived, not chosen.

In Recognition Science, this closes a gap in the derivation of the fine-structure constant's inverse. An earlier version of the framework required a calibration input, a unit convention, to fix the response's scale. The self-similar dressing removes that input: three structural premises, factorization, antitonicity, and the balance equation, force the entire response g(t) = φ⁻ᵗ on all nonnegative loads. The step_nonneg theorem is the small positivity lemma that makes the unique root possible.

What step_nonneg does not claim is just as important. It does not assert that the survival fraction is positive everywhere, only at the unit step. It does not establish the value φ⁻¹ by itself; that requires the balance equation and the nonzero result. And it says nothing about the fine-structure constant's numerical agreement with measurement, which remains a separate empirical check, not a theorem.

/-- The step is nonnegative. -/
theorem step_nonneg : 0 ≤ D.g 1 := by
  rw [D.step_eq_sq]
  exact sq_nonneg _

/-- The step is a square: `g(1) = g(1/2)²` (factorization). -/
theorem step_eq_sq : D.g 1 = D.g (1/2) ^ 2 := by
  have h := D.factorizes (1/2) (1/2) (by norm_num) (by norm_num)
  have h1 : (1/2 : ℝ) + 1/2 = 1 := by norm_num
  rw [h1] at h
  rw [h]
  ring

/-- The step is nonzero: `g(1) = 0` contradicts the balance equation. -/
theorem step_ne_zero : D.g 1 ≠ 0 := by
  intro h0
  have hbal := D.step_self_similar
  rw [h0] at hbal
  norm_num at hbal

/-- **STEP FORCING.** The balance equation has exactly one admissible
root: `g(1) = φ⁻¹`. The reciprocal of the step satisfies the T6
self-similarity equation `r² = r + 1`, whose unique positive root is φ. -/
theorem step_forced : D.g 1 = 1 / Constants.phi := by
  set ρ := D.g 1 with hρdef
  have hpos : 0 < ρ := D.step_pos
  have hbal : ρ = 1 / (1 + ρ) := D.step_self_similar
  have hsum_pos : 0 < 1 + ρ := by linarith
  have hsum_ne : (1 + ρ) ≠ 0 := ne_of_gt hsum_pos
  -- ρ² + ρ − 1 = 0
  have hmul : ρ * (1 + ρ) = 1 := by
    calc ρ * (1 + ρ) = (1 / (1 + ρ)) * (1 + ρ) := by rw [← hbal]
    _ = 1 := by field_simp
  have hquad : ρ ^ 2 + ρ - 1 = 0 := by nlinarith [hmul]
  -- 1/φ satisfies the same quadratic
  have hφ : Constants.phi ^ 2 = Constants.phi + 1 := Constants.phi_sq_eq
  have hφpos : 0 < Constants.phi := Constants.phi_pos
  have hφne : Constants.phi ≠ 0 := ne_of_gt hφpos
  have hinv_pos : 0 < 1 / Constants.phi := by positivity
  have hinv_quad : (1 / Constants.phi) ^ 2 + (1 / Constants.phi) - 1 = 0 := by
    field_simp
    nlinarith [hφ]
  -- difference of the two quadratics factors: (ρ − 1/φ)(ρ + 1/φ + 1) = 0
  have hfactor : (ρ - 1 / Constants.phi) * (ρ + 1 / Constants.phi + 1) = 0 := by
    linear_combination hquad - hinv_quad
  have hsum2_pos : 0 < ρ + 1 / Constants.phi + 1 := by linarith
  rcases mul_eq_zero.mp hfactor with h | h
  · linarith [sub_eq_zero.mp h]
  · linarith

What this page does not claim

The step is positive everywhere, only at the unit step. The value φ⁻¹ follows from step_nonneg alone, without the balance equation. The fine-structure constant's numerical agreement with measurement is a proved theorem.

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/Constants/AlphaGenesis/CalibrationForcing.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: