From 00ebc262ba652340c9066e38416202fa40a33cd9 Mon Sep 17 00:00:00 2001 From: "Claude Haiku 4.5 (1M context)" Date: Fri, 9 Oct 2026 16:51:08 +0200 Subject: [PATCH] fix(notebook,#17357): Lean-03b -- l'attente d'axiomes alignee sur la sortie (F1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Audit c.5857761593 (Hermes), 1 constat stale-claim reverifie sur main avant fix. F1 (cells 76c9a712 + 71b83b9f) : la prose annoncait « aucun `sorry`, aucune declaration non constructive importee en contrebande », alors que la sortie committee sous les yeux de l'apprenant liste [propext, Classical.choice, Quot.sound] pour `peirce_valid` ET `valuations_exhaustive`. Aucune cellule ulterieure ne reconciliait l'ecart. Cause racine (verifiee dans formal_logic_lean/FormalLogic/Bridge.lean) : `Valuation` est Prop-valuee (`α → Prop`, l.47) ; `valuations_exhaustive` decide `v 0 : Prop` par `by_cases` (l.64) -> `Classical.propDecidable` -> `Classical.choice` ; `peirce_valid` l'herite par `rcases valuations_exhaustive v` (l.97). C'est structurel au pont, pas une contrebande accidentelle : le fix est une reecriture de l'ATTENTE, pas de la preuve. - 76c9a712 : l'attendu reel -- aucun `sorry`, et les axiomes du pont la ou la semantique Prop-valuee les exige (`Classical.choice` en plus de `propext` et `Quot.sound`) ; `peirce_provable`, purement syntaxique, n'en utilise aucun. - 3cda04dd : ajout de la lecture de la liste effectivement imprimee, qui manquait entierement -- les deux regimes (peirce_provable sans axiome ; or_not_valid / or_satisfiable sous les seuls axiomes du noyau ; peirce_valid / valuations_exhaustive sous Classical.choice) sont nommes. Markdown seul : les 9 cellules de code gardent source, execution_count (1..9) et sorties identiques a main -- pas de re-execution due (C.2/C.3). Organes : check_split_reading_cells clean ; notebook_lint 1/1 ; ratchet output_failure_text 0 regressed. See #17357 Co-Authored-By: Claude Haiku 4.5 (1M context) --- ...-03b-Formalized-Formal-Logic-Lean-Python.ipynb | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb index c050b0f9c4..49d0f57cbe 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb @@ -534,9 +534,14 @@ "### Le noyau répond : audit des axiomes\n", "\n", "Un théorème Lean ne dit pas seulement *quoi* est prouvé — `#print axioms`\n", - "liste **sur quoi** il repose. Pour des théorèmes d'évaluation sur un fragment\n", - "fini, l'attendu est l'axiome minimal : aucun `sorry`, aucune déclaration\n", - "non constructive importée en contrebande." + "liste **sur quoi** il repose. Sur ce fragment, l'attendu est : **aucun `sorry`**, et **aucun axiome\n", + "au-delà de ceux que la sémantique du pont exige**. La sémantique FFL est\n", + "`Prop`-valuée (`Valuation α := α → Prop`), donc décider `v 0` ou `v 1` passe\n", + "par `Classical.propDecidable` : `valuations_exhaustive` — et `peirce_valid`,\n", + "qui l'appelle — portent `Classical.choice`, en plus de `propext` et\n", + "`Quot.sound`, les axiomes du noyau. Le seul théorème purement syntaxique du\n", + "lot, `peirce_provable`, n'en utilise aucun. La lecture ci-dessous sépare les\n", + "deux régimes." ] }, { @@ -627,7 +632,7 @@ " `or_satisfiable`.\n", "- **Au-delà de l'exécution** : `peirce_provable` donne la *dérivation* (versant\n", " preuve), et `completeness!` (Tait) garantit que table et dérivation ne\n", - " peuvent pas diverger sur ce fragment.\n", + " peuvent pas diverger sur ce fragment.\n- **Le prix en axiomes** : la lecture ci-dessus se fait en deux régimes —\n `peirce_provable` ne dépend d'**aucun** axiome (dérivation purement\n syntaxique), tandis que `or_not_valid` et `or_satisfiable` ne portent que\n `propext` et `Quot.sound`, les axiomes du noyau, et que `peirce_valid`\n comme `valuations_exhaustive` y ajoutent `Classical.choice`. C'est le\n `by_cases` sur `v 0 : Prop` de `valuations_exhaustive` qui le requiert, et\n `peirce_valid` l'hérite par `rcases`. La validité sémantique se paie d'un\n axiome non constructif ; elle ne se paie pas d'un `sorry`.\n", "\n", "**Dette assumée** (même position que\n", "[Tweety-5d](../Tweety/Tweety-05d-Stable-Synthesis-Lean-Python.ipynb)) : Tweety n'est pas\n", @@ -893,4 +898,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +}