Masses Mass Genesis T10 Source Window Naturality Phase Signed Posting Photon Sou

The source-window wall

The declaration phaseSignedPostingPhotonSource3_exactJ_background is a small but load-bearing theorem in the Recognition Science framework's account of how a photon source connects to a photon window. It states, for each of the eight phases a photon can carry, that the background field of the signed posting source equals the field the source itself carries. In plainer words: the source's own record of its field and the background field that the exact-J operator reads from it are the same object. The proof is a definitional equality, which means it holds by construction rather than by a chain of derived facts.

This equality matters because it sits inside a larger wall of negative results. The framework models a photon source as a signed posting on a finite torus of 27 sites, while a photon window is an eight-tick complex chord. Those two domains have different cardinalities, 27 versus 8, so no identity transport exists between them. The theorem no_equiv_torusGreenDomain_photonWindowDomain proves this non-equivalence. The current Maxwell/DEC channel used by the bridge has identically zero current, so it also fails to select a window. The wall concludes that any functional relation extending current physical-window compatibility cannot be a source-window naturality law; any functional signed-source relation that admits the gap-one window must exclude the gap-two window; and a constant gap-one relation is source-blind, so it cannot close the bridge.

What the declaration does not claim is just as important. It does not construct the missing transport map from a signed source to a raw photon window. The first missing physical premise remains a target: a source-dependent functional map that is not source-blind. The framework explicitly states that it does not build this map. The declaration also does not claim that the exact-J background equals the source field for any source other than the phase-bearing posting source defined in this framework. It is a statement about one specific construction, not a general equivalence.

Within the framework, this wall sharpens the boundary of what the mass-genesis chain can currently force. It proves a limitation: the source-to-window link cannot be closed by any functional relation that respects the current physical compatibility notion, because the two candidate windows are both physically compatible but functionally incompatible. The consequence is that the bridge from source to window requires a new physical premise, not a cleverer formal relation. That premise is named as a target, and the wall certifies that the target is real.

theorem phaseSignedPostingPhotonSource3_exactJ_background
    (phase : Fin 8) :
    (phaseSignedPostingPhotonSource3 phase).toExactJ.background =
      (phaseSignedPostingPhotonSource3 phase).field :=
  rfl

/-- There is no type equivalence between the torus Green domain and the
eight-tick photon window domain. A non-equivalence transport remains OPEN;
this only kills identity/domain-equivalence shortcuts. -/
theorem no_equiv_torusGreenDomain_photonWindowDomain :
    IsEmpty (Fin (TorusCard3 3) ≃ Fin 8) := by
  refine ⟨fun e => ?_⟩
  have hcard := Fintype.card_congr e
  rw [Fintype.card_fin, Fintype.card_fin, torusCard3_eq_twentySeven] at hcard
  exact (by decide : ¬(27 = 8)) hcard

/-- **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))

/-- **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_not_sourceWindowNaturalityLaw :
    ¬ ∃ law : SourceWindowNaturalityLaw3,
      law.relation = constantGapOneSignedSourcePhotonWindowRelation3 := by
  rintro ⟨law, hrel⟩
  exact law.not_source_blind
    (hrel ▸ constantGapOne_is_sourceBlind)

What this page does not claim

The declaration does not construct the missing transport map from source to window. The equality holds only for the phase-bearing posting source, not for arbitrary signed sources. The wall does not prove that no source-window link exists, only that no functional one exists under the current compatibility notion.

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: