A083833 - palindromes p with 5p+1 palindrome: Branicky's conjectures C1/C2 proved (Lean 4)

theorems A083833_C1 / A083833_C2 (unconditional, standard axioms only), proved in the carry-chain module A083833.lean (multiplier 5): for every palindrome p with m >= 1 decimal digits such that q = 5p+1 is also a palindrome (of m' digits), (C1) every digit of p is <= 3 - Branicky's first '(Conjectures)' item on the OEIS entry (Jun 2021: 'All terms contain only the digits {0,1,2,3}'); (C2) if the length m of p is EVEN then every digit of p equals 2, i.e. p = 22...2 - Branicky's second conjecture verbatim ('For d even, the only term with d digits is 2^d; equivalently, all terms starting with 1 have odd length'), proved in its full strong form. Both proved here for all digit lengths; the proof distinguishes the same-length case (m' = m: symmetric 2-periodic carry chain forcing m odd, a_0 = 1, alternating classes {0,1}/{2,3}) from the overflow case (m' = m+1: constant carry chain forcing p = 22...2, q = 11...1). The shared module also proves the image-sequence conjectures A083834_C1 (digits of q in {0,1,5,6}) and A083834_C2 (even-length q = repunit) for OEIS A083834, packaged separately - the companion theorems ship in this repository since they live in the same module. Universal properties of the members, NOT an enumeration of the sequence: membership of specific values, completeness of the published list, existence of members and finitude are not claimed. Trust base: standard axioms only [propext, Classical.choice, Quot.sound] expected; zero sorry, zero native_decide.