Constants Alpha Genesis Calibration Forcing Step Pos

The forced step

The declaration step_pos establishes a small but load-bearing fact about a self-similar dressing, which is a survival fraction: the share of something that persists under an increasing load. The framework models this survival fraction as a function g(t) of a nonnegative load t. The declaration proves that the value at the single step, g(1), is strictly positive. That sounds modest, but positivity is what lets the framework derive the step's exact value rather than assume it.

The proof runs through two intermediate results. Factorization over independent loads gives g(1) = g(1/2)², so the step is a square and therefore nonnegative. The self-similar balance equation, g(1) = 1 / (1 + g(1)), rules out zero: if g(1) were 0, the equation would read 0 = 1, a contradiction. Combining nonnegativity with nonzero yields strict positivity. This is the classical move of excluding a degenerate root before solving for the good one.

With positivity in hand, the framework's library proves the full forcing result: the balance equation has exactly one admissible root, namely g(1) = φ⁻¹, the reciprocal of the golden ratio. The reciprocal of the step satisfies r² = r + 1, the self-similarity equation whose unique positive root is φ. So the step is not a free parameter; it is derived from the same structural premises that force the recognition measure itself. The framework's library then extends this to all nonnegative loads, showing every self-similar dressing equals the forced measure φ⁻ᵗ.

What step_pos does not claim is any empirical content. It says nothing about measured values, CODATA references, or the fine-structure constant α. The declaration lives in a chain that eventually constructs an α object, but step_pos itself is purely structural: it establishes a positivity fact about a mathematical function under stated axioms. The connection to physical constants is a separate, later step, and the framework's own documentation marks the α expression as an identification, not a derived coupling.

/-- The step is strictly positive (derived, not assumed). -/
theorem step_pos : 0 < D.g 1 :=
  lt_of_le_of_ne D.step_nonneg (Ne.symm D.step_ne_zero)

/-- 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 nonnegative. -/
theorem step_nonneg : 0 ≤ D.g 1 := by
  rw [D.step_eq_sq]
  exact sq_nonneg _

/-- 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

/-- **CALIBRATION FORCING.** Every self-similar dressing is the forced
measure on nonnegative loads: `g(t) = φ⁻ᵗ`. No derivative condition, no
unit convention, no calibration input. -/
theorem response_forced : ∀ t : ℝ, 0 ≤ t →
    D.g t = Foundation.MeasureForcing.contWeight t := by
  intro t ht
  have hstep : D.g 1 = Foundation.MeasureForcing.rho := by
    rw [D.step_forced]
    rfl
  exact Foundation.MeasureForcing.continuum_weight_forced
    D.factorizes D.antitone hstep t ht

What this page does not claim

No claim that step_pos establishes any empirical value or measured constant. No claim that the fine-structure constant α is derived by step_pos alone. No claim that the self-similar balance equation has multiple admissible roots.

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: