Masses Mass Genesis T10 Spring Falsifier Cert Amplitude Eq Phi21 Mul Sqrt2 Div F

The derived amplitude

The declaration amplitude_eq_phi21_mul_sqrt2_div_four is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It proves that a specific quantity, called the intended gap-one factor amplitude and denoted intendedGapOneFactorAmplitude, equals φ²¹ · (√2 / 4). Here φ is the golden ratio, approximately 1.618, and √2 is the square root of two. The theorem is a statement of equality between two real numbers, derived from earlier definitions and lemmas within the framework.

The significance of this equality is not the arithmetic itself but the number's provenance. The framework's earlier work had confined all derived constants to the rational-φ field, the set of numbers of the form p + qφ where p and q are rational numbers. This field is closed under addition, multiplication, and division, so any constant built from it stays inside it. The new amplitude, however, contains a factor of √2, and the framework proves that √2 is not in the rational-φ field. This means the amplitude is a newly derived absolute that lives outside the original envelope, a development the framework's pre-registered falsifier was designed to detect.

The theorem is part of a larger certificate that adjudicates a pre-registered falsifier. The falsifier's condition was that a newly derived emission-side absolute outside the rational-φ field would fire a reopening condition. The framework's audit shows that the amplitude's derivation is premise-free, meaning it does not rely on measured values, and that it satisfies the acceptance and rejection criteria for the intended gap-one factor. The certificate also proves that the amplitude's square, φ⁴² / 8, does lie in the rational-φ field, and that the representation of the amplitude in the widened envelope is unique.

What the declaration does not claim is equally important. It does not claim that the amplitude is a measured value from experiment; it is a derived constant. It does not claim to derive the fine-structure constant α or any other coupling constant. It does not claim that the genesis-dynamics interpretation of the off-field factor is closed; that reading remains an open target, independent of the normalization and hence of the amplitude's value. The theorem establishes a specific equality and its provenance, nothing more.

/-- The amplitude factorization: `f = φ²¹ · (√2 / 4)`, a φ-field rung
scalar times the off-field transport factor. Banked components: C9's
`intended_eq_phi21_mul_creationDepositNorm` and
`creationDepositNorm_eq_sqrt2_div_four`. -/
theorem amplitude_eq_phi21_mul_sqrt2_div_four :
    intendedGapOneFactorAmplitude = Constants.phi ^ 21 * (Real.sqrt 2 / 4) := by
  rw [intended_eq_phi21_mul_creationDepositNorm, creationDepositNorm_eq_sqrt2_div_four]

/-- **√2 ∉ ℚ(φ).** The off-field factor's base is not a rational-φ
combination. The representation `√2 = p + qφ` would force
`2pq + q² = 0` and `p² + q² = 2` (rational independence of `{1, φ}`); the
first case gives `p² = 2` and the second `(5p)² = 10`, and both `2` and
`10` are `≡ 2 mod 4`, which no perfect square is. Since
`φ = (1 + √5)/2` we have `ℚ(φ) = ℚ(√5)`, so this is exactly
"√2 ∉ ℚ(√5)". -/
theorem sqrt_two_not_inQPhi : ¬ InQPhi (Real.sqrt 2) := by
  rintro ⟨p, q, h⟩
  have h1 : (Real.sqrt 2) ^ 2 = (2 : ℝ) := Real.sq_sqrt (by norm_num)
  have h2 : ((p : ℝ) + (q : ℝ) * Constants.phi) ^ 2 = (2 : ℝ) := by
    rw [← h]; exact h1
  have heq : (((p ^ 2 + q ^ 2 : ℚ) : ℝ)) + (((2 * p * q + q ^ 2 : ℚ) : ℝ)) *
        Constants.phi =
      (((2 : ℚ) : ℝ)) + (((0 : ℚ) : ℝ)) * Constants.phi := by
    push_cast
    linear_combination h2 - ((q : ℝ) ^ 2) * Constants.phi_sq_eq
  obtain ⟨hA, hB⟩ := rat_coeff_eq_of_phi_spring heq
  have hfactor : q * (2 * p + q) = (0 : ℚ) := by linear_combination hB
  rcases mul_eq_zero.mp hfactor with hq0 | h2pq
  · subst hq0
    have hp2 : (p : ℝ) ^ 2 = (2 : ℝ) := by
      have hp2q : p ^ 2 = (2 : ℚ) := by linear_combination hA
      exact_mod_cast hp2q
    exact not_rat_sq_of_mod_four_spring 2 (by norm_num) p hp2
  · have hqeq : q = -2 * p := by linear_combination h2pq
    have hq2 : q ^ 2 = 4 * p ^ 2 := by rw [hqeq]; ring
    have h10 : (5 * p) ^ 2 = (10 : ℚ) := by linear_combination 5 * hA - 5 * hq2
    have h10R : ((5 * p : ℚ) : ℝ) ^ 2 = (10 : ℝ) := by exact_mod_cast h10
    exact not_rat_sq_of_mod_four_spring 10 (by norm_num) (5 * p) h10R

theorem inQPhi_amplitude_sq : InQPhi (intendedGapOneFactorAmplitude ^ 2) := by
  have hsq : intendedGapOneFactorAmplitude ^ 2 = Constants.phi ^ (42 : ℕ) / 8 := by
    simpa [intendedGapOneFactorAmplitude] using
      gapOne_factorAmplitude_sq_eq_phi42_div_eight
  rw [hsq]
  exact inQPhi_phi42_div_eight

/-- The representation in the widened envelope is unique: the extension is
genuinely quadratic, with `f ∉ ℚ(φ)` doing the work. -/
theorem derivedEnvelope_repr_unique {u v u' v' : ℝ}
    (hu : InQPhi u) (hv : InQPhi v) (hu' : InQPhi u') (hv' : InQPhi v')
    (h : u + v * intendedGapOneFactorAmplitude =
      u' + v' * intendedGapOneFactorAmplitude) :
    u = u' ∧ v = v' := by
  by_cases hvv : v = v'
  · subst hvv
    refine ⟨?_, rfl⟩
    linarith
  · exfalso
    have hv0 : v - v' ≠ 0 := sub_ne_zero.mpr hvv
    have h1 : (v - v') * intendedGapOneFactorAmplitude = u' - u := by
      linarith
    have hf : intendedGapOneFactorAmplitude = (u' - u) / (v - v') := by
      rw [← mul_div_cancel_right₀ intendedGapOneFactorAmplitude hv0]
      rw [show intendedGapOneFactorAmplitude * (v - v') =
        (v - v') * intendedGapOneFactorAmplitude by ring, h1]
    exact intendedGapOneFactorAmplitude_not_inQPhi
      (hf ▸ (hu'.add hu.neg).div (hv.add hv'.neg) hv0)

What this page does not claim

The declaration does not claim the amplitude is a measured value from experiment. The declaration does not claim to derive the fine-structure constant α or any other coupling constant. The declaration does not claim that the genesis-dynamics interpretation of the off-field factor is closed.

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/Masses/MassGenesis/T10SpringFalsifierCert.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: