Masses Mass Genesis T10 Sourced Channel Emission

Sourced channel emission

The T10 sourced-channel emission module in the framework's MassGenesis library establishes how a ledger, a discrete record of recognition events, can act as the source of a photon channel. The module defines a photon channel as a structure on an eight-tick lattice, where each tick carries a current value. The central construction, postedPhotonChannel, sets this current from the real part of the difference in ledger occupation between consecutive ticks. This is the "sourced" channel: it is not a vacuum channel with zero current, but one whose activity is driven by the settled state of the ledger.

The module proves that this sourced current is not arbitrary. A theorem, channelTickCurrent_eq_commitSettlementWindow, shows that the current at any phase equals a specific settlement window, the commitSettlementWindow. This ties the channel's behavior directly to the ledger's settlement process. A second theorem, channelTickCurrent_eq_originLocalSettlement_at_phase, shows the same current is the amplitude of a local settlement readout, comparing occupation at a tick with the previous tick. Together, these establish that the emitted photon's window is exactly the sampled tick current of its own posted channel, with no free parameters.

The key structural result is about what windows can be emitted. The module defines an EmittedPhotonState carrying only an octave and a phase, and its window is definitionally the sampled current of its channel. A theorem, gapTwo_not_emittedPhotonWindow, proves that no emitted state can have a window equal to the gap-two two-phase mode. This is a direct consequence of the window being tied to the settlement readout, which itself never produces that mode. The proof is a simple contradiction: if such an emitted state existed, its window would equal the gap-two mode, but the settlement window theorem says it cannot.

In plain language, the module shows that if you let a settled ledger drive a photon channel, the resulting emissions are constrained. They cannot be arbitrary; they must reflect the ledger's settlement pattern. And specifically, one particular mode, the gap-two mode, is forbidden. This is a proof that the ledger's structure imposes a real restriction on what can be emitted, not just a definitional choice. The module also confirms the vacuum channel remains zero-current, so the sourced channel is the only one that carries activity.

The practical consequence is that the framework can distinguish between a photon that originates from a settled ledger and one that does not. The sourcedSettlementForcedMaxwellTick definition shows such a sourced emission inhabits the settlement-forced Maxwell tick primitive, meaning it is a legitimate physical state within the framework. This gives a concrete, checkable criterion for what counts as a sourced emission, and rules out a whole class of possible states.

/-- Sampling the posted channel's `J` recovers the difference settlement
window of the carried ledger occupation. -/
theorem channelTickCurrent_eq_commitSettlementWindow
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) :
    channelTickCurrent octave phase = commitSettlementWindow phase := by
  funext t
  simp only [channelTickCurrent, postedPhotonChannel, postedTickCurrent,
    eightTickSimplex]
  have hre := occupationDiff_eq_ofReal_re octave phase t
  have hlaw :=
    congrFun
      (settledLedger_settlement_law octave differenceSettlementReadout phase) t
  simp only [differenceSettlementReadout] at hlaw
  -- hlaw : occ t - occ (t-1) = commitSettlementWindow phase t
  -- goal  : ↑((occ t - occ (t-1)).re) = commitSettlementWindow phase t
  calc
    (↑(ledgerOccupationWindow octave phase t -
          ledgerOccupationWindow octave phase (t - 1)).re : ℂ) =
        ledgerOccupationWindow octave phase t -
          ledgerOccupationWindow octave phase (t - 1) := hre.symm
    _ = commitSettlementWindow phase t := hlaw

/-- Gap-two cannot arise as any emitted-photon window. -/
theorem gapTwo_not_emittedPhotonWindow :
    ¬ ∃ e : EmittedPhotonState, e.window = gapTwoTwoPhaseMode := by
  rintro ⟨e, he⟩
  exact e.window_ne_gapTwo he

theorem sourced_inhabits_settlementForcedMaxwellTick
    (octave : Q3SettledLedgerOctave) :
    PhysicalPhotonWindowIsOriginSettlementReadout
      (sourcedSettlementForcedMaxwellTick octave).photon
      (sourcedSettlementForcedMaxwellTick octave).octave
      (sourcedSettlementForcedMaxwellTick octave).L :=
  originSettlement_of_settlementForcedMaxwellTick
    (sourcedSettlementForcedMaxwellTick octave)

What this page does not claim

The module does not prove that the sourced channel is the only possible source of photon emission. The module does not define what a ledger occupation window is in physical terms. The module does not show that the gap-two mode is impossible in all channels, only in emitted ones.

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