Spezia's Pell circulant permanent-to-determinant ratio

Stefano Spezia's OEIS A392131, revision 16, FORMULA states:

Conjecture: lim_{n->oo} A392132(n)/a(n) = 1.

OEIS A392132, revision 10, FORMULA states the same conjecture as:

Conjecture: lim_{n->oo} a(n)/A392131(n) = 1.

In A392131, $a(n)$ is the signed determinant; in A392132, $a(n)$ is the permanent. These are two records of one assertion. The source is OEIS-only, submitted in 2025 and published in 2026, with no source DOI or arXiv identifier. Issue #21886 fixes the conventions and the settlement criterion. The source quotations and locators are in the Library note.

Statement echo

Let $P_0=0$, $P_1=1$ and $P_{k+2}=2P_{k+1}+P_k$. With indices in $\operatorname{Fin}(n)$, the matrix is $C_n(i,j)=P_{n-1-\operatorname{val}(i-j)}$, with natural subtraction truncated at zero and modular subtraction in $i-j$. Its first row is $(P_{n-1},P_0,\ldots,P_{n-2})$, the initial right rotation specified by the source COMMENT and four-by-four EXAMPLE. The formalization reuses the existing Pell sequence D5.S1.Recurrence.PellCompanionGcd.P and Mathlib's Matrix.circulant, Matrix.det and Matrix.permanent.

| Source clause | Formal counterpart | | --- | --- | | A392131 COMMENT: first column reversed Pell vector, first row initially rotated right | C, with the literal binding vector and Mathlib's modular circulant indexing | | A392131 determinant, including the source empty value | A392131 n = Matrix.det (C n); the determinant retains its sign | | A392132 permanent of the same matrix | A392132 n = Matrix.permanent (C n) | | The ratio tends to one | claim: every real $\varepsilon>0$ admits $N\ge2$ such that every $n\ge N$ has $|A392132(n)/A392131(n)-1|<\varepsilon$ | | No additional matrix-family hypothesis | result : claim has no hypotheses |

The threshold condition $N\ge2$ specifies an equivalent tail of the limit; it imposes no extra condition on the sequence. Both empty values are one. The zero determinant at $n=1$ does not affect a tail assertion.

The conjecture compares the unsigned sum over permutation products with its signed counterpart for a dense, sequence-defined matrix. Normalization reveals a unit diagonal and geometrically decreasing off-diagonal weights. A uniform estimate on all nontrivial cycles explains why both permutation sums approach the identity contribution.

The bounded source and literature screen recorded in #21886 found no settlement of this exact ratio in its searched scope. Related Pell-circulant papers concern determinants, inverses or norms; the read circulant-permanent papers concern other fixed-band or dense scalings. The unread relevant works, blocked endpoints, metadata-only screens and incomplete citing-work closure remain explicit boundaries. The literature status is not-found-in-searched-scope; completeness is ASSUMED-UNVERIFIED.

Write $B_n=C_n/P_{n-1}$ for $n\ge2$. The helper names below are private declarations of D5.S3.Combinatorics.Permanental.SpeziaA392131PellCirculantRatio.

1. pell_ratio_bounds, pell_growth and pell_entry_majorant give the off-diagonal estimate normalized_entry for $n\ge3$: at positive displacement $d$, the entry of $B_n$ is at most $(6/5)(12/5)^{-d}$. The helper normalized_diagonal proves its diagonal is one for $n\ge2$. The Pell recurrence and companion positivity are reused from PellCompanionGcd.
2. cycleCode_injective and composition_code_injective reconstruct a nontrivial cycle from a moved root and its positive modular displacement composition. The total displacement is a positive multiple of $n$. fixed_length_composition_count uses the imported CrownOrderPolytopeEnumeration.fixedLengthCompositionEquiv for the composition count.
3. cycle_activity_index_le and cycle_activity_le sum the weighted composition bounds, obtaining $S_n\le(6n/11)(11/12)^n/(1-(11/12)^n)$. cycleBound_tendsto shows this majorant tends to zero.
4. one_le_permanent and permanent_le_exp_activity squeeze the normalized permanent between $1$ and $\exp(S_n)$. determinant_error_le_permanent_error bounds $|\det(B_n)-1|$ by $\operatorname{per}(B_n)-1$.
5. normalized_permanent_tendsto and normalized_determinant_tendsto give the two limits. normalized_ratio cancels their common scalar factor, and result supplies the exact epsilon-threshold assertion.

A different initial rotation or an absolute determinant in the denominator would describe a different claim. C uses the source's initial rotation, and A392131 uses the signed determinant. The four-by-four matrix has first row $(5,0,1,2)$, determinant $640$ and permanent $772$.

Finite agreement does not prove convergence. The all-index conclusion follows from the compiled cycle-activity estimate and the normalized limits, without assuming positivity of every finite determinant. The limit implies eventual nonvanishing; positivity for every $n\ge2$ is a separate question.

Canonical module: D5/S3/Combinatorics/Permanental/SpeziaA392131PellCirculantRatio.lean. Its public theorem is result : claim; its public definitions are C, A392131, A392132 and claim. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

Frozen state: Golden/Frozen/state/D5/S3/Combinatorics/Permanental/SpeziaA392131PellCirculantRatio.lean.json.

Escape audit unfinished: #22411, for the sole public theorem result. The existing templates do not supply this delivery with a compiled reconstruction and intervention bridge for the full alternating epsilon-threshold assertion. No declared_validated registration is claimed.

Finite source-fidelity experiment

The pinned experiment directory contains check.py, SHA-256 d15fb92594c83cd80aa1092ad28bcfa4fa4963b61867dfc46f05398b2fd9a32c. The command, run in this worktree, is git -C ../trureturing-experiments show 0938258013ceeef91cdfa39de81dad341e6755cf:docs/reports/spezia-pellcirc/check.py | python3, with pipeline failure propagation enabled; exit 0, final result ALL_CHECKS_OK.

The finite scope is source terms at indices $0$ through $13$; exact determinant and permanent calculations through $n=16$, with Ryser cross-checks through $n=9$ and permutation cross-checks through $n=8$; Pell entry majorants through index $200$; positive-composition totals through $17$; simple directed cycles for $3\le n\le8$; and the cycle-product comparison for $3\le n\le6$. It also computes rational tail estimates at $n=50,100,200,500,1000$. These computations do not establish a uniform extension beyond their tested ranges.

Tier 1 external named OEIS FORMULA conjecture; resolution Proved; admission_basis: open-problem-resolution (#21886; Proved). There is no digestion atom.

What the settlement shows

| Item | Status and evidence | | --- | --- | | Binding Pell circulant ratio, source rotation and signed determinant | Proved, kernel-checked result | | Fixed-constant activity estimate for any nonnegative matrix on $\operatorname{Fin}(n)$, $n>0$, satisfying the off-diagonal bound $(6/5)/(12/5)^{\operatorname{val}(i-j)}$ | Proved, kernel-checked private cycle_activity_le; no unit-diagonal hypothesis occurs in this estimate. Unit diagonal is a hypothesis of one_le_permanent and permanent_le_exp_activity. | | Normalized permanent and determinant individually tend to one; $1\le\operatorname{per}(B_n)\le\exp(S_n)$ and $|\det(B_n)-1|\le\operatorname{per}(B_n)-1$ | Proved, kernel-checked private normalized_permanent_tendsto, normalized_determinant_tendsto, one_le_permanent, permanent_le_exp_activity and determinant_error_le_permanent_error | | Source terms through index $13$; $n=4$ determinant $640$, permanent $772$; exact matrices through $n=16$ and cycles through $n=8$ | Computed, the pinned experiment and exact scope above; command exit 0 and script SHA-256 as specified there | | Parameterized $q>1+c$ generalization | Open as a separately compiled theorem; the composition calculation suggests this sufficient condition, but the delivered theorem fixes $c=6/5$, $q=12/5$. | | Sharp asymptotic rate/constants, determinant positivity for every $n\ge2$, and further Fibonacci/Lucas/Jacobsthal source conjectures | Open in this delivery; the finite positivity checks do not supply an all-index theorem. | | Further source results conditional on the conjecture | Open literature boundary: none was identified in the recorded screen; this is no certificate of exhaustive closure. |

The decisive mechanism is that every nontrivial cycle accumulates at least one full cyclic displacement, while the geometric edge penalty exceeds the weighted number of compositions. The activity estimate applies beyond the source Pell matrix under the same fixed majorant; the unit diagonal enters the permanent comparison. The two OEIS formulas receive one common settlement. No further source theorem relying on the conjecture is identified in the searched scope.

Literature and citation completeness, unread related texts and later-author coverage remain ASSUMED-UNVERIFIED, as in #21886. The source is OEIS-only; no journal/arXiv source or DOI is asserted. The finite experiment is computational evidence, separate from the all-index Lean proof. The parameterized estimate, sharp asymptotics, all-index finite determinant positivity and other recurrence families remain outside this module's claims. The escape audit remains unfinished under #22411.