tooling(#13564): detect_organ_duplication aveugle aux lakes Lean -- etendre l'index et le scan aux declarations .lean #20210

Constat

L'organe de la regle organ-first, scripts/audit/detect_organ_duplication.py (#16776, ferme), ne regarde aucun lake Lean. Son index scripts/audit/organ_api_index.yaml ne contient aucune entree .lean, et le detecteur ne traite pas les declarations Lean (structure, def, theorem, instance).

Instance mesuree (2026-10-10) : #20111 ajoute dans MyIA.AI.Notebooks/ML/learning_theory_lean/MathUniverse.lean une formalisation de Tegmark R16, Annexe A §1 (« Aut(S) is a group ») : FinRelStruct, Preserves, aut. Le lake MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/ porte deja la meme semantique (MUH/Structure.lean : RelSig, Rel, Structure ; MUH/Aut.lean : StructureOn, IsAutomorphism, Aut). Le check-run du detecteur etait vert (« No organ-duplication »), et le dossier de prevalidation comme la review structurelle ne l'ont pas vu non plus. Le coordinateur l'a trouve a la main avant merge (CHANGES_REQUESTED sur #20111).

Ce qui est demande

Etendre l'organe existant, sans en creer un second :

1. Index : ajouter a organ_api_index.yaml les declarations publiques des lakes Lean du depot (nom de lake, module, noms declares), produites par un script plutot qu'a la main.
2. Scan de diff : dans un diff, extraire les structure / def / theorem / instance ajoutees dans un *.lean (hors _en.lean, jumeau i18n du meme module) et les comparer a l'index des AUTRES lakes.
3. Signal : la collision de noms exacte ne suffira pas ici, puisque les noms different (FinRelStruct contre StructureOn). Un second signal, peu couteux, est la source citee en docstring (meme article et meme section, par exemple R16 Annexe A) dans deux lakes differents. A mesurer avant de le rendre bloquant.
4. Exemption declaree : reutiliser la phrase « copie pedagogique declaree, motif : ... » deja reconnue.

Controles

• Controle positif : la tete 4a468093a8 de feat(lean,#16753): MathUniverse -- annexe A de R16 (structure finie, Aut(S), equivalence decidable) #20111 doit rougir (ou produire un avertissement nomme) contre tegmark_muh_lean.
• Controle negatif : un ajout Lean sans equivalent dans un autre lake reste vert. Les jumeaux _en.lean ne se signalent pas entre eux.
• Mesure du taux de faux positifs sur les 20 dernieres PRs Lean mergees, avant tout passage en bloquant.

See #13564 (regle organ-first), #16776 (organe d'origine), #20111 (instance).