Encyclopedia Masses Masses Mass Genesis T10 Jcost Transcendental Run Cone Terminal Wall Atomic

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Jcost Transcendental Run Cone Terminal Wall Atomic

A machine-checked proof closes a gap in the framework's mass-generation story by showing a transcendental number can never equal an algebraic one.

Verify this page

The terminal wall

In mathematics, a number is algebraic if it is the root of a polynomial with rational coefficients, like the square root of 2. A number is transcendental if it is not, like pi or e. The framework's machine-checked library of formal theorems proves that the hyperbolic cosine of 1, written cosh 1, is transcendental. Since cosh 1 is transcendental, subtracting 1 leaves it transcendental, and no nonzero integer multiple of it can equal an algebraic number.

The framework models a ledger, a discrete record of recognition events, with a cost function J(x) = (x + 1/x)/2 - 1. In its mass-genesis story, a factor amplitude f = φ²¹ / (2√2) is algebraic, built from the golden ratio φ and the square root of 2. The per-post recognition cost is cosh 1 - 1, which is transcendental. The theorem run_cone_terminal_wall_atomic proves that no nonzero multiple of this cost can equal the algebraic amplitude f. This closes a previously open case in the framework's derivation of particle masses.

What the theorem does not claim is that particle masses are derived. It proves a negative: a specific algebraic target is unreachable by a specific transcendental cost. It does not prove that the framework's mass ladder matches measured values, nor does it claim the physical recognition-to-linking bridge is closed. The theorem is a formal statement about numbers, not a measurement or a physical derivation.

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 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
THEOREM run_cone_terminal_wall_atomic · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean
run_cone_terminal_wall_atomic · IndisputableMonolith/Masses/MassGenesis/T10JCostTranscendental.lean:166 
/-- 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

The theorem does not derive particle masses from the framework. The theorem does not claim the framework's mass ladder matches measured values. The theorem does not close the physical recognition-to-linking bridge.

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