Encyclopedia Masses Masses Mass Genesis T10 Source Window Naturality

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Source Window Naturality

A machine-checked proof shows why the framework cannot yet derive which of two photon patterns a physical source produces, and names the exact missing step.

Verify this page

The source-window wall

In the Recognition Science account of how particles acquire mass, a recognition event (a discrete record of an interaction) must connect a source, the thing that emits, to a window, the pattern that registers the emission. The framework's library of formal theorems has already reached a detailed model of this connection: a signed source carries a real-valued field on a 27-site torus, and a photon window is an eight-tick complex chord, a pattern across eight steps of the recognition cycle. The library proves these two domains are not equivalent, since 27 and 8 differ. That mismatch is the first sign that no simple identity map can carry a source into a window.

The module goes further and proves a sharper wall. Any functional relation that extends the currently accepted physical window compatibility cannot be a proper source-window naturality law. The proof shows why: the current Maxwell channel used by the bridge has identically zero current, so it cannot select a window. A relation that picks the gap-one window must exclude the gap-two window, because a functional relation assigns at most one window per source. And a relation that always picks the same window regardless of source is source-blind, so it cannot close the bridge either. These are not conjectures; they are proved theorems in the machine-checked library.

The practical consequence is a precise statement of what remains open. The framework has not yet constructed a functional map from a signed source to a single raw photon window. The missing piece is a source-dependent rule that would decide, for a given source, which of two candidate windows it produces. Until that map exists, the mass-genesis chain cannot close its final link. The module does not construct that map; it certifies the wall and names the target.

THEOREM no_equiv_torusGreenDomain_photonWindowDomain · torusCard3_eq_twentySeven · photonWindowDomainCard · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean
no_equiv_torusGreenDomain_photonWindowDomain · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean:109 
/-- 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
torusCard3_eq_twentySeven · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean:97 
/-- The Green carrier domain has twenty-seven sites on the N=3 torus. -/
theorem torusCard3_eq_twentySeven :
    TorusCard3 3 = 27 := by
  unfold TorusCard3 TorusSite3
  rw [Fintype.card_eq_nat_card, Nat.card_fun, Nat.card_zmod, Nat.card_fin]
  norm_num
photonWindowDomainCard · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean:104 
/-- The photon window domain has eight ticks. -/
theorem photonWindowDomainCard :
    Fintype.card (Fin 8) = 8 :=
  Fintype.card_fin 8
THEOREM no_functional_sourceWindowRelation_extends_currentCompatibility · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean
no_functional_sourceWindowRelation_extends_currentCompatibility · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean:209 
/-- **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))
THEOREM sourceWindowNaturality_excludes_gapTwo · functional_sourceWindowRelation_excludes_gapTwo_of_gapOne · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean
sourceWindowNaturality_excludes_gapTwo · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean:267 
theorem sourceWindowNaturality_excludes_gapTwo
    (law : SourceWindowNaturalityLaw3) :
    ¬ law.relation
      (phaseSignedPostingPhotonSource3 0) gapTwoTwoPhaseMode :=
  functional_sourceWindowRelation_excludes_gapTwo_of_gapOne
    law.relation law.functional law.selects_gap_one
functional_sourceWindowRelation_excludes_gapTwo_of_gapOne · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean:182 
/-- **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 · constantGapOne_is_sourceBlind · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean
constantGapOne_not_sourceWindowNaturalityLaw · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean:274 
theorem constantGapOne_not_sourceWindowNaturalityLaw :
    ¬ ∃ law : SourceWindowNaturalityLaw3,
      law.relation = constantGapOneSignedSourcePhotonWindowRelation3 := by
  rintro ⟨law, hrel⟩
  exact law.not_source_blind
    (hrel ▸ constantGapOne_is_sourceBlind)
constantGapOne_is_sourceBlind · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean:172 
theorem constantGapOne_is_sourceBlind :
    IsSourceBlindSignedSourcePhotonWindowRelation3
      constantGapOneSignedSourcePhotonWindowRelation3 :=
  ⟨fun window => window = gapOneTwoPhaseMode, fun _ _ => Iff.rfl⟩
THEOREM finitePhotonChannel_J_zero · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean
finitePhotonChannel_J_zero · IndisputableMonolith/Masses/MassGenesis/T10SourceWindowNaturality.lean:121 
/-- The finite bridge channel used by the current physical-photon constructor
carries the identically zero Maxwell current. -/
theorem finitePhotonChannel_J_zero
    (s : Simplex MaxwellDEC.EightTickLattice.Mesh 1) :
    finitePhotonChannel.J s = 0 :=
  rfl

What this page does not claim

The framework has not constructed the source-to-window map. The module does not prove which window a physical source actually produces. The zero-current result does not rule out a different Maxwell channel.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND