Masses Mass Genesis T10 Channel Native Posting Channel Cover Native Amplitude Eq

Channel-derived amplitudes

The declaration channelCoverNativeAmplitude_eq_of_tickPatterns proves a consistency property about a specific way of assigning complex numbers to the eight ticks of a photon channel. A photon channel here is a model of a photon's internal state as a repeating eight-step cycle, and the assignment in question, called the cover-native amplitude, is built purely from the channel's eight-beat cover path, which is the sequence of patterns that the channel cycles through. The theorem states that if two channels have exactly the same tick-by-tick pattern sequence, then their cover-native amplitudes are identical as functions. In plainer terms: the amplitude depends only on the pattern sequence, not on any other hidden channel data.

This property is what makes the amplitude "channel-native" in the framework's sense: it is defined using only the channel's own cover path, with no reference to a separate window field. The theorem is proved in the machine-checked library of formal theorems, and it is a direct consequence of the way the amplitude is defined, since the definition reads off the pattern at each tick and converts it to a complex number. The proof is a simple extensionality argument: two functions are equal if they agree at every input, and the hypothesis supplies exactly that agreement.

What the theorem does not claim is more interesting. It does not say that the cover-native amplitude is sensitive to the channel's current. In fact, a companion theorem proves the opposite: the amplitude is current-blind, meaning two channels with different currents but the same cover patterns get the same amplitudes. The framework also proves that on the present finite bridge channel, the current is identically zero, so the current-native amplitude is also identically zero, and the combined posting amplitude reduces to the cover-native one. The theorem does not establish that this amplitude law is the final or only one; a named residual property, ChannelTickCurrentPostingPrimitive, remains open, asking for an amplitude law that kills zero-current channels yet is nontrivial on some channel with nonzero current.

The practical consequence is that the cover-native amplitude is a well-defined, reproducible object for any channel, but it is not a complete description of the channel's physics. It captures the pattern structure and ignores the current, which means it cannot distinguish channels that share a pattern sequence but differ in current. The framework's own theorems show that no channel-alone selector can recover every current-compatible window, so this limitation is not an accident of this particular definition but a structural feature of what can be derived from channel data alone.

/-- Cover-native amplitudes are determined by the reindexed cover path alone. -/
theorem channelCoverNativeAmplitude_eq_of_tickPatterns
    {pc₁ pc₂ : PhotonChannel}
    (h : ∀ t : Fin 8,
      channelCoverTickPattern pc₁ t = channelCoverTickPattern pc₂ t) :
    channelCoverNativeAmplitude pc₁ = channelCoverNativeAmplitude pc₂ := by
  funext t
  simp only [channelCoverNativeAmplitude, h t]

theorem channelCoverNativeAmplitude_is_currentBlind :
    IsChannelCurrentBlind channelCoverNativeAmplitude := by
  intro pc₁ pc₂ h
  exact channelCoverNativeAmplitude_eq_of_tickPatterns h

/-- **Present-surface current wall.** The finite bridge channel used by every
current physical-photon constructor has identically zero Maxwell current, so
its current-native Fin-8 amplitudes vanish. -/
theorem finiteChannelCurrentNativeAmplitude_eq_zero :
    finiteChannelCurrentNativeAmplitude = fun _ => 0 := by
  funext t
  simp only [finiteChannelCurrentNativeAmplitude, eightTickSimplex,
    finiteChannel_J_eq_zero, Complex.ofReal_zero]

theorem no_channelAlone_selector_recovers_every_currentCompatibleWindow :
    ¬ ∃ selector : ChannelAloneWindowSelector,
      RecoversEveryCurrentCompatibleWindow selector := by
  rintro ⟨selector, hselector⟩
  have hgapOne := hselector gapOneTwoPhaseMode
    gapOne_currentPhysicalPhotonWindowCompatible
  have hgapTwo := hselector gapTwoTwoPhaseMode
    gapTwo_currentPhysicalPhotonWindowCompatible
  exact gapOneTwoPhaseMode_ne_gapTwoTwoPhaseMode (hgapOne.symm.trans hgapTwo)

What this page does not claim

The theorem does not claim that the cover-native amplitude depends on the channel's current. It does not claim that the cover-native amplitude is the unique or final amplitude law for photon channels. It does not claim that any channel with nonzero current has been constructed or that the residual primitive property is inhabited.

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