Masses Mass Genesis T10 Load Reachability Audit Charged Row Wall Has Zero Width

The zero-width wall

In the Recognition Science framework, the mass of a particle is predicted as a specific real number, and the framework's ledger, a discrete record of posting events, is supposed to carry that number as a load. The declaration chargedRow_wall_has_zero_width establishes a precise and surprising fact about every charged row in the theory's particle table. For any such row, no composite posting, which is a combination of basic postings with rational multiplicities, produces a load exactly equal to the predicted mass divided by eight. Yet for any tolerance, no matter how small, some composite posting produces a load that falls within that tolerance of the target. The wall that seemed to block the mass spectrum has zero width: it is missed exactly, but approached to every possible degree of approximation.

This result is a theorem in the framework's machine-checked library of formal theorems, and it is built from two simpler facts. First, a posting with rational multiplicity c at a single phase has a load of 2c², and these loads are dense in the nonnegative real numbers. Second, every reachable load is a nonnegative rational number. Together these mean the reachable loads form a dense set of rationals, and a dense set misses any irrational point exactly while landing arbitrarily close to it. The declaration packages both halves for every charged row, so neither can be quoted without the other.

The honest verdict is that this theorem does not repair the wall; it measures it. The wall still stands, and the statement that no composite posting equals the target exactly remains true and kernel-checked. What changes is what may be concluded from it. The theorem licenses only the claim of exact inequality. It says nothing about whether the ledger can carry the mass spectrum, because carrying a mass spectrum does not require exact equality of real numbers, and no comparison in the library tests that requirement. The exclusion has strength zero, in the framework's own vocabulary: the tag is right, but the force is empty.

What survives is the real question: a wall with strength needs a derived, unit-free bound on posting complexity. Reaching a target to twenty digits with 2c² needs a rational c of height near 10¹⁰, and if the ledger bounds multiplicity, the reachable set becomes finite and the miss can be large and real. A sibling theorem, written immediately after this one, supplies exactly such a bound for the Boolean posting alphabet, whose loads are multiples of an eighth and lie in a finite set. That kills the Boolean anchor for the species table by a factor of 2.25 rather than by exactness. The composite-posting layer remains open, with unrestricted rational multiplicities and dense loads, and whether the ledger bounds posting multiplicity at all is the successor residual, an OPEN target.

/-- Every charged row in the theory's table, both halves at once. -/
theorem chargedRow_wall_has_zero_width (row : ChargedMassRow) (ε : ℝ) (hε : 0 < ε) :
    (∀ n : Fin 8 → ℚ,
        MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row) / 8
          ≠ normSq8 (neutralize (compositePosting n)))
      ∧ (∃ n : Fin 8 → ℚ,
          |normSq8 (neutralize (compositePosting n))
            - MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row) / 8| < ε) := by
  refine ⟨chargedRow_required_load_ne_compositePosting row, ?_⟩
  refine exists_compositePosting_within ?_ hε
  have hpos : 0 < MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row) :=
    MassLaw.predict_mass_pos _ _ _
  linarith

/-- Every charged row in the theory's table, both halves at once. -/
theorem chargedRow_wall_has_zero_width (row : ChargedMassRow) (ε : ℝ) (hε : 0 < ε) :
    (∀ n : Fin 8 → ℚ,
        MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row) / 8
          ≠ normSq8 (neutralize (compositePosting n)))
      ∧ (∃ n : Fin 8 → ℚ,
          |normSq8 (neutralize (compositePosting n))
            - MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row) / 8| < ε) := by
  refine ⟨chargedRow_required_load_ne_compositePosting row, ?_⟩
  refine exists_compositePosting_within ?_ hε
  have hpos : 0 < MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row) :=
    MassLaw.predict_mass_pos _ _ _
  linarith

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

This theorem does not claim that the ledger cannot carry the mass spectrum. This theorem does not claim that exact equality of real numbers is what carrying a mass spectrum requires. This theorem does not claim that the wall has been repaired or that any obstruction has been removed.

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: