bibkey: norton2026a398542
authors: Charles Cornell Norton
year: 2026
title: "OEIS A398542: fixed-bottom polynomial conjecture"
doi: null
url: https://oeis.org/A398542
claim: "For every nonempty 132-avoiding bottom b of length m, its actual two-cell completion count is p(k)*binomial(2*k,k)+q(k)*4^k, with degree bounds m-1 and m-2."
strata_touched:
  - D5/S1/Words/Patterns/A398542FixedBottom
  - D5/S1/Words/Patterns/A398542MinimumRecurrence
  - D5/S1/Words/Patterns/A398542Polynomial
license: citation-only
triage: anchor

The fixed-bottom conjecture in A398542

Verified locator

The original entry is Charles Cornell Norton’s A398542, authored August 1, 2026. The inspected source is revision 18, August 30, 2026, 18:45:04, at https://oeis.org/A398542/internal. Its revision identifier, defining comments, and formula were retrieved directly on September 21, 2026. The selected formula is exactly:

Conjecture: for every m >= 1 and every b in S(m), d(b,k) = p(k)binomial(2k,k) + q(k)*4^k for polynomials p and q depending on b, with deg p <= m-1 and deg q <= m-2. Verified for m <= 6 and k <= 12.

The preceding formula defines S(m) as the 132-avoiding permutations of [m] and d(b,k) as the number of ways to complete the lower-left cell b with k points above it. The comments impose 1324 avoidance on the whole gridded permutation and 213 avoidance on that upper cell. Fixing this value cut means that d(b,k) counts actual permutations of 1,…,m+k whose lower-value subsequence is exactly b. The upper subsequence is standardized by subtracting m. The upper cell may be empty, so d(b,0)=1.

The formal conclusion chooses p_b,q_b in Q[X] before universally quantifying k in N. Rational coefficients are a sufficient, explicit choice; the OEIS sentence itself does not specify the coefficient field. It proves deg p_b <= m-1 and deg q_b <= m-2 for m>=2, and q_b=0 for m=1. Lean uses natDegree, including natDegree(0)=0, together with this explicit zero condition. Nat.centralBinom k is Nat.choose (2*k) k.

The preregistration and complete ordinary proof are in https://github.com/the-omega-institute/trureturing/issues/9332. The current allocation is the first-tier recent fixed-bottom conjecture, supported by that full ordinary proof. The historical tier-3/note-only assessment in oeis2026triage0911 is preserved unchanged. This conclusion does not enumerate unrestricted 1324 avoiders, determine the full L-gridding generating function, settle A398446, or constitute a second problem.

Bounded literature comparison

The bounded source audit recorded in issue #9332 inspected these bodies:

• Bevan, Brignall, Elvey Price and Pantone, arXiv:1711.10325v3, Theorem 3.1 and Section 7.4. Theorem 3.1 counts aggregate dominoes, summing over bottoms; it does not specify the coefficients for every fixed b. The interleaved-ascent description preceding that theorem is an existing ingredient, used here with attribution. Section 7.4 addresses harder three-cell enumeration.
• Norton’s official program, https://oeis.org/A398542/a398542.txt. Its forced-descent recursion supplies a computational description, not a uniform proof of the fixed-bottom pole-degree bound.
• Gil, Lopez and Weiner, arXiv:2311.18227v3. Its positional statistics concern different enumeration questions.
• Norton’s Coq source at commit 62f6e61766b30959acc0517f02ade5b30379319d, as identified in the source audit: its diagonal two_term_law is Admitted, and two_term_law_of_fibres assumes the necessary fibre identity in H3. Neither is imported as a supplier.
• arXiv:2608.20292v3, Definition 3.4, Lemma 3.5, Theorem 3.6 and its proof, Remark 3.7, and Proposition 4.5 and its proof. The fixed-z inequalities and aggregate sums do not establish the fixed-b polynomial coefficients.

No exact complete proof or refutation was found in those inspected bodies. This is the scope of the caller’s completed source audit; the delivery worker directly rechecked the OEIS source, not every audited paper. Worldwide priority is unverified and unclaimed. The distinction between an aggregate sum and every fibre is essential: an identity after summing over b does not determine each individual d(b,k).

Actual objects and the proof

All finite permutations are bijections of Fin(n), translated to the source’s 1,…,n by adding one. Contains is the existing generic increasing-position, relative-value-order predicate. Actual b k retains the actual permutation, literal lower list equality, whole 1324 avoidance, and standardized upper 213 avoidance. count b k is Nat.card of this subtype, not a recurrence.

An ordered shuffle is equivalent to a weakly increasing list of upper gaps in 0,…,m; equal gaps are allowed. Insertion and extraction are mutually inverse even when either alphabet is empty. Under the two cell avoidance conditions, the only possible mixed 1324 occurrence is a lower ascent interleaved with an upper ascent. The first later bottom endpoint above a prefix minimum defines dead(g), with sentinel m+2. Such an upper ascent from gap g to gap t is legal exactly when t<dead(g). In particular dead(0)=m+2 and g<dead(g); monotonicity of dead is neither asserted nor used.

actualEquiv identifies actual permutations with these configurations. Restricting every upper gap to [l,h] keeps the same entire bottom b. Splitting a nonempty upper permutation at its minimum gives left size a, right size c, root zero, left values shifted by c+1, and right values shifted by one. Both children avoid 213, either can be empty, and their actual configuration intervals are [l,g] and [g,min(h,dead(g)-1)]. The split is unique. Its cardinality gives N(l,h,0)=1 and, for every k>=0,

$$N(l,h,k+1)=\sum _{g=l}^h\sum _{a=0}^{k}N(l,g,a)N(g,\min (h,\mathrm{dead}(g)-1),k-a).$$

Here N is the cardinality of IntervalActual, and N(0,m,k)=d(b,k). Thus the recurrence is proved about actual objects.

In Q[[X]], let F(l,h) have these actual cardinalities as coefficients, C be the pinned Catalan series, s=1-2XC, and T=s^(-1). The inverse exists because the constant coefficient of s is one; Q[[X]] is not treated as a field. The recurrence gives the exact series equation and F(g,g)=C. For l<h<=m with h<dead(l), guarded_polynomial constructs

$$F(l,h)=TA(T),A\in \mathbb{Q}[X],\mathrm{natDegree}(A)\le 2(h-l)-2.$$

Endpoint terms contribute C F(l,h) and F(l,h) C. Interior children either satisfy the strict guard at smaller width or are singleton Catalan states. The identities s^2=1-4X, 4XT^2=T^2-1 and 2XCT=T-1 close the induction. The full interval is guarded because dead(0)=m+2.

The live coefficient proof applies the pinned Catalan, inverse-unit, binomial-series, central-binomial and ascending-Pochhammer APIs. Odd powers T^(2r+1) have coefficient binomial(2k,k) times a rational polynomial of degree r; even powers T^(2r), r>=1, have coefficient 4^k times a rational polynomial of degree r-1. The finite polynomial A gives witnesses depending on b alone, the two sharp degree bounds, and an empty even sum when m=1. No analytic convergence hypothesis, opaque computation, or unverified Coq theorem is used. A tree datatype and correctness of the separate official program are not required by, and are not conclusions of, this theorem.

Admission semantics

All five first-Freeze modules have utility: none: their mathematical content consists of uniform symbolic constructions and proofs. Literal finite patterns are definitions of the source predicates, not a delivered enumeration, numeric reduction, certified example, or checker result. The computational-use fields are not applicable. The declarations below are assessed relative to the protected baseline, not to pins created by this delivery. These are semantic assessments, not machine classifications.

• A398542FixedBottom.gap_spec: content / escape-witness; prefix-cardinality order and recovery of every upper position. contains1324_iff_mixed: content / escape-witness; all lower/upper occurrence cases reduced to the exact two-ascent obstruction. gap_criterion: content / escape-witness; existence of an intervening lower ascent is equivalent to the strict deadline condition, including both sentinel facts. The equivalence-valued definitions insertionEquiv, gapEquiv, and actualEquiv contain the mutually inverse constructions consumed in that chain. The remaining public definitions specify the objects, maps and actual cardinality; they add no companion theorem claims.
• A398542MinimumRecurrence.join_avoids_iff: content / escape-witness; a crossing occurrence is excluded using the forced value blocks. minimum_factorization: content / escape-witness; the minimum position forces both value sets and unique standardized factors. actual_cardinal_recurrence: content / escape-witness; the actual split equivalence with the same bottom yields both the finite convolution and full-interval identification. The definitions retain these actual types and implement their reconstruction.
• A398542Polynomial.actual_series: content / escape-witness; coefficient induction identifies all singleton states with the Catalan series. guarded_polynomial: content / escape-witness; the guarded width induction constructs the finite inverse-power span. result: content / open-problem-resolution, preregistered in #9332; the guarded construction and coefficient extraction settle exactly the quoted external assertion. Series definitions add no forwarding theorem.
• Separable.ProperCut is a previously unfrozen imported supplier. Its public avoidance_proper_cut and private p4_free_separation, disconnected_spans_cut, and induced_path_contains are content / escape-witness. Their live arguments construct a maximal disconnected subset, a convex root component cut, and forbidden permutation occurrences. The component-insertion boundary arguments instantiate Mathlib’s Walk.exists_boundary_dart on induced-graph reachability directly at both consumers in p4_free_separation. They use ordinary binding, logic and subtype normalization, with no standalone declaration or new-content claim. The ordinary reachability-between-vertices step uses Mathlib’s boundary dart and walk-prefix APIs directly inside disconnected_spans_cut; it has no standalone declaration or escape-witness classification. The least omitted vertex of the root component still constructs the cut. They formalize known mathematics, attributed in fu2019two; no external problem resolution is claimed for this module.
• Separable.CutFactorization is also first-Freeze content. avoids_block_sum_iff and fixed_cut_factorization are content / escape-witness: crossing-pattern exclusion, unique rank reconstruction of actual factors, respectively. The definitions of actual block sums and descent counts are retained. The ordinary descent normalization is internal to the existing GreatestCutEnumeration.result proof and carries no standalone admission classification. That result retains its weighted equivalence and all finite recurrence contracts; it is outside this five-module first-Freeze closure. A398542 does not use descent weighting. This is known support, attributed in fu2019two, with no separate resolution claim.

The existing frozen project supplier is D5/S1/Words/Patterns/DerangementRatioNonconvergence.Contains. Library-first reuse is direct: there is no new containment predicate or forwarding wrapper. The sealed proof imports the pinned Mathlib series and Pochhammer modules; no external Lean library was added. The prior search and independently accepted mathematical implementation are recorded in #9332. Formalization of a known supplier is distinct from mathematical novelty, and support modules earn no separate open-problem credit.