Encyclopedia Masses Masses Mass Genesis T10 Inhomogeneous Field Current Selector Wall Target Constan
ARTICLE 3 claims 3 theorems
Masses Mass Genesis T10 Inhomogeneous Field Current Selector Wall Target Constan
A machine-checked theorem shows that the one law which can pick out a specific particle-mass amplitude does so only by naming that amplitude directly, and at that moment the recognition cost is zero.
The target law and its zero-cost point
In the Recognition Science framework, a field-to-current magnitude law is a simple rule of the form a * u = C, where a is an amplitude, u is a fixed unit magnitude, and C is a constant. The framework's library of machine-checked theorems asks whether any such law can pass a three-part admission gate: its unit and constant must be built from rational numbers and the golden ratio, it must accept one intended witness amplitude, and it must reject that witness's doubled copy.
The theorem targetConstantLaw_is_sigmaZero_at_intended concerns the one law that does pass the witness clauses: it sets the unit to 1 and the constant to the intended amplitude itself. The theorem proves that at the intended pattern, this law's recognition cost is exactly zero, and the intended amplitude equals the primitive positive stationary factor amplitude. In plainer terms, the law that can discriminate the target amplitude does so by naming it outright, and at that exact point the framework's ledger records no cost for the recognition event.
This is the sharpest possible form of a wall result. The admission gate's witness clauses are exact equalities, not tolerances, so the theorem that no rational-golden-ratio law can pass the gate is a wall with real width, not a near miss. The law with the target as its constant is the unique escape: it satisfies the witness clauses but fails the independence clause, because its constant is the target itself. The theorem does not claim that this law is a valid field-to-current magnitude law in the framework's full sense; it is the certificate that shows why the gate cannot be passed without naming the target.
What the theorem does not claim is equally precise. It does not prove that the intended amplitude itself is a rational-golden-ratio number; in fact the library proves it is not. It does not assert that the recognition cost is zero for all patterns, only for the intended one. And it does not establish that this zero-cost point is physically realized; that identification is a separate modeling choice, not a theorem. The wall result is arithmetic: the intended amplitude's square is phi^42 over 8, and that number cannot be written as a rational combination of 1 and phi, a fact the library proves by a modular-arithmetic argument on perfect squares.
For the reader, the consequence is that the framework's absolute scale for particle masses cannot be derived from a field-to-current law without already knowing the answer. The target amplitude is the canonical escape from the rational-golden-ratio field, and deriving a new absolute outside that field remains an open target, now typed exactly. The theorem closes one named route of the T10 program and sharpens the question of where the absolute scale comes from.
THEOREM targetConstantLaw_is_sigmaZero_at_intended · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
/-- 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⟩
THEOREM targetConstantLaw_accepts_intended · targetConstantLaw_rejects_doubled · intendedGapOneFactorAmplitude_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
theorem targetConstantLaw_accepts_intended :
LinearMagnitudeLaw 1 intendedGapOneFactorAmplitude
intendedGapOneFactorAmplitude := by
show intendedGapOneFactorAmplitude * 1 = intendedGapOneFactorAmplitude
exact mul_one _
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
/-- **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 intendedGapOneFactorAmplitude_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
/-- **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)
What this page does not claim
The theorem does not prove the intended amplitude is a rational-golden-ratio number. The theorem does not claim the zero-cost point is physically realized. The theorem does not establish that any field-to-current law can pass the full admission gate.
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:
- What new absolute, outside the rational-golden-ratio field, could supply the missing provenance for the target amplitude?
- Does the zero recognition cost at the intended pattern have a physical interpretation beyond the formal ledger?
- How does the T10 wall relate to the occupation-weight wall that preceded it?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM targetConstantLaw_is_sigmaZero_at_intended · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
/-- 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⟩The theorem proves that at the intended pattern, this law's recognition cost is exactly zero, and the intended amplitude equals the primitive positive stationary factor amplitude. targetConstantLaw_is_sigmaZero_at_intended · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.leanTHEOREM targetConstantLaw_accepts_intended · targetConstantLaw_rejects_doubled · intendedGapOneFactorAmplitude_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
theorem targetConstantLaw_accepts_intended : LinearMagnitudeLaw 1 intendedGapOneFactorAmplitude intendedGapOneFactorAmplitude := by show intendedGapOneFactorAmplitude * 1 = intendedGapOneFactorAmplitude exact mul_one _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/-- **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)The law with the target as its constant is the unique escape: it satisfies the witness clauses but fails the independence clause, because its constant is the target itself. targetConstantLaw_accepts_intended · targetConstantLaw_rejects_doubled · intendedGapOneFactorAmplitude_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.leanTHEOREM intendedGapOneFactorAmplitude_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
/-- **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)The library proves it is not a rational-golden-ratio number. intendedGapOneFactorAmplitude_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean