oeis_a300997_finite_difference_is_one_or_two.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 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were 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 source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

81 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def a A300997 line 46 source
Source documentation
A300997: $a(n)$ is the number of steps needed to reach a stable configuration in the 1D cellular automaton initialized with one cell with mass $n$ and based on the rule "each cell gives half of its mass, rounded down, to its right neighbor". The stable configuration is $n$ cells with mass 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, List, List.reverse, List.dropWhile, Decidable.decide, Eq, HAppend.hAppend, List.map, List.cons, List.nil, List.zipWith, Nat.add, ite, List.replicate, List.foldl, List.range, Set, setOf and 1 more
9 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/A309132_conjecture_carmichael.lean:45 (same statement text; different proof or body), APNOutputs/OEIS/a091669_conjecture_primitive_root.lean:46 (same statement text; different proof or body), APNOutputs/OEIS/a325046_odd_terms_at_k_times_k_plus_1.lean:52 (different declaration text), APNOutputs/OEIS/oeis_103311_conjecture_0.lean:47 (different declaration text), APNOutputs/OEIS/oeis_108_conjecture_2.lean:45 (different declaration text), APNOutputs/OEIS/oeis_113254_conjecture_0.lean:48 (different declaration text), APNOutputs/OEIS/oeis_175386_conjecture_0.lean:46 (different declaration text), APNOutputs/OEIS/oeis_194806_conjecture_0.lean:50 (same statement text; different proof or body), APNOutputs/OEIS/oeis_227582_conjecture_0.lean:60 (same statement text; different proof or body), APNOutputs/OEIS/oeis_228143_conjecture_1.lean:54 (same statement text; different proof or body), APNOutputs/OEIS/oeis_243106_conjecture_0.lean:47 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_0.lean:43 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_4.lean:43 (different declaration text), APNOutputs/OEIS/oeis_267581_conjecture_0.lean:71 (same statement text; different proof or body), APNOutputs/OEIS/oeis_271591_conjecture_0.lean:57 (different declaration text), APNOutputs/OEIS/oeis_2897_conjecture_0.lean:46 (different declaration text), APNOutputs/OEIS/oeis_306424_conjecture_0.lean:52 (same statement text; different proof or body), APNOutputs/OEIS/oeis_307865_conjecture_0.lean:46 (different declaration text), APNOutputs/OEIS/oeis_323557_conjecture_0.lean:48 (different declaration text), APNOutputs/OEIS/oeis_341254_conjecture_0.lean:52 (same statement text; different proof or body), APNOutputs/OEIS/oeis_372761_conjecture_2.lean:83 (same statement text; different proof or body), APNOutputs/OEIS/oeis_62567_conjecture_0.lean:49 (same statement text; different proof or body), APNOutputs/OEIS/oeis_A028859_conjecture_1.lean:43 (different declaration text), APNOutputs/OEIS/oeis_a211417_conjecture_specific.lean:44 (different declaration text), APNOutputs/OEIS/oeis_a237271_conjecture_2.lean:49 (different declaration text), APNOutputs/OEIS/oeis_a363102_conjecture_1.lean:56 (different declaration text), APNOutputs/OEIS/oeis_a368692_conjecture_integrality.lean:47 (different declaration text). Qualify references as a@path.
```
noncomputable def a (n : ℕ) : ℕ :=
…
```
def half_ceil line 111 source
no axioms what this means
Statement uses: Nat
Proof uses: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
def half_floor line 112 source
no axioms what this means
Statement uses: Nat
Proof uses: HDiv.hDiv, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
def trim_trailing_zeros line 114 source
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 ca_step_list line 117 source
no axioms what this means
Statement uses: List, Nat
Proof uses: HAppend.hAppend, List.map, half_ceil, List.cons, OfNat.ofNat, List.nil, half_floor, List.zipWith, Nat.add, trim_trailing_zeros
3 instances, coercions and auxiliary constants left out.
def initial_config_list line 123 source
no axioms what this means
Statement uses: Nat, List
Proof uses: List.cons, List.nil
def target_config_list line 124 source
no axioms what this means
Statement uses: Nat, List
Proof uses: List.replicate, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
def S_list line 126 source
no axioms what this means
Statement uses: Nat, List
Proof uses: List.foldl, ca_step_list, initial_config_list, List.range
def ca_step_fun line 129 source
no axioms what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, half_ceil, ite, Eq, OfNat.ofNat, half_floor, HSub.hSub
6 instances, coercions and auxiliary constants left out.
def F line 132 source
no axioms what this means
Statement uses: Nat
Proof uses: F.match_1, Unit, OfNat.ofNat, ite, Eq, Nat.succ, ca_step_fun
4 instances, coercions and auxiliary constants left out.
lemma a_eq_sInf line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, a, InfSet.sInf, setOf, List, S_list, target_config_list
Proof uses: id, Eq.mpr, Star.star, Decidable.rec, Decidable, Not, List.cons, List.nil, List.replicate, List.foldl, HAppend.hAppend, List.map, HDiv.hDiv, HAdd.hAdd, List.zipWith, Nat.add, List.reverse, List.dropWhile, Decidable.decide, List.range and 32 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def TargetF line 143 source
no axioms what this means
Statement uses: Nat
Proof uses: ite, LT.lt, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
def list_to_fun line 146 source
standard axioms: propext what this means
Statement uses: List, Nat
Proof uses: List.getD, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
lemma list_to_fun_initial line 148 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, list_to_fun, initial_config_list, F, OfNat.ofNat
Proof uses: id, funext, List.getD, F.match_1, Unit, ite, Nat.succ, ca_step_fun, Nat.casesAuxOn, Eq.refl, Eq.symm, HAdd.hAdd
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma list_to_fun_target line 152 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, list_to_fun, target_config_list, TargetF
Proof uses: id, funext, List.getD, OfNat.ofNat, ite, LT.lt, List, List.replicate, Eq.mpr, Option.getD, GetElem?.getElem?, List.length, congrArg, List.getD_eq_getElem?_getD, Decidable, Not, if_neg, of_eq_true, Eq.trans, Option.none and 13 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma trim_trailing_zeros_getD line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Eq, List.getD, trim_trailing_zeros, OfNat.ofNat
Proof uses: Eq.mpr, Option.getD, GetElem?.getElem?, LT.lt, List.length, List.reverse, List.dropWhile, Decidable.decide, id, congr, congrArg, List.getD_eq_getElem?_getD, List.reverseRecOn, Eq.refl, List.nil, HAppend.hAppend, List.cons, ite, Option, HSub.hSub and 53 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma getD_zipWith_add line 165 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Eq, List.length, List.getD, List.zipWith, Nat.add, OfNat.ofNat, HAdd.hAdd
Proof uses: Or.rec, GT.gt, Not, Or, of_eq_true, Eq.trans, GetElem.getElem, LT.lt, List.lt_length_right_of_zipWith, True, congrArg, Min.min, List.length_zipWith, min_self, eq_true, id, Eq.mp, Option.getD, Option.some, List.lt_length_left_of_zipWith and 12 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma getD_append_zero line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Eq, List.getD, HAppend.hAppend, List.cons, OfNat.ofNat, List.nil
Proof uses: LT.lt, List.length, LE.le, Or, lt_or_ge, Eq.mpr, id, congrArg, List.getD_append, Eq.refl, LE.le.eq_or_lt, Or.inl, of_eq_true, Eq.trans, Option.getD, Option.some, GetElem.getElem, HSub.hSub, True, HAdd.hAdd and 18 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma my_getD_cons_zero line 175 source
standard axioms: propext what this means
Statement uses: List, Nat, Eq, List.getD, List.cons, OfNat.ofNat, ite, HSub.hSub
Proof uses: Nat.casesAuxOn, Eq.refl, Eq.symm, HAdd.hAdd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma getD_map_half_ceil line 179 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Eq, List.getD, List.map, half_ceil, OfNat.ofNat
Proof uses: dite, LT.lt, List.length, of_eq_true, Eq.trans, Option.getD, Option.some, GetElem.getElem, Eq.rec, True, congrArg, List.length_map, eq_true, congr, GetElem?.getElem?, List.getD_eq_getElem?_getD, Option, getElem?_pos, List.getElem_map, eq_self and 9 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma getD_map_half_floor line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Eq, List.getD, List.map, half_floor, OfNat.ofNat
Proof uses: Or.rec, LT.lt, List.length, LE.le, Or, of_eq_true, HDiv.hDiv, Eq.trans, True, Option.getD, Option.some, GetElem.getElem, Eq.rec, congrArg, List.length_map, eq_true, True.intro, congr, GetElem?.getElem?, List.getD_eq_getElem?_getD and 9 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma list_to_fun_ca_step line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Eq, list_to_fun, ca_step_list, ca_step_fun
Proof uses: funext, id, List.getD, OfNat.ofNat, Eq.mpr, HAppend.hAppend, List.map, half_ceil, List.cons, List.nil, half_floor, List.zipWith, Nat.add, trim_trailing_zeros, congrArg, trim_trailing_zeros_getD, List.length, of_eq_true, HAdd.hAdd, Eq.trans and 14 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma S_list_zero line 199 source
standard axioms: propext what this means
Statement uses: Nat, Eq, List, S_list, OfNat.ofNat, initial_config_list
Proof uses: of_eq_true, eq_self
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma S_list_succ line 202 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, List, S_list, HAdd.hAdd, OfNat.ofNat, ca_step_list
Proof uses: id, Eq.mpr, List.foldl, HAppend.hAppend, List.map, half_ceil, List.cons, List.nil, half_floor, List.zipWith, Nat.add, trim_trailing_zeros, initial_config_list, List.range, congrArg, Nat.succ, List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil and 1 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma list_to_fun_S_list line 206 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, list_to_fun, S_list, F
Proof uses: Nat.recAux, Eq.mpr, OfNat.ofNat, initial_config_list, id, congrArg, List, S_list_zero, list_to_fun_initial, HAdd.hAdd, ca_step_list, S_list_succ, ca_step_fun, list_to_fun_ca_step, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def P line 217 source
no axioms what this means
Statement uses: Nat
Proof uses: F.match_1, Unit, OfNat.ofNat, Nat.succ, HAdd.hAdd, HMod.hMod, F
7 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/oeis_103311_conjecture_0.lean:121 (different declaration text). Qualify references as P@path.
def DiffByOneF line 222 source
no axioms what this means
Statement uses: Nat
Proof uses: Eq, HAdd.hAdd, ite, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
lemma ca_step_fun_DiffByOneF line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DiffByOneF, ca_step_fun, HAdd.hAdd, HMod.hMod, OfNat.ofNat
Proof uses: id, Eq.mpr, Eq, half_ceil, ite, half_floor, HSub.hSub, HDiv.hDiv, forall_congr, congr, congrArg, ite_congr, Eq.refl, Not, add_comm, ca_step_fun_DiffByOneF.match_1, Unit, Or, Nat.mod_two_eq_zero_or_one, Or.inl and 38 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma F_DiffByOneF line 231 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DiffByOneF, F, HAdd.hAdd, OfNat.ofNat, P
Proof uses: id, Eq, ite, F.match_1, Unit, Nat.succ, HMod.hMod, Nat.brecOn.go, ca_step_fun, Eq.mpr, half_ceil, half_floor, HSub.hSub, Nat.rec, PUnit, PProd, HDiv.hDiv, forall_congr, congr, congrArg and 7 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ca_step_fun_TargetF line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, ca_step_fun, TargetF
Proof uses: Eq.mpr, ite, LT.lt, HAdd.hAdd, half_ceil, half_floor, HSub.hSub, id, Eq.trans, forall_congr, congrArg, ite_congr, Eq.refl, Not, Or, em, Or.inl, of_eq_true, HDiv.hDiv, True and 20 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma F_n_plus_1_eq line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, F, HAdd.hAdd, OfNat.ofNat, ite, P
Proof uses: funext, F_DiffByOneF
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma F_zero_and_P_le line 250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LE.le, Eq, F, OfNat.ofNat, P
Proof uses: Nat.recAux, id, dite, ite, Eq.mpr, congrArg, if_pos, Decidable.byContradiction, Not, if_neg, HAdd.hAdd, HSub.hSub, HDiv.hDiv, Eq.refl, And.intro, le_refl, HMod.hMod, congrFun, F_n_plus_1_eq, And.left and 3 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
lemma F_zero_of_ge line 304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, F, OfNat.ofNat
Proof uses: And.left, P, F_zero_and_P_le
4 instances, coercions and auxiliary constants left out.
lemma P_le_n line 307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, P
Proof uses: And.right, Eq, F, OfNat.ofNat, F_zero_and_P_le
3 instances, coercions and auxiliary constants left out.
lemma list_eq_of_fun_eq line 310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Ne, Option, List.getLast?, Option.some, OfNat.ofNat, Eq, list_to_fun
Proof uses: List.ext_get, by_contra, List.length, Not, absurd, List.getD, HSub.hSub, False, congrFun, Function.comp, List.nil, Eq.symm, List.cons, Eq.refl, LT.lt, List.get, Fin.mk, of_eq_true, GetElem.getElem, Fin.isLt and 13 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma S_list_no_trailing_zeros line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Ne, Option, List.getLast?, S_list, Option.some
Proof uses: id, Eq.mpr, Not, Eq, List.foldl, List, ca_step_list, initial_config_list, List.range, Nat.iterate, trim_trailing_zeros, List.zipWith, Nat.add, HAppend.hAppend, List.map, half_ceil, List.cons, List.nil, half_floor, congrArg and 101 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma target_config_no_trailing_zeros line 330 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Ne, Option, List.getLast?, target_config_list, Option.some
Proof uses: id, of_eq_true, List.replicate, Eq.trans, ite, Eq, Option.none, True, congrArg, List.getLast?_replicate, Not, False, And, Option.some.injEq, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false and 5 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma F_eq_TargetF_iff_S_list_eq line 334 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Iff, Eq, F, TargetF, List, S_list, target_config_list
Proof uses: Iff.intro, list_eq_of_fun_eq, S_list_no_trailing_zeros, target_config_no_trailing_zeros, list_to_fun, list_to_fun_S_list, list_to_fun_target, Eq.mpr, id, congrArg, Eq.symm, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma a_is_stable_from_exists line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Eq, F, TargetF, a
Proof uses: InfSet.sInf, setOf, List, S_list, target_config_list, a_eq_sInf, Eq.mpr, id, congrArg, propext, F_eq_TargetF_iff_S_list_eq, Set.Nonempty, Exists.intro, Membership.mem, Set, Iff.mp, Nat.sInf_mem
7 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma a_min line 361 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, F, TargetF, a
Proof uses: InfSet.sInf, setOf, List, S_list, target_config_list, a_eq_sInf, Eq.mpr, id, congrArg, Nat.sInf_le, Membership.mem, Set, list_to_fun, list_to_fun_S_list, list_to_fun_target, list_eq_of_fun_eq, S_list_no_trailing_zeros, target_config_no_trailing_zeros, Eq.mp, Eq.symm
6 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma P_succ line 375 source
no axioms what this means
Statement uses: Nat, Eq, P, HAdd.hAdd, OfNat.ofNat, HMod.hMod, F
Proof uses: Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma P_moves_when_stable line 378 source
standard axioms: propext what this means
Statement uses: Nat, Eq, F, TargetF, LT.lt, P, HAdd.hAdd, OfNat.ofNat
Proof uses: id, of_eq_true, Nat.rec, PProd, PUnit, PProd.mk, PUnit.unit, HMod.hMod, Nat.brecOn.go, F.match_1, Unit, Eq.trans, True, congrArg, ite, congrFun, ite_cond_eq_true, eq_true, Nat.succ, eq_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma F_stable_forward line 383 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, F, TargetF, HAdd.hAdd
Proof uses: ca_step_fun, rfl, Eq.mpr, id, congrArg, ca_step_fun_TargetF
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma F_stable_add line 389 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, F, TargetF, HAdd.hAdd
Proof uses: id, F.match_1, Unit, ite, Nat.succ, ca_step_fun, LT.lt, Eq.mpr, half_ceil, half_floor, HSub.hSub, Nat.brecOn.go, Nat.rec, PUnit, PProd, HDiv.hDiv, congrArg, Eq.refl, funext, ite_congr and 8 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma P_add_stable line 396 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, F, TargetF, HAdd.hAdd, P
Proof uses: Nat.rec, Nat.zero, Eq.refl, Nat.succ, Eq.trans, HMod.hMod, Eq.mpr, id, congrArg, Nat.add_succ, P.eq_2, congr, Eq.mp, True, implies_congr, eq_true, le_of_lt, LT.lt, of_eq_true, implies_congr_ctx and 38 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma target_n_plus_1_eq line 413 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, TargetF, ite, OfNat.ofNat
Proof uses: Eq.mpr, LT.lt, id, Eq.trans, congrArg, funext, ite_congr, Eq.refl, Not, forall_congr
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma F_n_plus_1_at_D line 418 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, F, TargetF, P, HAdd.hAdd, HSub.hSub
Proof uses: F_stable_add, P_add_stable, Decidable.byContradiction, Not, ite, F_n_plus_1_eq, Eq.mpr, id, congrArg, Eq.mp, target_n_plus_1_eq
16 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma stable_at_some_time line 429 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Eq, F, TargetF
Proof uses: Nat.le_induction, Exists.intro, funext, id, dite, ite, LT.lt, Eq.mpr, congrArg, if_pos, Decidable.byContradiction, Not, False, Eq.trans, if_neg, eq_false', False.elim, noConfusion_of_Nat, Nat.ctorIdx, HAdd.hAdd and 4 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma a_is_stable line 440 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, F, a, TargetF
Proof uses: a_is_stable_from_exists, stable_at_some_time
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma not_stable_before_D line 443 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, F, TargetF, P, LT.lt, HSub.hSub, Ne, HAdd.hAdd
Proof uses: congrFun, F_stable_add, P_add_stable, Decidable.byContradiction, Not, ite, F_n_plus_1_eq, id, if_neg, if_pos, Eq.mp, congrArg
22 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma not_stable_before_a line 469 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, a, Ne, F, HAdd.hAdd, TargetF
Proof uses: Eq, congrFun, ite, P, F_n_plus_1_eq, id, if_pos, Decidable.byContradiction, Not, F_zero_of_ge, P_le_n, dite, False, funext, Eq.mpr, congrArg, Eq.mp, if_neg, a_min
24 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
lemma not_stable_before_a_plus_D line 509 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, a, HSub.hSub, P, Ne, F, TargetF
Proof uses: Or, Decidable.byContradiction, Not, not_stable_before_a, Exists, And, Eq, Exists.intro, And.intro, Eq.mpr, id, congrArg, not_stable_before_D, a_is_stable
24 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma coupling_diff line 518 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, P, a, Eq, HAdd.hAdd, HSub.hSub
Proof uses: F, TargetF, F_n_plus_1_at_D, a_is_stable, a_min, Decidable.byContradiction, Not, LT.lt, Ne, not_stable_before_a_plus_D
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma tail_preserved line 530 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, HSub.hSub, And, ca_step_fun
Proof uses: id, Decidable.byContradiction, Not, Ne, And.intro, HAdd.hAdd, HDiv.hDiv, ite, Eq.mpr, congrArg, if_neg, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma F_no_internal_zeros line 543 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, F, OfNat.ofNat, HAdd.hAdd
Proof uses: Nat.recAux, Eq.refl, id, half_ceil, Decidable.byContradiction, Not, Eq.mpr, half_floor, congrArg
9 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma F_sum_step line 556 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, Eq, F, OfNat.ofNat, Finset.sum, Finset.range, HAdd.hAdd
Proof uses: id, half_ceil, ite, half_floor, HSub.hSub, Finset.sum_add_distrib, Eq.mpr, congrArg, Finset.sum_range_succ', of_eq_true, Eq.trans, True, congr, Finset.sum_congr, Eq.refl, Finset, Membership.mem, ite_cond_eq_false, And, False and 11 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma F_sum line 580 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, HAdd.hAdd, F
Proof uses: Nat.recAux, id, OfNat.ofNat, ite, Nat.casesAuxOn, of_eq_true, Eq.trans, True, congrArg, EmptyCollection.emptyCollection, Finset, Finset.sum_congr, add_zero, Membership.mem, ite_self, Finset.sum_const_zero, eq_self, Eq.mpr, Finset.sum_eq_single, Ne and 14 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma F_n_minus_1_zero line 605 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, a, Eq, F, HSub.hSub
Proof uses: Decidable.byContradiction, Not, GE.ge, Nat.le_induction, HAdd.hAdd, F_no_internal_zeros, Finset.sum, Finset.range, Finset.sum_le_sum, Membership.mem, Finset, Eq.mp, congrArg, propext, Finset.mem_range, of_eq_true, Eq.trans, True, HSMul.hSMul, Finset.card and 27 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
lemma P_le_n_minus_1 line 668 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, a, P, HSub.hSub
Proof uses: Nat.recAux, id, Decidable.byContradiction, Not, HAdd.hAdd, LT.lt, dite, HMod.hMod, F, Eq, F_n_minus_1_zero, Eq.mpr, congrArg
23 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma P_lt_n line 685 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, P, a
Proof uses: HSub.hSub, P_le_n_minus_1, Decidable.byContradiction, Not
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma F_eq_one_of_ge_one line 689 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, GE.ge, F, OfNat.ofNat, Eq
Proof uses: Decidable.byContradiction, Not, Finset.sum, Finset.range, Finset.sum_lt_sum, Membership.mem, Finset, Iff.mp, Finset.mem_range, Exists.intro, And, And.intro, Iff.mpr, HAdd.hAdd, F_sum, Finset.Ico, Eq.symm, Finset.sum_range_add_sum_Ico, LE.le, Finset.sum_eq_zero and 15 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma F_a_minus_1_val_dummy line 713 source
no axioms what this means
Statement uses: Nat, Eq
Proof uses: rfl
lemma F_a_minus_1_n_minus_2_val line 715 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Or, Eq, F, HSub.hSub, a
Proof uses: GT.gt, Decidable.byContradiction, Not, TargetF, a_is_stable, congrFun, Eq.mp, congrArg, LT.lt, ite, if_pos, ca_step_fun, HAdd.hAdd, rfl, Eq.mpr, id, Eq.symm, F_n_minus_1_zero, half_ceil, half_floor and 4 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma F_a_minus_1_n_minus_2 line 753 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, F, HSub.hSub, a
Proof uses: GT.gt, Decidable.byContradiction, Not, TargetF, a_is_stable, congrFun, Eq.mp, congrArg, LT.lt, ite, if_pos, Or, F_a_minus_1_n_minus_2_val, GE.ge, Nat.le_induction, HAdd.hAdd, F_no_internal_zeros, Finset.sum, Finset.range, Finset and 29 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
lemma F_a_minus_1_ge_one line 808 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HSub.hSub, GE.ge, F, a
Proof uses: Decidable.byContradiction, Not, Eq, Nat.le_induction, HAdd.hAdd, F_no_internal_zeros, F_a_minus_1_n_minus_2
19 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma F_a_minus_1_val line 822 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HSub.hSub, Eq, F, a
Proof uses: Decidable.byContradiction, Not, GE.ge, F_a_minus_1_ge_one, Finset.sum, Finset.range, Finset.sum_lt_sum, Membership.mem, Finset, Iff.mp, Finset.mem_range, Exists.intro, And, And.intro, Iff.mpr, of_eq_true, Eq.trans, True, congrArg, HSMul.hSMul and 29 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
def ContiguousGT1 line 872 source
no axioms what this means
Statement uses: Nat
Proof uses: LT.lt, GE.ge, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
lemma step_ge_2_implies line 875 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, ca_step_fun, OfNat.ofNat, Or, And, GT.gt, HSub.hSub
Proof uses: dite, Eq, Decidable.byContradiction, Not, Eq.mp, HAdd.hAdd, HDiv.hDiv, ite, congrArg, if_pos, if_neg
21 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ge_2_of_step line 882 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, GE.ge, HSub.hSub, ca_step_fun
Proof uses: id, dite, HAdd.hAdd, HDiv.hDiv, ite, Eq, Eq.mpr, congrArg, if_pos, Decidable.byContradiction, Not, if_neg
18 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ContiguousGT1_le line 889 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ContiguousGT1, LE.le, GE.ge, OfNat.ofNat
Proof uses: Eq, LT.lt, Or, eq_or_lt_of_le
9 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma ContiguousGT1_step line 896 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ContiguousGT1, ca_step_fun
Proof uses: LT.lt, GE.ge, OfNat.ofNat, Or, And, GT.gt, HSub.hSub, step_ge_2_implies, Decidable.byContradiction, Not, ContiguousGT1_le, LE.le, And.right, ge_2_of_step
17 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma ContiguousGT1_F_zero line 920 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, ContiguousGT1, F, OfNat.ofNat
Proof uses: LT.lt, GE.ge, id, dite, ite, Eq, Decidable.byContradiction, Not, Eq.mp, congrArg, if_neg
9 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ContiguousGT1_F line 929 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ContiguousGT1, F
Proof uses: Nat.recAux, ContiguousGT1_F_zero, Eq, HAdd.hAdd, OfNat.ofNat, ca_step_fun, rfl, Eq.mpr, id, congrArg, ContiguousGT1_step
3 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma P_a_minus_1_ge line 937 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, GE.ge, P, HSub.hSub, a
Proof uses: Decidable.byContradiction, Not, ContiguousGT1, F, HAdd.hAdd, ContiguousGT1_F, Eq, ite, F_n_plus_1_eq, F_a_minus_1_n_minus_2, F_a_minus_1_val, LT.lt, congrFun, Eq.mp, congrArg, if_pos, rfl, Ne, if_neg
24 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma P_a_eq line 962 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, P, a, HAdd.hAdd, HSub.hSub, HMod.hMod, F
Proof uses: P_succ, GT.gt, Decidable.byContradiction, Not, TargetF, a_is_stable, congrFun, Eq.mp, congrArg, LT.lt, ite, if_pos, Eq.mpr, id, Eq.symm
25 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma chip_pos_ge_4 line 979 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Or, Eq, HSub.hSub, P, a
Proof uses: GE.ge, P_a_minus_1_ge, LT.lt, P_lt_n, Decidable.byContradiction, Not, HAdd.hAdd, HMod.hMod, F, P_a_eq, F_a_minus_1_n_minus_2, F_a_minus_1_val, GT.gt, TargetF, a_is_stable, congrFun, Eq.mp, congrArg, ite, if_pos and 6 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
lemma chip_pos_1 line 1017 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Or, Eq, Nat, HSub.hSub, OfNat.ofNat, P, a
Proof uses: F, TargetF, funext, id, dite, ite, LT.lt, Eq.mpr, congrArg, if_pos, Decidable.byContradiction, Not, False, Eq.trans, if_neg, eq_false', False.elim, noConfusion_of_Nat, Nat.ctorIdx, LE.le and 1 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma chip_pos_2 line 1029 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Or, Eq, Nat, HSub.hSub, OfNat.ofNat, P, a
Proof uses: F, TargetF, funext, GE.ge, Decidable.byContradiction, Not, Eq.refl, Eq.symm, F_zero_of_ge, id, Eq.mpr, ite, LT.lt, congrArg, if_neg, Ne, congrFun, LE.le, a_min, a_is_stable and 1 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma chip_pos_3 line 1058 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Or, Eq, Nat, HSub.hSub, OfNat.ofNat, P, a
Proof uses: F, TargetF, funext, GE.ge, Decidable.byContradiction, Not, Eq.refl, Eq.symm, F_zero_of_ge, id, Eq.mpr, ite, LT.lt, congrArg, if_neg, Ne, congrFun, LE.le, a_min, a_is_stable and 1 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
lemma chip_pos line 1096 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Or, Eq, HSub.hSub, P, a
Proof uses: LT.lt, lt_trichotomy, Decidable.byContradiction, Not, chip_pos_1, Eq.symm, chip_pos_2, eq_or_lt_of_le, chip_pos_3, chip_pos_ge_4
20 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
theorem target_theorem_0 line 1111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Or, Eq, a, HAdd.hAdd
Proof uses: HSub.hSub, P, chip_pos, coupling_diff, Decidable.byContradiction, Not
15 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/A224515_conjecture_existence.lean:269 (different declaration text), APNOutputs/OEIS/A309132_conjecture_carmichael.lean:375 (different declaration text), APNOutputs/OEIS/A382590_conjecture_kth_prime_factor_is_eventually_periodic.lean:303 (different declaration text), APNOutputs/OEIS/a091669_conjecture_primitive_root.lean:275 (different declaration text), APNOutputs/OEIS/a325046_odd_terms_at_k_times_k_plus_1.lean:187 (different declaration text), APNOutputs/OEIS/oeis_103311_conjecture_0.lean:240 (different declaration text), APNOutputs/OEIS/oeis_108_conjecture_2.lean:281 (different declaration text), APNOutputs/OEIS/oeis_113254_conjecture_0.lean:153 (different declaration text), APNOutputs/OEIS/oeis_175386_conjecture_0.lean:326 (different declaration text), APNOutputs/OEIS/oeis_194806_conjecture_0.lean:495 (different declaration text), APNOutputs/OEIS/oeis_227582_conjecture_0.lean:306 (different declaration text), APNOutputs/OEIS/oeis_228143_conjecture_1.lean:730 (different declaration text), APNOutputs/OEIS/oeis_243106_conjecture_0.lean:164 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_0.lean:223 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_4.lean:841 (different declaration text), APNOutputs/OEIS/oeis_256012_conjecture_0.lean:116 (different declaration text), APNOutputs/OEIS/oeis_267581_conjecture_0.lean:212 (different declaration text), APNOutputs/OEIS/oeis_271591_conjecture_0.lean:518 (different declaration text), APNOutputs/OEIS/oeis_278070_conjecture_0.lean:91 (different declaration text), APNOutputs/OEIS/oeis_282779_conjecture_0.lean:141 (different declaration text), APNOutputs/OEIS/oeis_289411_conjecture_0.lean:189 (different declaration text), APNOutputs/OEIS/oeis_2897_conjecture_0.lean:427 (different declaration text), APNOutputs/OEIS/oeis_306424_conjecture_0.lean:300 (different declaration text), APNOutputs/OEIS/oeis_307865_conjecture_0.lean:212 (different declaration text), APNOutputs/OEIS/oeis_323557_conjecture_0.lean:214 (different declaration text), APNOutputs/OEIS/oeis_340737_conjecture_0.lean:456 (different declaration text), APNOutputs/OEIS/oeis_341254_conjecture_0.lean:136 (different declaration text), APNOutputs/OEIS/oeis_363347_conjecture_2.lean:848 (different declaration text), APNOutputs/OEIS/oeis_372761_conjecture_2.lean:756 (different declaration text), APNOutputs/OEIS/oeis_51293_conjecture_0.lean:517 (different declaration text), APNOutputs/OEIS/oeis_62567_conjecture_0.lean:329 (different declaration text), APNOutputs/OEIS/oeis_A028859_conjecture_1.lean:432 (different declaration text), APNOutputs/OEIS/oeis_A258667_conjecture_0.lean:446 (different declaration text), APNOutputs/OEIS/oeis_a211417_conjecture_specific.lean:264 (different declaration text), APNOutputs/OEIS/oeis_a237271_conjecture_2.lean:124 (different declaration text), APNOutputs/OEIS/oeis_a363102_conjecture_1.lean:302 (different declaration text), APNOutputs/OEIS/oeis_a368692_conjecture_integrality.lean:182 (different declaration text). Qualify references as target_theorem_0@path.

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