Masses Mass Genesis T10 Sourced Channel Emission Finite Channel Current Native A

The zero-current vacuum channel

The declaration finiteChannelCurrentNativeAmplitude_still_zero proves that the finite photon channel, a discrete record of recognition events on an eight-tick cycle, has zero current at every tick. In plain terms: an unoccupied channel, with no events posted to its ledger, produces no signal amplitude. The proof is a theorem in the framework's machine-checked library of formal theorems, and it confirms that the vacuum channel remains silent.

This zero-current result is a necessity proof about the zero-signal world. It does not forbid a channel that is sourced, meaning one whose current is driven by the difference in ledger occupation between consecutive ticks. The framework separately constructs such a sourced channel, postedPhotonChannel, and proves that its tick current equals the committed settlement window. Sampling that current recovers the local settlement readout image, so the sourced channel carries a definite, nontrivial signal.

The theorem also establishes a boundary on what an emitted photon state can be. An emitted state carries only an octave and a phase, and its window is definitionally the sampled tick current of its own posted channel. The framework proves that this emitted window can never equal the gap-two mode, a specific two-phase pattern. The zero-current vacuum channel and the nontrivial sourced channel are therefore cleanly separated: one is silent, the other emits a definite pattern, and no emitted state can produce the gap-two window.

What the declaration does not claim is equally important. It does not claim that all channels are silent, nor that the sourced channel is forbidden. It does not derive any numerical value for a particle mass or coupling. It establishes a structural fact about the zero-signal world and the boundary of emitted states, within the framework's model of recognition events.

theorem finiteChannelCurrentNativeAmplitude_still_zero :
    finiteChannelCurrentNativeAmplitude = fun _ => 0 :=
  finiteChannelCurrentNativeAmplitude_eq_zero

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

What this page does not claim

The declaration does not claim that all photon channels are silent. The declaration does not derive any numerical value for a particle mass or coupling constant. The declaration does not claim the sourced channel is forbidden or unphysical.

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: