Masses Mass Genesis T10 Deposit Location Organ Sqrt Escape Uniform On Closed Set

The uniform escape

The golden ratio φ is the number satisfying φ² = φ + 1, about 1.618. The expression (1 + φ^k) / φ^k, for a whole number k, is a number built from powers of φ. The theorem in question takes the square root of that expression and asks whether the result belongs to Q(φ), the field of numbers of the form a + bφ with a and b rational. For odd k, and for the two special cases k = 0 and k = 1, the answer is no: the square root escapes the field.

The declaration sqrt_escape_uniform_on_closed_set packages this fact for two indices at once. If k₁ and k₂ are both odd, or equal to 0 or 1, then the square roots for both escape Q(φ). The uniformity is the point: every rung in this set escapes in the same way. No member of the set is singled out by field membership. The theorem is proved in the machine-checked library of formal theorems, with the proof resting on the odd case, the k = 0 case (which reduces to the square root of 2), and the k = 1 case (which reduces to the square root of φ).

In Recognition Science, the framework models particle masses as deposits on rungs of a ladder indexed by k. The question at this tier is whether some recognition-native organ, some principle built from the ledger of deposit counts, forces where deposits land. The uniform escape theorem contributes a negative result: because every odd rung and both anchors escape the field identically, field membership cannot select among them. This is part of a larger wall, deposit_location_organ_wall, which proves that at the cascade-spectral tier, no such organ forces a viable nonempty deposit location. The wall also records that order is invisible (same deposit counts give the same spectrum) and amplitude is invisible (the cascade eigenvalues do not depend on the amplitude a).

The theorem does not claim that no organ anywhere forces deposit locations. It leaves open the even k ≥ 2 case for the general escape, and it names the missing piece: a scale-bearing parent outside cascade-spectral data. The framework's own account says the physical bridge from recognition to linking is open. What the theorem does establish is a clean boundary: within this tier, the escape is uniform, so the answer to where deposits land must come from elsewhere.

/-- **Sqrt escape on every odd rung and the two banked anchors.** -/
theorem sqrt_response_not_inQPhi_odd_or_anchor (k : ℕ)
    (h : Odd k ∨ k = 0 ∨ k = 1) :
    ¬ InQPhi (Real.sqrt ((1 + phi ^ k) / phi ^ k)) := by
  rcases h with hodd | rfl | rfl
  · exact sqrt_response_not_inQPhi_odd hodd
  · exact sqrt_response_not_inQPhi_zero
  · exact sqrt_response_not_inQPhi_one

/-- **Uniformity on the closed escape set:** every odd rung and both anchors
escape `Q(φ)` alike, so field membership cannot select among them. -/
theorem sqrt_escape_uniform_on_closed_set {k₁ k₂ : ℕ}
    (h₁ : Odd k₁ ∨ k₁ = 0 ∨ k₁ = 1)
    (h₂ : Odd k₂ ∨ k₂ = 0 ∨ k₂ = 1) :
    (¬ InQPhi (Real.sqrt ((1 + phi ^ k₁) / phi ^ k₁))) ∧
      (¬ InQPhi (Real.sqrt ((1 + phi ^ k₂) / phi ^ k₂))) :=
  ⟨sqrt_response_not_inQPhi_odd_or_anchor k₁ h₁,
    sqrt_response_not_inQPhi_odd_or_anchor k₂ h₂⟩

/-- **DEPOSIT-LOCATION ORGAN WALL (THEOREM), cascade-spectral tier.**

At the named tier of principles whose observable data is a function of
cascade modular eigenvalues (equivalently, of deposit counts):

* order is invisible (`cascade_order_blind`);
* amplitude is invisible (`cascade_amplitude_blind`);
* the four C3 cascade shapes fail (`cascade_verdict`);
* sqrt-escape is uniform on every odd rung and the banked anchors, so it
  does not select a location among those rungs.

No recognition-native organ at this tier forces a viable nonempty deposit
location. The missing organ is a scale-bearing parent outside
cascade-spectral data (binding: `D-rs-t10-scale-bearing-parent-required`).
Even-`k` residual of the general sqrt escape (beyond the anchors) remains
recorded as the next named sub-tier to close; it cannot restore selection
by field membership alone, because the closed set is already uniform. -/
theorem deposit_location_organ_wall {N : ℕ} (hN : 2 ≤ N) {a : ℝ} (ha : a ≠ 0) :
    (∀ (ks ks' : List (Fin N)),
      (∀ n, depositCount ks n = depositCount ks' n) →
        cascadeSpectrum ks = cascadeSpectrum ks') ∧
    (∀ (b : ℝ), b ≠ 0 → ∀ (ks : List (Fin N)) (i j : SectorN N),
      cascadeEigenvalue a ks i j = cascadeEigenvalue b ks i j) ∧
    (∀ (ks : List (Fin N)) (k : Fin N),
      MatchesSinglePosting ks k → SpectrallyDistinguished k → k = rungOne hN) ∧
    (¬ InQPhi (Real.sqrt phi)) ∧
    (∀ k : ℕ, Odd k ∨ k = 0 ∨ k = 1 →
      ¬ InQPhi (Real.sqrt ((1 + phi ^ k) / phi ^ k))) := by
  refine ⟨?_, ?_, ?_, sqrt_phi_not_inQPhi, ?_⟩
  · intro ks ks' hc
    exact cascade_order_blind ha ks ks' hc
  · intro b hb ks i j
    exact cascade_amplitude_blind ha hb ks i j
  · intro ks k hm hd
    exact conditioning_collapses_to_killed_shape hN ks k hm hd
  · intro k hk
    exact sqrt_response_not_inQPhi_odd_or_anchor k hk

/-- **Order blindness.** Same deposit counts ⇒ identical cascade spectrum. -/
theorem cascade_order_blind {N : ℕ} {a : ℝ} (_ha : a ≠ 0)
    (ks ks' : List (Fin N))
    (hc : ∀ n : Fin N, depositCount ks n = depositCount ks' n) :
    cascadeSpectrum ks = cascadeSpectrum ks' := by
  ext x
  constructor
  · rintro ⟨n, m, rfl⟩
    exact ⟨n, m, by rw [hc n]⟩
  · rintro ⟨n, m, rfl⟩
    exact ⟨n, m, by rw [hc n]⟩

What this page does not claim

The theorem does not prove that no organ anywhere forces deposit locations, only that none does at the cascade-spectral tier. The even k ≥ 2 case of the general sqrt escape remains open. The theorem does not establish where deposits actually land, only that field membership cannot select among the closed set.

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/T10DepositLocationOrgan.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: