Foundation Qrft Gauge Tree Amplitudes Cert Amplitude Pos Off Threshold

The off-threshold positivity theorem

In the Recognition Science framework, the declaration amplitude_pos_off_threshold is a formal theorem about a specific function called the J-cost, which the framework uses to model the cost of a recognition event. The theorem states: for any positive real number r (a coupling ratio), if r is not equal to 1, then the value of the J-cost at r is strictly greater than zero. In plainer terms, it says that the amplitude of a process is positive whenever the system is not exactly at a threshold, and it is zero precisely at the threshold r = 1.

The theorem is a small but load-bearing piece of a larger structural claim about gauge tree amplitudes in the framework. The framework models three canonical processes: Compton scattering (γe⁻ → γe⁻), pair annihilation (e⁺e⁻ → γγ), and W⁺W⁻ → ZZ unitarisation. For each, the amplitude is defined as the J-cost of the relevant coupling ratio. The theorem amplitude_pos_off_threshold is the key positivity property: it guarantees that these amplitudes are positive away from threshold and vanish at threshold, matching the qualitative behavior of leading-order Standard Model results.

This theorem is proved in the machine-checked library of formal theorems, with zero unproved axioms. It is a direct consequence of a more general property of the J-cost function, namely that J-cost is positive for any r not equal to 1. The theorem is a structural certificate: it records a formal guarantee about the shape of the amplitude, not a numerical prediction of its value at any specific energy.

What this theorem does not claim is important. It does not assert that the J-cost model reproduces the exact numerical values of Standard Model amplitudes; that is a separate, broader structural claim that is still open. It does not claim that the amplitudes are physically realized in nature; it only establishes a mathematical property of a model. It does not claim anything about the full derivation of these amplitudes from first principles, which the framework notes requires a continuum limit that is still in progress.

theorem amplitude_pos_off_threshold {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
    0 < processAmplitude r := Jcost_pos_of_ne_one r hr hne

theorem amplitude_zero_at_threshold : processAmplitude 1 = 0 := Jcost_unit0

theorem amplitude_pos_off_threshold {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
    0 < processAmplitude r := Jcost_pos_of_ne_one r hr hne

What this page does not claim

The theorem does not assert that the J-cost model reproduces exact Standard Model amplitude values. The theorem does not claim the modeled amplitudes are physically realized in nature. The theorem does not provide a full derivation of the amplitudes from first principles.

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/Foundation/QRFT/GaugeTreeAmplitudesCert.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: