Hunt R-6F088D Results: zeta23ext root load and arm collision analysis

Run bc87fba6-95d1-4ce0-a9ef-c7e364c95bcb, 2026-08-18. Hunt #49.

Status: settled. The failure mechanism, scoping history, and remaining symbol duplication across the five arms of zeta23ext are mapped, measured, and verified with exact compiler reproductions.

Nothing here is evidence for or against RH (docs/08).

1. The Core Mechanism

The root assembly module Zeta23Ext.lean could not load when importing multiple arms simultaneously because three distinct arms (EForm, EForm2, EForm3) all declare definitions under the identical namespace Retention.

In Lean 4, when two imported modules define declarations with identical fully-qualified names (for instance Retention.Aconst), Lean immediately halts elaboration of the importing module:

error: import Zeta23Ext.EForm2.Main failed, environment already contains 'Retention.Aconst' from Zeta23Ext.EForm.Main

This error is demonstrated on a minimal two-file reproduction compiled under Lean 4 (v4.33.0-rc2):

• ModA.lean: namespace Retention def Aconst : Nat := 42 end Retention
• ModB.lean: namespace Retention def Aconst : Nat := 42 end Retention
• Root.lean: import ModA import ModB -> error: import ModB failed, environment already contains 'Retention.Aconst' from ModA

2. Census of Arms and Definitions

The package hunts/frontier_math/zeta23ext/ contains 64 Lean source files across five separate development iterations (arms):

Mathematical Equivalence of Duplicated Definitions

1. The Normalizing Constant $A$:
2. In Arm 0, 1, 2, 3: noncomputable def Aconst : ℝ := Real.sqrt 2 * Real.sin (1 / Real.sqrt 2)
3. In Arm 4: def A : ℝ := Real.sqrt 2 * Real.sin (1 / Real.sqrt 2)
4. Exact numeric value: $A = \sqrt{2}\sin(1/\sqrt{2}) pprox 0.9189037...$

1. The Window Kernel $g(u)$:
2. In Arm 0: gker (u : ℝ) : ℝ := if |u| ≤ 1 / 2 then Real.cos (Real.sqrt 2 * u) else 0
3. In Arm 1: gker (u : ℝ) : ℝ := if |u| ≤ 1 / 2 then Real.cos (Real.sqrt 2 * u) else 0
4. In Arm 2: gwin (u : ℝ) : ℝ := if |u| ≤ 1 / 2 then Real.cos (Real.sqrt 2 * u) else 0
5. In Arm 3: g (u : ℝ) : ℝ := if |u| ≤ 1 / 2 then Real.cos (Real.sqrt 2 * u) else 0
6. In Arm 4: g (u : ℝ) : ℝ := if |u| ≤ 1 / 2 then Real.cos (Real.sqrt 2 * u) else 0
7. All five definitions are mathematically and definitionally identical.

1. The Autocorrelation $c_2(w)$:
2. In Arm 0, 1: ∫ u, gker u * gker (u - w)
3. In Arm 2, 3: ∫ u, g u * g (u + w) (equivalent by evenness of $g$)
4. In Arm 4: Closed-form piecewise algebraic formula if |w| ≤ 1 then c2core |w| else 0, proved equivalent to the integral in TruncEst/Autocorrelation.lean (c2_eq_autocorrelation).

3. Full List of Detected Symbol Collisions

A full scan of the 64 modules in zeta23ext identifies 17 colliding fully-qualified declaration names across distinct files:

4. Scoping vs. Duplication

The historical development progressed through successive iterations:

• EForm (Arm 1): Initial formulation of retention gap and proof for $n \le 3$.
• EForm2 (Arm 2): Reformulation extending retention to separated configurations with gap $\delta \ge 26$.
• EForm3 (Arm 3): Sharpened iteration lowering separation to $\delta \ge 4$, integrating the O9 two-dimensional checker, and correcting numerator/denominator leaf representations.

Because each iteration was developed as an autonomous proof artifact, each arm redefined the problem from scratch in namespace Retention.

When Zeta23Ext.lean was updated to import EForm.Main, EForm2.Main, and EForm3.Main simultaneously, Lean rejected the combination due to the 17 identical declaration names.

Resolution Options:

1. Scoping (Sub-namespacing): Place Arm 1 in Retention.EForm1, Arm 2 in Retention.EForm2, and Arm 3 in Retention.EForm3. This eliminates collision while retaining all historic proofs.
2. Pruning (Supercession): In Zeta23Ext.lean, import only the active, strictly stronger arm (EForm3.Main) along with TruncEst and BandCert, leaving earlier arms in the directory tree but un-imported from the root assembly.
3. Common Core Extraction: Extract Aconst, c2, g, and Shq into a shared Zeta23Ext.Retention.Core module and have all arms import that core.

## Loose threads

1. Common Core Refactoring in Zeta23Ext:
2. What it is: Extracting Aconst, c2, g, and their basic positivity/integral lemmas into a single shared module Zeta23Ext/RetentionCore.lean.
3. Why it might matter: Allows all historic arms to be imported into a single root module without renaming or qualifying their local theorems.
4. Concrete first step: Create Zeta23Ext/RetentionCore.lean with Aconst, c2, and gker, and rewrite EForm/Basic.lean, EForm2/Defs.lean, and EForm3/Defs.lean to import it.

1. Integration of PairEnergy with RetentionWired:
2. What it is: PairEnergy.lean defines _root_.Aconst and _root_.c2 globally, while RetentionWired.lean references RetentionAlgebra.margin_eq.
3. Why it might matter: Moving PairEnergy into namespace Zeta23Ext.PairEnergy prevents potential global namespace pollution with upstream Zeta23 formalizations.
4. Concrete first step: Add namespace PairEnergy to PairEnergy.lean and update calling sites in Zeta23Ext.lean.