`Compfiles/Usa2019P3.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

24 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2019, Problem 3

Let K be the set of positive integers not containing the decimal digit 7. Determine all polynomials f(x) with nonnegative coefficients such that f(x) ∈ K for all x ∈ K.

Imports (6)

Imported by 1 file

Compfiles.lean

def Usa2019P3.K The set of positive integers whose decimal representation does not contain the digit 7 line 34 source
Source documentation
The set of positive integers whose decimal representation does not contain the digit 7.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, And, LT.lt, OfNat.ofNat, Not, Membership.mem, List, Nat.digits
3 instances, coercions and auxiliary constants left out.
```
def K : Set ℕ := {n | 0 < n ∧ 7 ∉ Nat.digits 10 n}
```
theorem Usa2019P3.mem_K line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, Set, Usa2019P3.K, And, LT.lt, OfNat.ofNat, Not, List, Nat.digits
Proof uses: Iff.rfl
5 instances, coercions and auxiliary constants left out.
determine Usa2019P3.solution_set The polynomials that map K into K: the constants with value in K, and the polynomials 10^e * x + k with k < 10^e and k ∈ K ∪ {0} line 40 source
Source documentation
The polynomials that map K into K: the constants with value in K, and the polynomials 10^e * x + k with k < 10^e and k ∈ K ∪ {0}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Polynomial, Nat
Proof uses: Set.ofPred, Or, Exists, And, Membership.mem, Usa2019P3.K, Eq, RingHom, Polynomial.C, LT.lt, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Polynomial.X
17 instances, coercions and auxiliary constants left out.
```
determine solution_set : Set (Polynomial ℕ) :=
…
```
theorem Usa2019P3.one_mem_K line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Nat, Set, Usa2019P3.K, OfNat.ofNat
Proof uses: And.intro, LT.lt, Not, List, Nat.digits, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq, List.cons, List.nil, Nat.digits_of_lt, Mathlib.Meta.NormNum.isNat_eq_false, Eq.mpr, id, congrArg, of_eq_true, Eq.trans and 6 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Usa2019P3.digits_len_le_of_lt_pow The decimal digits of a have length at most k when a < 10 ^ k line 73 source
Source documentation
The decimal digits of a have length at most k when a < 10 ^ k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, LE.le, List.length, Nat.digits
Proof uses: Iff.mpr, Nat.digits_length_le_iff, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem digits_len_le_of_lt_pow {a k : ℕ} (h : a < 10 ^ k) :
    (Nat.digits 10 a).length ≤ k :=
…
```
Mentions: h
theorem Usa2019P3.digits_mul_pow_add Documented declaration: digits_mul_pow_add line 80 source
Source documentation
Core concatenation lemma: if a < 10 ^ k and 0 < m, then the decimal digits of m * 10 ^ k + a are the digits of a, padded with zeros up to length k, followed by the digits of m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, HPow.hPow, Eq, List, Nat.digits, HAdd.hAdd, HMul.hMul, HAppend.hAppend, List.replicate, HSub.hSub, List.length
Proof uses: LE.le, Usa2019P3.digits_len_le_of_lt_pow, Eq.mpr, id, congrArg, Nat.add_sub_cancel', Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow, Mathlib.Tactic.Ring.Common.pow_prod_atom and 18 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem digits_mul_pow_add {m a k : ℕ} (hm : 0 < m) (ha : a < 10 ^ k) :
    Nat.digits 10 (m * 10 ^ k + a)
      = Nat.digits 10 a ++ List.replicate (k - (Nat.digits 10 a).length) 0
        ++ Nat.digits 10 m := by
…
```
theorem Usa2019P3.seven_mem_digits_of_le_lt Any natural number in [7 * 10 ^ E, 8 * 10 ^ E) contains the digit 7 (in fact, as its leading digit) line 94 source
Source documentation
Any natural number in [7 * 10 ^ E, 8 * 10 ^ E) contains the digit 7 (in fact, as its leading digit).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMul.hMul, OfNat.ofNat, HPow.hPow, LT.lt, Membership.mem, List, Nat.digits
Proof uses: HSub.hSub, Eq, HAdd.hAdd, Eq.mpr, id, congrArg, HAppend.hAppend, List.replicate, List.length, Usa2019P3.digits_mul_pow_add, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, List.cons, List.nil, Nat.digits_of_lt, Mathlib.Meta.NormNum.isNat_eq_false, List.mem_concat_self
36 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem seven_mem_digits_of_le_lt {y E : ℕ} (h1 : 7 * 10 ^ E ≤ y)
    (h2 : y < 8 * 10 ^ E) : 7 ∈ Nat.digits 10 y := by
…
```
theorem Usa2019P3.digits_ten_pow_sub_one The decimal digits of 10 ^ s - 1 are exactly s nines line 104 source
Source documentation
The decimal digits of 10 ^ s - 1 are exactly s nines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List, Nat.digits, OfNat.ofNat, HSub.hSub, HPow.hPow, List.replicate
Proof uses: Nat.recAux, of_eq_true, List.nil, Eq.trans, True, congrFun', congrArg, pow_zero, tsub_self, Nat.digits_zero, eq_self, LT.lt, pow_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, HAdd.hAdd, HMul.hMul and 15 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem digits_ten_pow_sub_one (s : ℕ) :
    Nat.digits 10 (10 ^ s - 1) = List.replicate s 9 := by
…
```
theorem Usa2019P3.seven_pow_sub_one_mem_K The number 7 * 10 ^ s - 1 (i.e. a six followed by s nines) lies in K line 121 source
Source documentation
The number 7 * 10 ^ s - 1 (i.e. a six followed by s nines) lies in K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Usa2019P3.K, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow
Proof uses: LT.lt, pow_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, And.intro, Not, List, Nat.digits, Eq, HAdd.hAdd, Nat.sub_lt, Eq.mpr, id, congrArg, HAppend.hAppend, List.replicate, List.length and 22 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem seven_pow_sub_one_mem_K (s : ℕ) : 7 * 10 ^ s - 1 ∈ K := by
…
```
Mentions: Usa2019P3.K
def Usa2019P3.dropTrailingZeros Remove the trailing (i.e. most significant) zeros of a digit list line 134 source
Source documentation
Remove the trailing (i.e. most significant) zeros of a digit list.

no axioms what this means
Statement uses: List, Nat
Proof uses: List.reverse, List.dropWhile, Decidable.decide, Eq, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def dropTrailingZeros (L : List ℕ) : List ℕ := (L.reverse.dropWhile (· = 0)).reverse
```
theorem Usa2019P3.ofDigits_eq_zero_of_forall_eq_zero line 136 source
standard axioms: propext what this means
Statement uses: List, Nat, Membership.mem, Eq, OfNat.ofNat, Nat.ofDigits
Proof uses: List.rec, List.nil, Eq.refl, List.cons, Eq.mpr, HAdd.hAdd, HMul.hMul, id, congrArg, Nat.ofDigits_cons, List.mem_cons_self, List.mem_cons_of_mem, MulZeroClass.mul_zero, add_zero
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2019P3.ofDigits_dropTrailingZeros line 144 source
standard axioms: propext what this means
Statement uses: List, Nat, Eq, Nat.ofDigits, OfNat.ofNat, Usa2019P3.dropTrailingZeros
Proof uses: HAppend.hAppend, List.reverse, List.takeWhile, Decidable.decide, List.dropWhile, rfl, Eq.mpr, id, congrArg, Eq.rec, Eq.refl, Eq.trans, Eq.symm, List.reverse_reverse, List.takeWhile_append_dropWhile, List.reverse_append, HAdd.hAdd, HMul.hMul, HPow.hPow, List.length and 10 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Usa2019P3.digits_ofDigits_eq_dropTrailingZeros line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Membership.mem, LT.lt, OfNat.ofNat, Eq, Nat.digits, Nat.ofDigits, Usa2019P3.dropTrailingZeros
Proof uses: List.reverseRecOn, List.nil, Eq.refl, HAppend.hAppend, List.cons, dite, Eq.mpr, id, congrArg, Nat.ofDigits_append_zero, List.mem_append_left, List.reverse, List.dropWhile, Decidable.decide, List.reverse_append, of_eq_true, Eq.trans, True, congrFun', List.reverse_cons and 23 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
theorem Usa2019P3.mem_dropTrailingZeros_of_mem line 185 source
standard axioms: propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, List, Membership.mem, Usa2019P3.dropTrailingZeros
Proof uses: id, Eq.mpr, List.reverse, List.dropWhile, Decidable.decide, Eq, congrArg, propext, List.mem_reverse, HAppend.hAppend, List.takeWhile, List.takeWhile_append_dropWhile, Or, Eq.mp, List.mem_append, Eq.symm, absurd, of_decide_eq_true, List.mem_takeWhile_imp
8 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Usa2019P3.not_mem_ofDigits_of_not_mem If all entries of L are digits and 7 does not occur in the digits of Nat.ofDigits 10 L, then 7 does not occur in L either line 198 source
Source documentation
If all entries of L are digits and 7 does not occur in the digits of Nat.ofDigits 10 L, then 7 does not occur in L either.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Membership.mem, LT.lt, OfNat.ofNat, Not, Nat.digits, Nat.ofDigits
Proof uses: Eq.mpr, Usa2019P3.dropTrailingZeros, id, Eq, congrArg, Usa2019P3.digits_ofDigits_eq_dropTrailingZeros, Usa2019P3.mem_dropTrailingZeros_of_mem, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false
10 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem not_mem_ofDigits_of_not_mem {L : List ℕ} (hL : ∀ l ∈ L, l < 10)
    (h : 7 ∉ Nat.digits 10 (Nat.ofDigits 10 L)) : 7 ∉ L := by
…
```
Mentions: h
theorem Usa2019P3.ofDigits_flatMap_digits_pad The base-10 value of the digit list obtained by concatenating the padded blocks of b 0, b 1, …, b (n - 1) (each block padded to width E) equals ∑ i, b i * 10 ^ (E * i) line 208 source
Source documentation
The base-10 value of the digit list obtained by concatenating the padded blocks of b 0, b 1, …, b (n - 1) (each block padded to width E) equals ∑ i, b i * 10 ^ (E * i).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Eq, Nat.ofDigits, List.flatMap, HAppend.hAppend, List, Nat.digits, List.replicate, HSub.hSub, List.length, List.range, Finset.sum, Finset.range, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, List.nil, List.flatMap_nil, eq_self, LE.le, Iff.mpr, Nat.digits_length_le_iff, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mpr, HAdd.hAdd, id and 21 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem ofDigits_flatMap_digits_pad {E : ℕ} (b : ℕ → ℕ) (hb : ∀ i, b i < 10 ^ E) (n : ℕ) :
    Nat.ofDigits 10 ((List.range n).flatMap fun i =>
        Nat.digits 10 (b i) ++ List.replicate (E - (Nat.digits 10 (b i)).length) 0)
      = ∑ i ∈ Finset.range n, b i * 10 ^ (E * i) := by
