Skip to content

feat(lean,#17845): tranche k3 — Komlos/Tent.lean complet (13 preuves reportées, 0 sorry) - #19563

Merged
myia-ai-01 merged 1 commit into
mainfrom
feature/komlos-k3-tent
Oct 7, 2026
Merged

feat(lean,#17845): tranche k3 — Komlos/Tent.lean complet (13 preuves reportées, 0 sorry)#19563
myia-ai-01 merged 1 commit into
mainfrom
feature/komlos-k3-tent

Conversation

@jsboige

@jsboige jsboige commented Oct 6, 2026

Copy link
Copy Markdown
Owner

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: LIGHT/docs #19538

Tranche k3 du lake discrepancy_lean : Komlos/Tent.lean complet (13 preuves reportées)

See #17845 (EPIC distillation Karingula–Lovett, tranche k3 — le fichier Tent.lean de l'oracle Dahia est désormais porté en intégralité).

Ce que la tranche livre

Les 13 preuves explicitement reportées en c.885 (delivery #17918) sont closes, chacune portée du grind v4.34 de l'oracle vers des tactiques disponibles au pin du lake (v4.33.0 / Mathlib db584cd6) :

support_tent_subset, Icc_neg_add_one, sum_Icc_comp_tent_add_one, sum_tent, sum_tent_sq, abs_tent_sub_le, step, abs_step_le_one, step_eq_zero, sum_step_sq_le, tent_sub_tent_eq_sum_step, sum_tent_sub_sq_le_nat, sum_tent_sub_sq_le.

Le résultat porteur est sum_tent_sub_sq_le (∑ (tent M j − tent M (j−m))² ≤ 2·M·m²) — l'ossature L² discrète du Lemme 4.1 (l'estimation de densité-tente). Mesure contre l'oracle : la voie Dahia est totalement discrète — Grid.lean consomme sum_tent_sq + sum_tent_sub_sq_le pour construire le poids normalisé gridF N (distance L² de translation ≤ |m|/(N·√12)) ; le « FTC sur segments » du papier est remplacé par la discrétisation sur grille. La tranche suivante (k3.2) est le port de Grid.lean.

Adaptations grind → v4.33 (détail par preuve en note de fin de fichier)

  • abs_tent_sub_le : la triangulaire inverse est reconstruite via abs_max_sub_max_le_abs + abs_abs_sub_abs_le_abs_sub (les noms abs_add/neg_le_abs_self de Mathlib récent sont absents au pin — sondé par lake env lean).
  • step_eq_zero / support_tent_subset : omega ne splitte pas |j| sur ℤ (atome opaque — mesuré) ; chaque borne M ≤ |j| passe par (by omega : M ≤ -j).trans ((le_abs_self _).trans_eq (abs_neg _)).
  • support_tent_subset : Function.support ... ⊆ Icc force Set.Icc (le Icc nu sous open Finset s'élabore en coercion ↑(Finset.Icc) — son mem_Icc ne s'applique pas, mesuré au probe).
  • Icc_neg_add_one / sum_Icc_comp_tent_add_one : les bornes en cast entier global ((M + 1 : ℕ) : ℤ) — (M + 1 : ℤ) se distribue en ↑M + 1 et ne matche jamais le ↑(M + 1) produit par l'induction ; les gardes sum_insert portent la forme cast explicite.
  • sum_tent : le rw direct avec f := id échoue (le pattern id (tent …) n'existe pas dans le but) — normalisation have h := …; simp only [id] at h avant le rw.
  • tent_sub_tent_eq_sum_step : sum_range_sub' absent au pin → induction manuelle sur k (Nat.cast_add/Nat.cast_one + sum_range_succ + ring).

Preuves de validation

  1. sorry réel avant/après : python scripts/lean/count_code_sorry.py --json → lake discrepancy : distinct_code_sorry 0 → 0 (tranche additive : les 13 preuves étaient absentes de main, pas des stubs sorry — aucune preuve existante n'est remplacée ; total dépôt inchangé à 12, hors périmètre de cette PR).
  2. lake build SUCCESS local (WSL, pin v4.33.0 / db584cd6, oleans Mathlib pré-construits) :
✔ [8707/8708] Built Discrepancy.Komlos.Tent_en (27s)
✔ [8708/8708] Built Discrepancy.Komlos.Tent (27s)
Build completed successfully (8708 jobs).
  1. Proof integrity (B.3) : non applicable — le job lean-axiom n'est pas câblé sur ce lake (aucune clé axiom-target-modules pour discrepancy dans scripts/lean/ci_lakes.json, cas (a) du §B.3). La gate sorry-baseline du lake ("sorry-baseline": "0", sorry-filter-mode: real) couvre le comptage réel.
  2. Jumeaux i18n (i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980) : python scripts/lean/check_i18n_siblings.py <Tent.lean> <Tent_en.lean> → OK — 1/1 pairs byte-identical | 0 drift | 0 orphan (rc=0).
  3. La ligne FORMAL_STATUS.md k3.1 documente la tranche + le reste mesuré de k3 (port de Grid.lean, la voie étant totalement discrète — la ligne de planification k3 est réécrite en conséquence).

Scope du diff

🤖 Generated with Claude Code

@jsboige @claude
feat(lean,#17845): tranche k3 -- Komlos/Tent.lean complet (13 preuves…
39aa436 
… reportees, 0 sorry)

Port integral du Tent.lean de l'oracle (gdahia/Komlos) au pin v4.33.0/db584cd6 :
sum_tent, sum_tent_sq, abs_tent_sub_le, step, abs_step_le_one, step_eq_zero,
sum_step_sq_le, tent_sub_tent_eq_sum_step, sum_tent_sub_sq_le_nat/_le (borne L2
discrete du Lemme 4.1), support_tent_subset, Icc_neg_add_one,
sum_Icc_comp_tent_add_one. lake build SUCCESS sur les deux jumeaux, i18n
byte-identical, distinct_code_sorry 0 -> 0 (additif). Ligne FORMAL_STATUS k3.1
+ reaudit k3 : la voie oracle est totalement discrete (Grid.lean ensuite).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@github-actions github-actions Bot added lean-visibility-drift La PR ajoute des declarations lake non citees par AUCUN notebook (borne large) (#11703) markdown-table-syntax Table syntax defect in changed files (CODE_SPAN_PIPE, NO_SEP, ...). Advisory. See #10097. labels Oct 6, 2026
This was referenced Oct 6, 2026
Open
Merged
This was referenced Oct 6, 2026
Merged
Merged
Merged
Merged
Closed
Merged
Merged
Open
Open
@github-actions

github-actions Bot commented Oct 6, 2026

Copy link
Copy Markdown
Contributor

Path-collision (organ #13359/#13615)

Cette PR #19563 (feat(lean,#17845): tranche k3 — Komlos/Tent.lean complet (13 preuves reportées, 0 sorry)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

@github-actions github-actions Bot added the pr-overlap Advisory: another open PR touches the same files (organ #13615) label Oct 6, 2026
clusterManager-Myia
clusterManager-Myia approved these changes Oct 6, 2026
View reviewed changes

@clusterManager-Myia clusterManager-Myia left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

VERDICT: LGTM

Deep review de la tranche k3 (Komlos/Tent.lean complet — 13 preuves reportées c.885 livrées, portage grind v4.34 → pin v4.33.0/db584cd6).

Vérifications (artefacts réels, head 39aa436) :

  • Diff lu en entier (674 lignes, 3 fichiers : Tent.lean +215/−26, jumeau Tent_en.lean +215/−27, FORMAL_STATUS.md +1 ligne k3.1 + ligne planification k3 réécrite). Les 13 lemmes annoncés sont bien présents en code, corps de preuve complets — support_tent_subset, Icc_neg_add_one, sum_Icc_comp_tent_add_one, sum_tent (Σ tent = M² par induction), sum_tent_sq (3·Σ tent² = M(2M²+1)), abs_tent_sub_le (1-Lipschitz via abs_max_sub_max_le_abs), step/abs_step_le_one/step_eq_zero, sum_step_sq_le (≤ 2M), tent_sub_tent_eq_sum_step (télescopage), sum_tent_sub_sq_le_nat, sum_tent_sub_sq_le (borne L² discrète ≤ 2·M·m², Cauchy–Schwarz sq_sum_le_card_mul_sum_sq). Chaîne de dépendances interne cohérente (chaque lemme ne consomme que des briques livrées au-dessus de lui dans le fichier).
  • Sorry-scan sur les blobs head : 0 occurrence de sorry en code (les 2 matches grep sont les déclarations « 0 sorry » de la prose). Claim « 0 sorry » vérifié, pas seulement affirmé.
  • Preuve-vive CI : lean-matrix / Lean CI (discrepancy_lean) SUCCESS sur le head — l'organe a réellement compilé ce module (le diff touche précisément Discrepancy/Komlos/Tent.lean, périmètre couvert). i18n sibling drift SUCCESS — jumeau EN cohérent (corps de preuve byte-identiques, prose traduite). prose-counts SUCCESS.
  • Comptes : 19 déclarations lemma/def par fichier au head = 21 briques annoncées moins tent/tent_nonneg déjà présents hors hunk diff — cohérent avec la liste « briques closes » du doc-comment.
  • FORMAL_STATUS.md : ligne k3.1 fidèle au diff livré (les adaptations listées — Set.Icc forcé, cast entier global, omega ne splitte pas |j|, sum_range_sub' absent → induction — correspondent aux corps de preuve réels du diff) ; ligne k3 du plan réécrite « voie totalement discrète » cohérente avec l'infrastructure livrée (pas de intervalIntegral dans le diff, sommes closes + L² discret seulement).
  • Security scan : 0 match.

PR gate failure = minuteur DWELL (plancher 120 min, écoule 21:07Z — mécanique, « rien à corriger dans le code », non-organe). Le seul autre check non-vert est l'advisory paragraph-length non-bloquant encore in_progress.

Note d'adaptation remarquable par sa précision mesurée (chaque substitution de tactique justifiée par ce qui est absent au pin, sondé via lake env lean) — c'est la partie la plus utile du fichier pour les tranches k4/k5.

[Hermes hermes-pr-review, cycle :19 06/10, host f6be46d1b7a3, sig=0d26130d]

This was referenced Oct 6, 2026
Open
Merged
@jsboige

jsboige commented Oct 7, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19563
head: 39aa436
complete: true
body: read
comments-reviewed: 1
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 2f050bedb027cc5a4bab6a5e05a72d27a830119466594e850b0115ccb6fe51f6
diff-files: 3
diff-additions: 469
diff-deletions: 111
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19563
organ-rc: 0
[/ADJOINT PREFLIGHT]

@myia-ai-01
myia-ai-01 merged commit 9eb7a38 into main Oct 7, 2026
28 of 29 checks passed
jsboige added a commit that referenced this pull request Oct 7, 2026
@jsboige @claude
Merge origin/main into feature/komlos-k22-convexhull -- union delimib…
bdc3783 
…eree FORMAL_STATUS.md

Conflit unique (content) : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md.
Cause : #19563 (tranche k3, Tent.lean, merge 9eb7a38) et cette branche (k2.2,
convexite) ecrivent la meme region du registre -- k3 ete livree sur main avant
la racine k2.2 de la pile.

Resolution UNION, verifiee par double construction (main+cotes-branche ==
branche+cotes-main, byte-identique) :
- tableau des briques : les DEUX lignes inserees conservees, ordre numerique
  k2.1 < k2.2 (branche) < k3.1 (main) ;
- tableau de planification : ligne k2 = version branche (k2.2 livre, reste
  pullback bloque sur transport de dimension) ; ligne k3 = version main
  (reaudit oracle discret) -- reecritures disjointes, lignes adjacentes.

Coherence verifiee : k3.1 (Tent.lean, algebre discrete) n'introduit aucun
convexHull -- l'affirmation k2 'convexHull passe de 0 a sa premiere occurrence'
survit a l'union. numstat: vs origin/main +2/-1 ; vs dd10e15 +2/-1.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@jsboige
jsboige deleted the feature/komlos-k3-tent branch October 7, 2026 07:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@clusterManager-Myia clusterManager-Myia clusterManager-Myia approved these changes

Assignees

No one assigned

Labels

lean-visibility-drift La PR ajoute des declarations lake non citees par AUCUN notebook (borne large) (#11703) markdown-table-syntax Table syntax defect in changed files (CODE_SPAN_PIPE, NO_SEP, ...). Advisory. See #10097. pr-overlap Advisory: another open PR touches the same files (organ #13615)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@jsboige @clusterManager-Myia @myia-ai-01