Encyclopedia Masses Masses Mass Genesis T10 Inhomogeneous Field Current Selector Wall Constant Eq Ta

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Inhomogeneous Field Current Selector Wall Constant Eq Ta

A machine-checked theorem shows that no law of a certain class can pick out a specific amplitude without already knowing the answer.

Verify this page

The selector wall

A field-to-current magnitude law is a rule that turns a field strength into a current magnitude. In the Recognition Science framework, such a law is written as a * u = C, where u is a unit magnitude, a is the field amplitude, and C is a constant that the law is supposed to derive from first principles. The declaration constant_eq_target_smul_of_accepts says something simple: if such a law accepts a specific, intended amplitude, then its constant C is forced to be that amplitude times its unit magnitude.

That statement is a theorem, proved in the framework's machine-checked library of formal theorems. It is not a discovery about the physical world; it is a fact about the algebra of the law. If the law's equation is a * u = C, and it accepts the intended amplitude f, then the equation must hold with a = f, which gives f * u = C. The theorem simply rearranges that equality.

The force of the theorem appears when it is combined with a second result. The intended amplitude f is not a rational combination of 1 and the golden ratio φ, meaning it cannot be written as p + qφ with rational p and q. The framework's library proves this by an arithmetic argument involving the Cassini identity for Fibonacci numbers. Since the unit magnitude u and the constant C of any law in the class are required to lie in that rational-φ field, the theorem forces the constant to be outside the field, which is impossible. No law in the class can pass the admission gate.

In Recognition Science, this is called the class wall: the last named route to an absolute scale for particle masses closes. The only law that accepts the intended amplitude and rejects its double is one whose constant is the amplitude itself, but that law names the target in its definition, which the gate forbids. The wall is not a failure of search; it is an arithmetic obstruction. The theorem establishes a precise boundary: any future absolute constant must live outside the rational-φ field, which is exactly what the framework leaves open.

The theorem does not claim that no field-to-current magnitude law exists. It does not claim that the intended amplitude is physically impossible. It does not claim that the framework has derived the mass spectrum. It claims only that within the typed class of laws, with the admission gate as defined, no law can satisfy all three clauses. The proof is exact, not approximate, and it is a theorem, not a hypothesis.

THEOREM constant_eq_target_smul_of_accepts · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
constant_eq_target_smul_of_accepts · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean:386 
/-- The banked reduction, restated for the class: acceptance of the intended
witness forces the constant to be the target amplitude scaled by the law's
unit. Independence from the target is therefore a question about the
provenance of the constant, and only that. -/
theorem constant_eq_target_smul_of_accepts (L : FieldCurrentMagnitudeLaw)
    (hacc : LinearMagnitudeLaw L.u L.C intendedGapOneFactorAmplitude) :
    L.C = intendedGapOneFactorAmplitude * L.u :=
  hacc.symm
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 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 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

What this page does not claim

The theorem does not claim that no field-to-current magnitude law exists at all. The theorem does not claim that the intended amplitude is physically impossible or unmeasurable. The theorem does not claim that the framework has derived the particle mass spectrum.

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