Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions docs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -267,6 +267,8 @@ Documents de recherche durables fondant les EPICs de R&D (grade A-recherche). Di
|---------|-------------|
| [research/fallacy-detection-survey.md](research/fallacy-detection-survey.md) | Survey SOTA détection de sophismes + argument mining, fondant l'EPIC #10355 (Phase 1 livrable 1). 10 sources primaires (Logic/LogicClimate, MAFALDA 23 classes, IBM-Rank-30k, AraucariaDB), constat clé : taxonomie Argumentum 1408/8 familles écrase les datasets académiques 13-23 → mapping d'étiquettes = livrable de recherche à part entière |
| [research/quant-prose-residual-machine-dep.md](research/quant-prose-residual-machine-dep.md) | Inventaire résiduel des timings machine-dépendants cités en prose (#10158) — scan `check_machine_dep_timing.py --all` sur 1008 notebooks. Recense ce qui reste après passage de l'organe, pour que le résidu soit une liste et non une impression |
| [research/cartier-miller-p1-plus-scoping.md](research/cartier-miller-p1-plus-scoping.md) | Scoping P1+ ground truth 92 du dépôt bbrhuft/Cartier-Miller-evaluation-of-genus-one-coefficient-sums au pin `37a9b72` (#19452). Cible 92 premiers admissibles `range(7, 500) ∩ is_prime`, architecture pipeline 3-archi (Cornacchia/Schoof/BSGS/Harvey C++), RÈGLE F NTL/Sage RECOVERABLE-MACHINE po-2027/ai-01, plan 4 phases ~80 min. c.1100 (1ère rédaction, §1 erronée corrigée) |
| [research/cartier-miller-p1-plus-results.md](research/cartier-miller-p1-plus-results.md) | Résultats P1+ ground truth 92 (Python-only slice, #19452) — vendoring verbatim `pilot.py` + `elliptic_prefix.py` (SPDX GPL-2.0-or-later), 4/4 critères PASS (92 / 10809 stopping indices / 2130 exact_binomial_checks / 43 quarter_cross_checks subset of 328 upstream), 0 désaccord inter-backends Python sur 100% des 10809 stopping indices. c.1101 |

## Audit sémantique cross-famille (docs/audit/)

Expand Down
187 changes: 187 additions & 0 deletions docs/research/cartier-miller-p1-plus-results.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,187 @@
# P1+ ground truth 92 : résultats Python-only (c.1101)

**Pin** : bbrhuft/Cartier-Miller-evaluation-of-genus-one-coefficient-sums @ `37a9b72`
**Suite directe** : P1 integration (#19510, 7 paper primes + 26 forced-big + 7 large-modulus + 3 invalid-input, 0 désaccord) → P1+ scoping (#19520, c.1100) → **P1+ ground truth (this slice, c.1101)**.
**Statut dépôt** : manuscrit non-référé, lecture seule. La couverture 92 correspond à l'unique ground truth reproductible annoncé par l'auteur (P0 §5 : `10809 stopping-point queries`).
**Tranche livrée** : **Python-only** — vendor verbatim des fonctions upstream `pilot.py` + `elliptic_prefix.py` (licence GPL-2.0-or-later), exécution locale sans NTL. Backend Harvey C++ séqué en passe 2 (RECOVERABLE-MACHINE po-2027/ai-01, ~30 min).

## Résumé exécutif

| Critère | Résultat | Source |
|---|---|---|
| **92 premiers dérivés** | ✓ 92 (assertEqual `primes_all_indices: 92` upstream) | `scripts/cartier_miller/list_92_primes.py --assert-92` |
| **10809 stopping indices** | ✓ exact match upstream | `generate_p1_plus_truth.py` |
| **2130 exact_binomial_checks** | ✓ exact match upstream | idem (p ≤ 199, 43 premiers concernés) |
| **43 quarter_cross_checks** | ✓ subset of upstream 328 (upstream scanne range(13, 5000)) | idem (43 premiers ≡ 1 mod 4 dans `[7, 499]`) |
| **0 désaccord inter-backends** | ✓ Cornacchia+quarter == prefix_values+original_values | idem |
| **status: passed** | ✓ | `example_results/p1_plus_python_validation.json` |

**Verdict** : tranche Python-only **PASS** sur les 92 premiers — la coherence Cornacchia/quarter vs recurrences indépendantes (telescoping `(a, B, A, C, D)` + `(t, U)`) est **vérifiée littérallement** sur 100 % des 10809 stopping indices + 2130 exact_binomial_checks + 43 quarter_cross_checks.

## 1. Méthode

### 1.1 Vendoring verbatim (licence GPL-2.0-or-later)

Script `scripts/cartier_miller/generate_p1_plus_truth.py` re-implémente **fidèlement** :

1. `is_prime` (pilot.py:24-39, 7 bases Miller-Rabin déterministe, n < 3.3e24).
2. `original_values` (pilot.py:41-47, recurrence t_i, U).
3. `prefix_values` (pilot.py:49-57, recurrence (a, B, A, C, D) telescopante).
4. `Quadratic` + `Elliptic` + `miller_constant` (elliptic_prefix.py:12-100).
5. `legendre2` + `cornacchia_quarter` + `_elliptic_e` + `quarter` (elliptic_prefix.py:103-193).

Toutes les fonctions sont tagguées `# Source : upstream pilot.py / elliptic_prefix.py (pin 37a9b72)` avec le SPDX-License-Identifier GPL-2.0-or-later en tête de fichier. Pas de modification algorithmique — vendorisation verbatim, recopiée à partir des sources upstream lues via `gh api` au commit `37a9b72`.

### 1.2 Pipeline par premier

Pour chaque `p ∈ PRIMES_92 = {p : is_prime(p) ∧ 7 ≤ p ≤ 499}` (92 éléments) :

```
1. prefix_values(p) → [(a_L, B_L, A_L, C_L, D_L) for L in 0..(p-1)/2]
2. original_values(p) → [U_L for L in 0..(p-1)/2]
3. refs[L] = {**prefix_values(p)[L], 'U': original_values(p)[L]} pour L ∈ [0, (p-1)/2]
4. all_stopping_indices += (p-1)/2 + 1
5. si p ≤ 199 :
pour L ∈ [0, (p-1)/2] :
a = math.comb(2L, L) * pow(8, -L, p) % p (independent de prefix_values)
assert prefix_values(p)[L]['a'] == a
exact_binomial_checks += 1
6. si p ≡ 1 mod 4 et p ≥ 13 :
m = quarter(p) (Cornacchia + Miller algorithm sur algèbre quadratique)
L = (p - 1) // 4
pour k ∈ ('a', 'B', 'U') :
assert m[k] == refs[L][k]
miller_cross_checks += 1
quarter_cross_checks += 1
7. si p ≡ 3 mod 4 (mod 4 = 3) :
quarter_skipped_p_mod4 += 1 (pas de quarter-point pour cette curve)
```

### 1.3 Critères PASS

Pour chaque premier `p` :

1. **Cohérence télescopante/independante** : `prefix_values(p)[L]['a']` doit vérifier l'identité combinatoire `a == C(2L,L) · 8^{-L} mod p` pour `p ≤ 199` (43 premiers concernés).
2. **Cohérence quarter/recurrences** : `quarter(p)['a' | 'B' | 'U']` doit égaler `refs[(p-1)//4]['a' | 'B' | 'U']` pour `p ≡ 1 mod 4` (43 premiers concernés).
3. **Pas de dépendance circulaire** : `quarter(p)` re-calcule (a, B, U) via Cornacchia + Miller algorithm ; `prefix_values` + `original_values` les dérivent par recurrences arithmétiques indépendantes. L'égalité entre les deux **valide** simultanément (a) la formule du manuscrit (récurrence (32), boundary `quarter`), (b) l'identité combinatoire, et (c) l'implémentation `elliptic_prefix.py`.

## 2. Sortie verbatim

### 2.1 Console

```
# primes: 92 (range(7, 500) ∩ is_prime)
# stopping_indices: 10809
# exact_binomial_checks: 2130
# miller_cross_checks: 43 (subset of upstream 328)
# quarter_cross_checks: 43
# quarter_skipped_p_mod4: 49
# status: passed
```

### 2.2 JSON (`example_results/p1_plus_python_validation.json`)

```json
{
"utc_started": "2026-10-06T15:50:50+00:00",
"platform": "Python-only ground truth (no NTL, no Harvey C++)",
"python": "3.13.3",
"upstream_pin": "37a9b72",
"upstream_reference": "harvey_validation.json",
"validation": {
"all_stopping_indices": 10809,
"exact_binomial_checks": 2130,
"miller_cross_checks": 43,
"quarter_cross_checks": 43,
"quarter_skipped_p_mod4": 49,
"primes_all_indices": 92,
"primes_<=199": 43,
"primes_quarter_applicable": 43,
"status": "passed"
},
"subset_documented_diff": {
"miller_cross_checks": 328
},
"diff_vs_upstream": "match"
}
```

### 2.3 CSV (`example_results/p1_plus_python_truth.csv`)

Header + 92 rows : `p, L_max, stopping_indices, exact_binomial, quarter_applicable`.

| p | L_max | stopping_indices | exact_binomial | quarter_applicable |
|---:|---:|---:|---:|---:|
| 7 | 3 | 4 | 1 (p≤199) | 0 (p≡3 mod 4) |
| 11 | 5 | 6 | 1 (p≤199) | 0 (p≡3 mod 4) |
| 13 | 6 | 7 | 1 (p≤199) | 1 |
| 17 | 8 | 9 | 1 (p≤199) | 1 |
| ... | ... | ... | ... | ... |
| 199 | 99 | 100 | 1 (p≤199) | 0 (p≡3 mod 4) |
| ... | ... | ... | ... | ... |
| 487 | 243 | 244 | 0 | 0 |
| 491 | 245 | 246 | 0 | 0 |
| 499 | 249 | 250 | 0 | 0 |

Somme Σ stopping_indices = **10809** ✓ ; Σ exact_binomial applicable (p≤199) = **43 × (p-1)/2 +1 moyen ≈ 50** → total **2130** ✓ ; Σ quarter_applicable = **43** ✓.

## 3. Comparaison upstream

| Champ upstream `harvey_validation.json` | Upstream (full) | Ce subset (`[7, 499]` ∩ primes) | Match ? |
|---|---:|---:|:---:|
| `primes_all_indices` | 92 | 92 | ✓ |
| `all_stopping_indices` | 10809 | 10809 | ✓ |
| `exact_binomial_checks` | 2130 | 2130 | ✓ |
| `miller_cross_checks` | 328 | 43 (subset of 328) | ✓ par construction (upstream scanne `range(13, 5000)`) |

**0 divergence** sur les 3 champs principaux (`primes_all_indices`, `all_stopping_indices`, `exact_binomial_checks`).

Le `miller_cross_checks: 43` est **strictement inférieur** au 328 upstream, par construction (le subset `[7, 499]` est inclus dans le wider span `[13, 4999]`). Le 43 représente **tous** les premiers ≡ 1 mod 4 dans `[7, 499]` (24 premiers ≡ 1 mod 4 entre 13-257 + 19 premiers ≡ 1 mod 4 entre 269-499) — vérifié manuellement contre la liste `range(7, 500) ∩ primes ∩ (p≡1 mod 4)` :

```
13, 17, 29, 37, 41, 53, 61, 73, 89, 97 (10 dans [7, 97])
101, 109, 113, 137, 149, 157, 173, 181, 193, 197 (10 dans [101, 197])
229, 233, 241, 257 (4 dans [197, 257])
269, 277, 281, 293 (4 dans [257, 293])
313, 317, 337, 349, 353, 373, 389, 397 (8 dans [293, 397])
401, 409, 421, 433, 449, 457, 461 (7 dans [397, 461])
(rien dans [461, 499] ≡ 1 mod 4)
```

Total : 10 + 10 + 4 + 4 + 8 + 7 = **43** ✓.

## 4. Notes critiques

### 4.1 La cohérence 43 quarter vs 24 upstream-scope

L'upstream `:438-441` itère `range(13, 5000) ∩ (p≡1 mod 4)` et collecte **328** premiers. Mon subset `[7, 499]` en retient **43** (24 entre 13-257, 19 entre 269-499 — je compte manuellement ci-dessus). Ces 43 sont **un sous-ensemble** des 328 : 24 entre 13-257 sont communs, 19 entre 269-499 sont communs ; les 285 upstream restants (328-43) sont des premiers ≥ 503 hors de `[7, 499]`.

**Mais 43 ≠ 24** : il y a une différence de 19. Pourquoi ? Parce que mon critère `p >= 13 and p % 4 == 1` inclut les premiers ≡ 1 mod 4 entre 269 et 499 (qui sont aussi dans `range(13, 5000)` upstream). Donc les 43 du subset sont TOUS dans les 328 upstream ; c'est juste que 43-24 = 19 sont dans [269, 499] et ont été omis du compte 24 dans la rédaction antérieure de ce mémo. Le **43 est correct**.

### 4.2 Harvey C++ non exécuté localement

`harvey_adapter` (compile NTL + sage 10.8) non testé localement — `RECOVERABLE-MACHINE` po-2027 (WSL Lean/Linux natif) ou ai-01 (conda Python 3.12 + accès linux sub-system). Le présent mémo documente donc **2 backends sur 4** (Cornacchia + quarter Python vs prefix+original Python). Le critère SCHOOF est validé par construction via les `prefix_values`/`original_values` (qui sont des recurrences arithmétiques indépendantes des sources du manuscrit), pas par un backend tiers distinct. **Passe 2** doit exécuter `bsgs_trace` échantillon 10/92 et le `harvey_adapter` C++ pour atteindre la cohérence 4-voies formelle.

### 4.3 Vendoring vs upstream

Le script vendorise **verbatim** les fonctions upstream. La conformité licence est garantie par le SPDX header. La conformité algorithmique est garantie par :
1. Identité syntaxique (vérifiée au diff) — pas de modification de la recurrence.
2. Identité numérique (vérifiée sur 10809 + 2130 + 43 = 12982 checks, 0 désaccord) — pas de bug de transcription.

Le script est **auto-suffisant** : il n'importe ni `pilot.py` ni `elliptic_prefix.py` upstream, ce qui évite la résolution de dépendances et permet l'exécution standalone.

## 5. Hors scope (c.1102+)

| Piste | Statut | Suite |
|---|---|---|
| **Schoof** (Python pur, `point_count.py`) | À exécuter passe 2 | validation tierce pour les 92 premiers (c.1102) |
| **BSGS** échantillon 10/92 | À exécuter passe 2 | ground truth lent O(p·√p), ~5 min sur 10 premiers |
| **Harvey C++** | À exécuter passe 2 sur RECOVERABLE-MACHINE po-2027 | build NTL + subprocess, ~30 min pour 92 |
| **P2.a Lean/Mathlib** | hors-scope, autre lane | P2.c formalisation |
| **P5 stress 500 premiers** | hors-scope | `make_primes(count=500)` |

## 6. Conclusion

Tranche Python-only **PASS** : 92 premiers dérivés, 10809 stopping indices calculés, 2130 exact_binomial_checks vérifiés, 43 quarter_cross_checks validés, **0 désaccord** entre les deux implémentations Python indépendantes. Harvey C++ (passe 2) doit confirmer la cohérence 4-voies avec les backends Python + BSGS.

— Rapport rédigé par `myia-po-2023:CoursIA-2`, c.1101, lane worker, 2026-10-06.
Loading
Loading