Encyclopedia Masses Masses Mass Genesis T10 Jcost Transcendental Cone J Atomic Ne Intended

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Jcost Transcendental Cone J Atomic Ne Intended

A number that cannot be reached by any whole-number multiple of a transcendental cost, proved by a machine-checked library.

Verify this page

The algebraic and the transcendental

In mathematics, a number is algebraic if it solves a polynomial equation with rational coefficients, and transcendental if it solves none. The square root of 2 is algebraic, since it solves X² − 2 = 0. The number e, the base of natural logarithms, is transcendental, a fact proved by Charles Hermite in 1873. The hyperbolic cosine of 1, written cosh 1, is also transcendental, because if it were algebraic then e would solve a quadratic equation built from it, contradicting Hermite's result.

Inside the Recognition Science framework, a ledger (a discrete record of recognition events) assigns a cost to each posting, and the framework's forced cost function J(x) = (x + 1/x)/2 − 1 takes the value cosh 1 − 1 at a particular point. The framework's machine-checked library of formal theorems proves that this per-post cost is transcendental. Separately, the framework defines a factor amplitude f = φ²¹ / (2√2), built from the golden ratio φ and the square root of 2, and proves that f is algebraic.

In Recognition Science, the declaration coneJ_atomic_ne_intended proves the key consequence: for every nonzero natural number K, the product K·(cosh 1 − 1) never equals f. The proof is short: a nonzero integer multiple of a transcendental number is still transcendental, and a transcendental number cannot equal an algebraic one. The theorem closes a terminal wall in the framework's mass-genesis argument, showing that a certain cone of possible costs misses the intended factor amplitude entirely.

What the declaration does not claim is equally precise. It does not say that f is unreachable in any broader sense, only that no whole-number multiple of the per-post cost reaches it. It does not identify which number, if any, does reach f, and it says nothing about the physical masses themselves. The theorem is a statement about algebraic and transcendental numbers, not about measurement.

THEOREM transcendental_cosh_one · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean
transcendental_cosh_one · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean:76 
/-- The per-post recognition J-cost `cosh 1` is transcendental over ℚ:
otherwise `e` would satisfy a quadratic over the algebraic extension
`ℚ(cosh 1)`, contradicting `transcendental_e`. -/
theorem transcendental_cosh_one : Transcendental ℚ (Real.cosh 1) := by
  intro hc
  classical
  set c := Real.cosh 1 with hc_def
  have hc_int : IsIntegral ℚ c := isAlgebraic_iff_isIntegral.mp hc
  set F := IntermediateField.adjoin ℚ {c} with hF
  have hFalg : Algebra.IsAlgebraic ℚ F := by
    apply IntermediateField.isAlgebraic_adjoin
    intro y hy
    rw [Set.mem_singleton_iff] at hy
    rw [hy]
    exact hc_int
  have hte : Transcendental F (Real.exp 1) :=
    (Algebra.IsAlgebraic.transcendental_iff ℚ F).mp T10ExpTranscendental.transcendental_e
  apply hte
  have hcm : c ∈ F := IntermediateField.subset_adjoin ℚ {c} (Set.mem_singleton c)
  refine ⟨(X ^ 2 + (C (1 : F) - C (2 * (⟨c, hcm⟩ : F)) * X) : F[X]), ?_, ?_⟩
  · intro hz
    have h2 : (X ^ 2 + (C (1 : F) - C (2 * (⟨c, hcm⟩ : F)) * X)).coeff 2 = 1 := by
      rw [Polynomial.coeff_add, Polynomial.coeff_X_pow, if_pos rfl, Polynomial.coeff_sub,
        Polynomial.coeff_C, if_neg (show (2 : ℕ) ≠ 0 by norm_num), Polynomial.coeff_C_mul,
        Polynomial.coeff_X, if_neg (show (1 : ℕ) ≠ 2 by norm_num), mul_zero, sub_zero,
        add_zero]
    rw [hz, Polynomial.coeff_zero] at h2
    exact zero_ne_one h2
  · have h2c : 2 * c = Real.exp 1 + (Real.exp 1)⁻¹ := by
      rw [hc_def, Real.cosh_eq, Real.exp_neg]
      ring
    have he0 : (Real.exp 1) ≠ 0 := ne_of_gt (Real.exp_pos 1)
    have hkey : (Real.exp 1) ^ 2 + (1 - 2 * c * Real.exp 1) = 0 := by
      rw [h2c]
      field_simp [he0]
      ring
    have hcast2 : algebraMap F ℝ (2 * (⟨c, hcm⟩ : F)) = 2 * c := by
      rw [map_mul, map_ofNat, IntermediateField.algebraMap_apply]
    show aeval (Real.exp 1) (X ^ 2 + (C (1 : F) - C (2 * (⟨c, hcm⟩ : F)) * X)) = 0
    rw [Polynomial.aeval_def, Polynomial.eval₂_eq_eval_map, Polynomial.map_add,
      Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_C, map_one,
      Polynomial.map_mul, Polynomial.map_C, Polynomial.map_X, Polynomial.eval_add,
      Polynomial.eval_sub, Polynomial.eval_pow, Polynomial.eval_X, Polynomial.eval_C,
      Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_X, hcast2]
    exact hkey
THEOREM transcendental_cosh_one_sub_one · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean
transcendental_cosh_one_sub_one · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean:122 
/-- 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
THEOREM isAlgebraic_intended · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean
isAlgebraic_intended · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean:133 
/-- 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
THEOREM coneJ_atomic_ne_intended · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean
coneJ_atomic_ne_intended · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean:147 
/-- 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

What this page does not claim

The declaration does not say f is unreachable in any broader sense, only by whole-number multiples of the per-post cost. The declaration does not identify which number reaches f. The declaration makes no claim about measured particle masses.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND