Encyclopedia Masses Masses Mass Genesis T10 Run Cone Full Wall Rat Func Algebraic Mem Qsqrt Two

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Run Cone Full Wall Rat Func Algebraic Mem Qsqrt Two

A machine-checked proof shows that within the framework's settlement cone, an algebraic number that is a rational function of a transcendental must itself be a simple square-root extension.

Verify this page

The algebraic wall

In mathematics, a number is algebraic if it solves a polynomial equation with rational coefficients, and transcendental if it does not. The square root of 2 is algebraic, since it solves x² − 2 = 0. The number cosh 1 − 1, about 0.543, is transcendental, a fact that follows from the Lindemann-Weierstrass theorem on exponential functions.

The declaration ratFunc_algebraic_mem_QsqrtTwo proves a structural lemma about these two kinds of numbers. It states: if a number x is both algebraic over the rationals and a rational function of a transcendental number t, with coefficients in the field ℚ(√2), then x must itself belong to ℚ(√2). In other words, an algebraic number that is built from a transcendental using only field operations and coefficients from ℚ(√2) cannot be anything more exotic than a number of the form a + b√2 with a and b rational.

The proof runs by adjoining √2, the coefficients of the rational function, and x itself to the rationals. The result is an algebraic extension field F. Since t is transcendental over the rationals, it remains transcendental over F. But the rational function equation P(t)/Q(t) = x rearranges to P(t) − x·Q(t) = 0, a polynomial in t with coefficients in F. A transcendental number cannot satisfy a nonzero polynomial, so this polynomial must be identically zero. Reading off coefficients gives P = x·Q, and since Q is not the zero polynomial, x is a ratio of two elements of ℚ(√2), hence lies in ℚ(√2).

In Recognition Science, this lemma serves as the algebraic wall that closes the settlement cone. The cone is the set of numbers reachable from rationals, √2, and the per-post recognition cost cosh 1 − 1 using field operations and natural powers. The framework's library proves that every element of the cone is a rational function of cosh 1 − 1 over ℚ(√2), and that the factor amplitude, a specific algebraic number, is not in ℚ(√2). The lemma then forces the conclusion: no element of the cone, at either marking, equals the factor amplitude. This is the terminal wall, a theorem with no unproved assumptions.

The lemma does not claim that every algebraic number is in ℚ(√2), nor that every rational function of a transcendental is transcendental. It does not identify the factor amplitude numerically, and it does not say anything about whether the cone's elements are physically realized. It is a precise statement about field extensions, and its role is to close a gap in the framework's derivation of mass structure.

THEOREM ratFunc_algebraic_mem_QsqrtTwo · IndisputableMonolith/Masses/MassGenesis/T10RunConeFullWall.lean
ratFunc_algebraic_mem_QsqrtTwo · IndisputableMonolith/Masses/MassGenesis/T10RunConeFullWall.lean:212 
/-- If `t` is transcendental over ℚ and `x` is a rational function of `t`
over ℚ(√2) that is algebraic over ℚ, then `x ∈ ℚ(√2)`. -/
theorem ratFunc_algebraic_mem_QsqrtTwo {t x : ℝ} (ht : Transcendental ℚ t)
    (hx : IsRatFuncOf t x) (hxa : IsAlgebraic ℚ x) : InQsqrtTwo x := by
  obtain ⟨P, Q, hP, hQ, hQ0, hQt, hxeq⟩ := hx
  classical
  -- The adjoin of the square root of 2, `x`, and every coefficient is
  -- algebraic over ℚ.
  set S0 : Set ℝ := ↑(P.support.image P.coeff) ∪ ↑(Q.support.image Q.coeff) ∪
      ({x} ∪ {Real.sqrt 2}) with hS0
  set F := IntermediateField.adjoin ℚ S0 with hF
  have hint_of_mem : ∀ y ∈ S0, IsIntegral ℚ y := by
    intro y hy
    rw [hS0] at hy
    rcases hy with (hA | hB) | (hyx | hy2)
    · rw [Finset.mem_coe, Finset.mem_image] at hA
      obtain ⟨i, _, rfl⟩ := hA
      obtain ⟨a, b, hab⟩ := hP i
      rw [hab]
      exact IsIntegral.add (T10JCostTranscendental.isIntegral_ratCast_real a)
        (IsIntegral.mul (T10JCostTranscendental.isIntegral_ratCast_real b)
          T10JCostTranscendental.isIntegral_sqrtTwo_real)
    · rw [Finset.mem_coe, Finset.mem_image] at hB
      obtain ⟨i, _, rfl⟩ := hB
      obtain ⟨a, b, hab⟩ := hQ i
      rw [hab]
      exact IsIntegral.add (T10JCostTranscendental.isIntegral_ratCast_real a)
        (IsIntegral.mul (T10JCostTranscendental.isIntegral_ratCast_real b)
          T10JCostTranscendental.isIntegral_sqrtTwo_real)
    · rw [Set.mem_singleton_iff] at hyx
      rw [hyx]
      exact isAlgebraic_iff_isIntegral.mp hxa
    · rw [Set.mem_singleton_iff] at hy2
      rw [hy2]
      exact T10JCostTranscendental.isIntegral_sqrtTwo_real
  have hFalg : Algebra.IsAlgebraic ℚ F :=
    IntermediateField.isAlgebraic_adjoin hint_of_mem
  have htF : Transcendental F t :=
    (Algebra.IsAlgebraic.transcendental_iff ℚ F).mp ht
  have hmemP : ∀ i, P.coeff i ∈ F := by
    intro i
    by_cases hi : P.coeff i = 0
    · rw [hi]; exact F.zero_mem
    · apply IntermediateField.subset_adjoin ℚ S0
      rw [hS0]
      refine Set.mem_union_left _ (Set.mem_union_left _ ?_)
      exact Finset.mem_coe.mpr
        (Finset.mem_image.mpr ⟨i, Polynomial.mem_support_iff.mpr hi, rfl⟩)
  have hmemQ : ∀ i, Q.coeff i ∈ F := by
    intro i
    by_cases hi : Q.coeff i = 0
    · rw [hi]; exact F.zero_mem
    · apply IntermediateField.subset_adjoin ℚ S0
      rw [hS0]
      refine Set.mem_union_left _ (Set.mem_union_right _ ?_)
      exact Finset.mem_coe.mpr
        (Finset.mem_image.mpr ⟨i, Polynomial.mem_support_iff.mpr hi, rfl⟩)
  have hxF : x ∈ F := by
    apply IntermediateField.subset_adjoin ℚ S0
    rw [hS0]
    exact Set.mem_union_right _ (Set.mem_union_left _ (Set.mem_singleton x))
  -- The vanishing polynomial over `F`.
  set supp := P.support ∪ Q.support with hsupp
  set WF : F[X] := ∑ i ∈ supp,
    monomial i (⟨P.coeff i - x * Q.coeff i, F.sub_mem (hmemP i)
      (F.mul_mem hxF (hmemQ i))⟩ : F) with hWF
  have hWF_map : WF.map (algebraMap F ℝ) = P - C x * Q := by
    ext i
    rw [Polynomial.coeff_map]
    simp only [hWF, Polynomial.finset_sum_coeff, Polynomial.coeff_monomial]
    by_cases hi : i ∈ supp
    · rw [Finset.sum_eq_single i
        (fun j _ hj => by rw [if_neg hj])
        (fun hni => absurd hi hni)]
      rw [if_pos rfl, IntermediateField.algebraMap_apply, Polynomial.coeff_sub,
        Polynomial.coeff_C_mul]
    · rw [Finset.sum_congr rfl (g := fun _j => (0 : F)) (by
          intro j hj
          have hij : j ≠ i := fun h => hi (h ▸ hj)
          rw [if_neg hij])]
      rw [Finset.sum_const_zero, map_zero, Polynomial.coeff_sub, Polynomial.coeff_C_mul]
      rw [hsupp, Finset.mem_union] at hi
      push_neg at hi
      rw [Polynomial.notMem_support_iff, Polynomial.notMem_support_iff] at hi
      rw [hi.1, hi.2, mul_zero, sub_self]
  have hWF_eval : aeval t WF = 0 := by
    rw [Polynomial.aeval_def, Polynomial.eval₂_eq_eval_map, hWF_map]
    rw [Polynomial.eval_sub, Polynomial.eval_mul, Polynomial.eval_C]
    have hxq : Q.eval t ≠ 0 := hQt
    have hmul : x * Q.eval t = P.eval t := by
      rw [hxeq]
      field_simp [hxq]
    linarith [hmul]
  have hWF0 : WF = 0 := by
    by_contra hne
    exact htF ⟨WF, hne, hWF_eval⟩
  have hcoeff : ∀ i, P.coeff i = x * Q.coeff i := by
    intro i
    have hmap : WF.map (algebraMap F ℝ) = 0 := by rw [hWF0, Polynomial.map_zero]
    rw [hWF_map] at hmap
    have hsub : P - C x * Q = 0 := hmap
    have heq : P = C x * Q := sub_eq_zero.mp hsub
    rw [heq, Polynomial.coeff_C_mul]
  obtain ⟨j, hj⟩ : ∃ j, Q.coeff j ≠ 0 := by
    by_contra hall
    push_neg at hall
    apply hQ0
    ext i
    rw [hall i]
    exact (Polynomial.coeff_zero i).symm
  have hxPQ : x = P.coeff j / Q.coeff j := by
    rw [eq_div_iff hj]
    exact (hcoeff j).symm
  rw [hxPQ, div_eq_mul_inv]
  exact inQsqrtTwo_mul (hP j) (inQsqrtTwo_inv (hQ j) hj)
THEOREM runCone_true_isRatFuncOf · IndisputableMonolith/Masses/MassGenesis/T10RunConeFullWall.lean
runCone_true_isRatFuncOf · IndisputableMonolith/Masses/MassGenesis/T10RunConeFullWall.lean:192 
/-- Every `true`-cone element is a rational function of the J-cost over
ℚ(√2). -/
theorem runCone_true_isRatFuncOf {x : ℝ} (h : RunCone true x) :
    IsRatFuncOf (Real.cosh 1 - 1) x := by
  have hr : ∀ {j : Bool} {x : ℝ}, RunCone j x → j = true →
      IsRatFuncOf (Real.cosh 1 - 1) x := by
    intro j x h
    induction h with
    | rat _ q => intro _; exact ratFunc_rat q
    | sqrtTwo _ => intro _; exact ratFunc_sqrtTwo
    | jcost => intro _; exact ratFunc_self
    | add _ _ ihx ihy => intro hj; exact ratFunc_add (ihx hj) (ihy hj)
    | neg _ ihx => intro hj; exact ratFunc_neg (ihx hj)
    | mul _ _ ihx ihy => intro hj; exact ratFunc_mul (ihx hj) (ihy hj)
    | inv _ hx0 ihx => intro hj; exact ratFunc_inv (ihx hj) hx0
    | pow _ n ihx => intro hj; exact ratFunc_pow (ihx hj) n
  exact hr h rfl
THEOREM runCone_ne_intended · IndisputableMonolith/Masses/MassGenesis/T10RunConeFullWall.lean
runCone_ne_intended · IndisputableMonolith/Masses/MassGenesis/T10RunConeFullWall.lean:330 
/-- No element of the registered settlement cone, at either marking, equals
the factor amplitude. THEOREM (both fragments). -/
theorem runCone_ne_intended {j : Bool} {x : ℝ} (h : RunCone j x) :
    x ≠ intendedGapOneFactorAmplitude := by
  intro hx_eq
  cases j with
  | false => exact runConePure_ne_intended h hx_eq
  | true =>
    have hxa : IsAlgebraic ℚ x := by
      have hf := T10JCostTranscendental.isAlgebraic_intended
      rwa [← hx_eq] at hf
    have hkey : InQsqrtTwo x :=
      ratFunc_algebraic_mem_QsqrtTwo T10JCostTranscendental.transcendental_cosh_one_sub_one
        (runCone_true_isRatFuncOf h) hxa
    rw [hx_eq] at hkey
    exact intended_not_in_QsqrtTwo hkey

What this page does not claim

The lemma does not prove that every algebraic number lies in ℚ(√2). The lemma does not identify the factor amplitude numerically. The lemma does not claim that the cone's elements are physically realized.

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