feat(lean,#15520): lake formal_logic_lean (FFL CONSUMER_PINNE) + notebook Lean-3b

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2024:CoursIA — prev: MED/readme #15510

Pilote FFL : verdict CONSUMER_PINNÉ + premier consommateur (Tranche A de l'EPIC #15066)

Closes #15520. Deux jambes, l'une livrée sur l'issue (verdict + mesures), l'autre
ici : les mêmes formules traversent le raisonneur Tweety (exécution) et le noyau
Lean (certification), sur un fragment fini sérialisable à deux atomes.

Livrables

• MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-3b-Formalized-Formal-Logic.ipynb —
  notebook companion Lean-3b (pattern Lean-Nb), kernel python3 : AST Python
  unique sérialisé vers les deux moteurs (to_tweety / to_lean), table de
  vérité par mondes possibles Tweety, contre-modèle calculé, versant certifié
  (build + #print axioms en subprocess WSL), 3 exercices stub C.1 ;
• MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/ — lake dédié
  CONSUMER_PINNÉ (toolchain v4.33.1, Foundation @ 81810b9f) :
  FormalLogic/Bridge.lean porte les mêmes formules comme objets FFL.Formula,
  les 4 lignes de table comme théorèmes d'évaluation (simp [models_iff_val, val] — la sémantique FFL est Prop-valuée : Valuation α := α → Prop, un
  decide y est structurellement impossible), l'exhaustivité des valuations,
  peirce_valid, le contre-modèle or_not_valid, le contrôle négatif
  satisfiable-non-valide, et peirce_provable (versant preuve) ;
• README.md de la série Lean : ligne cours + ligne exercice + entrée d'arbre
  pour le 3b.

Le point sémantique FFL (pourquoi pas decide)

FFL.Propositional.Boolean.Valuation α := α → Prop : la sémantique est
Prop-valuée par design, aucun Decidable ne peut exister sur v ⊧ φ.
Chaque ligne de table est donc un petit théorème prouvé par évaluation
propositionnelle (simp [models_iff_val, val]) — la table de vérité n'est pas
une image, ce sont des preuves vérifiées par le noyau.

Acceptance #15520 → preuves

Critère (protocole EPIC)	Preuve
Clone au pin exact	81810b9f22c49fbb32bd89c1e9737059d83a37e6 (lake-manifest.json du lake)
cache get + lake build	Mathlib oleans 5,7 GiB livrés ; Foundation ne publie pas d'oleans → 877 modules compilés from source, ~20 min, succès
Graphe d'import API minimale	fermeture Propositional/ = 17 modules (mesuré, fil #15520)
Compat toolchain CoursIA	v4.33.1 = Mathlib v4.33.1 exact (rev 0df444a360ea) — zéro adaptation
Audit licence/sorry/axiomes/maintenance	Apache-2.0 ; distinct_code_sorry Bridge = 0 ; #print axioms ci-dessous ; dernier commit upstream au pin 2026-09-10 (PR #921), push 2026-09-11, 33 issues ouvertes
Verdict	CONSUMER_PINNÉ — consommation par require foundation @ <pin>, zéro vendorising, zéro module adapté, zéro sorry ajouté

Validation

• lake build FormalLogic.Bridge : SUCCESS — ✔ Built FormalLogic.Bridge (214s), 878 jobs (451 s sous charge CI concurrently).
• #print axioms (5 théorèmes) :

  'peirce_valid' depends on axioms: [propext, Classical.choice, Quot.sound]
  'or_not_valid' depends on axioms: [propext, Quot.sound]
  'or_satisfiable' depends on axioms: [propext, Quot.sound]
  'valuations_exhaustive' depends on axioms: [propext, Classical.choice, Quot.sound]
  'peirce_provable' does not depend on any axioms
  

  Zéro sorryAx, zéro native_decide ; Classical.choice vient du by_cases
  de l'exhaustivité ; la dérivation est axiomatiquement vide.
• Papermill end-to-end : SUCCESS — 22/22 cellules, kernel python3, 0 erreur
  (9 cellules code, execution_count 1→9). Sorties clés :
  • double sérialisation depuis l'AST unique :
    phiPeirce tweety: (((p => q) => p) => p) / lean: (((Formula.atom 0 🡒 Formula.atom 1) 🡒 Formula.atom 0) 🡒 Formula.atom 0) ;
  • table Tweety : Peirce 1;1;1;1 → valid=True ; phiOr 1;1;1;0 → valid=False ;
  • contre-modèle calculé par Tweety : ['p=F,q=F'] — le même témoin que
    valFF certifie dans or_not_valid ;
  • cellule build (subprocess WSL) : Build completed successfully (878 jobs). lake build rc=0.
• Verdict SOTA : SOTA-OK — le raisonneur Tweety réel (jar shaded) est
  exécuté via jpype (JDK 17), pas de réimplémentation de substitution ;
  désambiguïsation d'overload JObject(pf, PlFormula) (patron Tweety-2).
• Numérotation Lean-3b conforme à la convention d'accretion (base Lean-3
  sans lettre, b = première accretion, 3b libre au claim).

Anti-régression

• Nouveau lake, aucun fichier Lean existant touché.
• distinct_code_sorry (scripts/lean/count_code_sorry.py) : Bridge.lean = 0.
• B.3 (proof-integrity) : non applicable, mesuré — grep -ln lean-axiom .github/workflows/*.yml liste 11 workflows câblés, aucun pour
  formal_logic_lean (lake neuf). La preuve d'axiomes est portée par
  #print axioms ci-dessus (sortie collée) + la cellule audit du notebook.
  Le câblage CI du lake est un grain de suivi distinct.

Catalogue

Catalogue byte-identique à main — la nouvelle entrée sera créée par le cron
catalog (règle catalog-pr-hygiene), pas à la main sur cette branche.

See #15066 (EPIC, reste ouvert). Fenêtre mémoire CI : issue #15440.

🤖 Generated with Claude Code

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 9
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	11.4s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	14.2s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	15.1s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	15.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	13.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	8.5s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	52.0s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	4.6s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[clusterManager-Myia]

VERDICT: LGTM (vérifié: code Lean intégral lu, manifest croisé vs lakefile, notebook outputs réels, CI verte au head)

[NanoClaw] structural review — PR +1285/8 fichiers : file list + 2 fichiers load-bearing lus intégralement (Bridge.lean 146 l., lakefile) + notebook extrait via protocole.

Vérifié firsthand :

• Bridge.lean lu en entier : 0 sorry, 0 axiom déclaré, 0 native_decide. Math saine : valuations_exhaustive (Fin 2, by_cases + fin_cases + funext) → peirce_valid par exhaustivité des 4 lignes ; contre-modèle or_not_valid sur valFF ; contrôle négatif satisfiable-sans-valide (or_satisfiable / or_not_universally_valid) ; peirce_provable := FFL.Entailment.peirce — citation de l'ancre amont, pas une redémonstration (assumé dans le docstring).
• Cohérence lakefile ↔ lake-manifest : foundation @ 81810b9f pin exact identique des deux côtés ; mathlib v4.33.1 (lakefile) ↔ SHA 0df444a3 (manifest) ; toolchain v4.33.1 aligné. Transitifs axiom-audit/doc-gen4 attendus pour Foundation. CONSUMER_PINNÉ effectif : 0 module FFL vendu/adapté.
• Notebook (22 cellules, 9 code) : exec_count 1-9 séquentiels, outputs réels — build lake « 878 jobs, rc=0 » et audit #print axioms par théorème : peirce_valid/valuations_exhaustive portent [propext, Classical.choice, Quot.sound] (via by_cases) tandis qu'or_not_valid/or_satisfiable sont sans Classical.choice et peirce_provable à 0 axiome — distribution cohérente avec le code lu, croisée Tweety ↔ Lean (φPeirce tautologie 4/4, φOr satisfiable non valide, FF falsifie — identique des deux côtés).
• CI au head b422a2d0 : 8 checks advisory success. 0 secret sur les fichiers texte du diff.

Notes (non bloquantes) :

1. Ancres Tait.soundness/Tait.completeness! citées en docstring sans import du module Tait — documentaires uniquement (aucune utilisation dans le code, assumé) ; à garder en tête si une future tranche s'y appuie réellement.
2. require mathlib explicite redondant (transitif de Foundation) — inoffensif, et il pinne le tag lisible v4.33.1.
3. Cellules « Exercice à compléter » : pédagogie volontaire, outputs non fake (le marqueur est le contenu de la cellule).

— [NanoClaw] (myia-ai-01)

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #15563 (feat(lean,#15520): lake formal_logic_lean (FFL CONSUMER_PINNE) + notebook Lean-3b) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- chore(catalog): scheduled auto-regenerate (long-lived PR) #15358 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md