diff --git a/.github/workflows/lean-axiom.yml b/.github/workflows/lean-axiom.yml
index aa9d7169b2..c3ce1e4e2d 100644
--- a/.github/workflows/lean-axiom.yml
+++ b/.github/workflows/lean-axiom.yml
@@ -79,6 +79,24 @@ jobs:
   axiom-check:
     name: "Proof integrity (${{ inputs.display-name }})"
     runs-on: ubuntu-latest
+    # BACKSTOP DE LIBERATION DE RUNNER -- PAS UN SEUIL DE SANTE (#15698).
+    #
+    # Sans borne, un `lake exe env lean` ou un `LeanVerifier.check_axioms`
+    # enlise retient le runner les 6 h du defaut GH Actions et le check ne
+    # conclut jamais -- le PR gate reste BLOCKED sur un verdict qui n'atterrit
+    # pas. La borne convertit l'enlisement en check ROUGE, que le merge-gate
+    # peut voir.
+    #
+    # 300 et pas 60. Maximum LEGITIME mesure de `proof-integrity` = 177 min,
+    # conclusion `success` (job 102677021168, step `lean-axiom` de 2 h 55) ;
+    # 1 succes sur 20 depasse 60 min, mediane 8 min (30 runs, 2026-09-12). La
+    # fenetre de 12 runs qui justifiait « 60 = 2x le pire observe » ratait la
+    # queue de distribution : le pire observe n'etait pas le pire legitime.
+    #
+    # NE PAS RESSERRER sur l'intuition : le maximum legitime et la pathologie
+    # vivent dans la meme plage de temps de mur. 300 laisse 1,7x de marge et
+    # rend le runner 3 h avant le defaut GH.
+    timeout-minutes: 300
     steps:
     - uses: actions/checkout@v4
 
diff --git a/.github/workflows/lean-build.yml b/.github/workflows/lean-build.yml
index 3a9c79283f..95b544cddb 100644
--- a/.github/workflows/lean-build.yml
+++ b/.github/workflows/lean-build.yml
@@ -70,6 +70,25 @@ jobs:
   ci:
     name: "Lean CI (${{ inputs.display-name }})"
     runs-on: ubuntu-latest
+    # BACKSTOP DE LIBERATION DE RUNNER -- PAS UN SEUIL DE SANTE (#15698).
+    #
+    # Sans borne, un process Lean enlise retient le runner les 6 h du defaut GH
+    # Actions et le check ne conclut jamais : la PR reste BLOCKED sur un verdict
+    # qui n'atterrit pas. La borne convertit l'enlisement en check ROUGE, que le
+    # merge-gate peut voir.
+    #
+    # 300 et pas 60. Mesure sur 30 runs de `lean-knot.yml` (2026-09-12, durees
+    # calculees depuis started_at/completed_at) : le job `ci` a un maximum
+    # LEGITIME -- conclusion `success` -- de 215 min, et 3 succes depassent
+    # 60 min. La mediane a 7 min est ce qui rend le piege : sur presque tous
+    # les runs, 60 parait genereux. C'est le cache Mathlib froid qui produit la
+    # queue, et il ne se voit pas dans une fenetre de douze runs.
+    #
+    # NE PAS RESSERRER sur l'intuition. Le maximum legitime (215 min) et la
+    # pathologie visee vivent dans la MEME plage de temps de mur : aucun seuil
+    # ne les separe. Cette valeur libere le runner 3 h avant le defaut GH ;
+    # elle ne detecte rien. Resserrer a 60 tuerait 3 succes mesures.
+    timeout-minutes: 300
     steps:
     - uses: actions/checkout@v4
 
diff --git a/.github/workflows/lean-knot.yml b/.github/workflows/lean-knot.yml
index 8475ecd6ef..7a37f4d5f5 100644
--- a/.github/workflows/lean-knot.yml
+++ b/.github/workflows/lean-knot.yml
@@ -142,6 +142,17 @@ jobs:
     name: "Lean CI (knot_lean)"
     runs-on: [self-hosted, coursia-ephemeral, coursia-lean]
     if: github.event.pull_request.head.repo.full_name == null || github.event.pull_request.head.repo.full_name == github.repository
+    # BACKSTOP DE LIBERATION DE RUNNER -- PAS UN SEUIL DE SANTE (#15698).
+    #
+    # L'enlisement d'origine (knot_lean proof-integrity, run 103451688746) a
+    # retenu la moitie du pool coursia-lean 3 h 17 sans jamais conclure. La
+    # borne convertit l'enlisement en check ROUGE, visible du merge-gate.
+    #
+    # 300 et pas 60 : maximum LEGITIME mesure du job `ci` = 215 min (succes),
+    # 3 succes au-dessus de 60 min sur 23, mediane 7 min (30 runs, 2026-09-12).
+    # Le maximum legitime et la pathologie vivent dans la meme plage : aucun
+    # seuil de temps de mur ne les separe. NE PAS RESSERRER.
+    timeout-minutes: 300
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/actions/lean-build
@@ -184,6 +195,18 @@ jobs:
     needs: ci
     runs-on: [self-hosted, coursia-ephemeral, coursia-lean]
     if: github.event.pull_request.head.repo.full_name == null || github.event.pull_request.head.repo.full_name == github.repository
+    # BACKSTOP DE LIBERATION DE RUNNER -- PAS UN SEUIL DE SANTE (#15698).
+    #
+    # C'est CE job qui s'est enlise 3 h 17 dans l'incident d'origine. La borne
+    # convertit l'enlisement en check ROUGE, sur lequel le merge-gate peut agir.
+    #
+    # 300 et pas 60 : maximum LEGITIME mesure de `proof-integrity` = 177 min,
+    # conclusion `success` (job 102677021168, branche
+    # feature/2874-conway-trivial-alexander, step `lean-axiom` 22:58:13Z ->
+    # 01:53:13Z = 2 h 55). Un `timeout-minutes: 60` l'aurait TUE -- exactement
+    # le faux positif que ce fichier cherche a eviter. Mediane 8 min sur
+    # 20 succes : la queue vient du cache Mathlib froid. NE PAS RESSERRER.
+    timeout-minutes: 300
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/actions/lean-axiom
@@ -227,6 +250,10 @@ jobs:
     # Retour arriere = remettre `runs-on: ubuntu-latest` + retrait de l'allowlist.
     runs-on: [self-hosted, coursia-ephemeral, coursia-linux]
     if: (github.event.pull_request.head.repo.full_name == null || github.event.pull_request.head.repo.full_name == github.repository) && always()
+    # Bound at 30 minutes (See #15698): this is a lightweight Python scan,
+    # not a Lean build -- a wedge here is much cheaper than on `ci`/`proof-
+    # integrity`, but still must not pin a runner forever.
+    timeout-minutes: 30
     steps:
       - uses: actions/checkout@v4
       - uses: actions/setup-python@v5
diff --git a/.github/workflows/lean-planning.yml b/.github/workflows/lean-planning.yml
index 4c53a80b2f..446d71b0c8 100644
--- a/.github/workflows/lean-planning.yml
+++ b/.github/workflows/lean-planning.yml
@@ -103,6 +103,10 @@ jobs:
     name: planning target-coverage
     runs-on: ubuntu-latest
     if: always()
+    # Bound at 30 minutes (See #15698): lightweight Python scan, not a Lean
+    # build -- a wedge here is much cheaper than on `ci`/`proof-integrity`,
+    # but still must not pin a runner forever.
+    timeout-minutes: 30
     steps:
       - uses: actions/checkout@v4
       - uses: actions/setup-python@v5
diff --git a/.github/workflows/lean-social-choice.yml b/.github/workflows/lean-social-choice.yml
index 7a39f043db..7ba7f4d4ac 100644
--- a/.github/workflows/lean-social-choice.yml
+++ b/.github/workflows/lean-social-choice.yml
@@ -72,6 +72,10 @@ jobs:
     # Retour arriere = remettre `runs-on: ubuntu-latest` + retrait de l'allowlist.
     runs-on: [self-hosted, coursia-ephemeral, coursia-linux]
     if: github.event.pull_request.head.repo.full_name == null || github.event.pull_request.head.repo.full_name == github.repository
+    # Bound at 30 minutes (See #15698): this is a cheap text-level grep gate,
+    # not a Lean build -- a wedge here is much cheaper than on `build`/`proof-
+    # integrity`, but still must not pin a runner forever.
+    timeout-minutes: 30
 
     steps:
     - uses: actions/checkout@v4
@@ -147,6 +151,11 @@ jobs:
   build:
     name: "Lake build"
     runs-on: ubuntu-latest
+    # Bound at 60 minutes (See #15698): a full Lake build on game_theory_lean
+    # (Mathlib + SocialChoice modules) routinely takes 20-30 minutes; a wedge
+    # here must not pin a runner forever. The bound converts a wedge into a
+    # red check that the merge-gate can act on.
+    timeout-minutes: 60
     # Serialized behind the CHEAP text-level gate (fail fast before spending a
     # Mathlib build). proof-integrity now depends on THIS job (c.327) so the two
     # full compiles run in series instead of in parallel.