0.70.3: x86-main passes with the proof ladder never run: a declined advisory section must read NOT_MEASURED, not success #4760

x86-main runs provable-ladder as one of its sections, and ci/sections.yml marks that section
continue-on-error: true (#4433), so the section driver's verdict skips it. A ladder that never ran
cannot turn x86-main red, and nothing reports that it never ran.

Measured (2026-10-04, x86-main jobs of ci.yml over the last 24 h):

• On a runner without the Lean toolchain, the section's precondition step declines (rc 2, "no elan")
  in about 5 s and the job verdict ignores it. In run 37222539899 (fix(ci): the determinism job waits for x86-main instead of holding an ARM64 runner for an hour (T42) #4755) the ladder declined, and the
  only error in the job came from another section. A merge-group run passed x86-main on a runner of
  the same kind.
• All 7 completed x86-main runs that failed also had a failed ladder. Its discharge step failed on
  every runner that reached it, and runners without elan declined before reaching it. No verdict read
  any of this. The 2 runs that passed were not read.
• The comment next to provable-ladder in ci/sections.yml says every runner in that pool has elan.
  The declines above show that comment is stale.

Rule: a skip or a decline is not measured, and it never counts as a pass. An advisory section that
declines or fails on every run measures nothing.

Ask (0.70.3):

1. The x86-main step summary and job outputs report the ladder as PASS, RED or NOT_MEASURED. A decline
   (rc 2) is NOT_MEASURED and is never folded into the job's success.
2. The ladder runs only where the Lean toolchain is present. That means either a runner label that
   provisioning sets when elan is installed, or a separate job that carries that label. x86-main's pool
   does not shrink for this.
3. The discharge failure seen on every runner gets its own row: cause first, then fix.
4. The section moves from advisory to blocking only under the ratchet rule: a measured baseline, then
   three green nights.
5. The stale comment is corrected.

Acceptance:

• A planted decline (no elan) shows NOT_MEASURED in the x86-main summary, with red/green proof.
• scripts/ci/ladder_skip_is_red.sh still goes RED on a skipped ladder.
• Two review lanes PASS.

Not in 0.70.2: a proposal to add a runner label to x86-main's runs-on was dropped. The ladder is
advisory, so that change fixes no red, and it would only shrink the pool.

Owner aprender-a7k. Refs #4678, #4433.