algo/docs/features/collatz_refinement_certificate_modular.md

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.
• applications/collatz/collatz_k_scripts/collatz_build_refinement_bundle_over_Sm_multilevel.py
  • wrapper pipeline: multilevel closure + open-roots obstruction profile + optional targeted diagnostic (tracked roots file).
  • can optionally include brother-derived D_minor leaves (--include-brother-derived-dminor) and verify them (--verify-brother-derived-dminor).

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}:

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