Masses Mass Genesis T10 Phased Posting Mass Ratio Wall Phased Posting Load Pos G

The floor under a phased posting

The declaration phasedPosting_load_pos_ge_sevenEighths is a theorem in the Recognition Science library. It states a lower bound on a quantity called load, which the framework defines as a measure of meaning carried by a discrete record of events. The theorem says: if a window of eight positions is a phased posting, meaning some single rotation of its amplitudes makes every position a Boolean posting, and if its load is positive, then that load is at least 7/8. A Boolean posting is an amplitude that takes one of three values: -1, 0, or 1.

The bound matters because it survives a symmetry that the raw Boolean condition does not. Multiplying every amplitude in a window by a unit-modulus complex number, a global phase rotation, leaves the load exactly unchanged. The theorem proves this by showing that both terms in the load formula are quadratic in the window, so the unit factor cancels. This is why the phased hypothesis costs nothing: it widens the class of allowed windows without changing the load. The class is strictly larger than the Boolean one, since a constant window of the imaginary unit i is a phased posting but no tick of it is Boolean.

The floor of 7/8 combines with a ceiling of 8 per site and at most eight sites to give a total load between 7/8 and 64 for any stable closed pattern. From that, the framework derives a ratio wall: any two stable closed patterns whose occupied windows are phased postings have rest mass ratio at most 512/7, about 73.14. The measured muon-to-electron mass ratio is 206.7682830, which exceeds that ceiling by a factor of 2.83. The exclusion is about 2.9 × 10^7 standard deviations from the measurement's uncertainty of 0.0000046.

The theorem does not claim that any physical particle has a load in this range. It bounds a quantity the library defines as rest mass, and that definition is a modelling choice, not a derived fact. The conjunction of "realized matter windows are phased postings" and "the site index is Fin 8" is refuted by the measured muon-to-electron ratio, but which conjunct fails is not decided. The theorem also does not provide a mass formula, a rung table, or a value for any fundamental constant. It is a ratio statement, so no unit enters and no unit-dependent absolute window appears.

/-- Floor: a phased posting site with positive load carries at least `7/8`. The
integrality of the tick sum survives a global rotation, which is what keeps the
floor away from zero. -/
theorem phasedPosting_load_pos_ge_sevenEighths {w : PhotonWindow}
    (h : IsPhasedPosting w) (hpos : 0 < normSq8 (neutralize w)) :
    7 / 8 ≤ normSq8 (neutralize w) := by
  obtain ⟨u, hu, hbool⟩ := h
  have heq := normSq8_neutralize_unit_mul hu w
  rw [← heq] at hpos ⊢
  exact booleanWindow_load_pos_ge_sevenEighths hbool hpos

/-- **A global rotation leaves the load exactly unchanged.** Both terms of the
neutralized norm are quadratic in the window, so a unit-modulus factor cancels.
This is the whole reason the phased hypothesis costs nothing. -/
theorem normSq8_neutralize_unit_mul {u : ℂ} (hu : Complex.normSq u = 1)
    (w : PhotonWindow) :
    normSq8 (neutralize (fun t => u * w t)) = normSq8 (neutralize w) := by
  unfold normSq8
  refine Finset.sum_congr rfl ?_
  intro j _
  rw [neutralize_mul_left u w j, Complex.normSq_mul, hu, one_mul]

/-- **The phased-posting mass ratio wall.** Any two stable closed patterns whose
occupied windows are ledger postings up to phase have rest mass ratio at most
`512/7 ≈ 73.14`. No Q3 hypothesis, no unit, no mass-law constant. -/
theorem phasedPosting_restMass_ratio_le {ψ χ : LightPattern (Fin 8)}
    (hsψ : StableClosedLightPattern ψ) (hsχ : StableClosedLightPattern χ)
    (hbψ : ∀ x ∈ ψ.support, IsPhasedPosting (ψ.window x))
    (hbχ : ∀ x ∈ χ.support, IsPhasedPosting (χ.window x)) :
    restMass ψ ≤ (512 / 7) * restMass χ := by
  rw [restMass_eq_integratedMeaningLoad_of_stable ψ hsψ,
      restMass_eq_integratedMeaningLoad_of_stable χ hsχ]
  have hup : integratedMeaningLoad ψ ≤ 64 :=
    phasedPosting_integratedLoad_le_sixtyFour hbψ
  have hlo : 7 / 8 ≤ integratedMeaningLoad χ :=
    phasedPosting_integratedLoad_ge_sevenEighths hbχ hsχ.2.1
  nlinarith [hup, hlo]

/-- The measured muon-to-electron mass ratio, PDG 2024: `206.7682830(46)`. An
external measurement, carried as a numeral so the exclusion below is a closed
arithmetic fact rather than a claim about the physical world. -/
def measuredMuonElectronMassRatio : ℝ := 206.7682830

What this page does not claim

The theorem does not establish that any physical particle has a load in the bounded range. It does not provide a mass formula, a rung table, or a value for any fundamental constant. It does not decide which of the two hypotheses in the refuted conjunction is false.

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