Masses Mass Genesis T10 Field Current Selector Degeneracy Posted Photon Channel

The vanishing potential

The declaration postedPhotonChannelScaled_potential_zero is a theorem in the framework's machine-checked library of formal theorems. It states that in a specific scaled model of a photon channel, the potential A is zero at every point of the underlying mesh. This is not an approximation or a numerical coincidence; it is an exact algebraic identity, proved by direct computation (the proof term is `rfl`, meaning the two sides are definitionally equal).

The consequence is that the field F, which is derived from the potential, also vanishes identically. In plain terms, this scaled channel has no field-side magnitude at all. The only quantities that carry the amplitude a are the current J and the derived window, and each is exactly a times its unit-amplitude value. So the amplitude enters only as a linear factor, never through the field.

This matters because the framework is trying to derive a law that selects a specific amplitude for a posted photon, rejecting a doubled copy. Since the field is zero, any such law must be a predicate on the amplitude alone. The theorem `selector_pin_eq_of_accepts` then shows that a uniquely pinning predicate which accepts the intended witness pins exactly that amplitude, and the constant it names is the inhomogeneity itself. The question of deriving that constant independently is left open.

What the declaration does not claim is any physical content about the electromagnetic field in ordinary spacetime. It is a statement about a formal model, `EmittedPhotonStateScaled`, which is hypothesized structure. The potential being zero is a property of that model, not a measurement or a claim about nature. The framework itself labels the missing derivation of the constant as OPEN.

/-- The scaled sourced channel's potential vanishes at every simplex. -/
theorem postedPhotonChannelScaled_potential_zero
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) (a : ℝ)
    (s : Simplex (postedPhotonChannelScaled octave phase a).mesh 1) :
    (postedPhotonChannelScaled octave phase a).A s = 0 := rfl

/-- The scaled sourced channel's field vanishes at every simplex, at every
amplitude. There is no field-side magnitude for a field-to-current law to
use. -/
theorem postedPhotonChannelScaled_field_zero
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) (a : ℝ)
    (s : Simplex (postedPhotonChannelScaled octave phase a).mesh 2) :
    (postedPhotonChannelScaled octave phase a).F s = 0 := rfl

/-- The scaled channel's current at every simplex is exactly the amplitude
times the unit-amplitude current. -/
theorem postedPhotonChannelScaled_current_smul
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) (a : ℝ)
    (s : Simplex (postedPhotonChannelScaled octave phase a).mesh 1) :
    (postedPhotonChannelScaled octave phase a).J s =
      a * (postedPhotonChannelScaled octave phase 1).J s := by
  simp only [postedPhotonChannelScaled, postedTickCurrentScaled, one_mul]

What this page does not claim

The theorem does not claim that the physical photon has zero potential in spacetime. The theorem does not derive the constant C that would select the intended amplitude. The theorem does not establish that the scaled model is physically realized.

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