Repository navigation
Preuves Lean de la théorie effective : R02 Props 1-2, R06 Théorème 1, R10 cercle C₇ #16752
Description
Part of #16741 — arc B — ouverte, responsable, prouvable, explicable
Livrable
Formaliser en Lean les énoncés mathématiquement propres du corpus : R02 Props 1-2 (loss nulle ⟹ parallélogrammes ; decoder injectif ⟹ formation) + lois de conservation C=ΣEk, Z₀ ; R06 Théorème 1 (injectivité ⟹ clustering par classe, preuve constructive par contradiction) + dC/dt=0 (App C, preuve calculatoire type Mathlib) + b=log2(n!/|Aut(G)|) (groupes d'automorphismes) ; R10 cercle des jours = représentation irréductible 2D de C₇ (Annexe C : réductibilité ⟺ décomposition en produit tensoriel) — « le LLM a ré-appris la théorie des représentations ».
Contenu à distiller
- R02 Props 1-2 + conservation C = Σ Ek et Z₀ (App C/D/F).
- R06 Th 1 (injectivité ⟹ clustering, par contradiction) + dC/dt = 0 (preuve calculatoire).
- b = log2(n!/|Aut(G)|) sur des groupes d'automorphismes concrets.
- R10 Annexe C : le cercle des jours comme représentation irréductible 2D de C₇.
Sources
- R02 — Towards Understanding Grokking — An Effective Theory of Representation Learning (arXiv:2205.10343)
PDF :G:\Mon Drive\MyIA\IA\Bibliographie IA\MachineLearning\2022 - Liu et al - Towards Understanding Grokking - An Effective Theory of Representation Learning.pdf(sha888CE88DB) - R06 — GenEFT — Understanding Statics and Dynamics of Model Generalization via Effective Theory (arXiv:2402.05916)
PDF :G:\Mon Drive\MyIA\IA\Bibliographie IA\MachineLearning\2024 - Baek Liu Tegmark - GenEFT - Understanding Statics and Dynamics of Model Generalization via Effective Theory.pdf(sha8B589C4EF) - R10 — Not All Language Model Features Are One-Dimensionally Linear (arXiv:2405.14860)
PDF :G:\Mon Drive\MyIA\IA\Bibliographie IA\XAI\2024 - Engels et al - Not All Language Model Features Are One-Dimensionally Linear.pdf(sha87DEAC929)
Localisation papier : R02 App C-D-F · R06 App C + Th 1 · R10 App C — [DISTILL R02-4, R06-3, R10-3]
Cible (vérifiée contre le dépôt)
Nouveau lake ou extension formal_groups/galois (21 lakes existants — choix à l'implémentation).
Priorité et contraintes
P2 — Énoncés courts, preuves constructives — le terrain Lean le plus propre du corpus. Sibling FR/EN si audience externe (#4980).
Activity
jsboige commentedon Sep 18, 2026
[CLAIMED] Grain: DEEP/lean -- lane myia-po-2026:CoursIA -- 2026-09-18T23:56Z -- preflight fait : FREE (aucun claim concurrent), 0 PR ouverte sur 16752/16741-sujet, cible vérifiée (21 lakes au dépôt, extension
ML/learning_theory_leanretenue — fit R02/R06 learning theory, pas de lake formal_groups dédié). paths: MyIA.AI.Notebooks/ML/learning_theory_lean/** — sources PDF R02/R06/R10 (sha8 88CE88DB / B589C4EF / 7DEAC929) lues firsthand avant énoncé.jsboige commentedon Sep 19, 2026
Delivered in PR #16794 —
lake build EffectiveTheorySUCCESS (8711 jobs), 0 sorry. R02 Props 1-2 + conservation identities (App F), R06 Th 1 + conserved hyperbola + infoBits anchors (trivial, order-2), R10 circle of days (representation + irreducibility). Residual for the issue: C₇ numeric anchorlog₂(5040/6)awaitingAut (ZMod p) ≃ (ZMod p)ˣ(documented in InfoBits.lean docstring). — lane myia-po-2026:CoursIAfeat(lean,#16752): InfoBits C7 anchor — infoBits_cyclicSeven
jsboige commentedon Sep 19, 2026
Résiduel C₇ livré dans #16794 (head
8dd0d8ff5) :infoBits_cyclicSeven—|Aut C₇| = φ(7) = 6viaIsCyclic.card_mulAut(voie canonique Mathlib, la carte expliciteAut (ZMod p) ≃ (ZMod p)ˣn'était pas nécessaire),b = log₂(7!/6) = log₂ 840.lake buildSUCCESS re-vérifié, 0 sorry. Reste ouvert sur cette issue : conservation R02 C=ΣEk le long du flot (règle de chaîne au-delà des cœurs Eq. 26-27 déjà livrés). — lane myia-po-2026:CoursIAfeat(lean,#16752): Grokking Flow section — R02 App F chain rule tranc…
jsboige commentedon Sep 19, 2026
[DELIVERED] Tranche 1 (R02) — PR #16905 (head
f44ca5a32).Lake
GrokkingdansMyIA.AI.Notebooks/ML/learning_theory_lean/:Effective(.lean/_en.lean): Déf. 1 parallélogrammes,prop1_zeroLoss,prop2_injectiveDecoder,permissible(P₀)Conservation(.lean/_en.lean):loss0_translate/loss0_smul/Z0_smul,Z0_conserved,C_conserved_l0,deriv_C_along_eff(terme résidueldC/dt = (2ℓ₀/Z₀²)·Comis par l'Appendice F du papier),meanZero_invariantPreuves :
lake buildSUCCESS 8712 jobs (v4.33.0 / mathlib db584cd6d), 0 sorry,#print axioms= propext/Classical.choice/Quot.sound uniquement, siblings i18n 2/2 byte-identical.R02 complet ; R06/R10 restent (tranches suivantes) — la PR porte
See #16752.jsboige commentedon Sep 19, 2026
[DELIVERED] Tranche 2 (R10) — PR #16910 (head
32a3363ba).Module
DaysCircle(.lean/_en.lean)dansMyIA.AI.Notebooks/ML/learning_theory_lean/(pair i18n #4980, lakefile + README du lake mis à jour) :zeta_primitive/zeta_pow_seven— exp(2πi/7) racine primitive 7e de l'unitéday_distinct/days_on_circle— les 7 jours distincts sur le cercle unitédayRep/dayRep_apply/dayRep_day— action de C₇ = ZMod 7 sur le plan réel ℂ, orbite homogènezeta_smul_eq_real_smul_imp— la rotation n'a aucun vecteur propre réelstable_eq_bot_or_top— irréductibilité (Annexe C) : tout sous-espace réel stable par C₇ est nul ou plein — le cercle des jours est véritablement 2DPreuves :
lake build DaysCircle DaysCircle_enSUCCESS 8708 jobs (v4.33.0 / mathlib db584cd6d), 0 sorry,#print axioms= propext/Classical.choice/Quot.sound uniquement, siblings 1/1 byte-identical.R02 + R10 livrés ; R06 (GenEFT) reste (dernière tranche). Voir #16741 pour l'EPIC.
feat(lean,#16752): EffectiveTheory — preuves R02/R06/R10 (parallélogr…
feat(lean,#16752): Grokking lake - R02 effective theory (Props 1-2 + …
feat(lean,#16752): Grokking lake - R02 effective theory (Props 1-2 + …
refactor(lean,#16752): recadrage — GrokkingLemmas sibling, dissolutio…
merge(lean,#16752): synchronise sur le head remote resynchronise (558…
refactor(lean,#16752): finale — re-dissolution de la lib Grokking ram…
feat(lean,#16752): GrokkingLemmas — delta R02 recadré (conservation C…