Encyclopedia Masses Masses Mass Genesis T10 Run Cone Full Wall

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Run Cone Full Wall

A machine-checked proof that no number built from the recognition cost can equal the factor amplitude, closing a long-open gap.

Verify this page

The settlement-cone wall

The factor amplitude is a specific algebraic number that the framework's mass-genesis program needs to exclude from a certain set of candidate numbers. The set is the settlement cone: a discrete record of all numbers reachable from the rationals, the square root of 2, and the per-post recognition cost, using only addition, subtraction, multiplication, division, and natural powers. The recognition cost is the forced price of a recognition event, equal to cosh 1 − 1.

Earlier work had closed the pure fragment of the cone, which omits the recognition cost. The remaining fragment, which includes it, was excluded only by an algebraic/transcendental split that was not fully checked. The module T10RunConeFullWall closes the whole cone at once, with a machine-checked proof that no element of either fragment equals the factor amplitude.

The argument runs through a key lemma. Every element of the full cone is a rational function of t = cosh 1 − 1, with coefficients in the field ℚ(√2). If such an element is algebraic over the rationals, the lemma forces it to lie in ℚ(√2) itself. Since the factor amplitude is algebraic but not in ℚ(√2), no cone element can equal it. The proof is fully formal: no gaps, no new axioms.

The module also bundles a stronger unconditional wall: every pure-cone-valued organ fails the four-witness interface at every octave, and no nonzero multiple of the per-post recognition cost equals the factor amplitude. This closes the last gap in the mass-genesis run cone, leaving the factor amplitude isolated from the entire cone.

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

This answer does not claim that the factor amplitude is physically realized or measured. This answer does not claim that the settlement cone is the only set of candidate numbers in mass genesis. This answer does not claim that the recognition cost is a measured quantity.

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