Masses Mass Genesis T10 Double Entry Mass Quantum Three Valued Discriminating Wi

The three-valued witness

The declaration threeValuedDiscriminatingWitness is a concrete example used inside a machine-checked library of formal theorems. It is a function that assigns one of three complex values to each of eight positions on a cycle: the value 1 at the first position, 2 at the second, and 0 at the remaining six. The name "discriminating" reflects its role: it separates the case where a two-valued condition holds from the case where it fails.

The library proves that this witness has a cut count of exactly 3. The cut count is the number of adjacent positions on the cycle where the assigned value changes. For the witness, the value changes from 1 to 2, from 2 to 0, and from 0 back to 1 when wrapping around the cycle's end, giving three changes in total. This is an odd number, and it matters because the library separately proves that any occupation taking only two distinct values (0 and some fixed complex number) must have an even cut count. The witness therefore demonstrates that the even-cut-count property genuinely requires the two-valued restriction; allowing a third value breaks it.

The witness is not a claim about any physical particle. It is a technical counterexample inside a formal development about a discrete settlement process on a single eight-tick cycle. The library uses it to show that the two-valued condition, not the derivative construction alone, is what forces the even cut count and the associated mass quantum. The witness itself has no measured mass, no experimental signature, and no role in any particle data table.

What the witness does not claim is broader than what it establishes. It says nothing about how many eight-tick cycles a real particle occupies; the library's own scope notes state that the substrate count is undefined in this formalism. It says nothing about the charged-lepton mass ratios, which would require a substrate-count ratio of at least 52 given the wall of 4 per cycle. And it does not derive the unit value lam; that remains a units choice that cancels in every mass ratio. The witness's entire content is the single fact that a three-valued pattern on one cycle has an odd cut count of 3.

theorem threeValuedDiscriminatingWitness_cutCount :
    cutCount threeValuedDiscriminatingWitness = 3 := by
  classical
  have hv := threeValued_values
  have hsub0 : ((0 : Fin 8) - 1) = 7 := by decide
  have hsub1 : ((1 : Fin 8) - 1) = 0 := by decide
  have hsub2 : ((2 : Fin 8) - 1) = 1 := by decide
  unfold cutCount
  have heq :
      Finset.univ.filter
          (fun t => threeValuedDiscriminatingWitness t ≠
            threeValuedDiscriminatingWitness (t - 1)) =
        ({0, 1, 2} : Finset (Fin 8)) := by
    ext t
    fin_cases t <;>
      simp [threeValuedDiscriminatingWitness, hv, hsub0, hsub1, hsub2]
  simp [heq]

/-- **R10.** For a two-valued occupation the cut count is even. -/
theorem twoValuedOccupation_cutCount_even
    (lam : ℂ) (occ : Fin 8 → ℂ) (h : TwoValuedOccupation lam occ) :
    Even (cutCount occ) := by
  classical
  by_cases hlam : lam = 0
  · have hall : ∀ t, occ t = 0 := by
      intro t
      rcases h t with h0 | hL
      · exact h0
      · simp [hL, hlam]
    have hz : cutCount occ = 0 := by
      unfold cutCount
      simp [hall]
    exact ⟨0, by simp [hz]⟩
  · set b : Fin 8 → ℂ := fun t => if occ t = lam then (1 : ℂ) else 0
    have hb : BooleanOccupation b := by
      intro t
      by_cases ht : occ t = lam <;> simp [b, ht]
    have hcut : cutCount occ = cutCount b :=
      twoValued_cutCount_eq_booleanized lam hlam occ h
    have hload : settlementLoad b = (cutCount b : ℝ) := by
      have := twoValuedOccupation_settlementLoad_eq_normSq_mul_cutCount
        (1 : ℂ) b hb.twoValued
      simpa [Complex.normSq_one] using this
    obtain ⟨k, hk⟩ :=
      integerOccupation_settlementLoad_even b hb.integerOccupation
    have hcard : (cutCount b : ℝ) = 2 * (k : ℝ) := by
      rw [← hload, hk]
    have hnat : cutCount b = k + k := by
      have : cutCount b = 2 * k := by exact_mod_cast hcard
      rw [this, two_mul]
    exact hcut ▸ ⟨k, hnat⟩

/-- Discrete tick-derivative of an occupation on the cyclic eight-tick clock. -/
def settlementWindow (occ : Fin 8 → ℂ) : PhotonWindow :=
  fun t => occ t - occ (t - 1)

What this page does not claim

The witness is not a physical particle and carries no measured mass. The witness does not establish how many cycles a particle occupies. The witness does not derive the charged-lepton mass ratios. The witness does not derive the unit value lam.

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: