feat(lean,#15062): FairBot par le théorème de Löb prouvé — FormalLogic.FairBotLoeb (L3)

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #17536

Résumé

Cette PR livre le module consommateur L3 promis par le body de l'EPIC #15062 (« si le pilote passe »). La coopération FairBot × FairBot y est déduite du théorème de Löb arithmétique que FFL prouve (ProvabilityAbstraction.löb_theorem), et non d'un champ postulé. Le résultat est ensuite instancié sur la prouvabilité standard de 𝗣𝗔.

Le module s'ajoute au lake formal_logic_lean (FFL CONSUMER_PINNÉ, #15520 / #15916 / #17017). Elle touche trois fichiers : le nouveau module FormalLogic/FairBotLoeb.lean, son import dans la racine FormalLogic.lean et le README.md du lake. Aucune dépendance n'est modifiée.

Contenu

Section abstraite. Elle vaut pour tout 𝔅 : Provability T₀ T sur une théorie T₀ diagonalisable.

Théorème	Énoncé	Hypothèses
fairBotSelf_spec	T₀ ⊢ FB 🡘 𝔅 FB (point fixe diagonal)	Diagonalization T₀
fairBot_self_cooperation	T ⊢ FB	𝔅.HBL
fairBot_mutual_cooperation	si p 🡘 𝔅 q et q 🡘 𝔅 p, alors T ⊢ p ⋏ q	𝔅.HBL
fairBot_unexploitable	si FairBot coopère, son adversaire coopère	𝔅.Kreisel
fairBot_vs_cooperateBot	FairBot coopère avec CooperateBot	D1 seul
fairBot_vs_defectBot	la coopération face à DefectBot n'est pas prouvable	Consistent T, Kreisel
fairBot_vs_defectBot_defection_unprovable	la défection n'est pas prouvable non plus (Gödel II)	Consistent T, HBL
contrarianBot_independent	la phrase de Gödel (ContrarianBot) est indépendante	Consistent T, Kreisel

Instanciation arithmétique. Elle porte sur T.standardProvability, pour toute théorie [T.Δ₁] [𝗜𝚺₁ ⪯ T], puis sur 𝗣𝗔.

• standard_fairBot_self_cooperation et pa_fairBot_self_cooperation : auto-coopération de FairBot.
• Paire de FairBots de codes distincts. fairBotA et fairBotB sont construits par exclusiveMultifixedpoint. fairBotA_ne_fairBotB établit qu'ils sont distincts, et fairBotA_spec / fairBotB_spec que chacun est le point fixe de la prouvabilité de l'autre. pa_fairBot_pair_cooperation en tire la coopération mutuelle. Cette coopération n'est donc pas réductible à l'auto-référence d'un seul code.
• pa_fairBot_vs_defectBot : ni la coopération ni la défection ne sont prouvables dans 𝗣𝗔.
• pa_fairBot_defects_in_standard_model : la défection est pourtant vraie dans ℕ (SoundOn).

Pourquoi ce module importe

L2 (#16414) a montré qu'une modalité bump vérifie D1–D3 sans vérifier Löb. Ce module rend lisible l'ingrédient qui manquait : le lemme diagonal (Diagonalization), et non une quatrième condition de dérivabilité. La correspondance L2 → L3 est tabulée dans la docstring du module : nec ↔ bew_def/D1, dist ↔ HBL2, posIntros ↔ HBL3, et loeb ↔ löb_theorem, qui est un théorème et non un champ.

Références : Barasz et al. 2014 (arXiv:1401.5577), Critch 2016 (arXiv:1602.04184).

Validation

Compte de sorry. Mesuré avec python scripts/lean/count_code_sorry.py --json sur le lake formal_logic_lean : distinct_code_sorry 0 → 0 (7 fichiers, naive_sorry 0).

Build du lake complet. Il est passé par l'organe scripts/lean/lean_exec.py, en WSL ext4, avec le lakefile.lean et le lake-manifest.json de la branche (sources identiques, diff -r). ModalLogic@71968137 a été cloné par lake.

✔ [1402/1403] Built FormalLogic.ModalBridge (1.1s)
Build completed successfully (1403 jobs).
[lean_exec] ok exit=0 duration=64.8s orphans=0

Le build ciblé lake build FormalLogic.FairBotLoeb compile 1225 jobs, sans aucun warning dans FormalLogic.

Axiomes. La sonde #print axioms a été exécutée sur le build complet (fichier temporaire hors dépôt, non committé).

'FormalLogic.FairBotLoeb.fairBotSelf_spec' depends on axioms: [propext, Quot.sound]
'FormalLogic.FairBotLoeb.fairBot_self_cooperation' depends on axioms: [propext, Classical.choice, Quot.sound]
'FormalLogic.FairBotLoeb.fairBot_mutual_cooperation' depends on axioms: [propext, Classical.choice, Quot.sound]
... (17 déclarations, toutes dans {propext, Classical.choice, Quot.sound})
'FormalLogic.FairBotLoeb.pa_fairBot_defects_in_standard_model' depends on axioms: [propext, Classical.choice, Quot.sound]

La sonde ne trouve ni sorryAx ni native_decide.

B.3 (proof-integrity) : non applicable (a). Aucun workflow n'appelle lean-axiom.yml pour formal_logic_lean : grep -ln 'formal_logic_lean' .github/workflows/*.yml ne rend rien (#8677). La sonde d'axiomes ci-dessus en tient lieu.

README : audit du fichier entier

Le README a été confronté au disque et au manifeste, et trois dérives préexistantes y ont été corrigées :

• la dépendance MyIntelligenceAgency/ModalLogic@71968137 (feat(lean,#15066): pont modal Tweety<->FFL — FormalLogic.ModalBridge (tranche C) #17017) était absente du tableau ;
• le pin cité de LeanTypst était périmé (888d8656, alors que le manifeste porte 2158f3de depuis feat(lean,#15066): pont modal Tweety<->FFL — FormalLogic.ModalBridge (tranche C) #17017). L'absence de licence racine a été re-vérifiée au nouveau pin, ainsi que la licence Apache-2.0 de ModalLogic ;
• la section Structure omettait FolBridge.lean et ModalBridge.lean. Les deux y figurent désormais, avec FairBotLoeb.lean.

Le paragraphe « import arithmétique isolé dans GLBridge » ne l'était plus : il est réécrit. Une mesure datée du nombre de jobs est ajoutée, et les mesures des pilotes sont conservées.

See #15062

🤖 Generated with Claude Code

[jsboige]

Concern: On n'a pas un notebook associé d'exposition?

[clusterManager-Myia]

[NanoClaw] review statique (conteneur ai-01 sans ceinture Lean : zéro rejeu ce tour ; vérification par lecture intégrale des sources, greps, et cohérence des artefacts).

VERDICT: LGTM (vérifié : lecture complète des 3 fichiers au head d326bf649c0867d99d5fd4463d71d0a6f11cdc53, +300/−9)

Ce qui est mesuré et exact

Module FormalLogic/FairBotLoeb.lean (249 lignes lues intégralement).

• Zéro axiome de secours : grep des 249 lignes → sorryAx/native_decide/sorry/admit/axiom/unsafe = 0 occurrence. Uniques hits : 3 noncomputable (fairBotPairBody, fairBotA, fairBotB) — attendu pour des points fixes multiples. Cohérent avec distinct_code_sorry 0 du body.
• Tous les énoncés cités par le body existent au bon endroit : fairBotSelf_spec (l.92, clause diagonale F ↔ 𝔅 F par diag sur la théorie de base), fairBot_self_cooperation (l.97, une application de ProvabilityAbstraction.löb_theorem sur la moitié K_right), fairBot_mutual_cooperation (l.105), fairBot_unexploitable (l.118, 𝔅.KR = Kreisel), fairBot_vs_cooperateBot (l.125, D1 (by simp) = nécessitation), fairBot_vs_defectBot (l.131), fairBot_vs_defectBot_defection_unprovable (l.143, via con_unprovable), contrarianBot_independent (l.154, gödel_independent).
• Preuve de fairBot_mutual_cooperation déroulée à la main : D2 distribue 𝔅(p ⋏ q) → 𝔅p ⋏ 𝔅q, les clauses croisées p ↔ 𝔅q / q ↔ 𝔅p fournissent 𝔅q → p et 𝔅p → q, Löb conclut sur la conjonction. Exactement la dérivation Barasz et al. 2014 annoncée.
• Paire arithmétique : fairBotA/fairBotB par exclusiveMultifixedpoint (fairBotPairBody T) 0/1 (l.185-190), fairBotA_ne_fairBotB (l.195), clauses croisées fairBotA_spec/fairBotB_spec par exclusiveMultidiagonal (l.201-215), puis standard_fairBot_pair_cooperation = fairBot_mutual_cooperation (fairBotA_spec T) (fairBotB_spec T) (l.218-220) — l'assemblage correspond exactement aux hypothèses du théorème abstrait.
• pa_fairBot_defects_in_standard_model (l.239-245) : ¬ (ℕ↓[ℒₒᵣ] ⊧ 𝗣𝗔.standardProvability ⊥) par SoundOn.sound_on + cohérence de 𝗣𝗔 — le commentaire relie correctement à pa_fairBot_vs_defectBot (ni coopération ni défection prouvables, défection vraie dans ℕ). Lecture du second théorème d'incomplétude correcte.
• En-tête : la table L2→L3 (l.19-24) est conforme au body — nec↔bew_def/D1, dist↔HBL2, posIntros↔HBL3, loeb↔löb_theorem (théorème, aucun champ), et le diagnostic « ce qui manque à L2 n'est pas une 4ᵉ condition mais la classe Diagonalization » est cohérent avec le rôle effectif de diag/exclusiveMultidiagonal dans le module.

FormalLogic.lean (+5/−0). Le patch ajoute l'entrée de documentation FormalLogic.FairBotLoeb dans la liste des modules consommateurs et l'import FormalLogic.FairBotLoeb en dernière position — cohérent avec les conventions du fichier (import après le docstring de clôture -/). Rien à redire.

README.md (+46/−9). Les trois dérives annoncées par le body sont réellement corrigées : (1) ModalLogic entre au tableau des pins avec 71968137 et sa justification compat 4.33.1 ; (2) le pin LeanTypst passe de 888d8656 à 2158f3de, avec la cause datée (#17017) ; (3) la structure des modules documente désormais FolBridge et ModalBridge (jusque-là absents). Le chiffre de build « 1403 jobs » du README concorde avec celui du body ; la mention de FairBotLoeb seul à 1225 jobs est cohérente avec le comptage propre. Derive (3) : la phrase d'isolation de l'import arithmétique est réécrite pour couvrir le nouveau module (« l'import arithmétique reste cantonné à deux modules ») — exact au vu des imports L.1-2 du module.

Réserves mineures

• Pas de rejeu. Ni lake build ni #print axioms rejoués depuis ce siège (pas de ceinture Lean dans le conteneur). Les claims « 17 déclarations aux axiomes {propext, Classical.choice, Quot.sound} » et « 0 sorryAx/native_decide » ne sont donc pas re-mesurés ici : les greps statiques confirment l'absence de secours dans les sources, et le build 1403/1225 jobs est cohérent entre body et README — mais la mesure noyau reste celle de l'auteur.
• fairBotA_ne_fairBotB par simp (l.195-196) : je n'ai pas rejoué la tactique. Elle est raisonnable (deux indices distincts de Fin 2 sur une fonction de point fixe), mais c'est le point le plus « magique » du module — à confirmer par le CI qui a la ceinture.
• La disjointure de ce module avec FormalLogic.ModalBridge et GLBridge (imports) se lit sur les patches fournis ; je n'ai pas re-diffé les fichiers antérieurs pour vérifier l'absence de chevauchement de contenu. La note de l'en-tête (« pont GL du même lake : FormalLogic.GLBridge #15923 ») suggère une complémentarité voulue, pas une duplication.
• Question ouverte de l'auteur sur le fil (jsboige, 11:16:28Z) : « On n'a pas un notebook associé d'exposition? » — non tranchée par cette PR ; à la décision de l'auteur, pas un défaut du module.

[jsboige]

Réponse à la question du 2026-09-23 à 11:16Z, « On n'a pas un notebook associé d'exposition ? » : non, pas encore. Aucun notebook de main n'expose la coopération FairBot prouvée par Löb, ni en L2 (#16414) ni avec ce module. Les trois notebooks voisins s'arrêtent avant ce point :

• GameTheory-06e-Open-Source-Game-Theory fait coopérer un FairBot_toy Python en cherchant la chaîne return "C" dans le source de l'adversaire. Il n'y a pas de preuve.
• GameTheory-06g-Bounded-Agents-Lean certifie des agents à budget, et son en-tête exclut explicitement Löb et Gödel.
• Lean-34-Calculabilite-et-Limites audite löb_theorem et annonce FairBot comme la suite, sans le traiter.

Le notebook n'est pas ajouté à cette PR, qui reste un module Lean de trois fichiers. La question est reportée sciemment dans l'issue de suivi #17552, ouverte avant le merge. Sa cible est Lean-34b-FairBot-Loeb.ipynb, une accrétion de Lean-34 : point fixe diagonal, coopération par Löb, paire de codes distincts, DefectBot indépendant mais défection vraie dans ℕ, et pont avec le FairBot_toy de 06e. La lane myia-po-2025:CoursIA la prend en charge et l'empilera sur cette branche en attendant le merge.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 17537
head: d326bf6
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 25ca6d558f0833cf8c377ac804cd243b89b9b70158940bc8aeba577204893e63
diff-files: 3
diff-additions: 300
diff-deletions: 9
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]