**Auteur** : Équipe 4NK

# Collatz — Refinement certificate at palier 2^M (instrumented domain L)

## Objective

Provide a deterministic, versionable artefact that makes “decidability from a coarse observable” explicit.

At palier \(2^M\), the modular register \(K_M\) only retains clauses with `stable_modulus_power <= M`.
When most witnesses require `m_stable > M`, an alternative is to keep \(M\) as the *root observable*
and record a finite refinement path to a finer modulus where a terminal clause \(D/F\) applies.

This feature builds and audits such refinement paths on the instrumented finite domain \(L\)
(the C3 witness domain), without claiming a global certificate on \(S_M\).

## Impacts

- Adds new versioned artefacts under `docs/artefacts/collatz/refinement_K/`.
- Does not change the extraction of terminal clauses (Option A); it reuses `clauses_universelles.json`.

## Modifications

### Script

- `applications/collatz/collatz_k_scripts/collatz_build_refinement_certificate_modular.py`
  - reads `clauses_universelles.json` (Option A) and the referenced C3 verification JSON,
  - for each `n` in the C3 domain \(L\), records a deterministic refinement path from \(n mod 2^M\)
    to the terminal stable residue at \(2^{m_{stable}}\),
  - produces a summary audit (depth buckets, max depth).

### S_M variant (full odd residue space)

- `applications/collatz/collatz_k_scripts/collatz_build_refinement_certificate_over_Sm.py`
  - reads `clauses_universelles.json` (Option A),
  - attempts to close the full refinement tree for each root residue in \(S_M\) using the finite
    set of terminal clauses, producing a closed/open partition of \(S_M\).

### S_M multilevel variant (root M to max M_max)

- `applications/collatz/collatz_k_scripts/collatz_generate_terminal_clauses_over_Sm.py`
  - generates terminal clauses directly decidable at \(2^m\) (criterion \(A+1\le m\)) on the full \(S_m\).
- `applications/collatz/collatz_k_scripts/collatz_build_refinement_certificate_over_Sm_multilevel.py`
  - closes roots in \(S_M\) by refinement up to \(2^{M_{max}}\) using leaf sets provided at multiple levels.

### Artefacts

For palier \(M\):

- `docs/artefacts/collatz/refinement_K/palier2pM/refinement_certificate_mod2pM.json`
- `docs/artefacts/collatz/refinement_K/palier2pM/refinement_certificate_mod2pM.md`
- `docs/artefacts/collatz/refinement_K/palier2pM/audit_refinement_certificate_mod2pM.json`
- `docs/artefacts/collatz/refinement_K/palier2pM/audit_refinement_certificate_mod2pM.md`

For palier \(M\) (S_M variant):

- `docs/artefacts/collatz/refinement_K/palier2pM/refinement_certificate_Sm_mod2pM.json`
- `docs/artefacts/collatz/refinement_K/palier2pM/refinement_certificate_Sm_mod2pM.md`
- `docs/artefacts/collatz/refinement_K/palier2pM/audit_refinement_certificate_Sm_mod2pM.json`
- `docs/artefacts/collatz/refinement_K/palier2pM/audit_refinement_certificate_Sm_mod2pM.md`

For palier \(M\) (S_M multilevel variant):

- `docs/artefacts/collatz/terminal_clauses_over_Sm/palier2p<m>/clauses_terminal_over_Sm_mod2p<m>.{json,md}`
- `docs/artefacts/collatz/refinement_K/palier2pM/refinement_certificate_Sm_multilevel_mod2pM_to2pMmax.{json,md}`
- `docs/artefacts/collatz/refinement_K/palier2pM/audit_refinement_certificate_Sm_multilevel_mod2pM_to2pMmax.{json,md}`

## Deployment

No deployment. Local scripts only; artefacts are intended to be committed.

## Analysis / Reproduction

Example for palier \(2^{15}\):

```bash
python3 applications/collatz/collatz_k_scripts/collatz_build_refinement_certificate_modular.py \
  --palier 15 \
  --repo-root /home/ncantu/code/algo
```