Foundation Born Rule Forcing Occupied Modes Two Branch Card Le Two

Two-branch states

A state in this framework is an eight-component list of complex numbers, called a signal: a discrete record of eight complex amplitudes. A mode is a position in that list. A state's occupied modes are the positions where the amplitude is not zero. The lemma occupiedModes_twoBranch_card_le_two says: any state built from two branches, meaning a state whose amplitudes are real and nonzero only in the first two positions, has at most two occupied modes. That is the entire content of the declaration.

The statement is a theorem in the machine-checked library of formal theorems. It is proved for the specific two-branch construction, which places a cosine amplitude in position zero and a sine amplitude in position one, with all other positions zero. The proof is a direct computation: the definition of occupied modes filters the list to nonzero entries, and the two-branch signal has zeros everywhere except the first two positions. The theorem is tagged private in the source, meaning it is an internal lemma used to support a larger result, not a standalone claim about all possible states.

The larger result is a uniqueness theorem for probability measures on eight-mode sectors. The library proves that any measure satisfying normalization, phase invariance, additivity, and consistency with the two-branch Born rule must equal the sum of squared amplitudes over the sector. The two-branch cardinality bound appears in the proof of that uniqueness theorem, where it helps control the behavior of a witness measure on states with few occupied modes. The bound itself does not establish the uniqueness theorem; it is one ingredient in a longer argument.

What the lemma does not claim: it says nothing about states with more than two branches, and it does not assert that a two-branch state must occupy exactly two modes, only at most two. The theorem also does not say anything about the Born rule or probability measures directly; it is a purely combinatorial fact about the support of a specific family of signals.

private theorem occupiedModes_twoBranch_card_le_two (rot : TwoBranchRotation) :
    (occupiedModes (twoBranchSignal rot)).card ≤ 2 := by
  classical
  have hsubset :
      occupiedModes (twoBranchSignal rot) ⊆ ({0, 1} : Finset (Fin 8)) := by
    intro k hk
    simp [occupiedModes, twoBranchSignal] at hk ⊢
    by_cases h0 : k = (0 : Fin 8)
    · simp [h0]
    · by_cases h1 : k = (1 : Fin 8)
      · simp [h1]
      · exfalso
        apply hk
        simp [h0, h1]
  have hle := Finset.card_le_card hsubset
  have hcard : ({0, 1} : Finset (Fin 8)).card = 2 := by decide
  omega

What this page does not claim

The lemma does not prove the Born rule uniqueness theorem by itself. The lemma does not apply to states with more than two branches. The lemma does not assert that two-branch states occupy exactly two modes.

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/Foundation/BornRuleForcing.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: