Encyclopedia Masses Masses Mass Genesis T10 Run Cone Full Wall Run Cone Terminal Wall Unconditional

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Run Cone Full Wall Run Cone Terminal Wall Unconditional

A machine-checked theorem proves that a certain class of numbers, built from rationals, the square root of two, and a transcendental constant, can never equal a specific physical amplitude.

Verify this page

The settlement-cone wall

The declaration run_cone_terminal_wall_unconditional is a formal theorem in the framework's machine-checked library of formal theorems. It establishes a negative result about a set of numbers called the settlement cone, a discrete record of values generated by field operations (addition, multiplication, division) and natural powers, starting from three kinds of generators: rational numbers, the square root of two, and a transcendental constant t = cosh(1) - 1.

The theorem proves that no element of this cone, under either of its two markings, equals a specific number called the factor amplitude. The argument splits into two cases. For the pure fragment (marking false), the result was already known. For the full fragment (marking true), the proof shows that every element is a rational function of t with coefficients in the field Q(√2). If such an element were algebraic over the rationals, the transcendence of t would force it to be a ratio of two elements of Q(√2), hence itself in Q(√2). But the factor amplitude is algebraic and not in Q(√2), so no cone element can equal it.

The bundled theorem also states two stronger consequences. First, every pure-cone-valued organ fails a certain four-witness interface at every octave. Second, no nonzero integer multiple of the per-post J-cost (cosh 1 - 1) equals the factor amplitude. All clauses are marked THEOREM-grade, with no unproved axioms in the framework's logic.

What this does not claim: it does not say the factor amplitude is physically realized or that the cone is empty. It only says the amplitude lies outside the cone. It also does not derive the amplitude's value from first principles; the amplitude is introduced as a definition, and its algebraic non-membership in Q(√2) is a separate theorem. The wall is a separation result, not a construction.

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
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 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 run_cone_terminal_wall_unconditional · IndisputableMonolith/Masses/MassGenesis/T10RunConeFullWall.lean
run_cone_terminal_wall_unconditional · IndisputableMonolith/Masses/MassGenesis/T10RunConeFullWall.lean:347 
/-- The unconditional settlement-cone wall: every clause THEOREM-grade. -/
theorem run_cone_terminal_wall_unconditional :
    (∀ {j : Bool} {x : ℝ}, RunCone j 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 => runCone_ne_intended h,
   fun A hA o => conePure_organ_fails_interface A hA o,
   fun K hK => T10JCostTranscendental.coneJ_atomic_ne_intended K hK⟩

What this page does not claim

Not a claim that the factor amplitude is physically realized. Not a derivation of the factor amplitude's value from first principles. Not a claim that the cone is empty or that its elements are all transcendental.

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