Determining a sequence from a symmetric index relation

The sequence $\{a_n\}_{n\geq 0}$ of real numbers satisfies the relation: $a_{m+n} + a_{m-n} - m + n -1 = \frac12 (a_{2m} + a_{2n})$ for all non-negative integers $m$ and $n$ , $m \ge n$ . If $a_1 = 3$ find $a_{2004}$ .

The required value is a₂₀₀₄=4018021.

Formalization Note: The source condition m≥n is an antecedent restricting when the recurrence applies. The original formalization asserted m≥n for every pair of natural numbers, making its assumptions inconsistent. This correction restores the implication and proves the requested value from the original recurrence and initial value.

Source: InternLM Lean-Workbook, record lean_workbook_plus_66265 (Apache-2.0).