Masses Mass Genesis T10 Jcost Transcendental

The algebraic divide

In mathematics, a number is transcendental when it is not the solution to any polynomial equation with rational coefficients. The number π is transcendental; so is e. The number √2 is not, since it solves X² − 2 = 0. This distinction, algebraic versus transcendental, is the backbone of a recent theorem in the Recognition Science framework, which models physical structure as the cost of maintaining a discrete record of events, called a ledger.

The theorem concerns two specific numbers. The first is cosh 1 − 1, roughly 0.543, which the framework uses as the per-event cost of recognition in one of its models. The second is a factor amplitude written as φ²¹ / (2√2), built from the golden ratio φ, and it is algebraic: it solves a polynomial with rational coefficients. The framework's machine-checked library of formal theorems proves that cosh 1 − 1 is transcendental. The argument is short: if cosh 1 were algebraic, then e would satisfy a quadratic equation over an algebraic extension of the rationals, contradicting the known theorem that e is transcendental.

Once both facts are established, a third follows immediately. No nonzero integer multiple of a transcendental number can equal an algebraic number. So for every positive integer K, the product K · (cosh 1 − 1) never equals φ²¹ / (2√2). The framework states this as the theorem coneJ_atomic_ne_intended, and it is proved in the module T10JCostTranscendental. The proof is complete: no gaps, no unproved assumptions beyond the standard axioms of the ambient type theory.

Why does this matter? The framework's account of particle masses runs through a chain of forced steps, and one step left a family of possible costs open: a cost that scales with the number of events in a run. That family would have allowed the factor amplitude to be reached by adding up enough per-event costs. The new theorem closes that possibility. It shows that the pure cost model can never hit the intended amplitude, and that any organ built purely from that model fails the interface at every octave. The result upgrades a previously unformalized derivation to a proved theorem.

The practical consequence is that the framework's mass-generation story no longer carries an unproved assumption at this point. The algebraic divide between the two numbers is what makes the exclusion possible. It is a small but load-bearing result: without it, the framework could not rule out a whole class of alternative cost models.

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

/-- No nonzero integer multiple of the per-post J-cost equals the factor
amplitude: the left side is transcendental, the right side algebraic. -/
theorem coneJ_atomic_ne_intended (K : ℕ) (hK : K ≠ 0) :
    (K : ℝ) * (Real.cosh 1 - 1) ≠ intendedGapOneFactorAmplitude := by
  intro h
  have ht : IsAlgebraic ℚ (Real.cosh 1 - 1) := by
    rw [isAlgebraic_iff_isIntegral]
    have hK0 : (K : ℝ) ≠ 0 := by exact_mod_cast hK
    have ht_eq : Real.cosh 1 - 1 = (K : ℝ)⁻¹ * intendedGapOneFactorAmplitude := by
      rw [← h, inv_mul_cancel_left₀ hK0]
    rw [ht_eq]
    have hinv : IsIntegral ℚ ((K : ℝ)⁻¹) := by
      refine ⟨X - C ((K : ℚ)⁻¹), Polynomial.monic_X_sub_C _, ?_⟩
      rw [← Polynomial.aeval_def]
      simp only [map_sub, aeval_X, aeval_C, eq_ratCast (algebraMap ℚ ℝ)]
      rw [Rat.cast_inv, Rat.cast_natCast, sub_self]
    exact IsIntegral.mul hinv (isAlgebraic_iff_isIntegral.mp isAlgebraic_intended)
  exact transcendental_cosh_one_sub_one ht

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

This does not prove that the framework's mass values match measured particle masses. This does not derive the fine-structure constant or any other coupling constant. This does not claim the framework's entire mass-generation chain is complete, only that this specific gap 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/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: