Masses Mass Genesis T10 Source Window Naturality Source Augmented Physical Photo

The missing transport

The declaration sourceAugmentedPhysicalPhotonQ3_does_not_force_rawAnchorSupport is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that even when a physical photon model is augmented with a signed source, the framework does not force that source to support a specific raw anchor phase. In plain terms, the theorem proves that adding source information to the model is not enough to pin down which of the eight ticks of the recognition cycle the photon's anchor occupies.

The proof works by exhibiting a concrete counterexample. The framework builds a model where the source is a phase-signed posting on a 27-point torus, and the photon window is an eight-tick complex chord. The theorem shows that a gap-two window exists in this augmented model that does not support the raw anchor phase. This gap-two model satisfies all the source-augmentation conditions, yet it fails to force the anchor. The existence of this single counterexample is enough to disprove the universal claim that augmentation forces anchor support.

The theorem is part of a larger wall of results in the T10 source-window naturality module. The module proves that the signed Green field domain (27 points) and the photon window domain (8 points) are not equivalent, so no identity transport exists between them. It also shows that the current Maxwell/DEC channel has identically zero current, so the channel does not select a window either. The wall concludes that any functional relation extending current physical-window compatibility cannot be a source-window naturality law, and that a constant gap-one relation is source-blind.

What the theorem does not claim is just as important. It does not claim that no source-augmented model can ever support a raw anchor; it only shows that the framework does not force it. It does not construct the missing transport map from source to window; the module explicitly states that this map remains a target. And it does not claim that the framework's derivation of mass is complete; rather, it identifies the exact missing physical premise that must be supplied before the bridge can close.

/-- **Sharper support wall.** Making the signed Green source and ExactJ
operator explicit still does not force raw phase-zero/one support. -/
theorem sourceAugmentedPhysicalPhotonQ3_does_not_force_rawAnchorSupport :
    ¬ ∀ model : SourceAugmentedPhasePostingPhysicalPhotonQ3Model3,
      RawAnchorPhase01Support model.base.pattern := by
  intro h
  exact gapTwo_worldline_not_rawAnchorPhase01Support
    (h gapTwoSourceAugmentedPhasePostingPhysicalPhotonQ3Model3)

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

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

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

The theorem does not claim that no source-augmented model can support a raw anchor. The theorem does not construct the missing transport map from source to window. The theorem does not claim the framework's mass derivation is complete.

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: