Masses Mass Genesis T10 Posting Photon Readout Phase01 Same Sign Window Current

The same-sign window

A photon window is a list of eight numbers, one per tick of the recognition cycle, that describes where photon energy may appear. The framework's current physical photon interface accepts any such window that is nontrivial, meaning it is not all zeros, and whose neutralized energy is nonzero. The declaration phase01SameSignWindow_currentPhysicalPhotonWindowCompatible proves that a particular window, one with ones in the first two positions and zeros elsewhere, meets that test.

That window is called the same-sign window because its first two entries share the same sign. The proof is a direct calculation: the window is nontrivial, and the neutralized energy works out to a nonzero number. The declaration is a theorem in the machine-checked library of formal theorems, so the result is not a matter of opinion or approximation. It is a fact about the framework's definitions.

What the declaration does not do is connect that window to a specific source. The framework's current compatibility relation is not functional: the same posting source, channel, and zero-cost carrier can produce both the gap-one and gap-two windows, and both pass the test. A separate theorem shows that no selector can recover every compatible window from a source. The same-sign window is one example of why the wall exists: it is compatible, but it does not force phase-zero or phase-one support in a raw photon readout.

The missing piece is a target-blind source-window naturality, a relation derived from the signed posting source that selects a unique raw photon window. That premise is not defined here, and the declaration does not supply it. The same-sign window simply demonstrates the current interface's breadth, not its power to pin down a readout.

theorem phase01SameSignWindow_currentPhysicalPhotonWindowCompatible :
    CurrentPhysicalPhotonWindowCompatible phase01SameSignWindow := by
  constructor
  · exact ⟨0, by simp [phase01SameSignWindow]⟩
  · simp [normSq8, neutralize, LightLanguage.Meaning.balanceOp,
      phase01SameSignWindow, Fin.sum_univ_eight, Complex.normSq_apply]
    norm_num

/-- **First readout wall.** Current posting/photon compatibility is not
functional: the same actual posting source, Maxwell/DEC channel, and zero-J
carrier admit the distinct gap-one and gap-two windows. -/
theorem currentPostingPhotonCompatibility_not_functional :
    ¬ IsFunctionalPostingPhotonRelation3
      CurrentPostingPhotonCompatibility3 := by
  intro hfunctional
  exact gapOneTwoPhaseMode_ne_gapTwoTwoPhaseMode
    (hfunctional
      (canonicalPhasePostingPhotonInput3 0)
      gapOneTwoPhaseMode
      gapTwoTwoPhaseMode
      gapOne_currentPhysicalPhotonWindowCompatible
      gapTwo_currentPhysicalPhotonWindowCompatible)

theorem gapObservations_same_posting_photon_input :
    gapOnePhasePostingPhotonObservation3.input =
      gapTwoPhasePostingPhotonObservation3.input :=
  rfl

theorem gapObservations_distinct_windows :
    gapOnePhasePostingPhotonObservation3.window ≠
      gapTwoPhasePostingPhotonObservation3.window :=
  gapOneTwoPhaseMode_ne_gapTwoTwoPhaseMode

theorem no_selector_recovers_every_currentCompatibleWindow :
    ¬ ∃ selector : PostingPhotonWindowSelector3,
      SelectsEveryCurrentCompatibleWindow3 selector := by
  rintro ⟨selector, hselector⟩
  have hgapOne := hselector
    (canonicalPhasePostingPhotonInput3 0)
    gapOneTwoPhaseMode
    gapOne_currentPhysicalPhotonWindowCompatible
  have hgapTwo := hselector
    (canonicalPhasePostingPhotonInput3 0)
    gapTwoTwoPhaseMode
    gapTwo_currentPhysicalPhotonWindowCompatible
  exact gapOneTwoPhaseMode_ne_gapTwoTwoPhaseMode
    (hgapOne.symm.trans hgapTwo)

What this page does not claim

The declaration does not claim that the same-sign window is the unique compatible window, nor that it is the desired gap-one window. The declaration does not claim that the compatibility test is a functional relation from source to window. The declaration does not claim that the same-sign window is neutral or that it forces raw photon phase support.

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