Masses Mass Genesis T10 Run Cone Full Wall Run Cone True Is Rat Func Of

The settlement cone's shape

The declaration runCone_true_isRatFuncOf establishes a structural fact about a set of real numbers called the settlement cone. In plain terms, it proves that every number in one half of this cone can be written as a ratio of two polynomials, where the variable is the number t = cosh(1) - 1 and every coefficient is a rational number or a rational multiple of the square root of 2. This is a precise algebraic shape: the cone's elements are not arbitrary; they are all rational functions of a single transcendental number.

The proof works by showing that the cone's generators, which are the rationals, the square root of 2, and t itself, all have this property, and that the property is preserved under addition, multiplication, and taking reciprocals. This closure argument is what the theorem formalizes. The immediate consequence is that any element of this cone is either transcendental or lies in the field Q(√2), the set of numbers built from rationals and √2 using field operations. Since the intended factor amplitude is algebraic but not in Q(√2), a separate theorem, runCone_ne_intended, concludes that no cone element equals it.

This is a theorem about a specific mathematical structure, not a statement about physical masses. The cone is a definitional choice, a model of possible values, and the theorem describes its algebraic form. It does not claim that any particular physical mass is in the cone, nor that the factor amplitude is a measured quantity. The result is conditional on the cone's definition and the framework's axioms, and it is proved in a machine-checked library of formal theorems with no unproved assumptions.

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

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

This theorem does not claim that any physical particle mass is an element of the settlement cone. It does not claim that the factor amplitude is a measured or empirically determined value. It does not claim that the cone's definition is the only possible model for mass values.

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: