Masses Mass Genesis T10 Run Cone Full Wall In Qsqrt Two Coeff Mul

The coefficient closure lemma

The declaration inQsqrtTwo_coeff_mul is a lemma about polynomials: if you take two polynomials whose every coefficient is a number of the form a + b√2, with a and b rational, then in their product, every coefficient is again of that same form. In plainer terms, multiplying such polynomials never produces a coefficient that escapes the field ℚ(√2), the set of numbers you can build from rationals and the square root of two using addition, subtraction, multiplication, and division. The proof is a direct computation: the coefficient of the product at any index is a finite sum of products of coefficients from the two factors, and each term in that sum stays in ℚ(√2).

This closure property matters because it is the first step in a longer argument that ends with a strong negative result. The framework's settlement cone, a discrete record of candidate values generated from rationals, √2, and a transcendental number t = cosh 1 − 1, is shown to consist entirely of rational functions of t with coefficients in ℚ(√2). The lemma inQsqrtTwo_coeff_mul is what guarantees that multiplying two such rational functions keeps the coefficients in ℚ(√2), and the companion lemma inQsqrtTwo_coeff_pow extends the same closure to powers. Without this closure, the later step that any algebraic element of the cone must lie in ℚ(√2) would fail at the first hurdle.

What the lemma does not claim is equally precise. It says nothing about the values of the polynomials, only about their coefficients. A polynomial with coefficients in ℚ(√2) can certainly evaluate to a number outside ℚ(√2) at a transcendental input; the lemma neither asserts nor denies that. It also does not say that every number in ℚ(√2) appears as a coefficient, nor that the product of two such polynomials is itself of the same simple form. The lemma is purely a statement about the coefficient ring of the polynomial ring over ℚ(√2).

In the context of the full wall theorem, this lemma is the unglamorous but indispensable gear. It is what lets the framework's library of machine-checked formal theorems conclude, with no gaps and no unproved assumptions, that no element of the settlement cone, at either marking, equals the factor amplitude. That final theorem, runCone_ne_intended, is the destination; inQsqrtTwo_coeff_mul is the road that gets there.

theorem inQsqrtTwo_coeff_mul {P Q : ℝ[X]} (hP : ∀ i, InQsqrtTwo (P.coeff i))
    (hQ : ∀ i, InQsqrtTwo (Q.coeff i)) (i : ℕ) :
    InQsqrtTwo ((P * Q).coeff i) := by
  rw [Polynomial.coeff_mul]
  exact inQsqrtTwo_sum (fun x _ => inQsqrtTwo_mul (hP x.1) (hQ x.2))

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

The lemma does not claim anything about the values of the polynomials, only about their coefficients. The lemma does not claim that every number in ℚ(√2) appears as a coefficient of such a polynomial. The full wall theorem does not claim that the factor amplitude is transcendental, only that it is not in the settlement cone.

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: