diff --git a/MyIA.AI.Notebooks/ML/learning_theory_lean/MathUniverse.lean b/MyIA.AI.Notebooks/ML/learning_theory_lean/MathUniverse.lean new file mode 100644 index 0000000000..0ff4990d56 --- /dev/null +++ b/MyIA.AI.Notebooks/ML/learning_theory_lean/MathUniverse.lean @@ -0,0 +1,344 @@ +import Mathlib + +/-! +# MathUniverse — structures mathématiques finies (Annexe A, R16 Tegmark) + +Formalisation Lean de l'**Annexe A** de R16 — *The Mathematical Universe* +(Tegmark, [arXiv:0704.0646](https://arxiv.org/abs/0704.0646), §A.1-A.2) — +la définition opérationnelle d'une structure mathématique sur laquelle repose +l'hypothèse de l'univers mathématique (MUH) : « une structure mathématique est +un ensemble d'entités abstraites et de relations entre elles ». + +Tranche formalisation de l'arc « ouvert, responsable, prouvable, explicable » +de l'EPIC **#16741** (issue **#16753**). Contenu distillé : + +1. **Définition** (`FinRelStruct`) : entités = un type fini `α` (l'union + `S₁ ∪ … ∪ Sₙ` du papier, ici mono-sortée), et une **signature** `σ : Fin n → ℕ` + donnant l'arité de chacune des `n` relations. Chaque relation est un + prédicat **décidable** sur les uplets d'arité `σ i`. Séparer la signature de + sa réalisation est exactement ce que fait la théorie des modèles — et c'est + ce qui rend l'équivalence de deux définitions de la *même* structure + énonçable sans transport d'arité. Les fonctions non booléennes se codent en + relations par leur graphe — « la relation R(a₁,…,aₙ₋₁) = aₙ holds » + (note 20 du papier). +2. **Aut(S) est un groupe** (`aut`) : les bijections préservant chaque + relation forment un sous-groupe de `Equiv.Perm` — le « easy to see » de + l'Annexe A, exercice idéal selon le papier. Témoin concret : le groupe + d'automorphismes de l'algèbre de Boole à deux éléments est **trivial** + (`aut_bool8_trivial`), ancre déjà utilisée par `EffectiveTheory.InfoBits` + (`b = log₂(n!/|Aut G|)` : 1 bit pour le groupe à deux éléments). +3. **Décidabilité de l'équivalence** (`EquivStruct`, `EquivStruct.decidable`) : + il existe « un simple algorithme haltant » pour décider si deux définitions + de structures finies sont équivalentes — rendu ici comme instance + `Decidable` par énumération exhaustive des fonctions entre types finis + (« l'énumération des tableaux » du papier). `decide` EST l'algorithme. +4. **Exemples** (§A.2 du papier) : le groupe cyclique **C₂** (table + d'addition de Z/2), le groupe cyclique **C₃** (Z/3), et l'**algèbre de + Boole à deux éléments** — les huit relations F, T, ¬, ∧, ∨, ⇒, ⇔, | de + l'équation (A1) — générée par **NAND seul** (équation A2) : les huit + formules de composition du papier (`nand_false`, `nand_true`, `nand_not`, + `nand_and`, `nand_or`, `nand_implies`, `nand_iff`) et la confirmation + structurelle par l'algorithme de décision lui-même + (`decide` sur `EquivStruct bool8 nand8`). + +Source PDF (GDrive, sha8) : R16 `85712871` +(`G:\Mon Drive\MyIA\IA\Bibliographie IA\Consciousness\ +2007 - Tegmark - The Mathematical Universe.pdf`). + +Frère de `Perceptron` (Novikoff), `PacLearning` (Valiant), `GradientFlow` +(vanishing/survie résiduelle) et `EffectiveTheory` (arc B, #16752) dans le +lake généraliste ML. Twin anglais `MathUniverse_en` (#4980). +-/ + +namespace MathUniverse + +variable {α : Type*} {β : Type*} [Fintype α] [Fintype β] {n : ℕ} {σ : Fin n → ℕ} + +/-! ## 1. La définition (Annexe A.1) -/ + +/-- Une **structure relationnelle finie** de signature `σ` : un type porteur +`α` fini (les entités — l'union `S₁ ∪ … ∪ Sₙ` du papier, ici mono-sortée), et +pour chaque `i : Fin n` une relation d'arité `σ i` — un prédicat sur les +uplets d'éléments. La décidabilité exigée par le champ `rel_dec` est celle que +réclame le §A.2 du papier : « all these functions must be computable » — une +structure finie se spécifie par ses tableaux, et un tableau fini se parcourt +entièrement. -/ +structure FinRelStruct (α : Type*) [Fintype α] {n : ℕ} (σ : Fin n → ℕ) where + /- chaque relation : prédicat sur les uplets d'arité `σ i` -/ + rel : (i : Fin n) → ((Fin (σ i) → α) → Prop) + /- la relation est décidable : le tableau est effectivement donnable -/ + rel_dec : (i : Fin n) → (t : Fin (σ i) → α) → Decidable (rel i t) + +/-! ## 2. Aut(S) est un groupe -/ + +/-- Une application préserve la structure quand chaque relation est +invariante par relabellisation de ses uplets. Pour une bijection, préserver +« à l'aller » suffit : l'iff est alors automatiquement symétrique. -/ +def Preserves (S : FinRelStruct α σ) (f : α → α) : Prop := + ∀ i (t : Fin (σ i) → α), S.rel i t ↔ S.rel i (f ∘ t) + +/-- **Aut(S)**, le groupe d'automorphismes de la structure : les bijections +préservant chaque relation. C'est un sous-groupe de `Equiv.Perm α` — le +« easy to see » de l'Annexe A : l'identité préserve, la composée de deux +préservations préserve, et le symétrique d'une préservation préserve. La +structure de groupe est ensuite celle que Mathlib donne à tout sous-groupe. -/ +def aut (S : FinRelStruct α σ) : Subgroup (Equiv.Perm α) where + carrier := {f | Preserves S f} + one_mem' := by + intro i t + simp + mul_mem' := by + intro f g hf hg i t + rw [Equiv.Perm.coe_mul, Function.comp_assoc] + exact (hg i t).trans (hf i (⇑g ∘ t)) + inv_mem' := by + intro f hf i t + have key : S.rel i (⇑f⁻¹ ∘ t) ↔ S.rel i (⇑(f * f⁻¹) ∘ t) := by + have h := hf i (⇑f⁻¹ ∘ t) + rwa [show ⇑f ∘ (⇑f⁻¹ ∘ t) = ⇑(f * f⁻¹) ∘ t by + simp only [Equiv.Perm.coe_mul, Function.comp_assoc]] at h + rw [mul_inv_cancel, Equiv.Perm.coe_one, Function.id_comp] at key + exact key.symm + +/-- La relation d'appartenance à Aut(S) se déplie en la préservation. -/ +theorem mem_aut_iff (S : FinRelStruct α σ) (f : Equiv.Perm α) : + f ∈ aut S ↔ Preserves S f := Iff.rfl + +/-! ## 3. Décidabilité de l'équivalence (énumération haltante) -/ + +/-- **Équivalence de structures** (même signature `σ`) : il existe une +bijection `f` telle que chaque relation de `S` corresponde exactement à la +relation de même indice de `T` via `f`. C'est l'isomorphisme relationnel — +le papier : « two structure definitions are equivalent if they generate +each other » ; pour des structures finies données par leurs tableaux, +génératrices comprises, l'équivalence passe par cette correspondance. -/ +def EquivStruct (S : FinRelStruct α σ) (T : FinRelStruct β σ) : Prop := + ∃ f : α ≃ β, ∀ i (t : Fin (σ i) → α), S.rel i t ↔ T.rel i (f ∘ t) + +/-- La version déployée sur les fonctions : même énoncé, mais quantifié sur +`α → β` — le type énumérable par excellence (`Fintype.pi`), ce qui porte la +décidabilité. -/ +theorem equivStruct_iff_functions (S : FinRelStruct α σ) (T : FinRelStruct β σ) : + EquivStruct S T ↔ + ∃ f : α → β, Function.Bijective f ∧ + ∀ i (t : Fin (σ i) → α), S.rel i t ↔ T.rel i (f ∘ t) := by + constructor + · rintro ⟨f, hrel⟩ + exact ⟨f, f.bijective, hrel⟩ + · rintro ⟨f, hf, hrel⟩ + exact ⟨Equiv.ofBijective f hf, hrel⟩ + +/-- **L'algorithme haltant de l'Annexe A** : l'équivalence de deux +structures finies est **décidable** — on énumère toutes les applications +`α → β` (tous les tableaux), chacune testée par des prédicats décidables, +et l'énumération d'un produit fini de types finis termine. Rendu comme +instance `Decidable`, `decide` est littéralement l'énumération des +tableaux du papier. + +Les deux `letI` locaux exposent les champs `rel_dec` comme instances : sans +eux, la résolution d'instances ne saurait pas remonter de `Decidable (S.rel i t)` +au champ qui l'atteste. -/ +instance EquivStruct.decidable (S : FinRelStruct α σ) (T : FinRelStruct β σ) + [DecidableEq α] [DecidableEq β] : Decidable (EquivStruct S T) := + letI : ∀ i (t : Fin (σ i) → α), Decidable (S.rel i t) := S.rel_dec + letI : ∀ i (t : Fin (σ i) → β), Decidable (T.rel i t) := T.rel_dec + decidable_of_iff (∃ f : α → β, Function.Bijective f ∧ + ∀ i (t : Fin (σ i) → α), S.rel i t ↔ T.rel i (f ∘ t)) + (equivStruct_iff_functions S T).symm + +/-! ## 4. Exemples (Annexe A.2) -/ + +namespace Examples + +/-! ### L'opérateur de Sheffer `|` (nand) -/ + +/-- NAND sur `Bool` (symbole de Sheffer `|`) — la relation R₈ de l'équation +(A1), et l'unique génératrice de l'équation (A2). -/ +def nand (x y : Bool) : Bool := !(x && y) + +/-! ### C₂ : le groupe cyclique Z/2 -/ + +/-- Signature de `c2` : une relation ternaire. -/ +@[reducible] +def c2Sig : Fin 1 → ℕ := fun _ => 3 + +/-- Le groupe cyclique **C₂** comme structure relationnelle : une seule +relation ternaire, la table d'addition de Z/2 (« generalized multiplication +table », §A.2 du papier) — le graphe de `(x, y) ↦ x XOR y` sur `Bool`, +codé en relation par la note 20 : R(x, y, z) ↔ x + y = z. -/ +def c2 : FinRelStruct Bool c2Sig where + rel := fun _ t => (t 0 ^^ t 1) = t 2 + rel_dec := fun i _ => + match i with + | 0 => inferInstance + +/-! ### C₃ : le groupe cyclique Z/3 -/ + +/-- Signature de `c3` : une relation ternaire. -/ +@[reducible] +def c3Sig : Fin 1 → ℕ := fun _ => 3 + +/-- Le groupe cyclique **C₃** : table d'addition de Z/3 sur `Fin 3` +(l'addition de `Fin n` est déjà modulaire). -/ +def c3 : FinRelStruct (Fin 3) c3Sig where + rel := fun _ t => (t 0 + t 1) = t 2 + rel_dec := fun i _ => + match i with + | 0 => inferInstance + +/-! ### L'algèbre de Boole à deux éléments (équation A1) -/ + +/-- Signature de `bool8` : les arités des huit relations de l'équation +(A1) — deux constantes (arité 1, codant « x = F » et « x = T »), une +fonction unaire (¬) et cinq binaires (∧, ∨, ⇒, ⇔, |). -/ +@[reducible] +def bool8Sig : Fin 8 → ℕ + | 0 => 1 + | 1 => 1 + | 2 => 2 + | 3 => 3 + | 4 => 3 + | 5 => 3 + | 6 => 3 + | 7 => 3 + +/-- Les huit relations de l'équation **(A1)** : F, T, ¬, ∧, ∨, ⇒, ⇔, | +(nand), chacune codée par son graphe (note 20). Les constantes F et T sont +des fonctions d'arité nulle, donc des relations unaires « x = F » et +« x = T » ; les opérateurs unaires et binaires deviennent relations d'arité +2 et 3. -/ +def bool8 : FinRelStruct Bool bool8Sig where + rel := fun i t => + match i with + | 0 => t 0 = false -- R₁ = F (constante fausse) + | 1 => t 0 = true -- R₂ = T (constante vraie) + | 2 => (!t 0) = t 1 -- R₃ = ¬ + | 3 => (t 0 && t 1) = t 2 -- R₄ = ∧ + | 4 => (t 0 || t 1) = t 2 -- R₅ = ∨ + | 5 => (!t 0 || t 1) = t 2 -- R₆ = ⇒ + | 6 => (t 0 == t 1) = t 2 -- R₇ = ⇔ + | 7 => nand (t 0) (t 1) = t 2 -- R₈ = | (nand) + rel_dec := fun i _ => + match i with + | 0 => inferInstance + | 1 => inferInstance + | 2 => inferInstance + | 3 => inferInstance + | 4 => inferInstance + | 5 => inferInstance + | 6 => inferInstance + | 7 => inferInstance + +/-- **Le groupe d'automorphismes de l'algèbre de Boole est trivial** : +préserver la relation R₁ (« x = F ») épingle la constante fausse, et une +bijection de `Bool` qui fixe `false` fixe `true`. Ancre concrète déjà +mobilisée par `EffectiveTheory.InfoBits` (`b = log₂(n!/|Aut G|)` : +2!/1 = 2, soit 1 bit). -/ +theorem aut_bool8_trivial (f : Equiv.Perm Bool) (hf : f ∈ aut bool8) : + f = 1 := by + have hnot : Preserves bool8 ⇑f := hf + have h0 : f false = false := by + simpa [bool8] using (hnot 0 (fun _ => false)).mp rfl + have h1 : f true = true := by + obtain ⟨a, ha⟩ := f.surjective true + cases a with + | false => exact absurd (h0 ▸ ha) (by simp) + | true => exact ha + ext x + cases x with + | false => simpa [Equiv.coe_refl] using h0 + | true => simpa [Equiv.coe_refl] using h1 + +/-! ### Générée par NAND seul (équation A2) -/ + +/-- **R₁ = F** par composition de NAND : la formule +`R(R(X, R(X, X)), R(X, R(X, X)))` du papier rend la constante fausse. -/ +theorem nand_false (x : Bool) : + nand (nand x (nand x x)) (nand x (nand x x)) = false := by + cases x <;> decide + +/-- **R₂ = T** : `R(X, R(X, X))` rend la constante vraie. -/ +theorem nand_true (x : Bool) : nand x (nand x x) = true := by + cases x <;> decide + +/-- **R₃ = ¬** : `R(X, X)` rend la négation. -/ +theorem nand_not (x : Bool) : nand x x = !x := by + cases x <;> decide + +/-- **R₄ = ∧** : `R(R(X, Y), R(X, Y))` rend la conjonction. -/ +theorem nand_and (x y : Bool) : + nand (nand x y) (nand x y) = (x && y) := by + cases x <;> cases y <;> decide + +/-- **R₅ = ∨** : `R(R(X, X), R(Y, Y))` rend la disjonction. -/ +theorem nand_or (x y : Bool) : + nand (nand x x) (nand y y) = (x || y) := by + cases x <;> cases y <;> decide + +/-- **R₆ = ⇒** : `R(X, R(Y, Y))` rend l'implication. -/ +theorem nand_implies (x y : Bool) : + nand x (nand y y) = (!x || y) := by + cases x <;> cases y <;> decide + +/-- **R₇ = ⇔** : `R(R(X, Y), R(R(X, X), R(Y, Y)))` rend l'équivalence +(la table `[[1,0],[0,1]]` du papier). -/ +theorem nand_iff (x y : Bool) : + nand (nand x y) (nand (nand x x) (nand y y)) = (x == y) := by + cases x <;> cases y <;> decide + +/-- La structure **(A2)** : la même signature que (A1) — huit relations — +mais chaque table est dorénavant **définie par composition de NAND seul**, +en suivant exactement les formules de l'équation (A2) du papier. Les deux +constantes restent des relations unaires « x = F » et « x = T » — donc +`x = `, et non ` = false` : la formule rend la constante, +elle ne l'affirme pas. -/ +def nand8 : FinRelStruct Bool bool8Sig where + rel := fun i t => + match i with + | 0 => t 0 = nand (nand (t 0) (nand (t 0) (t 0))) (nand (t 0) (nand (t 0) (t 0))) + | 1 => t 0 = nand (t 0) (nand (t 0) (t 0)) + | 2 => nand (t 0) (t 0) = t 1 + | 3 => nand (nand (t 0) (t 1)) (nand (t 0) (t 1)) = t 2 + | 4 => nand (nand (t 0) (t 0)) (nand (t 1) (t 1)) = t 2 + | 5 => nand (t 0) (nand (t 1) (t 1)) = t 2 + | 6 => nand (nand (t 0) (t 1)) (nand (nand (t 0) (t 0)) (nand (t 1) (t 1))) = t 2 + | 7 => nand (t 0) (t 1) = t 2 + rel_dec := fun i _ => + match i with + | 0 => inferInstance + | 1 => inferInstance + | 2 => inferInstance + | 3 => inferInstance + | 4 => inferInstance + | 5 => inferInstance + | 6 => inferInstance + | 7 => inferInstance + +/-- **L'équivalence des définitions (A1) et (A2)** : les huit relations +définies par composition de NAND coïncident exactement avec les huit +relations primitives — l'identité en est le témoin. La preuve est +littéralement le catalogue des formules de composition : chaque lemme +`nand_*` ci-dessus réécrit une ligne de (A2) en la ligne correspondante +de (A1). -/ +theorem equivStruct_bool8_nand8 : EquivStruct bool8 nand8 := by + refine ⟨Equiv.refl Bool, ?_⟩ + intro i t + fin_cases i + · simp [bool8, nand8, Equiv.coe_refl, nand_false] + · simp [bool8, nand8, Equiv.coe_refl, nand_true] + · simp [bool8, nand8, Equiv.coe_refl, nand_not] + · simp [bool8, nand8, Equiv.coe_refl, nand_and] + · simp [bool8, nand8, Equiv.coe_refl, nand_or] + · simp [bool8, nand8, Equiv.coe_refl, nand_implies] + · simp [bool8, nand8, Equiv.coe_refl, nand_iff] + · simp [bool8, nand8, Equiv.coe_refl] + +/-- **L'algorithme haltant confirme le papier** : `decide` — l'énumération +des tableaux de l'Annexe A — retrouve que (A1) et (A2) définissent la même +structure, sans qu'on lui donne le témoin. -/ +example : decide (EquivStruct bool8 nand8) = true := by + decide +kernel + +end Examples + +end MathUniverse diff --git a/MyIA.AI.Notebooks/ML/learning_theory_lean/MathUniverse_en.lean b/MyIA.AI.Notebooks/ML/learning_theory_lean/MathUniverse_en.lean new file mode 100644 index 0000000000..1c315db862 --- /dev/null +++ b/MyIA.AI.Notebooks/ML/learning_theory_lean/MathUniverse_en.lean @@ -0,0 +1,339 @@ +import Mathlib + +/-! +# MathUniverse — finite mathematical structures (Appendix A, R16 Tegmark) + +Lean formalization of **Appendix A** of R16 — *The Mathematical Universe* +(Tegmark, [arXiv:0704.0646](https://arxiv.org/abs/0704.0646), §A.1-A.2) — +the operational definition of a mathematical structure, on which the +Mathematical Universe Hypothesis (MUH) rests: "a mathematical structure is a +set of abstract entities and relations between them". + +Formalization slice of the "open, accountable, provable, explainable" arc of +EPIC **#16741** (issue **#16753**). Distilled content: + +1. **Definition** (`FinRelStruct`): entities = a finite type `α` (the union + `S₁ ∪ … ∪ Sₙ` of the paper, single-sorted here), and a **signature** + `σ : Fin n → ℕ` giving the arity of each of the `n` relations. Every relation + is a **decidable** predicate on tuples of arity `σ i`. Separating the + signature from its realization is exactly what model theory does — and it + is what makes the equivalence of two definitions of the *same* structure + statable without arity transport. Non-Boolean functions are encoded as + relations through their graph — "the relation R(a₁,…,aₙ₋₁) = aₙ holds" + (note 20 of the paper). +2. **Aut(S) is a group** (`aut`): the bijections preserving every relation + form a subgroup of `Equiv.Perm` — the "easy to see" of Appendix A, an + ideal exercise according to the paper. Concrete witness: the automorphism + group of the two-element Boolean algebra is **trivial** + (`aut_bool8_trivial`), an anchor already used by `EffectiveTheory.InfoBits` + (`b = log₂(n!/|Aut G|)`: 1 bit for the two-element group). +3. **Decidability of equivalence** (`EquivStruct`, `EquivStruct.decidable`): + there is "a simple halting algorithm" deciding whether two definitions of + finite structures are equivalent — rendered here as a `Decidable` instance + by exhaustive enumeration of the functions between finite types ("the + enumeration of the tableaus" of the paper). `decide` IS the algorithm. +4. **Examples** (§A.2 of the paper): the cyclic group **C₂** (addition table + of Z/2), the cyclic group **C₃** (Z/3), and the **two-element Boolean + algebra** — the eight relations F, T, ¬, ∧, ∨, ⇒, ⇔, | of equation (A1) — + generated by **NAND alone** (equation A2): the eight composition formulas + of the paper (`nand_false`, `nand_true`, `nand_not`, `nand_and`, `nand_or`, + `nand_implies`, `nand_iff`) and the structural confirmation by the decision + algorithm itself (`decide` on `EquivStruct bool8 nand8`). + +Source PDF (GDrive, sha8): R16 `85712871` +(`G:\Mon Drive\MyIA\IA\Bibliographie IA\Consciousness\ +2007 - Tegmark - The Mathematical Universe.pdf`). + +Sibling of `Perceptron` (Novikoff), `PacLearning` (Valiant), `GradientFlow` +(vanishing/residual survival) and `EffectiveTheory` (arc B, #16752) in the +generalist ML lake. English twin `MathUniverse_en` (#4980). +-/ + +namespace MathUniverse_en + +variable {α : Type*} {β : Type*} [Fintype α] [Fintype β] {n : ℕ} {σ : Fin n → ℕ} + +/-! ## 1. The definition (Appendix A.1) -/ + +/-- A **finite relational structure** of signature `σ`: a finite carrier type +`α` (the entities — the union `S₁ ∪ … ∪ Sₙ` of the paper, single-sorted here), +and for each `i : Fin n` a relation of arity `σ i` — a predicate on tuples of +elements. The decidability required by the `rel_dec` field is the one §A.2 of +the paper calls for: "all these functions must be computable" — a finite +structure is specified by its tableaus, and a finite tableau is walked end to +end. -/ +structure FinRelStruct (α : Type*) [Fintype α] {n : ℕ} (σ : Fin n → ℕ) where + /- each relation: a predicate on tuples of arity `σ i` -/ + rel : (i : Fin n) → ((Fin (σ i) → α) → Prop) + /- the relation is decidable: the tableau is effectively given -/ + rel_dec : (i : Fin n) → (t : Fin (σ i) → α) → Decidable (rel i t) + +/-! ## 2. Aut(S) is a group -/ + +/-- A map preserves the structure when every relation is invariant under +relabelling of its tuples. For a bijection, preserving "one way" is enough: +the iff is then automatically symmetric. -/ +def Preserves (S : FinRelStruct α σ) (f : α → α) : Prop := + ∀ i (t : Fin (σ i) → α), S.rel i t ↔ S.rel i (f ∘ t) + +/-- **Aut(S)**, the automorphism group of the structure: the bijections +preserving every relation. It is a subgroup of `Equiv.Perm α` — the "easy to +see" of Appendix A: the identity preserves, the composite of two preservations +preserves, and the inverse of a preservation preserves. The group structure is +then the one Mathlib gives to any subgroup. -/ +def aut (S : FinRelStruct α σ) : Subgroup (Equiv.Perm α) where + carrier := {f | Preserves S f} + one_mem' := by + intro i t + simp + mul_mem' := by + intro f g hf hg i t + rw [Equiv.Perm.coe_mul, Function.comp_assoc] + exact (hg i t).trans (hf i (⇑g ∘ t)) + inv_mem' := by + intro f hf i t + have key : S.rel i (⇑f⁻¹ ∘ t) ↔ S.rel i (⇑(f * f⁻¹) ∘ t) := by + have h := hf i (⇑f⁻¹ ∘ t) + rwa [show ⇑f ∘ (⇑f⁻¹ ∘ t) = ⇑(f * f⁻¹) ∘ t by + simp only [Equiv.Perm.coe_mul, Function.comp_assoc]] at h + rw [mul_inv_cancel, Equiv.Perm.coe_one, Function.id_comp] at key + exact key.symm + +/-- Membership in Aut(S) unfolds to preservation. -/ +theorem mem_aut_iff (S : FinRelStruct α σ) (f : Equiv.Perm α) : + f ∈ aut S ↔ Preserves S f := Iff.rfl + +/-! ## 3. Decidability of equivalence (halting enumeration) -/ + +/-- **Equivalence of structures** (same signature `σ`): there is a bijection +`f` such that every relation of `S` corresponds exactly to the relation of the +same index of `T` through `f`. This is the relational isomorphism — the paper: +"two structure definitions are equivalent if they generate each other"; for +finite structures given by their tableaus, generators included, the equivalence +goes through this correspondence. -/ +def EquivStruct (S : FinRelStruct α σ) (T : FinRelStruct β σ) : Prop := + ∃ f : α ≃ β, ∀ i (t : Fin (σ i) → α), S.rel i t ↔ T.rel i (f ∘ t) + +/-- The version unfolded onto functions: same statement, but quantified over +`α → β` — the enumerable type par excellence (`Fintype.pi`), which carries the +decidability. -/ +theorem equivStruct_iff_functions (S : FinRelStruct α σ) (T : FinRelStruct β σ) : + EquivStruct S T ↔ + ∃ f : α → β, Function.Bijective f ∧ + ∀ i (t : Fin (σ i) → α), S.rel i t ↔ T.rel i (f ∘ t) := by + constructor + · rintro ⟨f, hrel⟩ + exact ⟨f, f.bijective, hrel⟩ + · rintro ⟨f, hf, hrel⟩ + exact ⟨Equiv.ofBijective f hf, hrel⟩ + +/-- **The halting algorithm of Appendix A**: the equivalence of two finite +structures is **decidable** — one enumerates all maps `α → β` (all tableaus), +each tested by decidable predicates, and the enumeration of a finite product of +finite types terminates. Rendered as a `Decidable` instance, `decide` is +literally the tableau enumeration of the paper. + +The two local `letI`s expose the `rel_dec` fields as instances: without them, +instance resolution could not climb from `Decidable (S.rel i t)` back to the +field that witnesses it. -/ +instance EquivStruct.decidable (S : FinRelStruct α σ) (T : FinRelStruct β σ) + [DecidableEq α] [DecidableEq β] : Decidable (EquivStruct S T) := + letI : ∀ i (t : Fin (σ i) → α), Decidable (S.rel i t) := S.rel_dec + letI : ∀ i (t : Fin (σ i) → β), Decidable (T.rel i t) := T.rel_dec + decidable_of_iff (∃ f : α → β, Function.Bijective f ∧ + ∀ i (t : Fin (σ i) → α), S.rel i t ↔ T.rel i (f ∘ t)) + (equivStruct_iff_functions S T).symm + +/-! ## 4. Examples (Appendix A.2) -/ + +namespace Examples + +/-! ### The Sheffer operator `|` (nand) -/ + +/-- NAND on `Bool` (Sheffer symbol `|`) — relation R₈ of equation (A1), and +the single generator of equation (A2). -/ +def nand (x y : Bool) : Bool := !(x && y) + +/-! ### C₂: the cyclic group Z/2 -/ + +/-- Signature of `c2`: a single ternary relation. -/ +@[reducible] +def c2Sig : Fin 1 → ℕ := fun _ => 3 + +/-- The cyclic group **C₂** as a relational structure: a single ternary +relation, the addition table of Z/2 ("generalized multiplication table", §A.2 +of the paper) — the graph of `(x, y) ↦ x XOR y` on `Bool`, encoded as a +relation by note 20: R(x, y, z) ↔ x + y = z. -/ +def c2 : FinRelStruct Bool c2Sig where + rel := fun _ t => (t 0 ^^ t 1) = t 2 + rel_dec := fun i _ => + match i with + | 0 => inferInstance + +/-! ### C₃: the cyclic group Z/3 -/ + +/-- Signature of `c3`: a single ternary relation. -/ +@[reducible] +def c3Sig : Fin 1 → ℕ := fun _ => 3 + +/-- The cyclic group **C₃**: addition table of Z/3 on `Fin 3` (addition on +`Fin n` is already modular). -/ +def c3 : FinRelStruct (Fin 3) c3Sig where + rel := fun _ t => (t 0 + t 1) = t 2 + rel_dec := fun i _ => + match i with + | 0 => inferInstance + +/-! ### The two-element Boolean algebra (equation A1) -/ + +/-- Signature of `bool8`: the arities of the eight relations of equation +(A1) — two constants (arity 1, encoding "x = F" and "x = T"), one unary +function (¬) and five binary ones (∧, ∨, ⇒, ⇔, |). -/ +@[reducible] +def bool8Sig : Fin 8 → ℕ + | 0 => 1 + | 1 => 1 + | 2 => 2 + | 3 => 3 + | 4 => 3 + | 5 => 3 + | 6 => 3 + | 7 => 3 + +/-- The eight relations of equation **(A1)**: F, T, ¬, ∧, ∨, ⇒, ⇔, | (nand), +each encoded by its graph (note 20). The constants F and T are zero-arity +functions, hence unary relations "x = F" and "x = T"; the unary and binary +operators become relations of arity 2 and 3. -/ +def bool8 : FinRelStruct Bool bool8Sig where + rel := fun i t => + match i with + | 0 => t 0 = false -- R₁ = F (false constant) + | 1 => t 0 = true -- R₂ = T (true constant) + | 2 => (!t 0) = t 1 -- R₃ = ¬ + | 3 => (t 0 && t 1) = t 2 -- R₄ = ∧ + | 4 => (t 0 || t 1) = t 2 -- R₅ = ∨ + | 5 => (!t 0 || t 1) = t 2 -- R₆ = ⇒ + | 6 => (t 0 == t 1) = t 2 -- R₇ = ⇔ + | 7 => nand (t 0) (t 1) = t 2 -- R₈ = | (nand) + rel_dec := fun i _ => + match i with + | 0 => inferInstance + | 1 => inferInstance + | 2 => inferInstance + | 3 => inferInstance + | 4 => inferInstance + | 5 => inferInstance + | 6 => inferInstance + | 7 => inferInstance + +/-- **The automorphism group of the Boolean algebra is trivial**: preserving +relation R₁ ("x = F") pins the false constant, and a bijection of `Bool` +fixing `false` fixes `true`. Concrete anchor already used by +`EffectiveTheory.InfoBits` (`b = log₂(n!/|Aut G|)`: 2!/1 = 2, i.e. 1 bit). -/ +theorem aut_bool8_trivial (f : Equiv.Perm Bool) (hf : f ∈ aut bool8) : + f = 1 := by + have hnot : Preserves bool8 ⇑f := hf + have h0 : f false = false := by + simpa [bool8] using (hnot 0 (fun _ => false)).mp rfl + have h1 : f true = true := by + obtain ⟨a, ha⟩ := f.surjective true + cases a with + | false => exact absurd (h0 ▸ ha) (by simp) + | true => exact ha + ext x + cases x with + | false => simpa [Equiv.coe_refl] using h0 + | true => simpa [Equiv.coe_refl] using h1 + +/-! ### Generated by NAND alone (equation A2) -/ + +/-- **R₁ = F** by NAND composition: the formula +`R(R(X, R(X, X)), R(X, R(X, X)))` of the paper yields the false constant. -/ +theorem nand_false (x : Bool) : + nand (nand x (nand x x)) (nand x (nand x x)) = false := by + cases x <;> decide + +/-- **R₂ = T**: `R(X, R(X, X))` yields the true constant. -/ +theorem nand_true (x : Bool) : nand x (nand x x) = true := by + cases x <;> decide + +/-- **R₃ = ¬**: `R(X, X)` yields negation. -/ +theorem nand_not (x : Bool) : nand x x = !x := by + cases x <;> decide + +/-- **R₄ = ∧**: `R(R(X, Y), R(X, Y))` yields conjunction. -/ +theorem nand_and (x y : Bool) : + nand (nand x y) (nand x y) = (x && y) := by + cases x <;> cases y <;> decide + +/-- **R₅ = ∨**: `R(R(X, X), R(Y, Y))` yields disjunction. -/ +theorem nand_or (x y : Bool) : + nand (nand x x) (nand y y) = (x || y) := by + cases x <;> cases y <;> decide + +/-- **R₆ = ⇒**: `R(X, R(Y, Y))` yields implication. -/ +theorem nand_implies (x y : Bool) : + nand x (nand y y) = (!x || y) := by + cases x <;> cases y <;> decide + +/-- **R₇ = ⇔**: `R(R(X, Y), R(R(X, X), R(Y, Y)))` yields equivalence (the +table `[[1,0],[0,1]]` of the paper). -/ +theorem nand_iff (x y : Bool) : + nand (nand x y) (nand (nand x x) (nand y y)) = (x == y) := by + cases x <;> cases y <;> decide + +/-- The structure **(A2)**: the same signature as (A1) — eight relations — +but every table is now **defined by NAND composition alone**, following exactly +the formulas of equation (A2) of the paper. The two constants remain unary +relations "x = F" and "x = T" — hence `x = `, not +` = false`: the formula yields the constant, it does not assert +it. -/ +def nand8 : FinRelStruct Bool bool8Sig where + rel := fun i t => + match i with + | 0 => t 0 = nand (nand (t 0) (nand (t 0) (t 0))) (nand (t 0) (nand (t 0) (t 0))) + | 1 => t 0 = nand (t 0) (nand (t 0) (t 0)) + | 2 => nand (t 0) (t 0) = t 1 + | 3 => nand (nand (t 0) (t 1)) (nand (t 0) (t 1)) = t 2 + | 4 => nand (nand (t 0) (t 0)) (nand (t 1) (t 1)) = t 2 + | 5 => nand (t 0) (nand (t 1) (t 1)) = t 2 + | 6 => nand (nand (t 0) (t 1)) (nand (nand (t 0) (t 0)) (nand (t 1) (t 1))) = t 2 + | 7 => nand (t 0) (t 1) = t 2 + rel_dec := fun i _ => + match i with + | 0 => inferInstance + | 1 => inferInstance + | 2 => inferInstance + | 3 => inferInstance + | 4 => inferInstance + | 5 => inferInstance + | 6 => inferInstance + | 7 => inferInstance + +/-- **Equivalence of definitions (A1) and (A2)**: the eight relations +defined by NAND composition coincide exactly with the eight primitive +relations — the identity is the witness. The proof is literally the catalogue +of composition formulas: each `nand_*` lemma above rewrites one line of (A2) +into the corresponding line of (A1). -/ +theorem equivStruct_bool8_nand8 : EquivStruct bool8 nand8 := by + refine ⟨Equiv.refl Bool, ?_⟩ + intro i t + fin_cases i + · simp [bool8, nand8, Equiv.coe_refl, nand_false] + · simp [bool8, nand8, Equiv.coe_refl, nand_true] + · simp [bool8, nand8, Equiv.coe_refl, nand_not] + · simp [bool8, nand8, Equiv.coe_refl, nand_and] + · simp [bool8, nand8, Equiv.coe_refl, nand_or] + · simp [bool8, nand8, Equiv.coe_refl, nand_implies] + · simp [bool8, nand8, Equiv.coe_refl, nand_iff] + · simp [bool8, nand8, Equiv.coe_refl] + +/-- **The halting algorithm confirms the paper**: `decide` — the tableau +enumeration of Appendix A — finds that (A1) and (A2) define the same +structure, without being given the witness. -/ +example : decide (EquivStruct bool8 nand8) = true := by + decide +kernel + +end Examples + +end MathUniverse_en diff --git a/MyIA.AI.Notebooks/ML/learning_theory_lean/README.md b/MyIA.AI.Notebooks/ML/learning_theory_lean/README.md index 3dcba26a29..9330c5ec94 100644 --- a/MyIA.AI.Notebooks/ML/learning_theory_lean/README.md +++ b/MyIA.AI.Notebooks/ML/learning_theory_lean/README.md @@ -1,4 +1,4 @@ -# learning_theory_lean — Learning theory (Perceptron / Novikoff + PAC / Valiant + GradientFlow + EffectiveTheory), Lean 4 +# learning_theory_lean — Learning theory (Perceptron / Novikoff + PAC / Valiant + GradientFlow + EffectiveTheory + MathUniverse / Tegmark MUH), Lean 4 Lake Lean 4 (Mathlib) à la racine de la série **ML**, mutualisant des résultats fondamentaux de **théorie de l'apprentissage** sous un même umbrella généraliste @@ -49,6 +49,28 @@ fondamentaux de **théorie de l'apprentissage** sous un même umbrella général #16752) : conservation de `C` le long du flot de `ℓ₀` sans hypothèse, invariance de l'hyperplan centré le long du flot effectif, lemmes génériques de calcul différentiel. +5. **Module `MathUniverse`** — digestion #16741/arc B (issue #16753) : l'**Annexe A** + de R16, *The Mathematical Universe* (Tegmark, arXiv:0704.0646) — la définition + opérationnelle d'une **structure mathématique** sur laquelle repose l'hypothèse + de l'univers mathématique (MUH) : des entités (un type fini) et une + **signature** `σ : Fin n → ℕ` donnant l'arité de chacune des `n` relations, + chaque relation étant un prédicat **décidable** — une structure finie se + spécifie par ses tableaux, et un tableau fini se parcourt entièrement. Trois + apports : **`aut`** — les bijections préservant chaque relation forment un + sous-groupe de `Equiv.Perm` (le « easy to see » de l'Annexe A), avec le témoin + concret `aut_bool8_trivial` (le groupe d'automorphismes de l'algèbre de Boole + à deux éléments est **trivial** — ancre déjà mobilisée par + `EffectiveTheory.InfoBits`) ; **`EquivStruct`** et son instance `Decidable` — + le « simple halting algorithm » qui décide si deux définitions finies sont + équivalentes, rendu par **énumération exhaustive des tableaux** + (« l'énumération des tableaux » du papier : `decide` **est** l'algorithme) ; et + les exemples du **§A.2** : **C₂** (table d'addition de Z/2), **C₃** (Z/3), et + l'**algèbre de Boole à deux éléments** — les huit relations F, T, ¬, ∧, ∨, ⇒, ⇔, | + de l'équation **(A1)** — générée par **NAND seul** (équation **A2**) : les sept + formules de composition du papier (`nand_false`, `nand_true`, `nand_not`, + `nand_and`, `nand_or`, `nand_implies`, `nand_iff`), puis + `equivStruct_bool8_nand8` (le témoin est l'identité), et la confirmation par + l'algorithme de décision lui-même, à qui le témoin n'est **pas** donné. C'est le **premier lake Lean de la série ML** (aucun lake Lean en ML auparavant, roadmap #4038 Tier 2). La preuve de Novikoff est **géométrique élémentaire** : @@ -76,9 +98,12 @@ argument ERM dans `ERM`). les identités de l'appendice F (`loss0_grad_sum_zero`, `loss0_grad_dot_self`) et les lois de conservation (`flow_sumsq0_constant`, `flow_deriv_sum_apply` ; côté `GrokkingLemmas` : - `C_conserved_l0`, `meanZero_invariant`, `Z0_conserved`) sont 0-sorry. + `C_conserved_l0`, `meanZero_invariant`, `Z0_conserved`) sont 0-sorry. Côté + MathUniverse, `mem_aut_iff`, `aut_bool8_trivial`, les sept lemmes `nand_*`, + `equivStruct_iff_functions` et `equivStruct_bool8_nand8` sont 0-sorry. - **Build** : `lake build Perceptron` / `lake build PacLearning` / - `lake build GradientFlow` / `lake build EffectiveTheory` (dépend de Mathlib4) + `lake build GradientFlow` / `lake build EffectiveTheory` / + `lake build MathUniverse` (dépend de Mathlib4) ## Ce qui est formalisé @@ -206,24 +231,66 @@ par la dynamique de ces plongements sous la perte effective `ℓ_eff = ℓ₀/Z | `EffectiveTheory/CircleOfDays.lean` | 0 | R10 : la rotation des jours comme représentation de `C₇ = ZMod 7` (`rotation_cyclicSeven`) et son **irréductibilité** `circleOfDays_irreducible` (aucune droite stable : le discriminant `4(cos²(2π/7) − 1) < 0` exclut toute valeur propre réelle). | | `EffectiveTheory.lean` | 0 | Imports parapluie + cartographie du corpus (R02 `88CE88DB` / R06 `B589C4EF` / R10 `7DEAC929`). | +### Module `MathUniverse` (digestion #16741/arc B — Annexe A de R16, Tegmark) + +L'Annexe A de *The Mathematical Universe* donne la définition opérationnelle sur +laquelle repose la MUH : « une structure mathématique est un ensemble d'entités +abstraites et de relations entre elles ». Le module la formalise, sépare la +**signature** de sa **réalisation** (ce que fait la théorie des modèles, et ce qui +rend l'équivalence de deux définitions de la *même* structure énonçable sans +transport d'arité), et prend au mot la phrase du papier : il existe « un simple +algorithme haltant » pour décider l'équivalence de deux structures finies — ici, +`decide` **est** cet algorithme, rendu comme instance `Decidable`. + +Les fonctions non booléennes se codent en relations par leur graphe (note 20 du +papier), ce qui ramène les tables d'addition de C₂/C₃ et les tables de vérité de +l'algèbre de Boole au même objet. + +**Copie pédagogique déclarée** vis-à-vis de +`SymbolicAI/Lean/tegmark_muh_lean/` (MUH, série Lean-36), qui formalise la même +Annexe A **en noyau seul** (zéro Mathlib, cf son lakefile) : là-bas `Aut` porte +ses axiomes de groupe démontrés à la main (`autComp_assoc`, `autId_comp`, +`comp_autId`) et `MUH/Decidable.lean` décide l'égalité stricte des tables +binaires (`sameBinaryOperation`, avec théorème de correction) — sans renommage +des éléments. Ici, la structure de groupe est **héritée** de Mathlib +(`Subgroup (Equiv.Perm α)`) et l'équivalence est décidée **à renommage près**, +entre types porteurs différents (`EquivStruct.decidable`, confirmé par +`decide +kernel`). Ce que l'un prouve à la main, l'autre l'obtient par +héritage : l'écart entre les deux formalisations est lui-même le contenu +pédagogique. La décidabilité à renommage près ne peut pas migrer dans +`tegmark_muh_lean` sans y introduire Mathlib — ce qui y détruirait l'objet du +cours (Lean-36 enseigne précisément ce que le noyau fait seul). + +| Fichier | sorry | Contenu | +|---------|-------|---------| +| `MathUniverse.lean` | 0 | **Définition** : `FinRelStruct` (entités = type fini `α`, signature `σ : Fin n → ℕ`, relations décidables via le champ `rel_dec` — le « all these functions must be computable » du §A.2). **Aut(S)** : `Preserves` + `aut` (sous-groupe de `Equiv.Perm` : identité, composée, symétrique), pont `mem_aut_iff`, et le témoin **`aut_bool8_trivial`** (préserver la relation « x = F » épingle la constante fausse). **Décidabilité** : `EquivStruct` (isomorphisme relationnel), `equivStruct_iff_functions` (déploiement sur `α → β`, le type énumérable par excellence) et l'instance `EquivStruct.decidable` — énumération exhaustive des tableaux, les deux `letI` locaux exposant les champs `rel_dec` comme instances sans quoi la résolution ne saurait pas remonter de `Decidable (S.rel i t)` au champ qui l'atteste. **Exemples §A.2** : `nand` (symbole de Sheffer), **C₂** (`c2`, table d'addition de Z/2), **C₃** (`c3`, Z/3), **algèbre de Boole (A1)** (`bool8`, les huit relations F, T, ¬, ∧, ∨, ⇒, ⇔, \| ; signatures `c2Sig`/`c3Sig`/`bool8Sig` en `@[reducible]` — la résolution d'instances travaille à transparence `reducible` et ne déplie pas un `def` ordinaire), **génération par NAND seul (A2)** : les sept lemmes de composition `nand_false`/`nand_true`/`nand_not`/`nand_and`/`nand_or`/`nand_implies`/`nand_iff`, la structure `nand8`, l'équivalence `equivStruct_bool8_nand8` (témoin : l'identité) et la confirmation par l'algorithme — `decide (EquivStruct bool8 nand8) = true`, obtenu par `decide +kernel` (transparence complète) et **non** `native_decide`, qui ajouterait l'axiome `Lean.ofReduceBool` (banni par la discipline de preuve du dépôt). **Critère partiel, nommé** : la *génération par composition* n'est pas réifiée en opérateur général — les compositions sont prouvées nommément (les sept `nand_*`), la clôture générale d'une signature sous composition reste à écrire. | +| `MathUniverse_en.lean` | 0 | Sibling anglais (Epic #4980) — code byte-identique, docstrings et commentaires traduits. | + +Une difficulté de fond rencontrée (et corrigée, pas contournée) : écrite d'abord +avec ` = false` pour les deux constantes, l'équivalence (A1)/(A2) était +**fausse** — les formules de NAND rendent la constante, elles ne l'affirment pas. +Les lignes R₁/R₂ de `nand8` sont donc `t 0 = `, et c'est `decide` qui a +révélé l'erreur avant toute publication. + ### i18n FR/EN Chaque module est doublé d'un **sibling anglais** `Foo_en.lean` (namespace `PacLearning` ↔ `PacLearning_en`, `Perceptron` ↔ `Perceptron_en`, `GradientFlow` ↔ `GradientFlow_en`, `EffectiveTheory.GrokkingLemmas` ↔ `EffectiveTheory.GrokkingLemmas_en` -(le reste d'`EffectiveTheory` attend son twin, #17481), imports +(le reste d'`EffectiveTheory` attend son twin, #17481), +`MathUniverse` ↔ `MathUniverse_en`, imports `_en`-suffixés, **byte-identical hors docstrings/commentaires**) — livré sous -l'Epic **#4980** (Option A, pattern sibling-pair ratifié 2026-07-04). Les 22 -fichiers `_en` couvrent PacLearning, Perceptron, GradientFlow et -`GrokkingLemmas` : +l'Epic **#4980** (Option A, pattern sibling-pair ratifié 2026-07-04). Les twins +`_en` couvrent PacLearning, Perceptron, GradientFlow, `GrokkingLemmas` et +`MathUniverse` : `PacLearning_en.lean`, `PacLearning/{Agnostic,BernoulliMGF,Concentration,Data, ERM,Hoeffding,MGF,PacFiniteBound,Sample,SampleExpect,UniformConcentration, UnionBound}_en.lean`, `Perceptron_en.lean`, `Perceptron/{Convergence,Data,Perceptron,Tightness}_en.lean`, `GradientFlow_en.lean`, `GradientFlow/{Plain,Residual}_en.lean`, -`EffectiveTheory/GrokkingLemmas_en.lean`. +`EffectiveTheory/GrokkingLemmas_en.lean`, `MathUniverse_en.lean`. **Conséquence** : les futurs raffinements doivent conserver la symétrie FR/EN (les deux fichiers évoluent ensemble ou pas du tout). La CI `check_i18n_siblings` @@ -237,6 +304,7 @@ vérifie l'absence de drift (164/166 byte-identical, 0 orphan cluster-wide au lake build Perceptron # théorème de Novikoff lake build PacLearning # cadre PAC (modèle + propriétés élémentaires) lake build EffectiveTheory # corpus Tegmark : grokking + conservation + R06/R10 +lake build MathUniverse # Annexe A de R16 : structure finie, Aut(S), equivalence decidable # Dépend de Mathlib4 — le premier build est lourd, les builds suivants utilisent le cache ``` @@ -279,6 +347,11 @@ déclaration dans un notebook : Effective Theory of Representation Learning*, arXiv:2205.10343 (2022) — parallélogrammes de représentation (Partie 3) et lois de conservation (Appendice F). +- M. Tegmark, *The Mathematical Universe*, Foundations of Physics (2008), + arXiv:0704.0646 — Annexe A : la définition d'une structure mathématique + (entités + relations), Aut(S) comme groupe, l'algorithme haltant d'équivalence + de deux définitions finies, et les équations (A1)/(A2) — l'algèbre de Boole à + deux éléments engendrée par NAND seul. ## Voir aussi @@ -286,5 +359,6 @@ déclaration dans un notebook : - **Issue #4293** — renommage `perceptron_lean → learning_theory_lean` + module PacLearning (mutualisation, cf `decision_theory_lean`) - **EPIC #13106** — digestion : le module `GradientFlow` en est la tranche « forme formalisation » (grille 10 points dans `GradientFlow.lean`) - **Issue #16752 / EPIC #16741** — module `EffectiveTheory` : base `Grokking.lean` (#16794) + module frère `GrokkingLemmas.lean` (recadrage ai-01 2026-09-23 : delta propre du grain R02, arc « ouverte, responsable, prouvable, explicable ») +- **Issue #16753 / EPIC #16741** — module `MathUniverse` (arc B) : Annexe A de R16 — `FinRelStruct` (signature + relations décidables), `aut` (Aut(S) est un groupe, témoin `aut_bool8_trivial`), `EquivStruct` et son instance `Decidable` (l'algorithme haltant rendu exécutable), exemples §A.2 (C₂, C₃, algèbre de Boole engendrée par NAND seul) - **`ML/`** — série Machine Learning (ML.NET C#, Data Science with Agents Python) - **Epic #2651** — prose pédagogique README diff --git a/MyIA.AI.Notebooks/ML/learning_theory_lean/lakefile.lean b/MyIA.AI.Notebooks/ML/learning_theory_lean/lakefile.lean index 45fb666555..7fc13f5074 100644 --- a/MyIA.AI.Notebooks/ML/learning_theory_lean/lakefile.lean +++ b/MyIA.AI.Notebooks/ML/learning_theory_lean/lakefile.lean @@ -71,3 +71,18 @@ et `GradientFlow`. -/ @[default_target] lean_lib «EffectiveTheory» where globs := #[.submodules `EffectiveTheory, `EffectiveTheory] + +/-- Module `MathUniverse` — digestion #16741/arc B (issue #16753) : Annexe A de +R16 (*The Mathematical Universe*, Tegmark) — structures mathématiques finies +(signature + relations décidables), Aut(S) comme groupe, décidabilité de +l'équivalence de deux définitions finies (« simple algorithme haltant » rendu +comme instance `Decidable`), et les exemples §A.2 : C₂, C₃, algèbre de Boole à +deux éléments (A1) et sa génération par NAND seul (A2). Frère de +`Perceptron`, `PacLearning`, `GradientFlow` et `EffectiveTheory`. -/ +@[default_target] +lean_lib «MathUniverse» where + /- Pas de `.submodules` : MathUniverse est un module plat (deux fichiers + racine, aucune arborescence `MathUniverse/`). Un glob `.submodules` sur un + module sans repertoire fait echouer la resolution de la cible bibliotheque + (`no such file or directory: .../MathUniverse`). -/ + globs := #[`MathUniverse, `MathUniverse_en] diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/README.md index c0cb97b775..9ec94a817e 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/README.md @@ -66,6 +66,12 @@ $ lake build MUH - `finiteness_lean/` — précédent du même pattern (dérivées symboliques de Brzozowski, Lean 4 standalone, sans Mathlib). -- `coordinator-workflow.md` — le流程 de revision lake/coordinateur. +- `MyIA.AI.Notebooks/ML/learning_theory_lean/MathUniverse.lean` — la même + Annexe A formalisée **avec** Mathlib : `aut` comme `Subgroup (Equiv.Perm)` + hérité (les axiomes que ce lake démontre à la main y sont gratuits) et + `EquivStruct.decidable`, équivalence à renommage près décidée par + `decide +kernel`. Copie pédagogique déclarée des deux côtés : ce lake + enseigne ce que le noyau fait seul, l'autre ce que Mathlib abbrevie. +- `coordinator-workflow.md` — le processus de révision lake/coordinateur. - `decidable_instance_propagation.md` — le piège d'instance `Decidable` sans contexte. \ No newline at end of file