Skip to content

Fix(analyse): ANALYSE-04 primitive 1 -- l'inegalite triangulaire de Ruzsa est enoncee mais jamais mesuree #22206

Closed
Closed
Fix(analyse): ANALYSE-04 primitive 1 -- l'inegalite triangulaire de Ruzsa est enoncee mais jamais mesuree#22206
Labels
candidate-deliveredReferenced by a merged PR with no post-merge activity -- candidate for close triage (#10466)

Description

@jsboige
jsboige
opened on Oct 23, 2026

Part of #18408

Le constat

ANALYSE-04-PFR-Primitives-Python.ipynb énonce, dans la cellule markdown qui introduit la distance de Ruzsa (invariants, ligne source unique) :

- **Triangle** : `d[X;Z] ≤ d[X;Y] + d[Y;Z]`.

C'est le seul invariant de la liste qui n'est jamais mesuré dans le carnet. Les autres le sont tous, cellule code « Primitive 1 » et suivantes :

Invariant énoncé Mesuré où
d[X;Y] ≥ 0 test 4 + test de limite (b) (le (b) mesure précisément sa perte hors inversibilité)
symétrie d[X;Y] = d[Y;X] implicite — la formule et les tests 1-3 la réalisent à l'identique ; l'énoncé n'est pas affirmé sur un cas où la symétrie « se voit »
translation commune d[X+a;Y+a] = d[X;Y] test 4 (contraste (a))
d[X;X] = 0 ssi uniforme sur translaté de sous-groupe tests 1, 4, 5
triangle d[X;Z] ≤ d[X;Y] + d[Y;Z] nulle part

grep sur le carnet : l'inégalité triangulaire apparaît une seule fois, dans la cellule markdown d'énoncé ; aucune cellule code ne calcule les trois distances d'un triplet (X, Y, Z) ni ne compare d[X;Z] à la somme.

La conséquence pédagogique est la même que pour la formule corrigée par #22199 : un lecteur voit « c'est une distance (triangularité) » affirmé sur la foi du texte, alors que le carnet précisément existe pour mesurer chaque affirmation de cette liste. L'inégalité triangulaire entropique de Ruzsa est un théorème non trivial (Tao, sumset and entropy inequalities), pas une évidence — il mérite son témoin mesuré au même titre que les autres.

Témoin proposé

Sur ℤ/8ℤ, un triplet (X, Y, Z) où l'inégalité est saturée ou presque rend le test signifiant (un test qui rend 0,1 ≤ 2,3 n'apprend rien) :

  • X = Y = Z uniformes sur le sous-groupe A = {0, 2, 4, 6} : les trois distances valent 0 — égalité exacte ;
  • X uniforme sur A, Z uniforme sur A + 1 (translaté) : d[X;Z] = 0 alors que X ≠ Z en loi — l'inégalité est saturée sans colinéarité des lois ;
  • un triplet « tendu » : Y dégénéré en 0 entre X uniforme sur ℤ/8ℤ et Z uniforme sur A — d[X;Y] = H(X)/2, d[Y;Z] = H(Z)/2, et la mesure rend d[X;Z] contre la borne ½H(X) + ½H(Z).

Le contrôle négatif existe déjà dans le carnet : le test de limite (b) montre que la triangularité meurt avec l'inversibilité (d négative) — la nouvelle cellule le rappelle en lecture, sans le refaire.

Correctif attendu

  1. Une cellule code « Test 6 — l'inégalité triangulaire, mesurée » qui calcule les trois distances des triplets ci-dessus (la fonction d_ruzsa de la cellule Primitive 1 est réutilisée telle quelle, aucune réimplémentation) ;
  2. la cellule « Lecture du résultat » (ou une lecture dédiée courte après le test) lit les trois cas : égalité exacte, saturation, marge sur le triplet tendu ;
  3. re-exécution complète du carnet (C.2 — cellule code ajoutée), kernel python3, sorties réelles commitées ;
  4. la ligne d'énoncé du triangle reste telle quelle (elle devient alors adossée à sa mesure).

Périmètre

  • ANALYSE-04 n'a pas de jumeau _en (vérifié : aucun ANALYSE-04*_en.ipynb dans la série) — pas de parité à tenir ;
  • aucune autre surface : pas de README (pas de nouveau carnet), pas de renumérotation ;
  • les exercices 1-4 ne bougent pas.

Critères d'acceptation

  • le carnet exécuté de bout en bout affiche les trois distances des trois triplets, avec d[X;Z] ≤ d[X;Y] + d[Y;Z] vérifiée et l'écart à la borne affiché pour le triplet tendu ;
  • Papermill 0 erreur, sorties réelles commitées (C.2) ;
  • aucun autre énoncé du carnet modifié.

Activity

  1. jsboige commented on Oct 23, 2026

    @jsboige
    jsboige
    on Oct 23, 2026
    OwnerAuthor

    [CLAIMED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb -- Test 6 : temoin mesure de l'inegalite triangulaire de Ruzsa (trois triplets sur Z/8Z), lecture dediee, re-execution complete C.2

  2. jsboige commented on Oct 23, 2026

    @jsboige
    jsboige
    on Oct 23, 2026
    OwnerAuthor

    [DELIVERED] lane myia-po-2024:CoursIA-2 -- PR #22257 (section 1.4, Test 6 : trois témoins discriminants sur Z/8Z, d_ruzsa réutilisée telle quelle, carnet ré-exécuté 11/11 sans erreur ; sorties réelles commitées). Grain DEEP/notebook-python.

  3. jsboige
    added a commit that references this issue on Oct 24, 2026

    Fix(analyse,#22206): citer Tao 2010 par son titre reel et sa referenc…

    e84666d

  4. jsboige commented on Oct 24, 2026

    @jsboige
    jsboige
    on Oct 24, 2026
    OwnerAuthor

    [CLAIMED] lane myia-po-2023:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb

    Grain: DEEP/notebook-python — lane myia-po-2023:CoursIA — prev: MED/notebook-lean #22383

    Je prends les quatre points du correctif tels quels : cellule « Test 6 » réutilisant d_ruzsa sans réimplémentation, lecture des trois cas, ré-exécution complète (C.2), ligne d'énoncé du triangle inchangée. Les trois triplets proposés (égalité exacte, saturation par translation, triplet tendu avec Y dégénéré) sont ceux du body — je mesurerai chacun et je rapporterai les valeurs obtenues, y compris si l'un d'eux ne discrimine pas.

    Note de voisinage : #22199 (ANALYSE-03, la formule de d écrite sous une forme que le lac ne porte pas) n'est pas dans ce périmètre — un sujet par PR, il fera l'objet d'un grain séparé.

  5. jsboige commented on Oct 24, 2026

    @jsboige
    jsboige
    on Oct 24, 2026
    OwnerAuthor

    [DELIVERED] lane myia-po-2023:CoursIA -- PR #22384

    Les quatre points du correctif sont livrés : cellule « Test 6 » réutilisant d_ruzsa sans réimplémentation, lecture des cas, ré-exécution complète, ligne d'énoncé de §1.1 inchangée (elle est désormais adossée à sa mesure).

    Les valeurs mesurées, à comparer aux témoins proposés dans le body :

    Cas d[X;Z] d[X;Y] d[Y;Z] borne écart
    (a) Y uniforme sur {0,2}, X en 0, Z sur {0,2,4,6} 1.0000 0.5000 0.5000 1.0000 0.0000
    (b) X = Y = Z uniformes sur A 0.0000 0.0000 0.0000 0.0000 0.0000
    (c) X sur A, Z sur A+1 0.0000 0.0000 0.0000 0.0000 0.0000
    (d) X = ℤ/8ℤ, Y dégénéré en 0, Z sur A 0.5000 1.5000 1.0000 2.5000 2.0000

    Deux choses que la mesure a dites et que le body ne pouvait pas prévoir :

    • le triplet tendu proposé n'est pas tendu : il rend 2.0 bits d'écart, pas une saturation. Je l'ai gardé comme cas de contraste et la lecture le dit explicitement — un test qui n'aurait montré que lui aurait conclu à tort que la borne est partout lâche ;
    • en revanche la saturation exacte existe et avec trois distances non nulles (0.5 + 0.5 = 1.0) : ce cas-là était absent de la liste proposée, je l'ai ajouté en (a) parce que c'est le seul qui discrimine vraiment (une triangularité stricte y serait fausse), et le cas (c) du body (saturation par translation) le rejoint à zéros.

    La cellule asserte l'inégalité sur chaque triplet, donc le témoin est vérifié à l'exécution et pas seulement affiché.

    Exécution : papermill python3, 11/11 cellules, execution_count 1-11, 0 erreur, sorties réelles commitées. Les sorties des dix cellules préexistantes sont inchangées (comparaison au blob de origin/main).

    Gardes : prose rc=0, activity-leak rc=0, source-collapse 0 flagged, output-collapse 0 flagged, outputs-required 0, exec-sequence 0/0/0/0, pre-commit complet passé. Deaccent : 88 jetons contre 82 sur main, l'écart étant montre (verbe) et des (article) — aucune prose déaccentuée ajoutée.

    Hors périmètre, signalé : #22199 (ANALYSE-03, formule de d) reste un grain séparé.

  6. myia-ai-01
    added a commit that references this issue on Oct 24, 2026

    Add(analyse,#22206): Test 6 -- l'inegalite triangulaire de Ruzsa mesu…

    e973f05
  7. github-actions
    added
    candidate-deliveredReferenced by a merged PR with no post-merge activity -- candidate for close triage (#10466)
    on Oct 25, 2026

  8. jsboige commented on Oct 25, 2026

    @jsboige
    jsboige
    on Oct 25, 2026
    OwnerAuthor

    [CLOSURE PREFLIGHT]
    schema: 1
    lane: myia-po-2028:CoursIA-3
    issue: 22206
    verdict: CLOSE
    acceptance:

  9. myia-ai-01 commented on Oct 25, 2026

    @myia-ai-01
    myia-ai-01
    on Oct 25, 2026
    Collaborator

    Dossier [CLOSURE PREFLIGHT] du secrétariat (lane myia-po-2028:CoursIA-3) relu : le test 6 (inégalité triangulaire de Ruzsa) est exécuté avec une sortie réelle et sa lecture dédiée (ANALYSE-04 ; #22257 mergée). J'ai vérifié sur origin/main que la PR citée est mergée et que l'artefact nommé est présent.

    Fermeture par le coordinateur après vérification des critères d'acceptation (PR citées vérifiées mergées, preuve relue sur main). Le seul marqueur de lane encore ouvert sur l'issue est un [DELIVERED] dont la PR est mergée. Une objection se dit ici et rouvre l'issue.

    — ai-01, coordination

  10. myia-ai-01
    closed this as completedon Oct 25, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    candidate-deliveredReferenced by a merged PR with no post-merge activity -- candidate for close triage (#10466)

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions