# Catalan convolution and a divisibility certificate [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-catalan-numbers/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-catalan-numbers-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Generate C4 from C0 and check both closed forms. An exact n=4 instance and general integrality identity, not every Catalan bijection. ## Givens and symbols - work - G1 — C0=1 and for every n≥0 use C_(n+1)=sum_(i=0)^n C_i C_(n-i). Compare the two cited Catalan closed forms at n=4. - C_n — zero-based Catalan sequence ## Rules and sources - mko_definition · cited — C_(n+1)=sum over i=0..n of C_i*C_(n−i), and C_n=binomial(2n,n)/(n+1)=binomial(2n,n)−binomial(2n,n+1). Before division, certify that n+1 divides the central binomial coefficient; integer truncation is not a substitute. The domain is n≥0 and the C_0/C_1 indexing conventions must not be mixed. · mko-catalan-numbers - work · prerequisite — Finite convolution definition; binomial factorial identities and comb=0 beyond its upper index; the Catalan closed forms are cited MKO facts, not general theorems proved by this example. ## Main derivation S01 · impliesBefore C_0=1 After C_1=C_0C_0=1 Conditions: none Rule: work · Uses: G1, work Leaf basis: work Fix zero-based indexing first rather than mixing C1 conventions. S02 · impliesBefore C_2=C_0C_1+C_1C_0 After C_2=2 Conditions: none Rule: work · Uses: G1, S01, work Leaf basis: work At n=1 include both splits. S03 · impliesBefore C_3=C_0C_2+C_1C_1+C_2C_0 After C_3=2+1+2=5 Conditions: none Rule: work · Uses: G1, S02, work Leaf basis: work List all three splits at n=2. S04 · impliesBefore C_4=C_0C_3+C_1C_2+C_2C_1+C_3C_0 After C_4=5+2+2+5=14 Conditions: none Rule: work · Uses: G1, S03, work Leaf basis: work All four splits at n=3 give 14. S05 · impliesBefore \binom84=8!/(4!4!) After \binom84=70,\quad70\bmod5=0 Conditions: none Rule: work · Uses: G1, S04, work Leaf basis: work Compute the central binomial coefficient and certify remainder zero before integer division. S06 · impliesBefore \binom84/(4+1) After 70/5=14=C_4 Conditions: none Rule: work · Uses: G1, S05, work Leaf basis: work After divisibility, check the first closed form at n=4. S07 · impliesBefore \binom85=56 After \binom84-\binom85=70-56=14 Conditions: none Rule: work · Uses: G1, S06, work Leaf basis: work The second closed form gives the same integer as a cross-check. S08 · impliesBefore \binom{2n}{n+1}=\binom{2n}{n}\frac{n}{n+1}\quad(n\ge0) After \binom{2n}{n}-\binom{2n}{n+1}=\frac1{n+1}\binom{2n}{n}\in\mathbb Z Conditions: none Rule: work · Uses: G1, S07, work Leaf basis: work The factorial ratio gives the identity; an integer difference proves divisibility, with comb(0,1)=0 at n=0. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S07, work — This proves integrality, not the entire general closed-form solution of the convolution. - S07 · premise_audit · G1, S06, work — The lower index n+1=5 must not be replaced by n-1. - S06 · premise_audit · G1, S05, work — This numerical agreement alone does not prove the closed form for every n. - S05 · premise_audit · G1, S04, work — A truncated quotient is not a divisibility certificate. - S04 · premise_audit · G1, S03, work — Adding only endpoints would give the wrong value 10. - S03 · premise_audit · G1, S02, work — Do not omit the middle split. - S02 · premise_audit · G1, S01, work — Equal terms still have separate indices. - S01 · premise_audit · G1, work — C0 for the empty object is not zero. ## Error controls and negative controls IndexC4 uses n=3 in the convolution and n=4 in the closed form. Exact divisionCheck70 mod5=0 before 70/5=14. - C0=0 gives the same sequence. → reject — The first convolution would give C1=0 rather than 1. - 70//5 replaces the general remainder obligation. → reject — Truncation itself proves no divisibility; remainder zero must be checked. - C4 only needs C0C3+C3C0=10. → reject — The two middle splits each add2, giving 14. ## Result and limitations C4=14, central coefficient 70 is divisible by 5, and 70-56=14. ## Verification and source binding 4 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 7522ef04029fd7f26aab4081199d43b82a2d2f70998d7d556d7c788ecb395599 - original source SHA-256: ed47d97d69cfdf0cb831c56ec2b237fbcd2f49986cf1490c20647d56623f8552 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-catalan-numbers-01.json)