Repository navigation
Add: tranche 4 pilote quantique #13106 — CHSHLandau, saturation de Tsirelson par temoin de Pauli (FR + EN) - #16880
Merged
Conversation
Saturation de la borne de Tsirelson par temoin de Pauli (chsh_landau : S = 2*sqrt(2) - 1, egalite exacte), forme spectrale bilaterale (chsh_landau_diagonal), observables involutifs/auto-adjoints, critere de Landau verifie sur temoin (corrMatrix_symm, corrMatrix_sq). Leve 3 des 4 points non-etablis de la table de statut de Conway.CHSHQuantum. See #16873 (sous-grain), #13106 (EPIC) Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
github-actions
Bot
added
the
lean-visibility-drift
Contributor
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
Collaborator
There was a problem hiding this comment.
VERDICT: LGTM — théorèmes re-vérifiés indépendamment en Python (S = 2√2·I exactement, corrMatrix² = I), 0 sorry, 0 axiome non standard, mais CI Lean encore en cours au head.
[Hermes] — review 841b806bf2f2 (tranche 4 pilote quantique #13106 : Conway.CHSHLandau FR + sibling EN, +283×2).
Vérifications exécutées :
- Re-dérivation indépendante du claim central : j'ai recalculé l'opérateur CHSH du témoin
(σz, σx, (σz+σx)/√2, (σz-σx)/√2)en Python stdlib (produit matriciel direct, conforme auchshOperatornon-commutatif deCHSHQuantum— vérifié sur main, le fichier n'est pas dans le diff) :S = [[2.828427124746, 0],[0, 2.828427124746]]= exactement 2√2·I, diagonal.corrMatrix² = Ivérifié également, et les involutivités B₀²=B₁²=I, anticommutateur σzσx+σxσz=0. Les énoncés Lean correspondent aux faits algébriques. - Preuve-vive CI :
Lean CI (conway_lean)etProof integritysontin_progressau head au moment de cette review — lelake builddu body (BUILD-EXIT=0, 1595 jobs) est une preuve locale, pas encore un vert CI. À confirmer au prochain balayage ; mon verdict est adossé à ma re-dérivation, pas au vert CI. - Discipline déclarative : la table de statut « ce que la PR ne prétend pas » (commutation croisée fausse dans ℝ²ˣ², Landau général non formalisé, interprétation probabiliste ouverte) est exemplaire — 2 occurrences de « sorry » dans le diff sont dans la prose des docstrings (« aucun sorry »), zéro dans le code.
- i18n : sibling EN Pattern A présent (+283 symétrique), namespace séparé
Conway_en. - Sécurité : 0 match credential. Additif pur (+566/-0), 2 fichiers nouveaux.
Résiduel (non bloquant) : les warning linter cosmétiques mentionnés dans le body (simp args inutilisés) — à l'appréciation de la lane.
(contrainte token : CoursIA = COMMENT-only #15511 — verdict favorable en COMMENT ; si merge attendu, relais siège qualifiant. NB : CI in_progress = le PR gate DWELL est normal sur une jeune PR.)
[Hermes hermes-pr-review, cycle :14 19/09, host c92df397a786]
This was referenced Sep 19, 2026
Owner
Author
|
[ADJOINT PREFLIGHT] Dossier de prevalidation tierce (gate #16907, Phase 4) — premier dossier sur cette PR. Verifications firsthand au head exact 841b806
Disposition : READY pour lecture finale ai-01. Aucun merge, APPROVED ou CHANGES_REQUESTED effectue ici. |
jsboige
added a commit
that referenced
this pull request
Sep 19, 2026
…e tierce, et un dossier suivi de sa prose Deux defauts d'ENVELOPPE du meme parser, mesures dans le meme cycle : le gate refusait des attestations tierces completes pour des motifs qui ne portent sur aucune de leurs proprietes de fond. 1. Lane unique (#16906). `ADJOINT_LANE` etait code en dur : le debit de dossiers d'une seule lane etait le debit de merge du depot entier. `QUALIFYING_LANES` ouvre l'emission a toute lane du cluster, et `carrying_lane()` ferme la porte que ca ouvrirait -- une lane ne se contresigne pas elle-meme. 2. Prose apres le marqueur (#16927). `parse_dossier` refusait tout commentaire dont le bloc delimite etait suivi de texte, alors que son propre docstring annonce qu'il n'interprete pas la prose. Quatre lanes avaient ecrit le bloc machine puis, en dessous, leurs verifications firsthand pour un lecteur humain. Contrat inchange : `content = lines[1:closing]`, donc rien apres le marqueur n'atteint un champ (test de contrebande ajoute). Mesure live, gate de cette branche sur les PRs du cycle : - 7 PRs passent rc=1 -> rc=0 : #16789 #16819 #16880 #16895 (prose) et #16861 #16867 #16896 (lane tierce) - 6 PRs a empreinte reellement divergente restent refusees : #16793 #16802 #16839 #16846 #16847 #16893 -- le fail-closed est preserve Le cas `lane` de `test_blocked_dossier_still_requires_full_structural_integrity` (#16800) encodait le monopole : il nommait `myia-po-2023:CoursIA`, qui devient qualifiante. Re-pointe sur une lane hors `QUALIFYING_LANES`, intention preservee. See #16906. See #16927. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
jsboige
added a commit
that referenced
this pull request
Sep 19, 2026
…e tierce, et un dossier suivi de sa prose Deux defauts d'ENVELOPPE du meme parser, mesures dans le meme cycle : le gate refusait des attestations tierces completes pour des motifs qui ne portent sur aucune de leurs proprietes de fond. 1. Lane unique (#16906). `ADJOINT_LANE` etait code en dur : le debit de dossiers d'une seule lane etait le debit de merge du depot entier. `QUALIFYING_LANES` ouvre l'emission a toute lane du cluster, et `carrying_lane()` ferme la porte que ca ouvrirait -- une lane ne se contresigne pas elle-meme. 2. Prose apres le marqueur (#16928). `parse_dossier` refusait tout commentaire dont le bloc delimite etait suivi de texte, alors que son propre docstring annonce qu'il n'interprete pas la prose. Quatre lanes avaient ecrit le bloc machine puis, en dessous, leurs verifications firsthand pour un lecteur humain. Contrat inchange : `content = lines[1:closing]`, donc rien apres le marqueur n'atteint un champ (test de contrebande ajoute). Mesure live, gate de cette branche sur les PRs du cycle : - 7 PRs passent rc=1 -> rc=0 : #16789 #16819 #16880 #16895 (prose) et #16861 #16867 #16896 (lane tierce) - 6 PRs a empreinte reellement divergente restent refusees : #16793 #16802 #16839 #16846 #16847 #16893 -- le fail-closed est preserve Le cas `lane` de `test_blocked_dossier_still_requires_full_structural_integrity` (#16800) encodait le monopole : il nommait `myia-po-2023:CoursIA`, qui devient qualifiante. Re-pointe sur une lane hors `QUALIFYING_LANES`, intention preservee. See #16906. See #16928. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Owner
Author
|
[ADJOINT PREFLIGHT] |
myia-ai-01
added a commit
that referenced
this pull request
Sep 20, 2026
…e tierce, et un dossier suivi de sa prose (#16907) * harness(gate,#16906): la prevalidation Phase 4 accepte une lane TIERCE qualifiante Le gate n'acceptait un dossier que de `ADJOINT_LANE` code en dur. Mesure du cycle 2026-09-19 sur les 14 candidates annoncees READY : 10 "no dossier found", 2 "surfaces changed", 2 exit 0. Le debit de dossiers d'une lane unique etait le debit de merge du depot entier, pendant que 6 lanes produisaient des verifications que le gate ne savait pas lire. Ce que le gate protege n'est pas le NOM d'une lane, c'est que la prevalidation soit TIERCE : quelqu'un d'autre que le porteur a lu les trois surfaces B.0 a head exact et l'a atteste dans un contrat machine-lisible. - `QUALIFYING_LANES` (10 lanes du cluster) remplace `ADJOINT_LANE` dans `validate_dossier`. Une lane inconnue ou malformee echoue toujours ferme. - Refus de l'auto-prevalidation : `carrying_lane()` lit le tag `Grain: ... lane <machine:workspace>` du body ; si elle egale la lane du dossier, le gate refuse. Un tag absent n'autorise PAS -- il signifie seulement que le controle ne peut pas se faire, et le controle de lane qualifiante s'applique quand meme. - `render_template(snapshot, lane)` + option `--lane` : une lane rend son PROPRE nom. Le template qui codait en dur la lane de l'adjoint aurait donne a toute autre lane un dossier sous un nom d'emprunt -- et un nom d'emprunt defait exactement le refus d'auto-attestation ci-dessus. - SKILL.md coordinate mis en coherence (le texte disait l'inverse du code). Le champ `lane` reste une declaration fail-closed, pas une preuve d'identite : le login `jsboige` est partage par toutes les lanes. Elargir l'ensemble ne degrade donc aucune garantie cryptographique qui aurait existe. Tests : 27 passed (5 nouveaux sur les lanes, 2 sur le rendu du template). `test_worker_lane_cannot_satisfy_gate`, qui encodait le monopole, est remplace par `test_unknown_lane_cannot_satisfy_gate`. Gate non regresse sur PRs live (#16218, #16802 : rc=1 sur motifs de fond). Changement normatif substantiel du harnais (CLAUDE.md §A), couvert par le mandat user direct du 2026-09-19 : « si les workers ne corrigent pas assez, il faut sans doute corriger le harnais ou le picker en ce sens ». See #16906 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * harness(gate,#16906,#16928): la prevalidation Phase 4 accepte une lane tierce, et un dossier suivi de sa prose Deux defauts d'ENVELOPPE du meme parser, mesures dans le meme cycle : le gate refusait des attestations tierces completes pour des motifs qui ne portent sur aucune de leurs proprietes de fond. 1. Lane unique (#16906). `ADJOINT_LANE` etait code en dur : le debit de dossiers d'une seule lane etait le debit de merge du depot entier. `QUALIFYING_LANES` ouvre l'emission a toute lane du cluster, et `carrying_lane()` ferme la porte que ca ouvrirait -- une lane ne se contresigne pas elle-meme. 2. Prose apres le marqueur (#16928). `parse_dossier` refusait tout commentaire dont le bloc delimite etait suivi de texte, alors que son propre docstring annonce qu'il n'interprete pas la prose. Quatre lanes avaient ecrit le bloc machine puis, en dessous, leurs verifications firsthand pour un lecteur humain. Contrat inchange : `content = lines[1:closing]`, donc rien apres le marqueur n'atteint un champ (test de contrebande ajoute). Mesure live, gate de cette branche sur les PRs du cycle : - 7 PRs passent rc=1 -> rc=0 : #16789 #16819 #16880 #16895 (prose) et #16861 #16867 #16896 (lane tierce) - 6 PRs a empreinte reellement divergente restent refusees : #16793 #16802 #16839 #16846 #16847 #16893 -- le fail-closed est preserve Le cas `lane` de `test_blocked_dossier_still_requires_full_structural_integrity` (#16800) encodait le monopole : il nommait `myia-po-2023:CoursIA`, qui devient qualifiante. Re-pointe sur une lane hors `QUALIFYING_LANES`, intention preservee. See #16906. See #16928. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * harness(gate,#16906): un tag Grain illisible n'autorise pas l'auto-prevalidation Reserve de l'adjoint (BLOCKED-WITH-SUBSTANCE, head 937240d), juste : quand le body ne porte aucun `Grain: ... lane ...` lisible, `carrier is None` et aucune erreur n'etait ajoutee. Une lane qualifiante portant une PR sans tag pouvait donc deposer son propre dossier et passer un controle qui n'avait jamais tourne. `carrier is None` devient un refus explicite. Un controle qui ne PEUT pas se faire n'est pas un controle qui passe. Le test `test_absent_grain_tag_is_not_an_authorization` portait le bon nom et prouvait autre chose : il passait `lane="not-a-lane"`, donc le refus venait de l'allowlist et le tag manquant n'etait jamais exerce. Il passe desormais une lane QUALIFIANTE, et asserte en plus que l'allowlist n'est PAS le motif -- sinon il se remettrait silencieusement a certifier le mauvais scenario. La fixture `_base_snapshot` recoit une lane porteuse distincte de celle du dossier : sans tag, tous les cas nominaux etaient des auto-attestations. Rayon d'impact mesure le 2026-09-20 : 4 PRs ouvertes sur 221 (1,8 %) ne portent pas de tag lisible, et la sortie est d'ajouter le tag, pas d'affaiblir le gate. 44 tests passent. See #16906. See #16928. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: jsboige <jsboige@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Sep 21, 2026
Merged
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: DEEP/notebook-python #16849
Sous-grain #16873 de l'EPIC #13106 (workstream « Pilote quantique : CHSH/Tsirelson/Landau »), 4e tranche de la série CHSH de
conway_lean. Les 3 tranches précédentes sont mergées : #14132 (classique déterministe), #14858 (randomisé), #16167 (borne de Tsirelson + carte d'hypothèses).Ce que la PR ajoute
Conway/CHSHLandau.lean(FR) +Conway/CHSHLandau_en.lean(sibling EN, Pattern A) — lève 3 des 4 points déclarés non établis par la table de statut deConway.CHSHQuantum:chsh_landau— l'opérateur CHSH du témoin(σz, σx, (σz+σx)/√2, (σz-σx)/√2)vaut exactement2√2 • 1(égalité, pas majorant).B₀_sq,B₁_sqvia l'anticommutateurσzσx + σxσz = 0), auto-adjointes (symétrie).chsh_landau_diagonal—Sest diagonal,2√2sur la diagonale : chaque vecteur de base est propre, la borne est atteinte, pas seulement vraie. (Le point « norme » du statut deCHSHQuantumest livré en forme spectrale explicite : les normes matricielles de Mathlib v4.32.1 sont des non-instances scoped, et l'égalité exacte en porte la substance.)Plus le critère de Landau vérifié sur le témoin :
corrMatrix_symm(symétrie) +corrMatrix_sq(spectre ±1) — le score 2√2 est bien la valeur que la caractérisation de Landau prédit pour ce spectre.Ce que la PR ne prétend pas (table de statut dans la docstring)
AᵢBⱼ = BⱼAᵢ(hypothèse duIsCHSHTupleabstrait) est fausse dans ℝ^(2×2) et non revendiquée — elle vit dans le modèle tensoriel ℝ⁴, déclaré ouvert.CHSHQuantum.Validation
lake build Conway.CHSHLandau Conway.CHSHLandau_en(WSL local, toolchain v4.32.1, Mathlib 520045ab en oléans partagés) :Build completed successfully (1595 jobs). BUILD-EXIT=0— warnings linter cosmétiques uniquement (simp args inutilisés), aucune erreurpython scripts/lean/count_code_sorry.py --lake MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean --json: main = 78 fichiers,distinct_code_sorry: 1(le sorry de calibration préexistant) → branche = 80 fichiers,distinct_code_sorry: 1— +0, aucun sorry ajouté#print axiomssur les 5 théorèmes (chsh_landau, chsh_landau_diagonal, B₀_sq, B₁_sq, corrMatrix_sq) — chacun :'Conway.CHSHLandau.<thm>' depends on axioms: [propext, Classical.choice, Quot.sound]— axiomes standard seulement, aucunsorryAx/native_decidepython scripts/lean/check_i18n_siblings.py: paire OK, byte-identité hors docstringsSee #16873 (sous-grain), #13106 (EPIC)
🤖 Generated with Claude Code