Masses Mass Genesis T10 Jcost Transcendental Is Integral Rat Cast Real

Integrality of rationals

In mathematics, a number is algebraic if it is the root of a polynomial with integer coefficients. Every rational number, such as 3/4 or -7/2, is algebraic: the number p/q solves qx - p = 0, a linear polynomial with integer coefficients q and -p. The declaration isIntegral_ratCast_real in the framework's machine-checked library of formal theorems restates this classical fact in the precise language of algebra: it proves that any rational number, viewed as a real number, is integral over the rationals. Being integral over the rationals is a slightly stronger condition than being algebraic, but for rational numbers the two coincide; the declaration supplies the explicit polynomial X - q, which is monic (its leading coefficient is 1) and has q as its root.

The proof is short and direct. The declaration constructs the polynomial X - q, verifies it is monic, and then evaluates it at q using the algebraic structure of the real numbers. The calculation reduces to q - q = 0, which is exactly what it means for q to be a root. This is not a deep theorem about transcendental numbers; it is a foundational fact about how rational numbers sit inside the real numbers, recorded in a form the framework can use in larger arguments.

In Recognition Science, this declaration supports a larger argument about the algebraic and transcendental split of certain constants. The framework proves that the per-post recognition J-cost cosh 1 - 1 is transcendental, meaning it is not the root of any polynomial with integer coefficients. It also proves that the factor amplitude f = φ²¹ / (2√2) is algebraic, since φ and √2 are algebraic and algebraic numbers are closed under powers and multiplication. The declaration isIntegral_ratCast_real contributes to this by confirming that rational numbers, which appear throughout the construction, are algebraic. This matters because the framework's argument needs to show that no nonzero integer multiple of the transcendental cost can equal the algebraic amplitude: a transcendental number times a nonzero rational number is still transcendental, so it can never equal an algebraic number.

The declaration does not claim that all real numbers are algebraic, nor does it claim anything about the transcendence of cosh 1 - 1 by itself. It is a narrow, foundational statement about rational numbers. The transcendence of cosh 1 - 1 is a separate theorem in the same module, proved using the classical result that e is transcendental. The declaration isIntegral_ratCast_real is a building block, not the main result; it ensures that the rational coefficients used in the framework's constructions behave as expected.

theorem isIntegral_ratCast_real (q : ℚ) : IsIntegral ℚ ((q : ℝ)) :=
  ⟨X - C q, Polynomial.monic_X_sub_C q, by
    rw [← Polynomial.aeval_def]
    simp only [map_sub, aeval_X, aeval_C, eq_ratCast (algebraMap ℚ ℝ), sub_self]⟩

/-- The per-post recognition J-cost `cosh 1 - 1` is transcendental over ℚ. -/
theorem transcendental_cosh_one_sub_one : Transcendental ℚ (Real.cosh 1 - 1) := by
  intro hc
  have h1 : IsAlgebraic ℚ (Real.cosh 1) := by
    rw [isAlgebraic_iff_isIntegral] at hc ⊢
    have hone : IsIntegral ℚ (1 : ℝ) := isIntegral_one
    have heq : Real.cosh 1 = (Real.cosh 1 - 1) + 1 := by ring
    rw [heq]
    exact IsIntegral.add hc hone
  exact transcendental_cosh_one h1

/-- The factor amplitude is algebraic over ℚ: `f = φ²¹ · (√2/4)` with `φ`
and `√2` integral. -/
theorem isAlgebraic_intended : IsAlgebraic ℚ intendedGapOneFactorAmplitude := by
  rw [isAlgebraic_iff_isIntegral,
    SpringFalsifierCert.amplitude_eq_phi21_mul_sqrt2_div_four]
  have hsqrt2div4 : IsIntegral ℚ (Real.sqrt 2 / 4) := by
    refine ⟨X ^ 2 - C (1 / 8), Polynomial.monic_X_pow_sub_C ((1 : ℚ) / 8) (two_ne_zero),
      ?_⟩
    rw [← Polynomial.aeval_def]
    simp only [map_sub, map_pow, aeval_X, aeval_C]
    rw [div_pow, Real.sq_sqrt (by norm_num), eq_ratCast (algebraMap ℚ ℝ)]
    norm_num
  exact IsIntegral.mul (IsIntegral.pow isIntegral_phi_real 21) hsqrt2div4

What this page does not claim

The declaration does not prove that all real numbers are algebraic. The declaration does not establish the transcendence of cosh 1 - 1; that is a separate theorem. The declaration does not show that any specific multiple of the J-cost equals or differs from the factor amplitude.

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/T10JCostTranscendental.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: