Masses Mass Genesis T10 Pair Kernel Sourced Emission Amplitude Transport Wall

The amplitude transport wall

In physics, an amplitude is a number attached to a wave or particle state, and its absolute size often carries physical meaning. In Recognition Science, the framework models reality as a ledger, a discrete record of recognition events, and it tries to derive particle properties from the ledger's structure alone. The question at issue here is whether the ledger and its topology, the arrangement of its connections, can force a unique absolute amplitude for an emitted photon. The T10 pair kernel sourced emission amplitude transport wall answers that question in the negative.

The strongest available lower-level structure is tested. A signed Green equation, a standard tool for solving source problems, is combined with a scaled emission window, and the combined package is shown to be inhabited for every positive magnitude. That is, for any positive number q you choose, the ledger can support an emitted photon with that amplitude. The proof is constructive: the theorem sharedMagnitudeSignedGreenEmissionPackage_all_positive builds the package for any q, and sharedMagnitudeSignedGreenEmissionPackage_accepts_doubling shows it works for q and for 2q at once. A further theorem, exists_sharedMagnitudeSignedGreenEmission_amplitude_ne_factor, exhibits a specific amplitude that differs from the topology factor, and sharedMagnitudeSignedGreenEmission_does_not_force_amplitude states plainly that the package does not force the amplitude to equal that factor.

The affine off-shell action, a separate piece of structure that carries field dynamics, is also scale-blind. The theorems affineWeylEventAction27_mul_const and affineWeylDilationResponse27_mul_const show that rescaling the field by a constant c multiplies the action and the dilation response by c squared. Consequently, affineWeylDilationCritical27_mul_const_iff proves that the stationarity condition, the point where the action is critical, is invariant under any nonzero rescaling. The action can select a balance between shift and clock terms, but it cannot select an absolute field amplitude.

This is a transport wall, not a claim that scale selection is impossible in principle. The missing object is an independently derived, inhomogeneous field-to-current transport whose verdict reads field magnitude and rejects the doubled witness. The certificate structure T10PairKernelSourcedEmissionAmplitudeTransportWallCert packages all these results, and the final theorem t10PairKernelSourcedEmissionAmplitudeTransportWallCert assembles them with no gaps and no new axioms. What this means in plain language: the framework's present lower-level laws carry a chosen scale but do not choose it. The absolute amplitude remains an open target, and the wall tells future work exactly where the missing law must sit.

/-- The package is inhabited at every positive magnitude.  The Green source
equation and sourced-emission construction transport a chosen scale but do not
select it. -/
theorem sharedMagnitudeSignedGreenEmissionPackage_all_positive
    (octave : Q3SettledLedgerOctave) (q : ℝ) (hq : 0 < q) :
    SharedMagnitudeSignedGreenEmissionPackage octave q hq := by
  refine ⟨?_, ?_⟩
  · exact signedPostingSourceAttachment3_realGreen
      (N := 3) (by norm_num) q
      (phaseBearingPostingEvent3 0).1
      (phaseBearingPostingEvent3_is_S8 0)
      (Equiv.refl (Fin 3))
  · exact
      EmittedPhotonStateScaled.window_eq_scaledCommit
        (originEmittedPhotonStateScaled octave q hq)

/-- The same lower-level package holds at a positive magnitude and its doubled
copy. -/
theorem sharedMagnitudeSignedGreenEmissionPackage_accepts_doubling
    (octave : Q3SettledLedgerOctave) (q : ℝ) (hq : 0 < q) :
    SharedMagnitudeSignedGreenEmissionPackage octave q hq ∧
      SharedMagnitudeSignedGreenEmissionPackage octave (2 * q)
        (mul_pos (by norm_num) hq) :=
  ⟨sharedMagnitudeSignedGreenEmissionPackage_all_positive octave q hq,
    sharedMagnitudeSignedGreenEmissionPackage_all_positive
      octave (2 * q) (mul_pos (by norm_num) hq)⟩

/-- Shared Green/source magnitude plus exact scaled emission does not force
the topology-factor amplitude. -/
theorem sharedMagnitudeSignedGreenEmission_does_not_force_amplitude
    (octave : Q3SettledLedgerOctave) :
    ¬ ∀ (a : ℝ) (ha : 0 < a) (ψ : LightPattern (Fin 8)),
      SharedMagnitudeSignedGreenEmissionPackage octave a ha →
        Q3MatterCarrier ψ →
          SettledAnchorWindow a ψ →
            PhotonWindowReadsPatternAnchor
                (originEmittedPhotonStateScaled octave a ha).window ψ →
              a = primitivePositiveStationaryFactorAmplitude ψ := by
  intro hall
  obtain ⟨a, ha, ψ, hpackage, hcarrier, hwin, hread, hne⟩ :=
    exists_sharedMagnitudeSignedGreenEmission_amplitude_ne_factor octave
  exact hne (hall a ha ψ hpackage hcarrier hwin hread)

/-- The full affine action is quadratic in field amplitude at every
dilation. -/
theorem affineWeylEventAction27_mul_const
    (event : RealizedPostingEvent3 3)
    (dilation c : ℝ) (ψ : WeylEventAmplitude27) :
    affineWeylEventAction27 event dilation (fun s => c * ψ s) =
      c ^ 2 * affineWeylEventAction27 event dilation ψ := by
  unfold affineWeylEventAction27
  rw [finiteWeylShiftOccupationCost27_mul_const,
    finiteWeylClockOccupationCost27_mul_const]
  ring

/-- For a nonzero field rescaling, affine-Weyl dilation stationarity is
unchanged.  It can select a shift/clock balance but not absolute field
amplitude. -/
theorem affineWeylDilationCritical27_mul_const_iff
    (event : RealizedPostingEvent3 3)
    (dilation : EventDilationCoord)
    (c : ℝ) (hc : c ≠ 0)
    (ψ : WeylEventAmplitude27) :
    AffineWeylDilationCritical27 event (fun s => c * ψ s) dilation ↔
      AffineWeylDilationCritical27 event ψ dilation := by
  unfold AffineWeylDilationCritical27
  rw [affineWeylDilationResponse27_mul_const]
  exact mul_eq_zero.trans (or_iff_right (pow_ne_zero 2 hc))

What this page does not claim

The module does not prove that no future lower-level law can select scale. The module does not provide the missing field-to-current transport. The module does not claim that the ledger and topology are sufficient to derive all particle properties.

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