Masses Mass Genesis T10 Spring Falsifier Cert Not Rat Sq Of Mod Four Spring

The arithmetic guard

A rational number is any number that can be written as a fraction of two whole numbers, like 3/4 or 22/7. The square root of a whole number is rational only in special cases: the square root of 4 is 2, and the square root of 9 is 3, but the square root of 2 is famously not a fraction. The lemma not_rat_sq_of_mod_four_spring (a machine-checked theorem in the framework's library) pins down one precise condition: if a whole number leaves a remainder of 2 when divided by 4, then its square root is never rational. For example, 6 divided by 4 leaves remainder 2, and the square root of 6 is indeed irrational.

The proof is a standard number-theory argument. Suppose a number n leaves remainder 2 modulo 4, and suppose its square root were a rational number q. Writing q as a fraction in lowest terms and squaring, the equation q² = n forces a contradiction: the numerator and denominator would both have to be even, which is impossible for a fraction in lowest terms. The theorem is private to its module, meaning it is not exported for use elsewhere, but it is fully proved with no gaps and no unproven assumptions.

In the Recognition Science framework, this lemma is a stepping stone in a larger audit. The framework works with numbers built from the golden ratio φ, forming a field called ℚ(φ), where every element is p + qφ for rational p and q. The lemma helps show that the square root of 2 lies outside this field, because if √2 were in ℚ(φ), then squaring it would produce a representation that violates the remainder condition. This fact matters for a pre-registered falsifier test: the framework needed to check whether a certain derived amplitude, involving √2, genuinely escapes the original field of allowed constants.

What the lemma does not claim is broader than what it proves. It does not say that all irrational numbers are outside ℚ(φ), nor does it characterize which square roots are rational in general. It only handles the specific case where the number leaves remainder 2 modulo 4. The lemma also does not, by itself, establish anything about the physical amplitude or its interpretation; it is purely an arithmetic fact, and the framework's larger conclusions about the falsifier firing rest on additional theorems about field membership and uniqueness of representation.

/-- No integer congruent to `2 mod 4` is a rational square. Same statement
and proof as the frozen wall's private `not_rat_sq_of_mod_four`. -/
private theorem not_rat_sq_of_mod_four_spring (n : ℕ) (hn : n % 4 = 2) (q : ℚ)
    (hq : (q : ℝ) ^ 2 = (n : ℝ)) : False := by
  have hirr : Irrational (Real.sqrt n) := by
    rw [show (n : ℝ) = ((n : ℕ) : ℝ) by norm_num, irrational_sqrt_natCast_iff]
    rintro ⟨r, rfl⟩
    have hmod : (r * r) % 4 = 0 ∨ (r * r) % 4 = 1 := by
      rcases Nat.even_or_odd r with ⟨c, hc⟩ | ⟨c, hc⟩
      · left
        rw [hc]
        have hs : (c + c) * (c + c) = 4 * (c * c) := by ring
        rw [hs]
        omega
      · right
        rw [hc]
        have hs : (2 * c + 1) * (2 * c + 1) = 4 * (c * c) + 4 * c + 1 := by
          ring
        rw [hs]
        omega
    omega
  have habs : |(q : ℝ)| = Real.sqrt n := by
    have h1 : |(q : ℝ)| ^ 2 = (Real.sqrt n) ^ 2 := by
      rw [Real.sq_sqrt (by positivity : (0 : ℝ) ≤ n), sq_abs]
      exact hq
    exact (sq_eq_sq₀ (abs_nonneg _) (Real.sqrt_nonneg _)).mp h1
  have hqcast : ((|q| : ℚ) : ℝ) = |(q : ℝ)| := by norm_cast
  exact hirr ⟨|q|, hqcast.trans habs⟩

/-- No integer congruent to `2 mod 4` is a rational square. Same statement
and proof as the frozen wall's private `not_rat_sq_of_mod_four`. -/
private theorem not_rat_sq_of_mod_four_spring (n : ℕ) (hn : n % 4 = 2) (q : ℚ)
    (hq : (q : ℝ) ^ 2 = (n : ℝ)) : False := by
  have hirr : Irrational (Real.sqrt n) := by
    rw [show (n : ℝ) = ((n : ℕ) : ℝ) by norm_num, irrational_sqrt_natCast_iff]
    rintro ⟨r, rfl⟩
    have hmod : (r * r) % 4 = 0 ∨ (r * r) % 4 = 1 := by
      rcases Nat.even_or_odd r with ⟨c, hc⟩ | ⟨c, hc⟩
      · left
        rw [hc]
        have hs : (c + c) * (c + c) = 4 * (c * c) := by ring
        rw [hs]
        omega
      · right
        rw [hc]
        have hs : (2 * c + 1) * (2 * c + 1) = 4 * (c * c) + 4 * c + 1 := by
          ring
        rw [hs]
        omega
    omega
  have habs : |(q : ℝ)| = Real.sqrt n := by
    have h1 : |(q : ℝ)| ^ 2 = (Real.sqrt n) ^ 2 := by
      rw [Real.sq_sqrt (by positivity : (0 : ℝ) ≤ n), sq_abs]
      exact hq
    exact (sq_eq_sq₀ (abs_nonneg _) (Real.sqrt_nonneg _)).mp h1
  have hqcast : ((|q| : ℚ) : ℝ) = |(q : ℝ)| := by norm_cast
  exact hirr ⟨|q|, hqcast.trans habs⟩

What this page does not claim

The lemma does not characterize all irrational numbers or all square roots. The lemma does not, by itself, establish any physical claim about the amplitude. The lemma does not prove that the falsifier has fired; that requires additional theorems.

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: