Marche 2 escalier iit_lean : carnet IIT-08 Parite-et-Broadcast (theoremes B et C, critique d'Aaronson) #20649

Part of #20414 (escalier iit_lean, marche 2 sur 3) · Part of #16781 (veine 5, moitié formelle)

Marche 2 — le couple qui a mordu IIT : parité et broadcast

Deuxieme carnet pedagogique consommateur du lake iit_lean (SymbolicAI/Lean/iit_lean), prevu par la note de conception (docs/lean/iit-lean-escalier.md §2, inventaire items 11-19). La marche 1 (IIT-07, coupe/decomposabilite, theoreme A) est livree par #20645.

Livrables

1. Carnet IIT-08-Parite-et-Broadcast-Lean.ipynb (serie IIT, kernel lean4-wsl, outputs reels C.2) couvrant :
   • l'outil parite (parity, lemmes 13-16 : allFalse, allTrue, oneHot_zero, const) ;
   • le systeme broadcast-parite (broadcast) ;
   • un oracle executable (enumeration d'orbites) qui mesure la convergence en point fixe ;
   • theoreme B broadcast_integrated (l'objet qui a mordu IIT) et theoreme C broadcast_two_cycle + alias figes iit_lean Phase 1 : proxy relationnel de decomposition par coupe - produit decomposable / broadcast integre (Epic Aaronson veine 5) #18599 (broadcast_trivial_dynamics, product_decomposable rappelle marche 1) ;
   • la lecture : integration maximale, dynamique triviale — la critique d'Aaronson ;
   • 3 exercices C.1 (stubs sans erreur volontaire).
2. IIT/README.md : ligne table 8 + parcours 7->8 + contenu detaille + arbre (aucun total a la main — catalogue hors scope).
3. LEAN_INVENTORY.md : ligne iit_lean, Notebook cable 1->2.

Criteres d'acceptation

• Carnet execute de bout en bout sous lean4-wsl (0 erreur, execution_count reels) ;
• #print axioms des theoremes B et C cites dans le carnet (axiomes standard seuls) ;
• Aucune modification du lake (le carnet consomme, la formalisation ne bouge pas) ;
• Ligne README livree avec le carnet ;
• Nommage conforme a l'arbitrage coordinateur du 14/10 (« IIT-07/08 : pas de suffixe L ») et a la grammaire de la note (noyau -Lean en dernier).

Base : empilee sur la marche 1 (branche feature/20414-iit-escalier, PR #20645) — ordre de merge 1 puis 2.