Masses Mass Genesis T10 Load Reachability Audit

The reachability audit

In the Recognition Science framework, particle masses are meant to be carried by the ledger, a discrete record of recognition events. Each possible mass corresponds to a required anchor load, a numerical target. The question is whether the ledger can actually reach that target. Earlier work proved a wall: no composite posting, a combination of postings across the eight phases of a recognition cycle, equals the required load exactly. The wall looked like a serious obstruction to explaining the mass spectrum.

The audit module measures that wall and reports a surprising verdict. The set of reachable loads is dense in the nonnegative real numbers. For any positive target, no matter how precise, and any tolerance, however small, some composite posting lands within that tolerance. Scaling the unit posting by a rational multiplicity c produces a composite posting whose load is 2c², and twice a rational square comes arbitrarily close to any positive real. The wall is real, but its width is zero: it excludes exact equality and nothing else.

This changes what the wall can mean. The theorem that no composite posting equals the target exactly is still true and still kernel-checked. But carrying a mass spectrum does not require exact equality of real numbers. The audit states both halves together, that the required load is missed exactly and approached to every tolerance, so neither can be quoted without the other. The wall licenses no composite posting equals the target exactly, and it says nothing about whether the ledger can carry the mass spectrum, because no comparison anywhere in the library tests exact equality as the requirement.

The audit also names what a wall with real strength would need: a derived, unit-free bound on posting complexity. Reaching a target to twenty digits with 2c² needs a rational c of height near 10^10, and if the ledger bounds multiplicity the reachable set becomes finite and the miss can be large and real. A sibling result, written immediately after this audit, supplies such a bound for the Boolean posting alphabet, whose loads lie in a finite-ratio set, killing that anchor for the species table by a factor of 2.25 rather than by exactness.

What remains open is the composite-posting layer, which has no such bound: its multiplicities are unrestricted rationals, its loads are dense, and every obstruction stated against it so far is of the empty kind. Whether the ledger bounds posting multiplicity at all is the successor residual, and it is OPEN. The audit is not a repair of the wall; it is a measurement that turns a dramatic obstruction into a precise, limited statement about exact equality, and points to the kind of bound that would actually matter.

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

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

/-- **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 audit does not prove that the ledger can carry the mass spectrum. The audit does not repair or contradict the earlier wall theorem. The audit does not provide the derived bound on posting complexity that it identifies as necessary.

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: