Masses Mass Genesis T10 Double Entry Mass Quantum Two Valued Occupation Load Rat

The ratio that cancels units

In the Recognition Science account, mass is not a substance but a count of changes. The framework models a particle's state on a cycle of eight ticks, and a settlement window, a discrete record of how that state changes from one tick to the next, turns an occupation pattern into a load: the squared size of the change. The central theorem, tagged THEOREM on a MODEL carrier, states that for any occupation taking only two values, zero and some complex number lam, the settlement load equals the squared magnitude of lam times the number of cuts, the count of positions where the occupation changes value. Because the lam factor appears in both numerator and denominator, it cancels in every ratio of two such loads.

The classical content here is a double-entry bookkeeping intuition. If a ledger records a quantity at eight successive moments, the total change is the sum of the differences between consecutive entries. The theorem says that when the entries are only ever zero or a fixed value, that total change is exactly the fixed value squared, multiplied by the number of times the entries differ. The number of differences is the cutCount, a pure integer between zero and eight. This makes the load a multiple of the unit squared amplitude, and for Boolean occupations, where the values are only zero or one, the load must lie in the set {0, 2, 4, 6, 8}.

The framework's library, a machine-checked collection of formal theorems, proves this in the module T10DoubleEntryMassQuantum. The theorem supersedes an earlier bound of 64/7, about 9.14, and a general bound of 64, replacing them with a wall of four per voxel for any posting unit. The result makes the substrate requirement harder, not easier, because it forces a smaller ceiling on what a single voxel can contribute. The homogeneity of the settlement primitive means every nonnegative real load is realized by some occupation, so the two-valuedness, not the derivative construction alone, forces the quantum.

The honest wall is that the theorem does not fix a scale. The literal 1 in a unit commit occupation is an indicator of a decidable ledger predicate; the forced content is two-valuedness, and which two complex values appear is a units choice that cancels in ratios. The results concern one eight-tick voxel only, and nothing says how many voxels a particle occupies. The charged-lepton ratios are not addressed: with the wall at 4 per voxel, the muon-to-electron ratio of 206.768 needs a substrate-count ratio of at least 52, and the theory does not name a count.

What the theorem changes is the shape of the mass question. Instead of asking what mass is, the framework asks how many changes a state makes, and the answer is a small even integer times a unit that cancels. The reader can now see that the quantum of mass, in this account, is not a fitted constant but a consequence of two-valuedness on a discrete cycle, and that the remaining open question is how many voxels a particle occupies.

theorem t10DoubleEntryUnitFreeMassWallCert :
    T10DoubleEntryUnitFreeMassWallCert where
  unit_factors_out := twoValuedOccupation_settlementLoad_eq_normSq_mul_cutCount
  cutCount_even := twoValuedOccupation_cutCount_even
  cutCount_le_eight_field := cutCount_le_eight
  load_cutCount_cancel := twoValuedOccupation_load_cutCount_cancel
  unit_free_mass_ratio_le_four := twoValuedOccupation_mass_ratio_le_four
  wall_tight_at_cuts_two_and_eight := twoValuedOccupation_mass_ratio_wall_tight
  vacuum_and_full_cycle_massless :=
    ⟨twoValuedVacuum_settlementLoad, twoValuedFull_settlementLoad⟩
  three_valued_discriminates_R9 :=
    ⟨threeValuedDiscriminatingWitness_settlementLoad,
      threeValuedDiscriminatingWitness_cutCount,
      threeValuedDiscriminatingWitness_R9_fails_at_one⟩
  scope_one_eight_tick_voxel := trivial
  scope_lepton_ratios_not_addressed := trivial
  scope_posting_unit_not_derived := trivial

/-- Boolean settlement loads lie in `{0, 2, 4, 6, 8}`. -/
theorem booleanOccupation_settlementLoad_mem
    (occ : Fin 8 → ℂ) (h : BooleanOccupation occ) :
    settlementLoad occ ∈ ({0, 2, 4, 6, 8} : Set ℝ) := by
  obtain ⟨k, hk⟩ :=
    integerOccupation_settlementLoad_even occ h.integerOccupation
  have hle : settlementLoad occ ≤ 8 :=
    booleanOccupation_settlementLoad_le_eight occ h
  have hk_le : (k : ℝ) ≤ 4 := by
    have : 2 * (k : ℝ) ≤ 8 := by rw [← hk]; exact hle
    linarith
  have hk_nat : k ≤ 4 := by exact_mod_cast hk_le
  rw [hk]
  interval_cases k <;> norm_num

theorem t10DoubleEntryUnitFreeMassWallCert :
    T10DoubleEntryUnitFreeMassWallCert where
  unit_factors_out := twoValuedOccupation_settlementLoad_eq_normSq_mul_cutCount
  cutCount_even := twoValuedOccupation_cutCount_even
  cutCount_le_eight_field := cutCount_le_eight
  load_cutCount_cancel := twoValuedOccupation_load_cutCount_cancel
  unit_free_mass_ratio_le_four := twoValuedOccupation_mass_ratio_le_four
  wall_tight_at_cuts_two_and_eight := twoValuedOccupation_mass_ratio_wall_tight
  vacuum_and_full_cycle_massless :=
    ⟨twoValuedVacuum_settlementLoad, twoValuedFull_settlementLoad⟩
  three_valued_discriminates_R9 :=
    ⟨threeValuedDiscriminatingWitness_settlementLoad,
      threeValuedDiscriminatingWitness_cutCount,
      threeValuedDiscriminatingWitness_R9_fails_at_one⟩
  scope_one_eight_tick_voxel := trivial
  scope_lepton_ratios_not_addressed := trivial
  scope_posting_unit_not_derived := trivial

theorem scaledHalfSupportOccupation_settlementLoad
    (r : ℝ) (hr : 0 ≤ r) :
    settlementLoad (scaledHalfSupportOccupation r) = r := by
  have hnonneg : 0 ≤ r / 2 := by linarith
  set s : ℝ := Real.sqrt (r / 2)
  have hs : s * s = r / 2 := Real.mul_self_sqrt hnonneg
  have hnorm : Complex.normSq (s : ℂ) = r / 2 := by
    simp [Complex.normSq, Complex.ofReal_re, Complex.ofReal_im, hs]
  have hneg : Complex.normSq (-(s : ℂ)) = r / 2 := by
    rw [Complex.normSq_neg, hnorm]
  unfold settlementLoad
  rw [neutralize_settlementWindow, scaledHalfSupportOccupation_settlementWindow]
  -- Rephrase the window through the local `s`.
  change normSq8
      (fun t => if t = 0 then (s : ℂ) else if t = 1 then -(s : ℂ) else 0) = r
  unfold normSq8
  rw [Fin.sum_univ_eight]
  simp [hnorm, hneg]

What this page does not claim

The theorem does not fix the scale lam, which remains a units choice that cancels in ratios. The theorem does not say how many voxels a particle occupies, and the theory names no voxel count. The theorem does not address the charged-lepton mass ratios, which require a substrate-count ratio of at least 52.

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