6.9 André’s reflection method (Stanley §1.6.4)

Status. This section records a partial formalization. The development lives in experimental/reflection.v, which is not in the active build chain (excluded from _CoqProject). The headline recurrence euler_rec is proven from one named, precisely-stated Admitted lemma (sum_set_is_alt_eq_andre_sum). The companion document docs/internal/PHASE_C_RETROSPECTIVE.md captures the eight sessions of work, the structural obstacle (a 4-to-1 boundary reduction, not the 2-to-1 fibration suggested by the classical English proof), and a concrete \(\sim 510\) LOC discharge plan.

Definition 6.32 Euler numbers

Let \(\mathrm{alt\_ desc\_ set}\, n \subseteq \{ 0, \dots , n-1\} \) denote the alternating descent pattern \(\{ 0, 2, 4, \dots \} \). Define

\[ E_{n+1} \; :=\; \beta (\mathrm{alt\_ desc\_ set}\, n), \qquad A_{n+1} := E_{n+1}, \qquad A_0 := 1. \]

\(A_n\) is the number of alternating permutations of \(\mathfrak {S}_{n}\).

Theorem 6.33 The André recurrence — modulo one admit

For every \(n \in \mathbb {N}\),

\[ 2 \cdot A_{n+2} \; =\; \sum _{k=0}^{n+1} \binom {n+1}{k} \, A_k \, A_{n+1-k}. \]

Proof status. Derived in one line from two_eulerA_split (which uses beta_compl from beta_swap.v) and the named admit:

\begin{equation} \label{eq:andre-admit} \sum _{t \in \mathfrak {S}_{n+1}} \sum _{p \in \{ 0,\dots ,n+1\} } \mathrm{set\_ is\_ alt}(\mathrm{descent\_ set}(\mathrm{insert\_ max\_ perm}\, t\, p)) \; =\; \sum _{k=0}^{n+1} \binom {n+1}{k} A_k A_{n+1-k}. \end{equation}

Sanity. The base case \(n = 0\) (i.e. \(2 A_2 = 2\)) is proven unconditionally as euler_rec_n0_direct (no admit used). The cases \(n = 1, 2\) are stated via euler_rec and inherit the admit transitively.

Remark 6.34 The structural obstacle

The remaining admit 1 is the combinatorial heart of André’s reflection. After partitioning \(\sigma \in \mathfrak {S}_{n+2}\) by the position \(p\) of the maximum and the value-set \(L \subset [n+1]\) of size \(p\) left of the maximum, the descent at the boundary slot \(p-1\) depends on \((L, s_L, s_R)\) jointly: specifically, on whether the largest left value (selected by \(s_L\)) exceeds the smallest right value (selected by \(s_R\)). This couples the three decomposition components and prevents the \([\mathrm{descent\_ set} = E]\) indicator from factoring as \([s_L\text{-cond}] \cdot [s_R\text{-cond}]\).

The classical proof absorbs this coupling via the factor of \(2\) on the LHS: summing over alternating-and-anti-alternating descent patterns leaves the boundary parity free. Formally, of the four flavour pairs \((s_L\text{-flavour}, s_R\text{-flavour}) \in \{ \mathrm{alt}, \neg \mathrm{alt}\} ^2\), exactly one is consistent with the forced boundary value for each fixed \((L, s_L, s_R)\) — a 4-to-1 reduction whose formalization is estimated at \(\sim 510\) LOC. See docs/internal/PHASE_C_RETROSPECTIVE.md for the full lemma list and discharge plan.

Remark 6.35 Reusable infrastructure

Although the headline is open, the file experimental/reflection.v contains \(\sim 1500\) LOC of axiom-free, kernel-validated infrastructure for any future position-of-max bijective decomposition of permutations:

descent_set_insert_max_* — descent set under max-insertion at the three position cases.
embed_left/right, perm_left/right — standardisation of left/right sub-words to \(\mathfrak {S}_{j}\) and \(\mathfrak {S}_{n+1-j}\).
descent_set_decomp_partition — the L-part / boundary / R-part decomposition.
assemble_perm + assemble_decomp_inverse — the full bijection \(\mathfrak {S}_{n+1} \simeq \bigsqcup _j \{ L : |L|=j\} \times \mathfrak {S}_{j} \times \mathfrak {S}_{n+1-j}\), both directions.
sum_partition_image_left, sum_reindex_inner — bigop reindexing along the bijection.

These can be copied into a future formalization that needs the position-of-max decomposition without inheriting the open admit.