Masses Mass Genesis T10 Load Reachability Audit Composite Posting Load Nonneg Ra

Every reachable load

In the Recognition Science framework, a ledger (a discrete record of events) assigns mass-like values through a process called posting. A composite posting is a weighted combination of the eight basic posting phases, with each weight chosen as a rational number. The declaration compositePosting_load_nonneg_rat proves that the load, a measure of the posting's size after neutralization, is always a nonnegative rational number. Rational numbers are those expressible as a ratio of two integers, like 3/4 or 22/7, and nonnegative means zero or positive.

The theorem works by showing that any composite posting's load equals some rational number, and that this load cannot be negative. The proof combines two facts: that every composite posting maps to a Gaussian rational (a complex number with rational real and imaginary parts), and that the load is a sum of squared magnitudes, which are always nonnegative. The declaration is one half of a sandwich: the other half, proved in the same module, shows that these loads are dense, meaning any positive real number can be approached arbitrarily closely by some composite posting's load.

This density result is what gives the theorem its significance. Earlier work in the framework proved that no composite posting can exactly equal the mass value predicted by the mass law, a result called the irrationality wall. That wall might seem to block the ledger from carrying the mass spectrum. But compositePosting_load_nonneg_rat, together with the density theorem, shows the wall has zero width: for any tolerance, no matter how small, some composite posting lands within that tolerance of the target. The exclusion is only about exact equality, not about approximation.

What the declaration does not claim is that the ledger can carry the mass spectrum exactly. It says nothing about whether the ledger's loads can match the predicted masses to any required precision, because the density result is about approximation, not exactness. The theorem also does not claim that the ledger bounds posting multiplicity; whether it does remains an open question in the framework. The declaration is a precise, narrow statement about the arithmetic of loads, and its role is to measure the wall's strength, not to repair it.

/-- 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

/-- **For every tolerance, a composite posting lands inside it.** The target may
be any positive real, the required anchor load included. -/
theorem exists_compositePosting_within {L ε : ℝ} (hL : 0 < L) (hε : 0 < ε) :
    ∃ n : Fin 8 → ℚ,
      |normSq8 (neutralize (compositePosting n)) - L| < ε := by
  obtain ⟨c, hc⟩ := exists_rat_sq_within hL hε
  exact ⟨singlePhaseMultiplicity c, by rw [singlePhaseMultiplicity_load]; exact hc⟩

/-- **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ε

What this page does not claim

The ledger can carry the mass spectrum exactly, only that it can approximate any target to any tolerance. The ledger bounds posting multiplicity, which remains an open question. The irrationality wall is repaired or contradicted, only that its exclusion is limited to exact equality.

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: