Encyclopedia Masses Masses Mass Genesis T10 Inhomogeneous Field Current Selector Wall Intended Gap O
ARTICLE 5 claims 5 theorems
Masses Mass Genesis T10 Inhomogeneous Field Current Selector Wall Intended Gap O
A machine-checked proof shows a specific target amplitude cannot be built from the framework's own rational-golden-ratio numbers, closing a named route in the mass-genesis program.
The arithmetic wall
The declaration intendedGapOneFactorAmplitude_not_inQPhi is a theorem in the framework's machine-checked library of formal theorems. It establishes that a particular real number, the intended gap-one factor amplitude, cannot be written as p + qφ, where p and q are rational numbers and φ is the golden ratio (1 + √5)/2. The set of all such numbers, called the rational-φ field, is the framework's explicit envelope for constants it can derive from first principles: it contains 1, the coherence quantum φ⁻⁵, and every power of φ, and it is closed under addition, multiplication, division, and powers.
The proof is arithmetic, not a search failure. The amplitude f satisfies f² = φ⁴²/8. If f were p + qφ, then rational independence of {1, φ} would force q² to be either 29953729/2 or 74884322/5. Both are impossible for rational q, because 4q² or 25q² would be an integer congruent to 2 mod 4, and no perfect square has that form. The discriminant of the elimination is the Cassini identity for Fibonacci numbers in disguise, so the obstruction is structural, not a matter of computational effort.
In Recognition Science, this theorem closes a named route in the T10 absolute-scale program. The program sought a field-to-current magnitude law, a rule of the form a·u = C, that would select the intended amplitude without naming it. The admission gate required three things: the law's unit magnitude u and constant C must both lie in the rational-φ field (independence from the target), the law must accept the intended amplitude, and it must reject its doubled copy. The theorem shows no such law exists: acceptance forces f = C/u, and since C and u are both in the field, f would be too, contradicting the arithmetic wall.
What the theorem does not claim is that nothing can select the amplitude. A law with u = 1 and C = f passes both witness clauses: it accepts f and rejects 2f. 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 equation, meaning the recognition cost is zero. So discrimination is available, but only at the price of naming the target, which the framework treats as a model identification, not a derived constant.
The wall has real width because clauses (ii) and (iii) are exact equalities, not tolerances. The named falsifier, the condition that would reopen the route, is sharp: a newly derived emission-side absolute outside the rational-φ field. The field is closed under every operation the banked corpus performs, so no derivation assembled from banked absolutes can supply such a constant. The target itself is the canonical escape: f is a square root of the field element φ⁴²/8, and square roots of non-square field elements are exactly what the field lacks. Deriving such a non-field absolute remains OPEN and is now typed exactly: the new absolute must live outside ℚ(φ).
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)
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)
THEOREM no_fieldCurrentLaw_passes_selectorGate · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
/-- **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
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
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⟩
What this page does not claim
The theorem does not claim that no law can select the intended amplitude; it only rules out laws whose constants lie in the rational-φ field. The theorem does not claim the intended amplitude is irrational in any stronger sense; it only shows it is not a rational-φ combination. The theorem does not claim the T10 program is complete; deriving a non-φ-field absolute remains an OPEN target.
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 is the physical interpretation of a recognition cost of zero at the intended gap-one pattern?
- What would a newly derived emission-side absolute outside the rational-φ field look like, and what physical quantity could it represent?
- How does the T10 absolute-scale program relate to the broader mass-genesis ladder of particle masses?
- What is the role of the Cassini identity in the arithmetic proof, and does it generalize to other gap factors?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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)The declaration intendedGapOneFactorAmplitude_not_inQPhi is a theorem in the framework's machine-checked library of formal theorems. 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)It establishes that a particular real number, the intended gap-one factor amplitude, cannot be written as p + qφ, where p and q are rational numbers and φ is the golden ratio (1 + √5)/2. intendedGapOneFactorAmplitude_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.leanTHEOREM no_fieldCurrentLaw_passes_selectorGate · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean
/-- **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)The theorem shows no such law exists: acceptance forces f = C/u, and since C and u are both in the field, f would be too, contradicting the arithmetic wall. no_fieldCurrentLaw_passes_selectorGate · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.leanTHEOREM targetConstantLaw_accepts_intended · targetConstantLaw_rejects_doubled · 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' linarithA law with u = 1 and C = f passes both witness clauses: it accepts f and rejects 2f. targetConstantLaw_accepts_intended · targetConstantLaw_rejects_doubled · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.leanTHEOREM 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⟩At the intended pattern, this law's acceptance predicate is exactly the σ-zero equation, meaning the recognition cost is zero. targetConstantLaw_is_sigmaZero_at_intended · IndisputableMonolith/Masses/MassGenesis/T10InhomogeneousFieldCurrentSelectorWall.lean