Masses Mass Genesis T10 Double Entry Posting Wall Double Entry Ceiling Lt Phased

The double-entry ceiling

In the Recognition Science framework, a ledger is a discrete record of events, and a posting is one unit of change recorded between two consecutive ticks. The declaration doubleEntry_ceiling_lt_phasedPosting_ceiling is a proved inequality: it states that 32 is strictly less than 512 divided by 7, which is about 73.14. The statement is a theorem in the framework's machine-checked library of formal theorems, meaning it is a logical consequence of the framework's definitions and prior results, not an independent assumption.

The inequality matters because it compares two ceilings on the ratio of masses that the framework can describe. Under the framework's double-entry posting rule, where each posting is balanced by a corresponding posting on the next tick, the largest possible ratio between two rest masses is 32. Under a looser rule called phased posting, the ceiling is higher, about 73.14. The theorem says the double-entry ceiling is strictly lower. This is a tightening: the more restrictive accounting rule permits a smaller range of mass ratios.

The tightening has a consequence that the framework's own documentation calls honest. The measured ratio of the muon mass to the electron mass is about 206.77. The double-entry ceiling of 32 falls far below that measured value, by a factor of about 6.46. The framework does not claim to derive the muon-to-electron ratio; it claims the opposite. The theorem doubleEntry_excludes_measured_muonElectron states that no two stable patterns satisfying the double-entry rule can have a mass ratio equal to the measured muon-to-electron ratio. The framework's stricter accounting rule makes the disagreement with experiment sharper, not weaker.

The theorem does not stand alone. It relies on a premise called OnePostingPerTick, which says that at most one unit of posting occurs at any tick. That premise is assumed, not derived, and the framework's own audit flags it as an open gap. The ceiling of 32 depends on this assumption; the lower bound of 2 on any nonzero mass load does not, since it follows only from integer counting. The framework also notes that the result bounds a quantity called restMass, which is defined as an integrated load, a modelling choice rather than a derived physical quantity.

What the theorem establishes is a precise, machine-checked relationship between two ceilings. What it does not establish is a derivation of any measured mass ratio, a proof that the double-entry rule is the one nature uses, or a resolution of the open question of why the framework's posting model applies to physical reality. The framework's own documentation is explicit on these limits.

/-- The tightening is a checked fact, not a remark: `32 < 512/7`. -/
theorem doubleEntry_ceiling_lt_phasedPosting_ceiling : (32 : ℝ) < 512 / 7 := by norm_num

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

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

/-- Ceiling: one posting per tick caps a site's load at eight. Inherited from the
Boolean ceiling now that Boolean-ness is derived rather than assumed. -/
theorem onePostingPerTick_load_le_eight {w : PhotonWindow} {p : Fin 8 → ℤ}
    (hp : ∀ t, w t = ((p t - p (t + 1) : ℤ) : ℂ)) (hrate : OnePostingPerTick p) :
    normSq8 (neutralize w) ≤ 8 :=
  booleanWindow_neutralizedNormSq_le (booleanWindow_of_onePostingPerTick hp hrate)

What this page does not claim

The framework does not derive the measured muon-to-electron mass ratio. The theorem does not prove that the double-entry rule is the one nature uses. The result does not resolve the open question of why the posting model applies to physical reality.

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: