fix(lean,#15742): seuil R3 — énoncer le contrat réel (< 2 modèle, bande à 2 au replay)

docs/lean/life-components-schema.md

@@ -168,11 +168,17 @@ exactement une satisfait la congruence — le test de non-régression l'exige.
 ### Fenêtres spatiales (R3)
 
 Deux événements aux fenêtres spatiales chevauchantes, ou dont un objet vivant
-passe à moins de 3 (Chebyshev) des cellules d'une fenêtre étrangère, sont
+passe à moins de 2 (Chebyshev) des cellules d'une fenêtre étrangère, sont
 rejetés — avec une exception structurelle : un produit est *par construction*
 la dernière image de la fenêtre de son propre événement, il n'est jamais
 confronté à elle (le replay aux bornes exactes couvre déjà cette transition).
-Le seuil 3 n'est pas un réglage, c'est la mesure ci-dessous.
+La bande à distance exactement 2 passe l'élagage : l'interaction y dépend du
+contenu (mesure ci-dessous) ; c'est le replay de certification qui tranche —
+c'est lui, pas le modèle, qui produit `replay_rejected ≥ 1` sur la variante
+stricte de `two_blocks_catalyse`. Le seuil du modèle est donc 2 — à moins de
+2, les cellules sont dans le voisinage 3×3 l'une de l'autre, influence
+directe — tandis que 3 est la mesure physique de la non-interaction
+universelle, pas le seuil d'élagage.
 
 ### Dédup d'états (R1)
 
@@ -207,7 +213,10 @@ des confusions non fondées, pas par du travail évité. La sensibilité de la c
    n'interagissent jamais ; à distance 2, tout dépend du contenu. Deux blocs
    gap-1 sont stables, mais un glider à distance 2 d'un bloc engendre des
    naissances croisées — une cellule morte voit 2 voisins d'un objet plus 1 de
-   l'autre. Le seuil 3 de R3 est cette mesure, pas une heuristique.
+   l'autre. Cette mesure fixe les deux seuils : le modèle rejette sous 2
+   (influence directe, voisinage 3×3), et la bande contenu-dépendante à
+   exactement 2 est déléguée au replay de certification (cf §Fenêtres
+   spatiales).
 2. **Atteignabilité du placement déclaré.** Le placement tranche 1+2 de
    `block_catalyses_glider` démarrait au milieu de l'interaction : l'approche
    naturelle du glider annihile tout (population 0). La réaction a été

scripts/lean/life_compose.py

@@ -72,9 +72,14 @@
     measure_motif,
 )
 
-# Seuil de non-interaction de Conway : deux groupes de cellules à distance
-# de Chebysyshev >= 2 ne se voient pas. Gonfler chaque enveloppe de 1
-# matérialise exactement cette frontière.
+# Frontière d'influence directe de Conway : à distance de Chebyshev < 2, deux
+# groupes de cellules sont dans le voisinage 3x3 l'un de l'autre (rejet du
+# modèle) ; à distance exactement 2, seules des naissances croisées sont
+# possibles et tout dépend du contenu — la bande passe l'élagage et le replay
+# de certification tranche ; à distance >= 3, jamais d'interaction (mesuré,
+# test_chebyshev_3_est_sur_sans_interaction). Gonfler chaque enveloppe de 1
+# fait entrer toutes les paires à distance <= 2 dans le contrôle exact, qui
+# rejette alors à < 2.
 GROW = 1
 
 DEFAULT_NODE_BUDGET = 200_000
@@ -792,9 +797,11 @@ def _spatial_ok(
                     ra = swept_rect(catalog, a, 0, t_end)
                     rb = swept_rect(catalog, b, 0, t_end)
                     if ra and rb and _rects_overlap(_grown(ra), _grown(rb)):
-                        # emprises proches : contrôle exact, instant par instant
-                        # (deux blocs séparés d'une colonne sont à Chebyshev 2 :
-                        # non-interaction réelle que les rectangles se touchent)
+                        # emprises proches (Chebyshev <= 2) : contrôle exact,
+                        # instant par instant. Rejet à < 2 (influence directe) ;
+                        # la bande à exactement 2 (naissances croisées possibles
+                        # seulement) coexiste et sera tranchée par le replay de
+                        # certification.
                         for t in range(max(t_start(a), t_start(b)), t_end + 1):
                             if _min_chebyshev(
                                 cells_at(catalog, a, t), cells_at(catalog, b, t)

scripts/lean/tests/test_life_compose.py

@@ -328,6 +328,49 @@ def test_elagage_rejette_le_spawn_dans_la_fenetre() -> None:
     assert not s._spatial_ok(state0, (gspawn, bspawn), ev1, consumed)
 
 
+def test_elagage_r3_bande_chebyshev_2_passe_le_modele() -> None:
+    """Contrat R3 du code (schéma §Fenêtres spatiales) : le rejet du modèle
+    tombe à < 2 (influence directe, voisinage 3x3) ; la bande à exactement 2
+    passe l'élagage — c'est le replay de certification qui tranche
+    (naissances croisées contenu-dépendantes, cf la leçon mesurée)."""
+    state0, _, ev0 = _state_after_e0()
+    goal = lc.OBJECTIVES["two_blocks_catalyse_free"]
+    s = lc.Searcher(CATALOG, goal, node_budget=10)
+    reaction = CATALOG.reactions[ev0.reaction_id]
+    window_ever: set = set()
+    for cells in lc.reaction_window_cells(CATALOG, reaction, ev0.offset):
+        window_ever |= cells
+    block_phase0 = lc._motif_phases(CATALOG, "block")[0]
+
+    def block_cells(anchor: tuple[int, int]) -> set:
+        return {(x + anchor[0], y + anchor[1]) for (x, y) in block_phase0}
+
+    def in_clearance(cell: tuple[int, int]) -> bool:
+        for x0, y0, w, h in reaction.clearance:
+            abs_rect = (x0 + ev0.offset[0], y0 + ev0.offset[1], w, h)
+            if lc._rect_contains_cell(abs_rect, cell):
+                return True
+        return False
+
+    def anchor_at_distance(d: int) -> tuple[int, int]:
+        for x in range(-8, 24):
+            for y in range(-8, 24):
+                cells = block_cells((x, y))
+                if lc._min_chebyshev(cells, window_ever) == d and not any(
+                    in_clearance(c) for c in cells
+                ):
+                    return (x, y)
+        raise AssertionError(f"aucune ancre de bloc à distance {d} hors clearance")
+
+    consumed = {lc.handle_key(b) for b in ev0.bindings}
+    # distance 1 : bande d'influence directe -> rejet par le modèle
+    b1 = lc.Spawn("block", anchor_at_distance(1), 0)
+    assert not s._spatial_ok(state0, (b1,), ev0, consumed)
+    # distance exactement 2 : passe l'élagage, le replay décidera
+    b2 = lc.Spawn("block", anchor_at_distance(2), 0)
+    assert s._spatial_ok(state0, (b2,), ev0, consumed)
+
+
 # ---------------------------------------------------------------------------
 # Budgets (critere 3 : contraintes bornées)
 # ---------------------------------------------------------------------------