Masses Mass Genesis T10 Pair Kernel Sourced Emission Amplitude Transport Wall Sh

The amplitude transport wall

The declaration sharedMagnitudeSignedGreenEmission_does_not_force_amplitude is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It proves a negative result: the strongest present combination of lower-level equations, the signed PairKernel Green source equation and the scaled sourced-emission window, cannot determine the absolute value of a posted amplitude. The theorem states that it is not the case that for every positive magnitude a and every light pattern ψ, if the shared-magnitude package holds and the pattern is a matter carrier anchored to that magnitude, then a must equal the primitive positive stationary factor amplitude. In plain words, the equations transport a chosen scale but do not select it.

The proof works by exhibiting a countermodel. The library shows that the shared-magnitude package is inhabited for every positive q, including the doubled copy 2q. It then constructs a specific positive magnitude a and a light pattern ψ such that the package holds, the pattern is a matter carrier, the anchor window reads the pattern, but a is not equal to the primitive factor amplitude. This countermodel is the banked scaled-emission witness, and it remains a countermodel even after the canonical signed Green source at the same magnitude is attached. The theorem also shows that the affine Weyl off-shell action is quadratic in field amplitude, so its dilation stationarity is invariant under every nonzero rescaling of the field. This means the action can select a shift/clock balance but not an absolute field amplitude.

This result is a transport wall, not a claim that no future lower-level law can select scale. The missing physical object is an independently derived, inhomogeneous field-to-current transport whose verdict reads field magnitude and rejects the doubled witness. The theorem does not prove that the doubled witness is physically realized; it proves that the current equations cannot rule it out. It also does not claim that the shared-magnitude package is the final word on mass genesis, only that it is the strongest present join being tested. The theorem is axiom-clean, with no sorry and no new Lean axiom.

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

/-- 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 theorem does not claim that the doubled witness is physically realized. The theorem does not claim that no future lower-level law can select scale. The theorem does not claim that the shared-magnitude package is the final word on mass genesis.

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: