A COLLATZ-DAMMROZE - Non-Ergodic Deterministic Local-Obstruction Framework - Review Package: Algebra-Total Part6-Aligned Audit

https://github.com/dammroze/collatz-dammroze-coq-review # Collatz–Dammroze Coq/Rocq Review Package ## Algebra-Total / Part6-Aligned Audit Release — May 2026IMPORTANT NOTICE ---- # Semantic independence audit: amplification vs tail-control This note addresses a specific objection about the proof architecture. The remaining objection is semantic: > Are the amplification lower bound and the Part6/tail-control upper bound genuinely non-circular proof sources, or is one side smuggling in information from the other? ## Required independence The independence required here is not independence from the `3n+1` map itself. Both bounds necessarily concern the same map. The required independence is non-circular separation of proof sources. That is, the lower-bound mechanism must not import the upper-bound conclusion, and the upper-bound mechanism must not import the lower-bound amplification conclusion or an equivalent obstruction-exclusion claim. ## Amplification source The amplification side is intended to derive its lower bound from the assumed existence of a global obstruction, together with local combinatorial mechanisms: - global obstruction hypothesis; - finite alphabet inside dyadic bands; - pigeonhole/repetition mechanism; - repeated local certificate; - witness/certificate block; - persistence of the local configuration; - deterministic lower amplification. This side is a combinatorial/local consequence of assuming an obstruction. It is not intended to use endpoint-budget bounds, sparse-residue upper bounds, or the Part6 tail-control conclusion. ## Tail-control / Part6 source The Part6/tail-control side is intended to derive its upper bound from the intrinsic algebraic structure of the Collatz map: - dyadic inverse / odd coefficient inverse modulo powers of two; - affine-prefix structure; - aligned residues; - sparse interval uniqueness; - dyadic class intersection; - modulus refinement; - finite-union dyadic stability; - endpoint-budget and multiplicative endpoint-budget accounting; - Regime A conditional glue; - two-regime recombination. This side is a structural upper-bound mechanism imposed by the map. It is not intended to use the amplification lower-bound conclusion, the repeated-witness conclusion, or the final obstruction-exclusion conclusion. ## Separation principle The intended separation is: Lower bound = combinatorial consequence of the obstruction assumption. Upper bound = structural constraint imposed by the map itself. The contradiction is valid only if these two proof sources meet at the final recombination/contradiction point, and not earlier through a hidden circular dependency. ## Review target A valid criticism should identify one of the following: an amplification lemma that imports a Part6/tail-control conclusion; a Part6/tail-control lemma that imports the amplification lower bound; a bridge file that assumes obstruction exclusion instead of deriving it; a coverage-matrix entry that overstates what has been proved; a theorem/definition whose antecedent is equivalent to the final conclusion. Suggested issue format: File: Theorem/Lemma/Definition: Line number: Command run: Observed output: Claimed leakage/circularity: Reason: ## Current position The current repository should be read as: Coq/Rocq dependency ledger + algebra-total / Part6-aligned audit layer + semantic-independence review target The bookkeeping is intended to be not only syntactically explicit, but adversarial enough to let reviewers test whether the lower and upper mechanisms are genuinely separated proof sources rather than the same argument repackaged twice. ------------------------------------------------------------------------------------------------------------------------This Zenodo record archives the current Coq/Rocq, LaTeX, PDF, audit, and documentation package for technical review of the Collatz–Dammroze non-ergodic local obstruction framework for the \(3n+1\) map. GitHub repository: https://github.com/dammroze/collatz-dammroze-coq-review GitHub Actions: https://github.com/dammroze/collatz-dammroze-coq-review/actions --- ## Current release focus This release updates the repository with a consolidated algebra-total audit layer aligned with the existing Part 6 TeX-first proof route. The release includes: - the LaTeX manuscript and generated PDF;- Coq/Rocq `.v` files;- accepted v20/v21 ledger files;- algebra-total generic Coq layers;- Part6-aligned bridge files;- a global Part6-aligned algebra monolith;- SHA256 audit hashes;- GitHub Actions build verification;- coqdoc-generated HTML documentation;- a small optional Alectryon audit for selected Coq files;- final algebra status and coverage documentation. The proof-bearing checks remain: - `coqc`;- `coqchk`;- GitHub Actions CI;- SHA256 audit hashes;- Coq/Rocq source files;- TeX/PDF manuscript. --- ## Important clarification about Alectryon Alectryon is used only as an optional reviewer-facing presentation layer. The incomplete full-site Alectryon audit was intentionally removed from the proof package because the available SerAPI/sertop environment was Coq 8.20.x while the proof-bearing repository is built and audited under Coq 8.18.0. To avoid confusing reviewers, this release does **not** claim a complete full-site Alectryon audit. Instead, the release includes: - `audit/coqdoc_v1/` — full coqdoc HTML documentation;- `audit/alectryon_v1/` — small optional Alectryon rendering for selected Coq files with clean logs. These HTML renderings do not replace the proof-bearing checks. --- ## Algebra-total / Part6-aligned status The current repository separates the algebra layer into four categories: 1. **DONE-SANITY** Narrow algebra sanity checks for specific objections. 2. **DONE-GENERIC** General Coq algebra theorems already formalized. 3. **DONE-GLUE / PART6-ALIGNED** Existing TeX-first Part 6 proof-bearing glue exposed through algebra-total bridge files. 4. **NOT CLAIMED** Items not yet independently re-proved from first principles as standalone generic Coq theorems. The main global algebra bridge is: ```textcoq/Collatz_Dammroze_Algebra_Total_Part6_Global_Monolith_v1.v It collects the Part6-aligned bridges for: dyadic inverse / odd coefficient inverse modulo powers of two; affine-prefix step and induction; aligned residue counting and sparse interval uniqueness; dyadic class intersection; modulus refinement; finite-union dyadic stability; endpoint-budget and multiplicative endpoint-budget; Regime A conditional glue; two-regime budget recombination; internal solution total closure. This release does not present a newly invented parallel gcd(3^s, 2^K)=1 proof route as the proof-bearing path. The formal route exposed in the repository is the existing Part 6 TeX-first chain, surfaced through algebra-total bridge files and a global monolith. Critical reader advisory This manuscript must be read in the order specified by its internal Reader’s Guide / Logical Map. The framework is not probabilistic, not ergodic, not statistical, and not based on global averaging. It does not use: ergodic theory; probability theory; mixing; independence assumptions; Cesàro averaging; statistical limits; global random-walk heuristics; typical-behavior reasoning. The intended review object is a finite deterministic non-ergodic obstruction-exclusion chain. A critique that imports probabilistic, ergodic, averaging, independence, or mixing assumptions into the framework is not reviewing the stated proof object. It is reviewing a different framework. Core mechanism The proof framework is a finite, local, non-ergodic contradiction engine. In compressed form: Assuming a global Collatz obstruction exists, one derives a finite locally admissible obstruction certificate inside dyadic bands. The manuscript’s proof route then excludes such certificates through deterministic local arithmetic constraints, affine-prefix structure, aligned residues, sparse interval uniqueness, endpoint-budget bounds, and two-regime recombination. Therefore, the obstruction class is excluded. This is not an “almost all”, “typical orbit”, or average-case argument. It is intended as a deterministic local-obstruction exclusion argument. Main review files Key documentation files include: README.mdREFEREE_READING_GUIDE.mdTEX_COQ_ALIGNMENT_REPORT_FOR_REFEREES.mdREADING_ORDER_EXTRACTION_AUDIT.mdALGEBRA_TOTAL_FINAL_STATUS.mdALGEBRA_TOTAL_COVERAGE_MATRIX.mdALGEBRA_TOTAL_FORMALIZATION_ROADMAP.mdPART6_DYADIC_INVERSE_ALIGNMENT_NOTE.mdALECTRYON_STATUS.md Key Coq/Rocq files include: coq/Collatz_Dammroze_CoqLedger_v20_ACCEPTED.vcoq/Collatz_Dammroze_CoqLedger_v21_ACCEPTED.vcoq/Collatz_Dammroze_Final_Coq3_LocalDrop_Closure_v1.vcoq/Collatz_Dammroze_Final_Theorem_FromTex_v1.vcoq/Collatz_Dammroze_InternalSolution_TotalClosure_v1.vcoq/Collatz_Dammroze_Algebra_Total_Part6_Global_Monolith_v1.v The repository also includes coqdoc HTML documentation under: audit/coqdoc_v1/ and selected Alectryon HTML rendering under: audit/alectryon_v1/ Coq/Rocq build status The GitHub repository includes passing GitHub Actions checks for: Coq build; Coq3 non-ergodic local-drop closure. Local reproduction: git clone https://github.com/dammroze/collatz-dammroze-coq-review.gitcd collatz-dammroze-coq-review/coqcoqc --versioncoq_makefile -f _CoqProject -o Makefilemake clean || truemake -j1 The repository also includes audit folders with SHA256 checksums for the relevant proof, documentation, and release artifacts. Review request This Zenodo record and its companion GitHub repository are open for technical review. The requested review concerns: Coq/Rocq soundness; assumption depend