…
```
theorem Usa2019P3.coeff_stable Reduction to monomials: if f maps K into K and its i-th coefficient is nonzero, then f.coeff i * m ^ i ∈ K for every m ∈ K line 235 source
Source documentation
Reduction to monomials: if f maps K into K and its i-th coefficient is nonzero, then f.coeff i * m ^ i ∈ K for every m ∈ K. The idea: evaluate at 10 ^ E * m for a huge E; the decimal digits of the result are the padded blocks of the digits of f.coeff i * m ^ i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Nat, Membership.mem, Set, Usa2019P3.K, Polynomial.eval, Ne, Finsupp, Polynomial.coeff, OfNat.ofNat, HMul.hMul, HPow.hPow
Proof uses: LT.lt, Not, List, Nat.digits, Eq, rfl, Finset.sum, Finset.range, HAdd.hAdd, Polynomial.natDegree, dite, LE.le, Finset.single_le_sum, Finset, Nat.zero_le, Iff.mpr, Finset.mem_range, Nat.lt_succ_of_le, Nat.lt_pow_self, Mathlib.Meta.NormNum.isNat_lt_true and 79 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
```
theorem coeff_stable {f : Polynomial ℕ} (hf : ∀ n ∈ K, f.eval n ∈ K)
    {m : ℕ} (hm : m ∈ K) {i : ℕ} (hi : f.coeff i ≠ 0) : f.coeff i * m ^ i ∈ K := by
…
```
Mentions: f, Usa2019P3.K
theorem Usa2019P3.eq_ten_pow_of_stable Linear classification: if x ↦ c * x maps K into K and c ≠ 0, then c is a power of ten line 305 source
Source documentation
Linear classification: if x ↦ c * x maps K into K and c ≠ 0, then c is a power of ten. Otherwise, with d * 10 ^ e ≤ c < (d + 1) * 10 ^ e and d ∈ {1, …, 9} ∖ {7}, an explicit multiplier x ∈ K (depending on d) makes c * x begin with the digit 7.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Membership.mem, Set, Usa2019P3.K, HMul.hMul, Exists, Eq, HPow.hPow
Proof uses: Classical.byContradiction, Not, Usa2019P3.one_mem_K, Eq.mp, congrArg, mul_one, LT.lt, List, Nat.digits, False, List.length, List.length_pos_of_ne_nil, Iff.mpr, List.nil, Nat.digits_ne_nil_iff_ne_zero, HSub.hSub, rfl, pow_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat and 86 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 268 steps (first 200 of 268)
Open to load the checked before-and-after goal states.
```
theorem eq_ten_pow_of_stable {c : ℕ} (hc : c ≠ 0) (hstab : ∀ m ∈ K, c * m ∈ K) :
    ∃ e, c = 10 ^ e := by
…
```
Mentions: Usa2019P3.K
theorem Usa2019P3.coeff_zero_pow_linear The constant coefficient of (a * x + b) ^ d is b ^ d line 459 source
Source documentation
The constant coefficient of (a * x + b) ^ d is b ^ d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, Polynomial.X, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', eq_natCast, pow_zero, Polynomial.coeff_one_zero, eq_self, Eq.mpr, id, pow_succ, Polynomial.mul_coeff_zero, Polynomial.coeff_add, ite, Polynomial.coeff_natCast_ite, ite_eq_left_of_eq_true, Polynomial.coeff_X_zero and 2 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem coeff_zero_pow_linear (d a b : ℕ) : ((C a * X + C b) ^ d).coeff 0 = b ^ d := by
…
```
theorem Usa2019P3.coeff_one_pow_linear The coefficient of x in (a * x + b) ^ d is d * a * b ^ (d - 1) line 467 source
Source documentation
The coefficient of x in (a * x + b) ^ d is d * a * b ^ (d - 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, Polynomial.X, OfNat.ofNat, HSub.hSub
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, ite, congrFun', eq_natCast, pow_zero, Polynomial.coeff_one, ite_eq_right_of_eq_false, MulZeroClass.zero_mul, zero_tsub, mul_one, eq_self, Eq.mpr, id, pow_succ, Polynomial.mul_coeff_one and 45 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem coeff_one_pow_linear (d a b : ℕ) :
    ((C a * X + C b) ^ d).coeff 1 = d * a * b ^ (d - 1) := by
…
```
theorem Usa2019P3.not_stable_of_degree_two_le Higher-degree classification: no monomial c * x ^ d with d ≥ 2 maps K into K line 489 source
Source documentation
Higher-degree classification: no monomial c * x ^ d with d ≥ 2 maps K into K. Otherwise c * (10x + 3) ^ d would be stable too, and reducing to monomials forces c * d * 3 ^ (d - 1) * 10 to be a power of ten, which is impossible since it is divisible by 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, LE.le, Membership.mem, Set, Usa2019P3.K, HMul.hMul, HPow.hPow, False
Proof uses: HAdd.hAdd, LT.lt, Not, List, Nat.digits, And.intro, Eq, HAppend.hAppend, List.replicate, HSub.hSub, List.length, Usa2019P3.digits_mul_pow_add, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.natPow_one, Bool, Bool.false, List.cons and 84 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
```
theorem not_stable_of_degree_two_le {c d : ℕ} (hc : c ≠ 0) (hd : 2 ≤ d)
    (hstab : ∀ m ∈ K, c * m ^ d ∈ K) : False := by
…
```
Mentions: Usa2019P3.K
theorem Usa2019P3.const_lt_of_linear_stable If x ↦ 10 ^ e * x + k maps K into K and k ≠ 0, then k < 10 ^ e line 536 source
Source documentation
If x ↦ 10 ^ e * x + k maps K into K and k ≠ 0, then k < 10 ^ e. Otherwise, writing k = q * 10 ^ e + r with q ≥ 1, the input x = 7 * 10 ^ q - 1 ∈ K makes x + q start with the digit 7.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Usa2019P3.K, HAdd.hAdd, HMul.hMul, HPow.hPow, OfNat.ofNat, LT.lt
Proof uses: Decidable.byContradiction, Not, pow_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Exists, And, Eq, False, Exists.intro, HDiv.hDiv, HMod.hMod, And.intro, Nat.div_pos, Eq.mp, LE.le, Nat.mod_lt and 49 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
theorem const_lt_of_linear_stable {e k : ℕ}
    (hstab : ∀ n ∈ K, 10 ^ e * n + k ∈ K) : k < 10 ^ e := by
…
```
Mentions: Usa2019P3.K
theorem Usa2019P3.stable_of_form Documented declaration: stable_of_form line 571 source
Source documentation
The polynomials 10 ^ e * x + k with k < 10 ^ e and k ∈ K ∪ {0} do map K into K: the decimal digits of 10 ^ e * n + k are the digits of k padded to width e, followed by the digits of n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Or, Eq, Membership.mem, Set, Usa2019P3.K, Polynomial.eval, HAdd.hAdd, Polynomial, HMul.hMul, RingHom, Polynomial.C, Polynomial.X
Proof uses: Not, List, Nat.digits, of_eq_true, Eq.trans, True, congrFun', congrArg, congr, eq_natCast, Nat.cast_pow, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_ofNat, Polynomial.eval_X, Polynomial.eval_natCast, eq_self, Eq.mpr, id and 29 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
theorem stable_of_form {e k : ℕ} (hlt : k < 10 ^ e) (hk : k = 0 ∨ k ∈ K) :
    ∀ n ∈ K, (C (10 ^ e) * X + C k).eval n ∈ K := by
…
```
Mentions: Usa2019P3.K
problem Usa2019P3.usa2019_p3 line 597 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Nat, Iff, Membership.mem, Set, Usa2019P3.K, Polynomial.eval, Usa2019P3.solution_set
Proof uses: id, Iff.intro, Or, Exists, And, Eq, RingHom, Polynomial.C, LT.lt, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Polynomial.X, Ne, False, Usa2019P3.one_mem_K, absurd, And.left, Not and 68 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.