Encyclopedia Masses Masses Mass Genesis T10 Inhomogeneous Field Current Selector Wall

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Inhomogeneous Field Current Selector Wall

A machine-checked proof shows that no simple rule can pick out the exact amplitude that gives particles their mass, unless that rule already contains the answer.

Verify this page

The selector wall

In the Recognition Science account of mass, the framework models the world as a discrete record of recognition events, and the cost of each recognition is forced by a proved equation. From that cost, a chain of theorems derives constants such as the golden ratio and the number of spatial dimensions. One open problem in this program has been the origin of the absolute scale of particle masses: what fixes the specific amplitude, the size of the fluctuation, that corresponds to a particle at rest?

The module T10InhomogeneousFieldCurrentSelectorWall.lean closes one named route toward that scale. It considers a class of laws that connect a field's magnitude to a current's magnitude, written as a * u = C, where u is a unit magnitude and C is a constant. The admission gate for a law to be a viable selector has three clauses: the constant must be built from previously derived absolutes, the law must accept the intended witness amplitude, and it must reject a doubled copy of that amplitude. The theorem no_fieldCurrentLaw_passes_selectorGate proves that no law in this class passes all three clauses.

The reason is arithmetic. The intended amplitude f satisfies f² = φ⁴²/8, where φ is the golden ratio. The previously derived absolutes all lie in the field Q(φ), the set of numbers of the form p + qφ with p and q rational. But f does not lie in that field: the proof shows that if it did, a rational square would have to be congruent to 2 mod 4, which is impossible. Since acceptance forces f = C/u, and both C and u would lie in Q(φ), their ratio would too, contradicting the fact that f does not. The obstruction is not a search failure; it is a theorem about rational numbers.

The wall has a sharp edge. The certificate shape is satisfiable: a law with u = 1 and C = f accepts the intended witness and rejects the doubled copy. It fails only the independence clause, because its constant is the target itself. At the intended pattern, this law's acceptance predicate is exactly the zero-cost condition, the R4 foundational model content. So the wall does not say nothing can discriminate; it says discrimination is available only at the price of naming the target, which is the model identification the framework already prices.

In plain language, the module proves that the absolute scale of mass cannot be derived from the previously established constants by any law of this simple linear form. The named falsifier, the reopening condition, is sharp: a newly derived emission-side absolute outside the field Q(φ). The φ-field is closed under sums, products, ratios, and powers, so no derivation assembled from banked absolutes can supply such a constant. The target itself is the canonical escape, as a square root of a φ-field element. Deriving a non-φ-field absolute on the emission side remains OPEN, and is now typed exactly: the new absolute must live outside Q(φ).

THEOREM no_fieldCurrentLaw_passes_selectorGate · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
no_fieldCurrentLaw_passes_selectorGate · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean:376 
/-- **The class wall (THEOREM).** No field-to-current magnitude law with
target-free (φ-field) provenance accepts the intended witness: acceptance
forces `f = C / u` into the φ-field, and `f` is not there. -/
theorem no_fieldCurrentLaw_passes_selectorGate (L : FieldCurrentMagnitudeLaw) :
    ¬ PassesSelectorGate L := by
  rintro ⟨hu, hC, hacc, -⟩
  have hf : intendedGapOneFactorAmplitude = L.C / L.u :=
    (eq_div_iff L.u_ne).mpr hacc
  exact intendedGapOneFactorAmplitude_not_inQPhi (hf ▸ hC.div hu L.u_ne)
THEOREM fieldCurrentSelectorWallCert · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
fieldCurrentSelectorWallCert · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean:475 
theorem fieldCurrentSelectorWallCert : FieldCurrentSelectorWallCert where
  no_law_passes := no_fieldCurrentLaw_passes_selectorGate
  acceptance_forces_target_constant := constant_eq_target_smul_of_accepts
  class_inhabited := fieldCurrentMagnitudeLaw_inhabited
  target_member_passes_witnesses :=
    ⟨targetConstantLaw_accepts_intended, targetConstantLaw_rejects_doubled⟩
  target_fails_independence := intendedGapOneFactorAmplitude_not_inQPhi
  target_member_is_sigma_zero := targetConstantLaw_is_sigmaZero_at_intended.1
  intended_amplitude_sq := by
    simpa [intendedGapOneFactorAmplitude] using
      gapOne_factorAmplitude_sq_eq_phi42_div_eight
THEOREM intendedGapOneFactorAmplitude_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
intendedGapOneFactorAmplitude_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean:283 
/-- **Exact algebra.** The intended gap-one factor amplitude `f`
(`f² = φ⁴²/8`, banked) is not of the form `p + q φ` with rational `p, q`.
The representation would force `p² + q² = F₄₁/8` and `2pq + q² = F₄₂/8`
(by rational independence of `{1, φ}` and the Fibonacci reduction), hence
`q² = 29953729/2` or `q² = 74884322/5`; in the first case `(2q)² = 59907458`
and in the second `(5q)² = 374421610`, both integers `≡ 2 mod 4`, which no
perfect square is. The elimination's discriminant is the Cassini identity
`F₄₁² + F₄₁F₄₂ − F₄₂² = 1`, equivalently `299537289² − 80 · 33489287² = 1`. -/
theorem intendedGapOneFactorAmplitude_not_inQPhi :
    ¬ InQPhi intendedGapOneFactorAmplitude := by
  rintro ⟨p, q, h⟩
  have hsq : intendedGapOneFactorAmplitude ^ 2 = Constants.phi ^ (42 : ℕ) / 8 := by
    simpa [intendedGapOneFactorAmplitude] using
      gapOne_factorAmplitude_sq_eq_phi42_div_eight
  have hexpand : intendedGapOneFactorAmplitude ^ 2 =
      ((p : ℝ) ^ 2 + (q : ℝ) ^ 2) +
        (2 * (p : ℝ) * (q : ℝ) + (q : ℝ) ^ 2) * Constants.phi := by
    rw [h]
    linear_combination ((q : ℝ) ^ 2) * Constants.phi_sq_eq
  have hpow : Constants.phi ^ (42 : ℕ) / 8 =
      (165580141 : ℝ) / 8 + (33489287 : ℝ) * Constants.phi := by
    have hf := phi_pow_fib 42
    have hf42 : Nat.fib 42 = 267914296 := by decide
    have hf43 : Nat.fib 43 = 433494437 := by decide
    rw [hf42, hf43] at hf
    have hf' : Constants.phi ^ (42 : ℕ) =
        (267914296 : ℝ) * Constants.phi + 165580141 := by
      rw [hf]
      push_cast
      ring
    linear_combination hf' / 8
  have heq := hexpand.symm.trans (hsq.trans hpow)
  have heq2 : (((p ^ 2 + q ^ 2 : ℚ) : ℝ)) +
        (((2 * p * q + q ^ 2 : ℚ) : ℝ)) * Constants.phi =
      (((165580141 / 8 : ℚ) : ℝ)) + (((33489287 : ℚ) : ℝ)) * Constants.phi := by
    push_cast
    linear_combination heq
  obtain ⟨hA, hB⟩ := rat_coeff_eq_of_phi heq2
  have hT : 5 * q ^ 4 - (299537289 / 2 : ℚ) * q ^ 2 + (33489287 : ℚ) ^ 2 = 0 := by
    have h1 : p ^ 2 = (165580141 / 8 : ℚ) - q ^ 2 := by linear_combination hA
    have h2 : 2 * p * q = (33489287 : ℚ) - q ^ 2 := by linear_combination hB
    have h3 : 4 * p ^ 2 * q ^ 2 = ((33489287 : ℚ) - q ^ 2) ^ 2 := by
      linear_combination (2 * p * q + ((33489287 : ℚ) - q ^ 2)) * h2
    rw [h1] at h3
    linear_combination -h3
  have hT' : (10 * q ^ 2 - (299537289 / 2 : ℚ)) ^ 2 = (1 / 2 : ℚ) ^ 2 := by
    have hconst : (299537289 / 2 : ℚ) ^ 2 - 20 * (33489287 : ℚ) ^ 2 = 1 / 4 := by
      norm_num
    have hsq : (10 * q ^ 2 - (299537289 / 2 : ℚ)) ^ 2 = 1 / 4 := by
      linear_combination 20 * hT + hconst
    rw [hsq]
    norm_num
  rcases sq_eq_sq_iff_eq_or_eq_neg.mp hT' with hcase | hcase
  · have hq2 : q ^ 2 = (29953729 / 2 : ℚ) := by linear_combination hcase / 10
    have h2q : (2 * q) ^ 2 = (59907458 : ℚ) := by
      have hqq : (2 * q) ^ 2 = 4 * q ^ 2 := by ring
      rw [hqq, hq2]
      norm_num
    exact not_rat_sq_of_mod_four 59907458 (by norm_num) (2 * q)
      (by exact_mod_cast h2q)
  · have hq2 : q ^ 2 = (74884322 / 5 : ℚ) := by linear_combination hcase / 10
    have h5q : (5 * q) ^ 2 = (374421610 : ℚ) := by
      have hqq : (5 * q) ^ 2 = 25 * q ^ 2 := by ring
      rw [hqq, hq2]
      norm_num
    exact not_rat_sq_of_mod_four 374421610 (by norm_num) (5 * q)
      (by exact_mod_cast h5q)
THEOREM targetConstantLaw_accepts_intended · targetConstantLaw_rejects_doubled · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
targetConstantLaw_accepts_intended · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean:417 
theorem targetConstantLaw_accepts_intended :
    LinearMagnitudeLaw 1 intendedGapOneFactorAmplitude
      intendedGapOneFactorAmplitude := by
  show intendedGapOneFactorAmplitude * 1 = intendedGapOneFactorAmplitude
  exact mul_one _
targetConstantLaw_rejects_doubled · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean:423 
theorem targetConstantLaw_rejects_doubled :
    ¬ LinearMagnitudeLaw 1 intendedGapOneFactorAmplitude
      (2 * intendedGapOneFactorAmplitude) := by
  have hf : 0 < intendedGapOneFactorAmplitude := gapOne_factorAmplitude_pos
  intro h
  have h' : 2 * intendedGapOneFactorAmplitude * 1 =
      intendedGapOneFactorAmplitude := h
  rw [mul_one] at h'
  linarith
THEOREM targetConstantLaw_is_sigmaZero_at_intended · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
targetConstantLaw_is_sigmaZero_at_intended · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean:433 
/-- At the intended pattern, the target-constant law's acceptance predicate
is the σ-zero equation (banked
`scalePattern_gapOne_at_factorAmplitude_sigmaZero`). -/
theorem targetConstantLaw_is_sigmaZero_at_intended :
    loadRecognitionCost intendedGapOneFactorPattern = 0 ∧
      intendedGapOneFactorAmplitude =
        primitivePositiveStationaryFactorAmplitude
          intendedGapOneFactorPattern := by
  obtain ⟨-, -, hcost, hamp⟩ := scalePattern_gapOne_at_factorAmplitude_sigmaZero
  exact ⟨hcost, hamp⟩

What this page does not claim

This module does not prove that the absolute mass scale is impossible to derive, only that this particular class of laws cannot do it. This module does not identify the intended amplitude with any measured particle mass. This module does not derive the R4 zero-cost condition; it assumes it as model content.

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