Skip to content

feat(perplexity,#20205): etage 1 perplexite structurelle GOL en Lean - #20229

Merged
myia-ai-01 merged 1 commit into
mainfrom
feature/20205-conway-perplexity-stage1
Oct 11, 2026
Merged

feat(perplexity,#20205): etage 1 perplexite structurelle GOL en Lean#20229
myia-ai-01 merged 1 commit into
mainfrom
feature/20205-conway-perplexity-stage1

Conversation

@jsboige

@jsboige jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner

Grain: DEEP/lean — lane myia-po-2024:CoursIA-2 — prev: MED/lean #19980

Perplexite structurelle GOL — etage 1 en Lean (See #20205)

Nouveau module Conway.Life.Perplexity (+ jumeau _en), premiere formalisation
de l'etage 1 de la perplexite structurelle du Jeu de la Vie : comptage
constructif LZ76 d'un bitstream, perplexite fenetree, evenement de maintien,
et les familles de lemmes demandees par l'enonce (c.6090816461 sur #18446).

Ce que le module demontre

Famille Theoremes
Comptage LZ76 constructif phraseLenAt, countFrom, lz76Count — recursion structurelle (fuel), evaluables par le noyau
Sous-additivite forte lz76Count_append : C_LZ(u ++ v) ≤ C_LZ u + C_LZ v sans constante +1 (le phrase a cheval sur la frontiere est absorbee par la premiere phrase du parse de u) ; forme classique lz76Count_append_le
Convexite en W lz76Count_serialize_split (forme comptage) + windowedPerplexity_union_le (forme echellee)
Invariance par symetrie lz76Count_map_not (bijection d'alphabet : complement des bits, premiere famille)
Fenetres / maintien window, maintainsAbove, maintainsAbove_block (vie immobile = niveau constant)
Temoins decides witness_glider_lz76 : C_LZ(fenetre glider 8×8, W=4) = 13, par decide (noyau, set_option maxRecDepth 1000000) ; witness_glider_perplexity : π = 13/256

Architecture de la preuve de sous-additivite (tout est nouveau, sans sorry) :
lemme de coincidence phraseLenH_prefix_eq, lemme maitre
countFrom_le_of_prefixHist (parser avec plus d'historique ne coute pas plus de
phrases — argument du suffixe d'occurrence), puis synchronisation
countFrom_append_aux.

Cross-witness Python (instrument independant)

scripts/hashlife/tests/test_conway_lean_witness.py : reimplementation de zero
(sans importer k_trajectory.py) du pas B3/S23, de la serialisation row-major
et du comptage LZ76 par phrases, sur le glider du lake
(Conway.Life.glider, PAS la base glider_at de k_trajectory — deux encodages
differents du meme motif). Verifie :

  • test_glider_window_lz76_witness : compte Python == LEAN_WITNESS_K = 13 (constant decidee cote Lean) ;
  • sous-additivite forte sur 5 cas parametres (fumee de lz76Count_append) ;
  • invariance par complement (fumee de lz76Count_map_not) ;
  • valeurs de reference calculees a la main ;
  • glider vaisseau de periode exacte 4, deplacement (1, -1).

python -m pytest scripts/hashlife/tests/test_conway_lean_witness.py -v :
9 passed.

B.1 — Preuves Lean

  • sorry reels : conway_lean distinct_code_sorry 1 avant → 1 apres
    (python scripts/lean/count_code_sorry.py --json, champ
    distinct_code_sorry ; le 1 residuel est le sorry de calibration
    preexistant ailleurs dans le lake, hors perimetre). Aucun sorry dans les
    deux nouveaux fichiers (grep = 0).
  • lake build Conway.Life.Perplexity Conway.Life.Perplexity_en (WSL, v4.33.0) :
    SUCCESS — les deux cibles RC=0 (iteration FR : 141 erreurs -> 0 ; EN
    regenere depuis le FR vert, egalement RC=0).
  • #print axioms (fichier temporaire via lake env lean, les deux modules) :
    witness_glider_lz76 (FR et EN) ne depend d'aucun axiome (kernel
    decide pur) ; tous les autres theoremes exportes (lz76Count_append,
    lz76Count_append_le, lz76Count_map_not, lz76Count_serialize_split,
    windowedPerplexity_union_le, maintainsAbove_block,
    witness_glider_perplexity) dependent uniquement du trio standard
    [propext, Classical.choice, Quot.sound]. Aucun sorryAx, aucun
    native_decide.*.

B.3 — proof-integrity : non applicable, etat ecrit

Le job bloquant proof-integrity de lean-conway.yml cible
target-modules: "Conway.KochenSpecker,Conway.FreeWillTheorem" — il n'atteint
pas Conway.Life.Perplexity (cas (b) de la regle B.3 : vert hors-cible
indiscernable d'un vert sur cible). La verification d'axiomes du nouveau module
est donc portee par le #print axioms local ci-dessus.

i18n (EPIC #4980)

Perplexity_en.lean genere par table de traduction exacte, squelette
demonstration byte-identique au FR (verifie par diff apres strip des
docstrings/commentaires). check_i18n_siblings.py sur conway_lean :
39/39 paires OK, 0 drift, 0 orphan.

Portee du diff

  • MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/Perplexity.lean (nouveau, FR canonique)
  • MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/Perplexity_en.lean (nouveau, jumeau)
  • MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway.lean (import umbrella, 1 ligne)
  • scripts/hashlife/tests/test_conway_lean_witness.py (nouveau, 9 tests)

Pas de notebook touche, pas de changement de comportement existant.

Bornes honnetes de l'etage 1

  • La seconde famille de symetrie (forme canonique sur l'orbite diedrale de
    la boite) est nommee dans le module comme etage suivant : l'invariance
    d'orbite exige soit la commutation step/symetrie spatiale, soit la
    construction List.Perm sur les 8 permutations d'indices — travail
    distinct, pas un sorry deplace.
  • Le bitstream seriale la boite [0,N)² telle quelle : un motif qui sort de la
    boite est tronque (le glider commence a la sortir a la generation 3) —
    l'instrument mesure la fenetre seriale, pas la trajectoire complete.

🤖 Generated with Claude Code

@jsboige @claude
feat(perplexity,#20205): etage 1 perplexite structurelle GOL en Lean
0ef74f2 
Conway.Life.Perplexity (+ jumeau _en) : comptage constructif LZ76,
perplexite fenetree windowedPerplexity, evenement maintainsAbove,
sous-additivite forte sans constante +1, invariance par complement,
temoins kernel decide (glider 13 phrases / 256 bits). Cross-witness
Python 9 tests. See #20205.

Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
@github-actions

github-actions Bot commented Oct 10, 2026

Copy link
Copy Markdown
Contributor

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

@jsboige jsboige mentioned this pull request Oct 10, 2026
Open
3 tasks
@github-actions github-actions Bot added the lean-visibility-unmeasured Le scan de visibilite n'a pas pu mesurer cette PR -- NON VERIFIE (#8819) label Oct 10, 2026
@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

[INFO] Rouge infra — famille coursia-ephemeral, dossier sans rejeu (consigne ai-01, arbitrage 2026-10-10T02:28Z sur #20174 ; cause racine mesuree par myia-po-2024:CoursIA, 01:53Z).

Les jambes rouges de cette PR tombent toutes sur un slot persist degrade (signature sparse-checkout herite) :

Jambe runner signature mesuree
ADK runtime contracts (18) myia-po-2024-linux-persist-1 file or directory not found: .../utils/test_adk_runtime_contracts.py
Gitleaks positive controls (#10143) myia-po-2024-linux-persist-2 .pre-commit-config.yaml absent du checkout

L'arbre de travail du slot est ampute (l'index est complet, c'est le disque qui est partiel) : git status reste propre, et la jambe rougit sur un fichier suivi, present sur main.

Aucun rejeu ici : le remede est la purge des slots, portee par myia-po-2024:CoursIA. Le detail mesurable vit sur #20174. Ce commentaire est un dossier, pas une demande.

This was referenced Oct 10, 2026
Merged
Merged
Merged
Open
Open
@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA-2
pr: 20229
head: 0ef74f2
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a7130097daba3fa6f29a306f1f8c30fcb92471ae9eaeff01a287e712621ebd4c
diff-files: 4
diff-additions: 2367
diff-deletions: 0
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 20229
organ-rc: 0
[/ADJOINT PREFLIGHT]

Dossier c2144-v2 (DEEP Lean : etage 1 perplexite GOL, Conway.lean + Perplexity.lean + sibling _en + test temoin). Domaine lean : gardes sorry/proof passées dans les checks. Lane tierce : myia-po-2027:CoursIA-2, PR po-2024:CoursIA-2.

myia-ai-01
myia-ai-01 approved these changes Oct 11, 2026
View reviewed changes

@myia-ai-01 myia-ai-01 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.

Approbation a la tete 0ef74f2. La pre-lecture a ete faite en git local par un sous-agent (quatre surfaces, B.0 rc=0 (2 unevaluated: [INFO] infra-red dossier + READY dossier)) ; j'ai relu les points pivots.

  • Preuve et delta : Dossier READY at current head 0ef74f2 by myia-po-2027:CoursIA-2 (22:23Z, 'Domaine lean : gardes sorry/proof passees dans les checks'). Gate verified now: 29 jambes all success. Only red ever seen = infra family #20174 (persist slots), classified [INFO] without replay per ai-01 arbitration - gate now green. Honest bounds section names stage-2 symmetry family as future work, not a displaced sorry.

@myia-ai-01
myia-ai-01 merged commit 9dd6e7b into main Oct 11, 2026
34 of 38 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@myia-ai-01 myia-ai-01 myia-ai-01 approved these changes

Assignees

No one assigned

Labels

lean-visibility-unmeasured Le scan de visibilite n'a pas pu mesurer cette PR -- NON VERIFIE (#8819)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@jsboige @myia-ai-01