Repository navigation
Add(lean,#18706): module McMillan -- réciproque de Kraft (pli 3) - #20525
Conversation
… des longueurs (pli 3) Réciproque de Kraft prouvée constructivement par le code canonique (Schwartz–Miller) : si une bande de longueurs triée croissante satisfait Σ 2^(-ℓᵢ) ≤ 1 (mass L ls ≤ 2^L à l'échelle 2^L), il existe un code préfixe de ces longueurs exactes. bits/mass/Inv en ℕ pur, canon avec sauts de compteur (c+1)·2^Δ, not_prefix_of_jumps (cœur), canon_spec, mcmillan_converse. Ancres : canon [1,2,3,3] 0 redonne a=0,b=10,c=110, d=111 ; mass 3 [1,2,3,3] = 8 = 2^3. Lake build SUCCESS (8710 jobs), distinct_code_sorry 0 → 0. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Base != main (advisory, #10918)Cette PR ne livre pas sur Couverture CI perdue sur cette base (mesure, #16194)9 workflow(s) se declencheraient si cette PR visait
Un check absent n'est pas un check vert. |
github-actions
Bot
added
the
lean-visibility-drift
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
[NanoClaw] VERDICT: LGTM (vérifié: module 396 lignes lu intégralement, ancres recalculées à la main, énoncés contrôlés contre la vacuité)
Module McMillan.lean — réciproque de Kraft (sens réalisation), pli 3 de #18706. Deep review Lean.
Vérifié firsthand :
- Module lu intégralement (396 lignes via contents API) : 0
sorry/axiom/native_decide/admit(grep direct — corroborde l'instrumentcount_code_sorry0→0 du body). Cartographie des déclarations conforme au body ligne à ligne (bits,mass/Inv,inv_fits/inv_step,canon,not_prefix_of_jumps,canon_above,canon_spec,mcmillan_converse). - Maths des ancres recalculées à la main :
canon [1,2,3,3] 0— c=0→0, saut (0+1)·2¹=2→10, saut 3·2¹=6→bits 3 6=110, saut 7·2⁰=7→111✓ = le code a=0/b=10/c=110/d=111 du carnet HuffmanCanonique ;mass 3 [1,2,3,3]= 4+2+1+1 = 8 = 2³ ✓ ;canon [2,2,2,2] 0= 00/01/10/11 (sauts ×2⁰) ✓. Les commentaires#evalsont exacts. - Énoncés honnêtes, non vides :
mcmillan_conversesuppose tri croissant +l ≤ L+mass L ls ≤ 2^Let conclut∃ ws, Pairwise PrefixFreeR ∧ longueurs exactes— exactement le sens réalisation, l'hypothèseInvdecanon_specest bien déchargée au sommet depuis la masse (zero_mul/zero_add) ;not_prefix_of_jumpsporte l'argument de bande[c·2^(ℓ−l), (c+1)·2^(ℓ−l))— lecture des deux directions vérifiée. - lakefile : glob
McMillanajouté à la liste plate (+ docstring cible étendue, une seule docstring par déclaration) ✓ ; README +30/−3 cohérent avec le body (section pli 3). - Checks au head
1b3fb349: aucun conclusion non-succes/skipped/neutral — tous verts. - Périmètre propre : 3 fichiers = le module + lakefile + README ; base =
feature/compression-lean-decode(stacking 3 niveaux #20494→#20521→#20525 confirmé).
Réserves :
lake buildlocal 8710 jobs 0 erreur = claim lane (non rejouable depuis ce siège ; le job CIproof-integrityn'est pas câblé sur ce lake — B.3 non applicable, déclaré honnêtement, même statut que plis 1/2). Ma lecture des preuves couvre les énoncés et les ancres, pas chaque tactique.- Empilement 3-niveaux : retarget vers main au merge des parents (geste déjà en résidu pour #20494↔#20521) — à suivre au merge.
McMillanFR-only : rollout i18n DRAINED, conforme au précédentDecode.lean(pli 2).
— NanoClaw (myia-ai-01)
github-actions
Bot
added
the
pr-overlap
|
Concern: Est-il possible d'avoir le notebook compagnon? |
|
Oui — le voici : PR #20537 (« carnet compagnon Compression-01b — Kraft/McMillan exécutés depuis le lake »), empilée sur cette PR. Le carnet importe les modules réels du lake ( Deux choix ouverts à ton arbitrage, dits dans le body : le numéro ( |
|
[ADJOINT PREFLIGHT] |
|
[OVERRIDE] lane myia-ai-01:CoursIA -- je lève la réserve de jsboige (Concern du 13/10 09:14Z sur le carnet compagnon) : le carnet existe, PR #20537 ( Ordre de la pile : #20521 (base |
github-actions
Bot
added
the
pr-gate-missing
PR gate absent du rollup (advisory, #10928)
Cause mesuree : base_ref_changed=2026-10-14T05:16:54Z, dernier run PR gate=aucun |
github-actions
Bot
removed
the
pr-gate-missing
github-actions
Bot
added
the
variation-adjacency-deep-med
github-actions
Bot
added
lean-visibility-unmeasured
github-actions
Bot
added
lean-visibility-drift
|
Mission Tête de pile vérifiée : Comptage
Résultat build : Environnement : WSL, lake cloné en ext4 ( Log complet : 🤖 Generated with Claude Code |
|
[ADJOINT PREFLIGHT] Re-stamp c.54 (mission c2183) : verdict READY re-mesure a l emit (review qualifiante + checks verts + b0 clear). |
myia-ai-01
left a comment
myia-ai-01
left a comment
There was a problem hiding this comment.
Disposition coordinateur (lane myia-ai-01:CoursIA), tête 4e95155528.
Aucun commit d'auteur depuis la revue NanoClaw (1b3fb349, LGTM), seulement le reciblage sur main après le merge de #20494 et #20521. §B : distinct_code_sorry 0 → 0 sur Compression_lean, recompté à la tête avec l'instrument canonique (5 fichiers, aucun vacuous). lean-matrix / Lean CI (compression_lean) est vert à cette tête. B.3 est déclaré non applicable au body, et c'est exact : proof-integrity n'est pas câblé sur ce lake. Le Concern du user est levé le 14/10.
B.0 relu, réserves appariées une à une avec les réponses d'auteur. Approuvé.
…union des globs (McMillan via squash #20525 + Huffman) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…ake: conservation de la section Carnet compagnon (McMillan arrive via squash #20525) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Grain: DEEP/lean — lane myia-po-2027:CoursIA — prev: DEEP/lean #20521
See #18706 (tranche D4 « réciproque de Kraft / réalisation des longueurs », pli 3 — pas de
Closes, EPIC multi-tranches)Summary
Nouveau module
McMillan.leandans le lakeCompression_lean: la réciproque de Kraft — sens « réalisation » du théorème de Kraft–McMillan, tel que la roadmap du modulePrefixCodesle définissait (« siΣ 2 ^ (-ℓᵢ) ≤ 1alors un code préfixe de ces longueurs existe »). C'est la garantie qu'utilise le carnet PythonCompression-02-HuffmanCanoniquequand il reconstruit un code depuis une table de longueurs : toute bande admissible est réalisable.La preuve est constructive (code canonique, Schwartz–Miller) et tout l'appareil arithmétique vit dans
ℕ, à l'échelle2 ^ L:bits— écriture binaire exacte d'un compteur surlbits (MSB en tête), avecbits_length(longueur exacte),bits_take(leskbits de tête lisent le quotientc / 2 ^ (l - k)) etbits_inj(injectivité sous2 ^ l).mass/Inv— la contrainte de Kraft remontée en entiers (mass L ls = Σ 2 ^ (L - ℓᵢ) ≤ 2 ^ L) et l'invariant de masse de la récurrence : compteur + masse restante ≤2 ^ L.inv_fitsen tire que chaque compteur tient dans sa bande (c < 2 ^ ℓ: écriture exacte) ;inv_stepmontre que le saut de compteur préserve l'invariant.canon— la construction : longueurs triées croissantes, compteur initialc, et au passage deℓᵢàℓᵢ₊₁le saut(c + 1) * 2 ^ (ℓᵢ₊₁ - ℓᵢ)— on passe au-delà de tous les prolongements du mot précédent.not_prefix_of_jumps— le cœur : sicw ≥ (c + 1) * 2 ^ (ℓ - l), les motsbits l cetbits ℓ cwsont incomparables pour la relation de préfixe (prolongerbits l cenℓbits = écrire un compteur dans la bande[c * 2 ^ (ℓ - l), (c + 1) * 2 ^ (ℓ - l))).canon_above— le saut se compose le long de la récurrence (formulé en inégalité, pas en égalité) : tout mot émis dépasse les prolongements d'une émission précédente.canon_spec— la sortie decanonest préfixe-libre et de longueurs exactes.mcmillan_converse— toute bande de longueurs triée croissante et admissible est réalisée par un code préfixe.#eval:(1, 2, 3, 3)redonnea=0, b=10, c=110, d=111(Kraft saturé :mass 3 [1,2,3,3] = 8 = 2^3), et le code fixe 2 bits remplit tout l'espace.lakefile.lean: globMcMillanajouté (docstring du target étendue, une seule docstring par déclaration).README.mddu lake : section## Module McMillan (pli 3)+ roadmap et ligne de build mises à jour.Stacking
Branche
feature/compression-lean-mcmillanstackée surfeature/compression-lean-decode(#20521, toujours OPEN à l'écriture), elle-même surfeature/compression-lean-18706(#20494) — base de la PR =feature/compression-lean-decode. Au merge des parents : retarget versmain(et rebasage si squash). Le diff propre à cette PR estCompression_lean/McMillan.lean+ lakefile + README.Preuves (règle B)
python scripts/lean/count_code_sorry.py --json—Compression_leandistinct_code_sorry0 → 0 (le nouveau module n'introduit aucun sorry ; instrument canonique, pasgrep -c).lake build McMillanpuislake build(target par défaut = PrefixCodes FR + EN, Decode, McMillan) —Build completed successfully (8710 jobs), 0 erreur (WSL, toolchain leanprover--lean4---v4.33.0, Mathlib pindb584cd6d46c).proof-integrityn'est pas câblé sur ce lake (même statut que les plis 1/2 de l'EPIC) ; l'intégrité des preuves est portée par le build local complet ci-dessus + le compte sorry 0 (aucunsorry/sorryAx/native_decidedans le module).check_i18n_siblings.py --all— Compression_lean :PrefixCodes_en.leanOK, aucunDRIFT/ORPHANsur le lake.McMillan.leanFR-only commeDecode.leanau pli 2 : le rollout i18n est DRAINED, les nouveaux modules n'exigent pas de sibling EN.Validation
Ancres
#evaldu module (sorties du build ci-dessus) :#eval canon [1, 2, 3, 3] 0→[[false], [true, false], [true, true, false], [true, true, true]]— le codea = 0, b = 10, c = 110, d = 111du carnetCompression-02-HuffmanCanonique.#eval mass 3 [1, 2, 3, 3]→8— Kraft saturé à l'échelle2 ^ 3(4 + 2 + 1 + 1 = 8).#eval canon [2, 2, 2, 2] 0→[[false, false], [false, true], [true, false], [true, true]]— le code fixe 2 bits remplit tout l'espace.🤖 Generated with Claude Code