Skip to content

feat(lean,#16753): ClosedUnderCompSet + Fin.pi + generation mutuelle explicitee (tegmark_muh_lean) - #19233

Merged
myia-ai-01 merged 1 commit into
mainfrom
feature/16753-muh-annex-a-impl
Oct 5, 2026
Merged

feat(lean,#16753): ClosedUnderCompSet + Fin.pi + generation mutuelle explicitee (tegmark_muh_lean)#19233
myia-ai-01 merged 1 commit into
mainfrom
feature/16753-muh-annex-a-impl

Conversation

@jsboige

@jsboige jsboige commented Oct 5, 2026

Copy link
Copy Markdown
Owner

Grain: DEEP/lean -- lane myia-po-2023:CoursIA-2 -- prev: MED/docs #19188

Résumé

Tranche d'implémentation formelle sur la queue de l'Annexe A de la MUH
(Tegmark R16) dans tegmark_muh_lean. Sans Mathlib, sans lake build
externe : tout est core Lean 4 + le harnais Tegmark déjà en place
(MUH.Structure, MUH.Cyclic). Livré :

  • Fin.pi (alias du produit dépendant indexé par Fin n) + lemmes
    canoniques (Fin.pi_ext, Fin.pi_const) + helper d'énumération
    toBinaryTableList. C'est la pièce qui manquait pour Encoding.lean
    (mention « Fin.pi hors scope ici » ligne 15) et Decidable.lean:73.
  • ClosedUnderCompSet (structure à champs composeB + composeB_arity)
    avec constructeur standard stdClausé (composée gauche-droite
    classique f (g a b) c) et théorème closedUnderComp_of_arbitrary.
    Le stub inductif ClosedUnderComp est conservé pour rétro-compatibilité
    avec la doc existante (cf. PR fix(lean,#16958): align MUH/Boolean/Decidable docstrings to scope réel — Concern #2 Hermes (re-apport) #17431 c.802) — sa docstring pointe
    maintenant vers ClosedUnderCompSet.
  • mutualGenerationEq (définition) + mutualGenerationEq_eq_sameBinaryOperation
    (théorème de coïncidence sur le cas restreint 1-ensemble) + 3 exemples
    exécutants (C₂ vs C₂, C₃ vs C₃, C₂ vs constante 0). Le « simple halting
    algorithm » de Tegmark R16 Annexe A §1 in fine est maintenant une
    définition nommée, pas un commentaire.

Anti-régression — comptage sorry réel

Mesure python scripts/lean/count_code_sorry.py --json :

Lake Avant (main 1e92a29f7) Après (commit f9403405e)
tegmark_muh_lean 0 distinct_code_sorry (9 fichiers, baseline clean) 0 distinct_code_sorry (10 fichiers — Pi.lean ajouté)

Aucun sorry introduit. lake build post-modification SUCCESS (10 jobs,
1.5 s/job) — aucune erreur, aucun warning bloquant.

Arbitrage vs #16958 (CLOSED 2026-09-23)

#16958 avait été clos par alignement doc/code (PR #17431 par c.802) :
les docstrings de MUH.lean + MUH/Boolean.lean + MUH/Decidable.lean
avaient été restreintes au scope réel (stubs honnêtes marqués en gras).
Le présent grain ne renie pas cet arbitrage — les docstrings
restent honnêtes — mais ajoute le contenu formel que Concern #2
avait différé. La sémantique réelle de ClosedUnderComp (structure à
preuve composeB_arity) est désormais disponible pour des grains
ultérieurs qui voudraient l'instancier sur des structures concrètes
au-delà du cas 1-ensemble.

Preuves vs #17283 / #16942 — Concern #1 vérifié

Rel.table reste curryfié en (i : Fin sig.arity) → Fin (sizes (sig.args i)) → Fin (sizes sig.out) (retypage Concern #1). Les nouveaux ajouts
n'introduisent pas de re-dégradation de ce typage — composeB opère sur
des (Fin m → Fin m → Fin m) curryfiés.

B.0 — éléments de body Lean PR (pr-review-discipline §B)

  1. distinct_code_sorry avant/après : 0 → 0 (cf. tableau ci-dessus).
    Mesure : python scripts/lean/count_code_sorry.py --json (pas
    grep -c sorry : sur-compte la prose d'un facteur 23).
  2. Lake build SUCCESS local : lake build 10 jobs, 1.5 s/job, 0 erreur.
  3. Preuve d'intégrité (proof-integrity job CI) : à vérifier post-push
    par gh pr checks <N> — la cible est tegmark_muh_lean qui est
    câblé dans scripts/lean/ci_lakes.json depuis Concern Ajout du notebook TP #3 (PR feat(lean,#16753): Tegmark R16 Annexe A — Boolean NAND + C₂/C₃ + structures finies #16942).
  4. Pas de refactor du prover Python (n/a).

Suite logique (hors scope de cette PR)

  • PR distincte : instancier ClosedUnderCompSet sur Cyclic.c2 et
    Cyclic.c3 (preuve que la composée des mult2/+mod3 avec elle-même
    est bien une relation Tegmark légitime — c'est trivial mais la
    formalisation est pédagogique).
  • PR distincte : porter boolBinaryTableCount (Decidable.lean:70) à
    une énumération effective des 16 tables Booléennes (le docstring dit
    « stub documentaire, implémentation effective non livrée ; voir
    lean(#16753): suivi Concerns #1+#2 Hermes sur tegmark_muh_lean (PR #16942) #16958 » — le scope est rouvert par cette tranche).

Fichiers modifiés

Fichier +lignes / −lignes Type
MUH/Pi.lean +67 / 0 nouveau
MUH/Decidable.lean +81 / −10 extension sémantique + section génération mutuelle

Total : +148 / −10 = +138 lignes nettes, 1 nouveau fichier
(Pi.lean), aucune suppression de code existant.

See #16753 #16741 #16958

🤖 Generated with Claude Code

@jsboige @claude
feat(lean,#16753): ClosedUnderCompSet + Fin.pi helper + generation mu…
f940340 
…tuelle explicitee (tegmark_muh_lean)

Part of #16741 -- arc B (Tegmark R16 Annexe A).

## Scope reel implemente (sans Mathlib)

- `MUH/Pi.lean` (nouveau, 67 lignes) : `Fin.pi` (alias du produit dependant
  indexe par `Fin n`) + `Fin.pi_ext` (extensionnalite via funext) +
  `Fin.pi_const` (cas constant = exponentiel) + `toBinaryTableList`
  (helper d'enumeration des tables 2D). Tegmark Annexe A §c avait besoin
  de `Fin.pi` (cf Encoding.lean:15 mention « hors scope ici ») — la
  reimplementation est dans le scope du Decidier (sans pretention
  bibliotheque complete).
- `MUH/Decidable.lean` (+81/-10) :
  - `ClosedUnderCompSet` (structure reelle de cloture par composition
    binaire, avec champs `composeB` + `composeB_arity`) — constructeur
    `stdClausé` (composee gauche-droite classique `f (g a b) c`) +
    theoreme `closedUnderComp_of_arbitrary` (temoignage executant).
  - `ClosedUnderComp` inductive (stub) conserve pour retro-compatibilite
    docstring actualisee pointant vers `ClosedUnderCompSet`.
  - Section « Generation mutuelle » ajoutee avec `mutualGenerationEq`
    (def) + `mutualGenerationEq_eq_sameBinaryOperation` (theoreme de
    coïncidence) + 3 examples : C2 vs C2 / C3 vs C3 / C2 vs constante 0.

## Mesures (build + reproche)

- Avant : `tegmark_muh_lean` 0 distinct_code_sorry (lake baseline
  clean, mesure `scripts/lean/count_code_sorry.py --json` du 2026-10-05).
- Apres : 0 distinct_code_sorry (lake build SUCCESS, 10 jobs,
  1.5s/job — aucun `sorry` introduit).
- `lake build` post-modif : SUCCESS, 10 cibles (Structure, Encoding, Aut,
  Boolean, Cyclic, Decidable, Examples, Pi + 2 bases), 0 erreur.

## Arbitrage vs #16958 (CLOSED)

#16703 (PR #17431 par c.802, MERGED 2026-09-23) avait tranche
Concern #2 Hermes par alignement doc/code (les docstrings ont ete
restreints au scope reel). Le present grain re-ouvre le volet
**implementation** au niveau EPIC #16741 (ouvert) : `ClosedUnderWork`
prend une semantique reelle (composee gauche-droite sur `Fin m` ->
`Fin m -> Fin m -> Fin m`) et `mutualGenerationEq` explicite le
« simple halting algorithm » de Tegmark par enumeration des tables.
La tranche n'invalide pas #17431 (les docstrings restent honnetes) mais
ajoute le contenu formel que Concern #2 avait differe.

## Conventions i18n #4980

Pas de sibling `_en` pour cette tranche (le fichier Pi.lean et
les ajouts Decidable.lean sont des nouveautés sur le FR-only — pas
d'enonce ou de lemme à mirrorer ; les exemples `rfl` sont des valeurs
pédagogiques Tegmark, pas un lexique anglais à dupliquer). La
convention s'applique aux énoncés de théorèmes : le `rfl` sur
`composeB_arity` reste en notation FR (memes alpha, pas alpha miroir).

See #16753 #16741 #16958

Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
@github-actions github-actions Bot added the lean-visibility-drift La PR ajoute des declarations lake non citees par AUCUN notebook (borne large) (#11703) label Oct 5, 2026
@jsboige jsboige mentioned this pull request Oct 5, 2026
Merged
jsboige added a commit that referenced this pull request Oct 5, 2026
@jsboige @claude
docs(qc,#19163): BOOK_MAPPING 05/02 PolynomialRegression "1/2/5" -> "…
22c3e43 
…1/2/3" (sorties reelles)

L'adjoint po-2025 (commentaire 5988553485 sur tete c569700) a releve
trois contradictions dans le body de la PR : (1) table Objet "degres
1/2/5" -> "1/2/3", (2) table Sorties mesurees polynomial -> 0,0356 /
0,0399 / 0,1507 (R2 test -0,14 / -0,44 / -19,5), (3) table Sorties
mesurees OPTICS -> 1 cluster, 0 bruit, silhouette=None sur les 3
parametrages, 662 jours.

Cette tranche porte la correction BOOK_MAPPING.md seule (la table du
body sera mise a jour par `gh pr edit --body-file` sur la PR dans la
meme action) : ligne 68 "degres 1/2/5 compares" -> "degres 1/2/3
compares" (10 features, colonnes 10/65/285).

Aucune cellule de carnet touchee. Aucune sortie modifiee. Le cliquet
prose-counts verra 1 mot corrige (1/2/5 -> 1/2/3), aucun compte
quantitatif ajoute au-dessus du seuil.

Suite -> `gh pr edit 19163 --body-file <scratchpad>` puis push du
commit et commentaire de reponse a l'adjoint (notification READY
adjoint po-2025).

Grain: MED/docs -- lane myia-po-2023:CoursIA-2 -- prev: DEEP/lean #19233

Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
This was referenced Oct 5, 2026
Merged
Merged
Merged
Merged
Merged
@jsboige

jsboige commented Oct 5, 2026

Copy link
Copy Markdown
Owner Author

Ripe-signal #19233 — feat(lean,#16753) ClosedUnderCompSet + Fin.pi

Grain: LIGHT/ripe-signal -- lane myia-po-2023:CoursIA-2 -- prev: LIGHT/ripe-signal #19234 (c.1054)

Firsthand (Tell c.1190 ★★ + c.971 ★)

gh pr view 19233 --json ... direct :

  • Tête : f9403405ee4757e91fbe76f5e501de887b2ae365 (1 commit, base=main, CLEAN MERGEABLE).
  • Author : jsboige (cette lane — auto-ripe-signal).
  • Review : aucune (auto-ripe, lane=po-2023, owner=lane).
  • PR gate : SUCCESS 2026-10-05T09:07:12Z (run rerun depuis 06:25, DWELL passé).
  • Jambes vertes critiques : Always-on guards, Always-on metadata, Lean CI Matrix (tegmark_muh_lean ✓, autres ✓), Lean visibility drift (advisory ✓), i18n sibling drift ✓, Notebook plan-loss, Secret Scan, CodeQL (4 langages ✓), perimeter-review-guard (fast-lane).
  • Head SHA f9403405e distinct de lastSHA du run précédent, pas de mutation depuis.

Substance vérifiée (Tell c.1038 ★★ instrument canonique)

scripts/lean/count_code_sorry.py --json tegmark_muh_lean avant/après la PR :

  • Avant : 0 distinct_code_sorry (lake baseline clean)
  • Après : 0 distinct_code_sorry (aucun introduit)

lake build post-modif : SUCCESS, 10 cibles (Structure, Encoding, Aut, Boolean, Cyclic, Decidable, Examples, Pi + 2 bases), 0 erreur.

Périmètre

  • MUH/Decidable.lean (+81/-10) : ClosedUnderCompSet (structure réelle de cloture par composition binaire), constructeur stdClausé, théorème closedUnderComp_of_arbitrary, mutualGenerationEq + 3 exemples (C2/C2, C3/C3, C2/constante 0).
  • MUH/Pi.lean (+70/0) : nouveau fichier, Fin.pi + Fin.pi_ext + Fin.pi_const + toBinaryTableList (helper enumeration tables 2D).

Total +151/-10, 2 fichiers Lean, scope Tegmark R16 Annexe A. Sous le seuil composite.

Pourquoi ripe-signal maintenant

Action attendue côté ai-01

Lecture B.0 finale (rapide, propre) + signature de merge sous myia-ai-01 (gh pr merge 19233 --squash, sans --delete-branch).

@jsboige

jsboige commented Oct 5, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19233
head: f940340
complete: true
body: read
comments-reviewed: 1
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: b27672956ed7db0ec117bf6433ff524c66066254c88f0375a09c117bc702db85
diff-files: 2
diff-additions: 151
diff-deletions: 10
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19233
organ-rc: 0
[/ADJOINT PREFLIGHT]

note: DEEP/lean ClosedUnderCompSet + Fin.pi (tegmark_muh_lean), lane porteuse myia-po-2023:CoursIA-2. Fichiers: Decidable.lean + Pi.lean, 161 lignes, 2 fichiers, aucun interdit. PR gate SUCCESS (job 111690892013 à 09:06:23Z), B.0 rc=0 OK avec 1 commentaire A RELIRE (ripe-signal auto-rétroactif de la lane porteuse, post-commit 09:20:32Z, non bloquant). count_code_sorry.py 0 distinct_code_sorry avant/après, lake build SUCCESS 10 jobs 1.5s/job (cf body PR). Anti-régression 4.1 OK. DEEP -> merge_ready refusera le tag, lecture coordinateur requise pour merge manuel.

@myia-ai-01
myia-ai-01 merged commit 71514d5 into main Oct 5, 2026
25 of 28 checks passed
myia-ai-01 pushed a commit that referenced this pull request Oct 5, 2026
@jsboige @claude
feat(qc,#18957): port de quatre exemples courts du livre (IQR, RFE, p…
2c73cc5 
…olynomial, OPTICS) (#19163)

* feat(qc,#18957): port IQR et RFE du livre dans QC-Py-18

Porte deux scripts courts de HandsOnAITradingBook (commit e025f21) :

- 04/05 IQR : detection des valeurs aberrantes par ecart interquartile,
  pose comme instrument de diagnostic avant la normalisation (Partie 7
  applique un RobustScaler pour cette raison) ;
- 04/18 RFE : elimination recursive des variables sur les features deja
  filtrees par correlation, adaptee a la cible de classification du
  notebook (RandomForestClassifier au lieu du regresseur du script).

Chaque sous-section suit la structure du notebook (markdown + code +
interpretation ancre sur les sorties mesurees). Le notebook est re-execute
(27/27 cellules, 0 erreur) : toutes les cellules de code portent un
execution_count et des outputs reels (C.2).

See #18957

Co-Authored-By: Claude-Code <noreply@anthropic.com>

* feat(qc,#18957): port regression polynomiale et OPTICS du livre dans QC-Py-20

Porte deux scripts courts de HandsOnAITradingBook (commit e025f21) :

- 05/02 regression polynomiale : nouvelle sous-section en fin de Partie 2,
  degres 1/2/5 compares sur la relation quadratique du script source
  (RMSE test 20,6 -> 10,1 -> 10,2 : le degre 5 cesse de progresser) ;
- 05/15 OPTICS : nouvelle Partie 8 (clustering par densite pour la detection
  de regimes), trois parametrages compares — le bruit passe de 30 % a 0 %
  selon min_samples, contre une silhouette qui recule de 0,901 a 0,880.

Le script source classait tous les points en coeur (core_samples laisse a
False) ; la version portee utilise core_sample_indices_ et les vraies
metriques sklearn. Notebook re-execute (28/28 cellules, 0 erreur) : toutes
les cellules de code portent un execution_count et des outputs reels (C.2).

See #18957

Co-Authored-By: Claude-Code <noreply@anthropic.com>

* docs(qc,#18957): BOOK_MAPPING -- les quatre exemples 04/05, 04/18, 05/02, 05/15 passent a COVERED

Le port des quatre scripts courts du livre dans QC-Py-18 (IQR, RFE) et
QC-Py-20 (regression polynomiale, OPTICS) ferme les quatre lignes GAP de
l'inventaire. La ligne correspondante quitte la section "Exemples sans
reproduction".

See #18957

Co-Authored-By: Claude-Code <noreply@anthropic.com>

* fix(qc,#18957): address review -- poly and OPTICS demos on notebook market data

NanoClaw review on PR #19163, five points:

1. NB18 c.49: RobustScaler claim replaced by what Partie 7 actually
   applies (rolling z-score); RobustScaler restated as an open choice.
2. NB18 c.41: false Exercice 3 renvoi replaced by the actual CV recipe
   (grid over n_features_to_select, keep best CV score).
3. NB20 c.1: Partie 8 added to Structure du Notebook; stale
   "absence of outputs is intentional" note rewritten to match the
   executed/REFERENCE two-part reality.
4. NB20 c.75: OPTICS added to the conclusion recap, key-points table,
   model comparison table, and academic references (Ankerst 1999).
5. NB20 c.26/c.73: both demos now run on the notebook's own market
   feature matrix (X_train/X_test, X_train_scaled) instead of the
   book's synthetic draws (2.5x^2 parabola, make_blobs). Papermill
   re-execution 28/28: poly degree sweep shows overfitting from
   degree 2 onward (R2 test -0.14 / -0.44 / -19.45); OPTICS finds
   exactly one regime and no noise -- the honest answer for a
   constant-parameter random walk. Interpretations c.27/c.74
   rewritten from the measured outputs.

Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>

* Fix(qc,#18957): retirer l'ouvreur decoratif *** des deux en-tetes de section ajoutees

Le cliquet Split-reading (base vs PR) lisait ces deux cellules comme de la
prose -- leur premiere ligne etait un separateur *** et non un titre -- et les
classait SECOND_READING (QC-Py-18, cellule 39) et READING_BEFORE_CODE
(QC-Py-20, cellule 72). L'en-tete passe en premiere ligne ; aucune autre
modification (diff : deux lignes retirees par notebook, markdown seul).

Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>

* docs(qc,#19163): BOOK_MAPPING 05/02 PolynomialRegression "1/2/5" -> "1/2/3" (sorties reelles)

L'adjoint po-2025 (commentaire 5988553485 sur tete c569700) a releve
trois contradictions dans le body de la PR : (1) table Objet "degres
1/2/5" -> "1/2/3", (2) table Sorties mesurees polynomial -> 0,0356 /
0,0399 / 0,1507 (R2 test -0,14 / -0,44 / -19,5), (3) table Sorties
mesurees OPTICS -> 1 cluster, 0 bruit, silhouette=None sur les 3
parametrages, 662 jours.

Cette tranche porte la correction BOOK_MAPPING.md seule (la table du
body sera mise a jour par `gh pr edit --body-file` sur la PR dans la
meme action) : ligne 68 "degres 1/2/5 compares" -> "degres 1/2/3
compares" (10 features, colonnes 10/65/285).

Aucune cellule de carnet touchee. Aucune sortie modifiee. Le cliquet
prose-counts verra 1 mot corrige (1/2/5 -> 1/2/3), aucun compte
quantitatif ajoute au-dessus du seuil.

Suite -> `gh pr edit 19163 --body-file <scratchpad>` puis push du
commit et commentaire de reponse a l'adjoint (notification READY
adjoint po-2025).

Grain: MED/docs -- lane myia-po-2023:CoursIA-2 -- prev: DEEP/lean #19233

Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude-Code <noreply@anthropic.com>
@jsboige
jsboige deleted the feature/16753-muh-annex-a-impl branch October 7, 2026 07:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

lean-visibility-drift La PR ajoute des declarations lake non citees par AUCUN notebook (borne large) (#11703)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@jsboige @myia-ai-01