Masses Mass Genesis T10 Jcost Transcendental Transcendental Cosh One Sub One

The transcendental split

The number cosh(1) − 1, roughly 0.543, is transcendental: it is not the root of any polynomial with rational coefficients. This is a classical fact about the hyperbolic cosine function, and it is now also a proved theorem in the Recognition Science framework's machine-checked library of formal theorems. The proof runs through the transcendence of e, the base of natural logarithms. If cosh(1) were algebraic, then e would satisfy a quadratic equation with coefficients built from cosh(1), which would make e algebraic too, contradicting the known theorem that e is transcendental.

In the framework, this number appears as the per-post recognition cost: the cost of recording one event in a ledger, a discrete record of events. The framework's cost function J(x) = (x + 1/x)/2 − 1, evaluated at x = e, gives exactly cosh(1) − 1. The new theorem, called transcendental_cosh_one_sub_one, proves this per-post cost is transcendental. A companion theorem proves that the factor amplitude, a specific algebraic number built from the golden ratio and the square root of two, is algebraic. Since a nonzero rational multiple of a transcendental number can never equal an algebraic number, no integer multiple of the per-post cost can match the factor amplitude.

That inequality closes a structural gap in the framework's derivation of particle masses. The framework had previously shown that a certain "terminal wall" condition must hold for the mass generation chain to be consistent, but one case remained open: whether a scaled version of the per-post cost could accidentally equal the factor amplitude. The new proof rules out that possibility for every nonzero integer scaling. The terminal wall theorem, run_cone_terminal_wall_atomic, is now closed at the same confidence level as the rest of the chain: it is a proved theorem with no unproved assumptions.

What the theorem does not claim is broader. It does not say that the framework's mass values match measured particle masses; that comparison is an empirical check, not a theorem. It does not derive the fine-structure constant or any other coupling constant. It does not prove the Riemann Hypothesis. The theorem is a precise, narrow result about one number's algebraic status, and the structural consequence that follows from it.

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

/-- 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 settlement-cone terminal wall with the J-cost fragment closed
THEOREM-grade: the pure cone misses `f`, every pure-cone-valued organ
fails the interface at every octave, and no nonzero multiple of the
per-post J-cost equals `f`. -/
theorem run_cone_terminal_wall_atomic :
    (∀ {x : ℝ}, RunCone false x → x ≠ intendedGapOneFactorAmplitude) ∧
      (∀ (A : OrganArrowReduction.OrganArrow),
        (∀ o : Q3SettledLedgerOctave, RunCone false (A.level (A.W o))) →
        ∀ o : Q3SettledLedgerOctave,
          ¬ RunPatternScaleCouplingInterface A.filter o) ∧
      (∀ K : ℕ, K ≠ 0 → (K : ℝ) * (Real.cosh 1 - 1) ≠ intendedGapOneFactorAmplitude) :=
  ⟨fun h => runConePure_ne_intended h,
   fun A hA o => conePure_organ_fails_interface A hA o,
   fun K hK => coneJ_atomic_ne_intended K hK⟩

What this page does not claim

This theorem does not claim that the framework's mass predictions match measured particle masses. This theorem does not derive the fine-structure constant or any other coupling constant. This theorem does not prove the Riemann Hypothesis.

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: