Repository navigation
feat(lean,#14546): CHSH randomized strategies — frontiere classique |expectedScore mu| <= 2 - #14858
Conversation
…expectedScore mu| <= 2 Adds CHSHRandomized.lean (FR) + CHSHRandomized_en.lean (EN i18n sibling) in the Conway lake: a randomized deterministic local strategy as a finite family of non-negative rational weights over the 16 profiles, the expected CHSH score as a convex combination, and the proof that |expectedScore mu| <= 2 via the triangle inequality plus the deterministic CHSH.classical_abs_score bound. Also gives a Dirac mixture reaching 2 and a balanced mixture of the two antagonist profiles giving 0 (linearity of the expected score). See #13106, See #14546
jsboige
left a comment
jsboige
left a comment
There was a problem hiding this comment.
[Hermes] Review — frontière CHSH randomisée (head 14ebf92)
Vérifications effectuées sur le diff complet (353 LOC, 2 fichiers FR/EN) :
- Sorry-scan : 0
sorry/admit/native_decide— propre. - Security scan : aucun secret dans le diff.
- Issue-first method match (#14546) : ✅ la PR fait exactement ce que l'issue demande — paire i18n autonome, combinaison convexe de profils déterministes, réutilisation de
CHSH.classical_abs_score(tranche #14132) plutôt que re-dérivation, Tsirelson explicitement hors périmètre (renvoi à MathlibMathlib.Algebra.Star.CHSH). - Preuve
randomized_bound: structure vérifiée — triangulaire (Finset.abs_sum_le_sum_abs) →abs_of_nonnegsur μ ≥ 0 → borne déterministe par profil →h_totalpour conclure ∑μ·2 = 2. Les deux hypothèsesh_nonneg/h_totalsont effectivement utilisées. - Saturation :
dirac pPosatteint 2 etbalancedMixdonne 0 via linéarité (expectedScore_add/_mul) — cohérent avec le body. - Parité FR/EN : les deux fichiers sont structuralement identiques (mêmes théorèmes, mêmes preuves).
Un point à confirmer au merge : l'instance locale Fintype CHSH.Outcome (l.53) — si CHSH.lean en définit déjà une, elle sera un doublon (diamond bénin mais bruit). La Lean CI (conway_lean), encore pending à l'instant du review, tranchera.
Verdict : contenu solide, méthode conforme à l'issue. (contrainte token : COMMENT only)
|
Complément preuve (B.1 / acceptance « build global du lake Conway ») : |
|
Point infra (statut lane, pas un défaut du livrable) — diagnostic des rouges Les 8 échecs du rollup portent tous la même signature, avant tout checkout du code : Concerne notamment Always-on guards, Always-on metadata guards, i18n sibling drift, Scripts Tests (CPU), conway target-coverage, PR gate — aucun n'a atteint l'étape de build Lean. Cause racine connue et documentée flotte-wide : saturation egress Décision de lane : aucun rerun tant que le gate de guérison n'est pas tenu (RTT gateway < 10 ms / perte 0 %, puis clone témoin OK) — chaque tentative brûle ~1h45 de runner. La lane documente et continue de produire ; les checks seront relancés dès le feu vert réseau. |
|
[INFRA] Échecs WAN-ère, pas contenu — vérifié 06/09 ~13:05Z.
|
|
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 |
github-actions
Bot
added
the
lean-visibility-drift
…in) vs survie (1-c)^n (pile residuelle) (#14980) Tranche digestion (forme formalisation, cf pilote CHSH #14858) : troisieme frere du lake learning_theory_lean apres Perceptron (Novikoff) et PacLearning (Valiant). Ancres numeriques du notebook 4.2-ConvNet-Profonde-Residuelles (facteur 0,4/bloc, 20 blocs) : two_fifths_pow_twenty_lt / three_fifths_pow_twenty_gt. Siblings EN (convention #4980). lake build SUCCESS, 0 sorry, axioms standards. Co-authored-by: Claude-Code <noreply@anthropic.com>
…39 -> 1/39 modules noirs (#15851) * feat(lean,#11703): Lean-16f expose la frontiere CHSH du lac conway_lean Le notebook FWT (Lean-16f) ne citait aucune declaration de Conway/CHSH.lean ni Conway/CHSHRandomized.lean : les deux tranches formelles livrees par #14132 et #14858 existaient dans le lac sans qu'aucun notebook ne les montre, donc invisibles au critere de l'epic #11703 (modules "noirs"). Ajoute la section 6 "La non-localite quantitative : la frontiere CHSH" (miroir python des 16 profils deterministes + inventaire des declarations reelles des deux modules, 0 sorry), renumerote les ancres 6->7 / 7->8, etend le plan a 8 entrees, le registre (+2 lignes) et le resume (+2 modules). Execution ciblee (regle C.3) : seules les 3 cellules code ajoutees sont executees ; les cellules preexistantes gardent leurs sorties commitees, leurs libelles execution_count etant renumerotes en ordre de fichier pour satisfaire le ratchet check_exec_sequence.py (verdict CLEAN 1..17). See #11703 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(notebooks,#11703): retirer les blocs papermill perimes du transplant nbclient Le gate CI `Papermill ratchet (base vs PR)` rendait FAILURE sur cette PR : outputs/execution_count changed but the metadata.papermill block is identical to origin/main - the block describes the previous run. C'est exact, et c'est le defaut du transplant : les 3 cellules CHSH ont ete executees au nbclient (regle C.3, re-execution ciblee) et seules leurs `outputs` ont ete recopiees. Les sorties commitees ne viennent donc PAS du run papermill du 2026-06-11 dont le bloc porte encore l'empreinte. Voie sanctionnee par le message du gate lui-meme (« re-execute the notebook via an executor that rewrites the block, or remove the block ») : on RETIRE le bloc. Le reecrire a la main serait faux -- il decrirait un run papermill qui n'a pas eu lieu -- et le scrub d'output est banni (Stop & Repair, secrets-hygiene regle 6). Retrait complet : bloc top-level + `cell.metadata.papermill` des 39 cellules qui en portaient (25 markdown, 14 code), sans filtre de `cell_type`. Le gate ne lit que le top-level, mais laisser les blocs de cellule laisserait 39 empreintes d'un run qui n'a pas produit ces sorties. Ecriture en JSON brut : le round-trip `json.dumps(indent=1, ensure_ascii=False)` est verifie byte-identique sur ce fichier, donc le diff ne contient QUE les retraits (0 insertion / 285 suppressions, aucune autre ligne touchee). Verification locale : `check_papermill_ratchet.py origin/main` -> 0 regression, `BLOCK_REMOVED`. Scan des sorties : 0 chemin machine absolu. See #15851 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
2 participants
Grain: DEEP/lean — lane myia-po-2027:CoursIA-2 — prev: MED/docs #14558
Objet
Issue #14546 — « lean(#13106): borne CHSH pour les stratégies locales randomisées ». Ajoute dans le lake Conway la paire i18n
Conway/CHSHRandomized.lean(FR) /Conway/CHSHRandomized_en.lean(EN), modulesConway.CHSHRandomized/Conway_en.CHSHRandomized_en, qui formalise la frontière classique pour les stratégies aléatoires localement déterministes.Acceptations (carte)
Profile = CHSH.Outcome × CHSH.Outcome × CHSH.Outcome × CHSH.Outcome;Profile.scoreréutiliseCHSH.score(CHSH_en.scorepour l'EN) sur le quadruplet de résultats binaires.Strategy = Profile → ℚ— famille finie de poids rationnels non négatifs de somme 1 (hypothèsesh_nonneg : ∀ p, 0 ≤ μ peth_total : ∑ p, μ p = 1).expectedScore μ = ∑ p : Profile, μ p * (Profile.score p : ℚ)— combinaison convexe des scores déterministes.randomized_bound : |expectedScore μ| ≤ 2— inégalité triangulaire (Finset.abs_sum_le_sum_abs) + borne déterministeCHSH.classical_abs_scoresur chaque profil.dirac pPosatteint la borne (score espéré2, donc|expectedScore _| ≤ 2est saturée) ;balancedMix(poids 1/2 surpPos+2 etpNeg−2) donne0, prouvé par la linéarité du score espéré (expectedScore_add,expectedScore_mul).Preuves (B.1 / B.3 / H.4)
sorryréel —count_code_sorry.py --json, champdistinct_code_sorry:code_sorry=2,distinct_code_sorry=1;code_sorry=2,distinct_code_sorry=1.sorry(grep -nE "sorry|admit|native_decide"→ 0 occurrence). Ledistinct_code_sorry=1résiduel est pré-existant (autre module du lake).lake build Conway.CHSHRandomized Conway.CHSHRandomized_en→ Build completed successfully (950 jobs) (Lean 4.32.1,lakenatif Windows). Changement purement additif : 2 nouveaux fichiers, aucun module existant modifié, donc aucune régression globale du lake.lean-conway.yml(jobtarget-modules: "*", cf lean: target-modules tenu a la main -> proof-integrity vert hors-cible (26 modules hors vue sur 4 lakes) #10889) appellelean-axiom.yml→LeanVerifier.check_axioms(module, fail_on_sorry=True), qui dérive la liste des modules en marchant chaque*.leansousproject-path.Conway.CHSHRandomizedetConway.CHSHRandomized_ensont donc couverts — B.3 écrit « non applicable » uniquement si non couvert, ce qui n'est pas le cas ici.#print axioms) :randomized_bound,balancedMix_eq_zero,expectedScore_addne dépendent que de[propext, Classical.choice, Quot.sound]— aucunsorryAx, aucunnative_decide.*, aucunClassical.choicenon whitelisté.python scripts/lean/check_i18n_siblings.py Conway/CHSHRandomized_en.lean→OK:1/1 pairs byte-identical | 0 consumer-pattern | 0 drift | 0 orphan | 0 unbuilt | 0 half-done.git diff --cached --check— propre (0 défaut d'espacement).Notes
See #13106,See #14546— pas deCloses: le pilote quantique EPIC: Digestion et canonicalisation des mathématiques assistées par IA #13106 reste ouvert (la borne quantique 2√2 / Tsirelson est hors périmètre, cf docstring du module).