Masses Mass Genesis T10 Source Window Naturality Functional Source Window Relati

The source-window wall

In the Recognition Science framework, a ledger (a discrete record of events) must connect a source, such as a signed posting that carries a phase, to a window, an eight-tick complex chord that represents a photon. The declaration functional_sourceWindowRelation_excludes_gapTwo_of_gapOne proves a narrow but decisive fact: if a functional relation assigns the gap-one window to a given source, that same relation cannot also assign the gap-two window to that source. A functional relation is one where each source leads to exactly one window, no more and no less. The proof is a theorem in the machine-checked library of formal theorems, so it is not a heuristic or a numerical accident.

The theorem matters because it sharpens a wall in the framework's account of how particle masses arise. The signed Green field of a phase-bearing posting lives on a finite torus with 27 sites, while the physical photon window is an eight-tick chord; the two domains are not equivalent, so no identity transport exists between them. The theorem shows that any functional relation that admits the gap-one window must exclude the gap-two window. A constant relation that always picks gap-one is functional and does select gap-one, but it is source-blind: it ignores the source entirely, so it cannot serve as a naturality law that ties source to window. The framework proves that no functional relation can extend the current physical-window compatibility, because that compatibility already relates the source to both gap-one and gap-two windows, which would violate the single-window requirement.

What the declaration does not claim is just as important. It does not construct the missing map from a signed source to a raw photon window; that map remains an open target. It does not prove that the gap-one window is the physically correct choice for any source, only that a functional relation selecting gap-one must exclude gap-two. It also does not claim that the framework has closed the bridge from recognition to physical photon windows. The theorem is a negative result that names a precise obstruction, not a positive construction of the missing transport.

/-- **Discriminator theorem.** Any functional signed-source relation that
admits the gap-one window on the phase-zero source must exclude the gap-two
window. The exclusion is forced by functionality and the distinct windows,
not by inspecting support after the fact. -/
theorem functional_sourceWindowRelation_excludes_gapTwo_of_gapOne
    (relation : SignedSourcePhotonWindowRelation3)
    (hfunctional : IsFunctionalSignedSourcePhotonWindowRelation3 relation)
    (hgapOne :
      relation (phaseSignedPostingPhotonSource3 0) gapOneTwoPhaseMode) :
    ¬ relation (phaseSignedPostingPhotonSource3 0) gapTwoTwoPhaseMode := by
  intro hgapTwo
  exact gapOneTwoPhaseMode_ne_gapTwoTwoPhaseMode
    (hfunctional
      (phaseSignedPostingPhotonSource3 0)
      gapOneTwoPhaseMode
      gapTwoTwoPhaseMode
      hgapOne
      hgapTwo)

theorem constantGapOne_is_functional :
    IsFunctionalSignedSourcePhotonWindowRelation3
      constantGapOneSignedSourcePhotonWindowRelation3 := by
  intro source left right hleft hright
  exact hleft.trans hright.symm

theorem constantGapOne_is_sourceBlind :
    IsSourceBlindSignedSourcePhotonWindowRelation3
      constantGapOneSignedSourcePhotonWindowRelation3 :=
  ⟨fun window => window = gapOneTwoPhaseMode, fun _ _ => Iff.rfl⟩

/-- **Naturality wall.** No functional signed-source relation can extend the
current physical-window compatibility class: that class already contains both
gap-one and gap-two. -/
theorem no_functional_sourceWindowRelation_extends_currentCompatibility :
    ¬ ∃ relation : SignedSourcePhotonWindowRelation3,
      IsFunctionalSignedSourcePhotonWindowRelation3 relation ∧
        ExtendsCurrentPhysicalWindowCompatibility3 relation := by
  rintro ⟨relation, hfunctional, hextends⟩
  exact gapOneTwoPhaseMode_ne_gapTwoTwoPhaseMode
    (hfunctional
      (phaseSignedPostingPhotonSource3 0)
      gapOneTwoPhaseMode
      gapTwoTwoPhaseMode
      (hextends _ _ gapOne_currentPhysicalPhotonWindowCompatible)
      (hextends _ _ gapTwo_currentPhysicalPhotonWindowCompatible))

What this page does not claim

It does not construct the missing source-to-window map. It does not prove that gap-one is the physically correct window for any source. It does not claim that the framework has closed the bridge from recognition to physical photon windows.

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