Masses Mass Genesis T10 Double Entry Posting Wall Unbalanced Unit Window Load Eq

The 7/8 floor

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is the act of registering one such event. The declaration unbalancedUnitWindow_load_eq_sevenEighths computes the cost of the simplest possible unbalanced record: a window of eight ticks in which exactly one tick is occupied and the other seven are empty. The theorem states that the load, defined as the squared norm of the window after subtracting its mean, equals exactly 7/8.

This number is not arbitrary. The framework proves that any window expressible as a balanced posting, meaning a record where every entry at tick t is offset by an equal and opposite entry at tick t+1, has zero total sum. The unbalanced unit window, with its single occupied tick, fails this test. Its load of 7/8 is therefore the minimum possible load for any window that is not balanced, establishing a floor below which no genuine recognition pattern can fall.

The result matters because it feeds directly into the framework's account of particle masses. Later theorems show that under the additional assumption of one posting per tick, the load of any balanced window is an even integer, raising the floor from 7/8 to 2. The ceiling, meanwhile, is 8, so the ratio of the heaviest to the lightest possible mass in this model is at most 32. The measured muon-to-electron mass ratio is about 206.77, which exceeds 32 by a factor of 6.46. The framework's double-entry structure therefore excludes the measured ratio, a refutation that is stated as a theorem, not a hypothesis.

The declaration itself does not claim that the unbalanced unit window is physically realized, nor that the 7/8 value corresponds to any observed particle. It is a statement about the mathematical properties of a defined object within the framework. The floor of 7/8 is later superseded by the stronger floor of 2 under the one-posting-per-tick assumption, which is itself an assumption, not a derived result. The declaration also does not claim that the framework's mass model is complete; the bridge from the abstract ledger to physical particles remains an open problem.

/-- **Why the floor rises from `7/8` to `2`.** The window attaining the Boolean
floor is exactly one that posts without settling, so double entry excludes it. The
tightening is therefore not an artefact of a smaller class chosen for convenience:
it is the removal of unbalanced windows, and those are precisely the cheap ones. -/
theorem unbalancedUnitWindow_load_eq_sevenEighths :
    normSq8 (neutralize unbalancedUnitWindow) = 7 / 8 := by
  rw [normSq8_neutralize_eq]
  norm_num [normSq8, unbalancedUnitWindow, Fin.sum_univ_eight, Complex.normSq_apply]

/-- **Balanced postings are neutral.** The debits and credits telescope around the
cycle. -/
theorem sum_coboundary (q : Fin 8 → ℂ) : (∑ t : Fin 8, coboundary q t) = 0 := by
  unfold coboundary
  rw [Finset.sum_sub_distrib, sum_succ_eq]
  ring

/-- Load floor for an integer posting with positive load. -/
theorem integerPosting_load_ge_two {w : PhotonWindow} {p : Fin 8 → ℤ}
    (hp : ∀ t, w t = ((p t - p (t + 1) : ℤ) : ℂ))
    (hpos : 0 < normSq8 (neutralize w)) :
    2 ≤ normSq8 (neutralize w) := by
  rw [load_eq_postingLoadInt hp] at hpos ⊢
  have : 0 < postingLoadInt p := by exact_mod_cast hpos
  exact_mod_cast postingLoadInt_ge_two_of_pos this

/-- **The double-entry mass ratio wall.** Deriving the posting alphabet instead of
assuming it tightens the ceiling from `512/7 ≈ 73.14` to exactly `32`. -/
theorem doubleEntry_restMass_ratio_le {ψ χ : LightPattern (Fin 8)}
    (hsψ : StableClosedLightPattern ψ) (hsχ : StableClosedLightPattern χ)
    (hdψ : DoubleEntrySettledPattern ψ) (hdχ : DoubleEntrySettledPattern χ) :
    restMass ψ ≤ 32 * restMass χ := by
  rw [restMass_eq_integratedMeaningLoad_of_stable ψ hsψ,
      restMass_eq_integratedMeaningLoad_of_stable χ hsχ]
  have hup : integratedMeaningLoad ψ ≤ 64 := doubleEntry_integratedLoad_le_sixtyFour hdψ
  have hlo : 2 ≤ integratedMeaningLoad χ := doubleEntry_integratedLoad_ge_two hdχ hsχ.2.1
  nlinarith [hup, hlo]

/-- **The instantiated refutation, tighter than the phased-posting one.** No two
double-entry settled stable patterns on `Fin 8` can stand in the measured
muon-to-electron mass ratio, which exceeds 32 by a factor of 6.46. -/
theorem doubleEntry_excludes_measured_muonElectron {ψ χ : LightPattern (Fin 8)}
    (hsψ : StableClosedLightPattern ψ) (hsχ : StableClosedLightPattern χ)
    (hdψ : DoubleEntrySettledPattern ψ) (hdχ : DoubleEntrySettledPattern χ) :
    restMass ψ ≠ measuredMuonElectronMassRatio * restMass χ := by
  intro hEq
  have hle := doubleEntry_restMass_ratio_le hsψ hsχ hdψ hdχ
  have hpos : 0 < restMass χ := by
    rw [restMass_eq_integratedMeaningLoad_of_stable χ hsχ]
    have := doubleEntry_integratedLoad_ge_two hdχ hsχ.2.1
    linarith
  rw [hEq] at hle
  have hr : (32 : ℝ) < measuredMuonElectronMassRatio := by
    unfold measuredMuonElectronMassRatio; norm_num
  nlinarith [hle, hpos, hr]

What this page does not claim

The unbalanced unit window is a physically realized recognition pattern. The 7/8 value corresponds to any observed particle mass. The one-posting-per-tick assumption is derived rather than assumed. The framework's mass model is complete or closed.

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