Masses Mass Genesis T10 Load Reachability Audit Required Load Missed Exactly And

The zero-width wall

In the Recognition Science framework, the ledger, a discrete record of events, assigns each composite posting a load, a squared norm that behaves like an energy. The declaration required_load_missed_exactly_and_approached_to_every_tolerance states two facts together. First, for any sector, rung, and integer parameter, no composite posting produces a load exactly equal to the mass predicted by the framework's mass law, divided by eight. Second, for any positive tolerance, however small, some composite posting produces a load within that tolerance of the same target. The two halves are packaged in one theorem so that neither can be quoted without the other.

The reason is arithmetic, not bad luck. Scaling the unit posting by a rational number c yields a composite posting whose load is 2 c². As c ranges over the rationals, these loads form a dense set: they come arbitrarily close to any positive real number. Every reachable load is a nonnegative rational, by a separate lemma. A dense set of rationals misses any irrational point exactly, yet approaches it to every tolerance. The predicted mass divided by eight is such an irrational point, so the wall that excludes exact equality has width zero.

This result does not repair the wall; it measures it. The earlier theorem that no composite posting equals the target exactly remains true and kernel-checked. What changes is the conclusion one may draw. Exact equality of reals is not what carrying a mass spectrum requires, and no comparison in the library tests it. The declaration licenses only the statement about exact equality, and says nothing about whether the ledger can carry the mass spectrum in any practical sense.

The same shape appears in a sibling result: no Gaussian-rational-preserving map scales a load by the golden ratio phi. That theorem has identical strength, meaning it excludes exact scaling but permits approximation to any tolerance. A wall with real strength would need a derived, unit-free bound on posting complexity. Reaching a target to twenty digits with 2 c² requires a rational c of height near 10^10; if the ledger bounds multiplicity, the reachable set becomes finite and the miss can be large and real. Whether the ledger bounds posting multiplicity at all remains OPEN.

In Recognition Science, this declaration refines the meaning of an obstruction. The nine-attack campaign against the mass wall hit a wall of zero width: it excludes exactness only. The framework's library, a machine-checked collection of formal theorems, records this verdict so future work does not mistake an empty exclusion for a substantive one. The successor question, whether the ledger bounds posting multiplicity, is the real target.

/-- **The wall, measured.** The required anchor load is missed exactly, and
approached to every tolerance. Both halves in one statement, so neither can be
quoted without the other. -/
theorem required_load_missed_exactly_and_approached_to_every_tolerance
    (s : Anchor.Sector) (r Z : ℤ) (hZ : 0 ≤ Z)
    (hp : Int.fib (Anchor.r0 s + r - 13)
            + Z * Int.fib (Anchor.r0 s + r - 14) ≠ 0) :
    (∀ n : Fin 8 → ℚ,
        MassLaw.predict_mass s r Z / 8
          ≠ normSq8 (neutralize (compositePosting n)))
      ∧ (∀ ε : ℝ, 0 < ε → ∃ n : Fin 8 → ℚ,
          |normSq8 (neutralize (compositePosting n))
            - MassLaw.predict_mass s r Z / 8| < ε) := by
  refine ⟨required_load_ne_compositePosting s r Z hZ hp, fun ε hε => ?_⟩
  have hpos : 0 < MassLaw.predict_mass s r Z / 8 := by
    have := MassLaw.predict_mass_pos s r Z
    linarith
  exact exists_compositePosting_within hpos hε

/-- **The wall, measured.** The required anchor load is missed exactly, and
approached to every tolerance. Both halves in one statement, so neither can be
quoted without the other. -/
theorem required_load_missed_exactly_and_approached_to_every_tolerance
    (s : Anchor.Sector) (r Z : ℤ) (hZ : 0 ≤ Z)
    (hp : Int.fib (Anchor.r0 s + r - 13)
            + Z * Int.fib (Anchor.r0 s + r - 14) ≠ 0) :
    (∀ n : Fin 8 → ℚ,
        MassLaw.predict_mass s r Z / 8
          ≠ normSq8 (neutralize (compositePosting n)))
      ∧ (∀ ε : ℝ, 0 < ε → ∃ n : Fin 8 → ℚ,
          |normSq8 (neutralize (compositePosting n))
            - MassLaw.predict_mass s r Z / 8| < ε) := by
  refine ⟨required_load_ne_compositePosting s r Z hZ hp, fun ε hε => ?_⟩
  have hpos : 0 < MassLaw.predict_mass s r Z / 8 := by
    have := MassLaw.predict_mass_pos s r Z
    linarith
  exact exists_compositePosting_within hpos hε

/-- **Its load is `2 c ^ 2`.** Neutralization is linear and the load is a squared
norm, so the rational multiplicity comes out squared against the unit posting's
load of `2`. -/
theorem singlePhaseMultiplicity_load (c : ℚ) :
    normSq8 (neutralize (compositePosting (singlePhaseMultiplicity c)))
      = 2 * (c : ℝ) ^ 2 := by
  rw [singlePhaseMultiplicity_compositePosting, normSq8_neutralize_smul,
    unitPosting_load]
  ring

/-- The other side of the sandwich, restated from the existing rationality lemma:
every reachable load is a nonnegative rational. -/
theorem compositePosting_load_nonneg_rat (n : Fin 8 → ℚ) :
    ∃ q : ℚ, 0 ≤ q ∧ normSq8 (neutralize (compositePosting n)) = (q : ℝ) := by
  obtain ⟨c, hc⟩ := gaussianRational_load_rat (compositePosting_gaussianRational n)
  refine ⟨c, ?_, hc⟩
  have hnn : (0 : ℝ) ≤ normSq8 (neutralize (compositePosting n)) :=
    Finset.sum_nonneg fun i _ => Complex.normSq_nonneg _
  rw [hc] at hnn
  exact_mod_cast hnn

What this page does not claim

The declaration does not claim the ledger cannot carry the mass spectrum, only that exact equality is impossible. It does not claim the wall has any width or that the miss is large; the miss has radius zero. It does not claim the framework derives particle masses; the mass law prediction is a separate statement.

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