Verify YM C263 massless relative-tail soft-mode firewall

[stevemoraco]

Public guarded replay for the finite scalar source from RH-Lean C263.

The source proves only the massless soft-mode firewall: if 1/lam is split into a uniformly bounded finite-scale part and a complementary tail, sufficiently soft modes force that tail to carry arbitrarily close to the full Green weight. This blocks a naive uniform strict relative-tail argument without an additional soft-mode zero.

Failed-first chronology

• run/job 32213025438 / 95949262067: parser failure from the reserved Greek lambda token; non-evidence.
• run/job 32213081789 / 95949418683: two core declarations compiled, optional third reformulation failed and produced sorryAx; strict linter also caught dead/unused proof material; non-evidence.

The source was reduced to the two load-bearing declarations without weakening them.

Clean guarded replay

head:            5eefcee9d022e78642d839d06a23af4f399cf94f
run/job:         32213182980 / 95949698317
checker:         AXLE Lean 4.30.0
source SHA-256:  d3ef84b547379b583ccbed5d063a034c7e969c456fb4937a18d57e5b8df7a7ea
okay:            true
cached_response: true
failed decls:    []
errors/warnings: none
axiom union:     {propext, Classical.choice, Quot.sound}
artifact:        9351442886
artifact digest: sha256:40c4401ef146c7d07d58781cea83ec009b7bb85209a7dba5cd74f658083df515

Cached status is explicitly disclosed.

It does not formalize finite-range decomposition, BKAR, Yang–Mills, OS reconstruction, a mass gap, or a Clay theorem.

FIVE-ALARM OFF.