= Certificate for [pi]_q (first 4 coefficients) =

Input: the real number x = pi. The continued fraction is truncated to the depth that locks the first 4 coefficients (MGO Proposition 1.1).

(a) continued fraction and even-length MGO form
    regular continued fraction: [3, 7]
    even-length MGO form:       [3, 7]
    even-length form evaluates to the convergent 22/7

(b) MGO formula folded step by step
    odd positions carry [a]_q with q^a above; even positions
    carry [a]_(q^-1) with q^-a above (MGO eqn 1.1).
    innermost term a_2 = 7:  (q**6 + q**5 + q**4 + q**3 + q**2 + q + 1)/q**6
    fold in a_1 = 3:  (q**9 + q**8 + 2*q**7 + 3*q**6 + 3*q**5 + 3*q**4 + 3*q**3 + 3*q**2 + 2*q + 1)/(q**6 + q**5 + q**4 + q**3 + q**2 + q + 1)
    [22/7]_q (the convergent, whose Taylor expansion gives [x]_q) = (q**9 + q**8 + 2*q**7 + 3*q**6 + 3*q**5 + 3*q**4 + 3*q**3 + 3*q**2 + 2*q + 1)/(q**6 + q**5 + q**4 + q**3 + q**2 + q + 1)
    Taylor coefficients: 1 + q + q^2 + O(q^4)

(c) independent cross-checks
    [pass] the first 4 coefficients are unchanged when 8 are asked for
    [pass] [x+1]_q computed from its own continued fraction equals q*[x]_q + 1
    [n/a]  the series [pi]_q diverges at q=1; q=1 is for rationals
    [n/a]  pi is irrational, so the continued fraction does not terminate
    summary: verified: truncation stable to 4, shift law [x+1]=q[x]+1; n/a: q=1 specialisation; exact rational function

References
    S. Morier-Genoud and V. Ovsienko, q-deformed rationals and
    q-continued fractions, Forum Math. Sigma 8 (2020), e13.
    Per-function theorem and check mapping: docs/CORRECTNESS.md.

This is a human-auditable derivation, not a formal machine proof;
every line above is checkable by hand.
