LeanFrontier / corpus
Generated after merged submissions from Lean source and immutable submission claims. Source and receiver reports remain canonical.
Whether machine-generated mathematics accumulates, or merely piles up, is a question about the dependency graph rather than the theorem count. These are the numbers that answer it, regenerated with the catalogue.
The last line is the one that resists gaming. An import costs a line and need not be used; a constant reaching another submission's statement means a theorem was written about it.
BoundedSlope.minorant — 2 submissionsBoundedSlope.slack — 2 submissionsCalkinWilf.pair — 2 submissionsChangeRinging.AdjSwap — 2 submissionsChangeRinging.rows — 2 submissionsDescartesCircle.IsQuadruple — 2 submissionsDiscriminantTower.CoprimalityIsLoadBearing — 2 submissionsDynamics.logisticMapIcc — 2 submissionsDynamics.tentMapIcc — 2 submissionsFarey.IsStrictlyBetween — 3 submissionsFordCircle.euclideanSphere — 2 submissionsFordCircle.radius — 3 submissionsHoradam.W — 3 submissionsInt.arithProgression — 2 submissionsInt.furstenbergTopology — 4 submissionsJosephus.survivor — 2 submissionsMarkovEquation.IsSolution — 5 submissionsMarkovEquation.jump — 2 submissionsMarkovTree.Move — 9 submissionsMarkovTree.NonBacktrackingFrom — 2 submissionsMarkovTree.OrientedNode — 11 submissionsMarkovTree.OrientedNode.back — 6 submissionsMarkovTree.OrientedNode.forwardCoordinate — 2 submissionsMarkovTree.OrientedNode.markovNumber — 6 submissionsMarkovTree.OrientedNode.state — 11 submissionsMarkovTree.State — 12 submissionsMarkovTree.State.IsSolution — 8 submissionsMarkovTree.State.coordinate — 2 submissionsMarkovTree.State.mk — 4 submissionsMarkovTree.State.otherSquareSum — 2 submissionsMarkovTree.State.x — 6 submissionsMarkovTree.State.y — 6 submissionsMarkovTree.State.z — 6 submissionsMarkovTree.branchNode — 2 submissionsMarkovTree.child — 5 submissionsMarkovTree.commonAncestor — 2 submissionsMarkovTree.move — 3 submissionsMarkovTree.pathMoves — 2 submissionsMarkovTree.sternMarkovNumber — 2 submissionsMarkovTree.sternNode — 7 submissionsMarkovTree.walk — 4 submissionsMatrix.fibMatrix — 2 submissionsMediant.crossDet — 7 submissionsNat.lucas — 3 submissionsNat.oneTwoCompositions — 2 submissionsNat.sylvesterNumber — 2 submissionsNat.thueMorse — 2 submissionsSternBrocot.bounds — 3 submissionsSternBrocot.pair — 6 submissionsSternDiatomic.fusc — 4 submissionsEach connected group of modules is drawn on its own. Arrows point from a module to the modules that import it; hover over a box for its full name.
Modules that neither import another corpus module nor are imported by one.
Algebra.BinomialAlgebra.Polynomial.TranslationRigidityAnalysis.FibonacciReciprocalAnalysis.HornichHlawkaAnalysis.NesbittGeometry.EulerQuadrilateralGeometry.InversiveGeometryGeometry.VarignonGeometry.WeitzenbockNumberTheory.A053067.ResidueOneNumberTheory.MarkovEquation.SlopeScaleGCDNumberTheory.PadovanNumberTheory.Transcendental.HermiteLindemannNumberTheory.TribonacciProbability.CantelliLeanFrontier.Algebra.add_add_sq{α : Type*} (a b c : α) [CommRing α] : (a + b + c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + 2 * a * b + 2 * a * c + 2 * b * c
import LeanFrontier.Algebra.BinomialA three-variable square identity for the initial library seed.
LeanFrontier.Polynomial.eq_C_eval_zero_of_comp_X_add_C_eq_self{p : R[X]} {a : R} (ha : a ≠ 0) (hperiod : p.comp (X + C a) = p) : p = C (p.eval 0)
import LeanFrontier.Algebra.Polynomial.TranslationRigidityc67573a56e6c4d3406c1fbbf2a95a1a95fe337b1 · downstream import passpropext, Classical.choice, Quot.sound4471db112a180535628781ebb0b5f4883b29fbaca8befa7ba4b3bcf16bdcd0d9A polynomial over a characteristic-zero integral domain with a nonzero additive period is constant.
LeanFrontier.Polynomial.natDegree_eq_zero_of_comp_X_add_C_eq_self{p : R[X]} {a : R} (ha : a ≠ 0) (hperiod : p.comp (X + C a) = p) : p.natDegree = 0
import LeanFrontier.Algebra.Polynomial.TranslationRigidity2a51df4552d5e32022d389d736d1a6b441f415d8 · downstream import passpropext, Classical.choice, Quot.sounde837b697abf2a5e34742cdb8a2ab48e26c51161cb766e2a468488a2421ac4ec3A polynomial with a nonzero additive period has degree zero.
LeanFrontier.Nat.three_pow_le_two_pow_mul_fib: ∀ n : ℕ, 3 ^ n ≤ 2 ^ n * Nat.fib (n + 3) | 0 => by decide | n + 1 => by have ih
import LeanFrontier.Analysis.FibonacciReciprocaldf9328d310d8df9e1c6348d7c21dbbd4de9a59e9 · downstream import passpropext, Classical.choice, Quot.soundb1fa558d0766f970035c48b3c171e8e2182cce0b0e1e6c803639909cb088d4d6Exponential growth of the Fibonacci numbers, in `ℕ`: `3 ^ n ≤ 2 ^ n * fib (n + 3)`, i.e. `fib (n + 3)` dominates `(3 / 2) ^ n`.
LeanFrontier.Nat.inv_fib_add_three_le(n : ℕ) : ((Nat.fib (n + 3) : ℝ))⁻¹ ≤ (2 / 3) ^ n
import LeanFrontier.Analysis.FibonacciReciprocaldf9328d310d8df9e1c6348d7c21dbbd4de9a59e9 · downstream import passpropext, Classical.choice, Quot.sounddd17b6f60d74a30eb73a3f910f22c90c9ac79ffdba32af1f9deeb5c8d4f9521aThe reciprocal Fibonacci numbers are dominated by the geometric sequence `(2 / 3) ^ n` after shifting the index by three.
LeanFrontier.Nat.summable_inv_fib: Summable fun n : ℕ => ((Nat.fib n : ℝ))⁻¹
import LeanFrontier.Analysis.FibonacciReciprocaldf9328d310d8df9e1c6348d7c21dbbd4de9a59e9 · downstream import passpropext, Classical.choice, Quot.sounda20dbe7adf8e9a119c458d3f9554e15fe8298def801836d1d5bf2a3136fe1a36The reciprocal Fibonacci series converges. The term at `n = 0` is `(0 : ℝ)⁻¹ = 0`, so summing over all indices is harmless.
LeanFrontier.Nat.tsum_inv_fib_le: ∑' n : ℕ, ((Nat.fib n : ℝ))⁻¹ ≤ 5
import LeanFrontier.Analysis.FibonacciReciprocaldf9328d310d8df9e1c6348d7c21dbbd4de9a59e9 · downstream import passpropext, Classical.choice, Quot.sound72b64989eeca51cf3fb26f2403c65def68771fcfcadda8f024a8231ff088a065A crude explicit bound on the reciprocal Fibonacci constant: the head `1/1 + 1/1` plus the geometric tail bound `∑ (2/3) ^ n = 3`. The true value is `ψ ≈ 3.36`.
LeanFrontier.InnerProductGeometry.hornich_hlawka(x y z : E) : ‖x + y‖ + ‖y + z‖ + ‖z + x‖ ≤ ‖x‖ + ‖y‖ + ‖z‖ + ‖x + y + z‖
import LeanFrontier.Analysis.HornichHlawkad60481ed851b466a413885d1589d3717c36b46b6 · downstream import passpropext, Classical.choice, Quot.soundc00924ad4279807a4af08db87e7d45c24c4fdf53b2f077a8a88789d9cf4184d8**Hornich-Hlawka inequality.** In a real inner-product space, the sum of the norms of the three pairwise sums is bounded by the sum of the three individual norms and the norm of the total sum.
LeanFrontier.Nesbitt.inequality(a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (3 : ℝ) / 2 ≤ a / (b + c) + b / (c + a) + c / (a + b)
import LeanFrontier.Analysis.Nesbitt9ea660b09c15b3e3f21a733fbc8f49724805778e · downstream import passpropext, Classical.choice, Quot.sound1bd32427bebb26df667d23823d01207c95f89df0e66f6023feeac9a63ecce09f**Nesbitt's inequality** for three positive real numbers.
LeanFrontier.BoundedSlope.slack_nonneg(ha : 0 ≤ a) (hb : 0 ≤ b) (i j : ℕ) : 0 ≤ slack a b i j
import LeanFrontier.Analysis.SlopeMinorant.Constraints8e0d50f1dbc28194211c7852b6bafc0a669dbea0 · downstream import passpropext, Classical.choice, Quot.soundaacc577c8b1017b46468d85e2e433704692758249e39fb053134f6149ea9ab9eThe slack budget between two indices is nonnegative when both rates are.
LeanFrontier.BoundedSlope.minorant_anti_constraints(hst : s ⊆ t) (hs : s.Nonempty) (ht : t.Nonempty) (i : ℕ) : minorant a b L t ht i ≤ minorant a b L s hs i
import LeanFrontier.Analysis.SlopeMinorant.Constraints8e0d50f1dbc28194211c7852b6bafc0a669dbea0 · downstream import passpropext, Classical.choice, Quot.soundbd1f8c8944996295f2d4287341f8f30c61051f34b16de247a9be48fea7832174Constraining the ceiling at more indices can only lower the greatest minorant.
LeanFrontier.BoundedSlope.inf_ceiling_le_minorant(ha : 0 ≤ a) (hb : 0 ≤ b) (hs : s.Nonempty) (i : ℕ) : s.inf' hs L ≤ minorant a b L s hs i
import LeanFrontier.Analysis.SlopeMinorant.Constraints8e0d50f1dbc28194211c7852b6bafc0a669dbea0 · downstream import passpropext, Classical.choice, Quot.sound6801f6442f31a878fae5d8f8c0a89c752261880f661ab2c04825a628326eeb63At every index the minorant stays at or above the least constrained ceiling value.
LeanFrontier.BoundedSlope.minorant_le_ceiling(a b : ℝ) (L : ℕ → ℝ) (hs : s.Nonempty) {i : ℕ} (hi : i ∈ s) : minorant a b L s hs i ≤ L i
import LeanFrontier.Analysis.SlopeMinorant6dde113ebc31f6ae5f5444bbdb61190659fd7e30 · downstream import passpropext, Classical.choice, Quot.sounda97331fd25e2bd2be513b9fa4754bfdec2c46fd1c72c60f691194cd05b74affaLeanFrontier.BoundedSlope.minorant_stepBounded(ha : 0 ≤ a) (hb : 0 ≤ b) (L : ℕ → ℝ) (hs : s.Nonempty) : StepBounded a b (minorant a b L s hs)
import LeanFrontier.Analysis.SlopeMinorant6dde113ebc31f6ae5f5444bbdb61190659fd7e30 · downstream import passpropext, Classical.choice, Quot.sound85ae034f74f95c0c22b37c896f15544e45542f533ba36f3dc03a6d888ec4f035The minorant is admissible: it satisfies the increment bounds everywhere, including outside the constrained set.
LeanFrontier.BoundedSlope.le_minorant(hs : s.Nonempty) (hv : StepBounded a b v) (hL : ∀ j ∈ s, v j ≤ L j) (i : ℕ) : v i ≤ minorant a b L s hs i
import LeanFrontier.Analysis.SlopeMinorant6dde113ebc31f6ae5f5444bbdb61190659fd7e30 · downstream import passpropext, Classical.choice, Quot.sound0ad724b6bd89284df7cf3816163c2a2b87a29de3825e74bd9b009fcb5d1760b1The minorant is the greatest admissible sequence: any step bounded competitor that respects the ceiling on `s` lies below it at every index.
LeanFrontier.BoundedSlope.minorant_eq_ceiling_of_stepBounded(hs : s.Nonempty) (hL : StepBounded a b L) {i : ℕ} (hi : i ∈ s) : minorant a b L s hs i = L i
import LeanFrontier.Analysis.SlopeMinorant6dde113ebc31f6ae5f5444bbdb61190659fd7e30 · downstream import passpropext, Classical.choice, Quot.sound1d615de98a2af54921c788845af7ab55ce22b451e41435c79233a038885f687fA ceiling that already satisfies the increment bounds is left untouched on `s`.
LeanFrontier.GraphTheory.caroWei_implies_turan_bound(G : SimpleGraph V) [DecidableRel G.Adj] : ∃ I : Finset V, G.IsIndepSet (I : Set V) ∧ ((Fintype.card V : ℚ) ^ 2) / (2 * (G.edgeFinset.card : ℚ) + (Fintype.card V : ℚ)) ≤ (I.card : ℚ)
import LeanFrontier.Combinatorics.CaroWei.TuranBound93c9556d72795bfa829bd00b267e5f4ab370a72b · downstream import passpropext, Classical.choice, Quot.sound1b812366a80c34e72660d36e09ac4f7e9ba0b7108a2b42b039bc084b052d3371**Turán's average-degree lower bound for independent sets**, obtained as a corollary of Caro-Wei. Every finite simple graph has an independent finset `I` satisfying `|V|² / (2 |E| + |V|) ≤ |I|`. The statement is over `ℚ`, avoiding floor/ceiling noise. For the empty graph both numerator and denominator vanish, and Lean's field convention makes the left-hand side zero.
LeanFrontier.GraphTheory.caroWei(G : SimpleGraph V) [DecidableRel G.Adj] : ∃ I : Finset V, G.IsIndepSet (I : Set V) ∧ (∑ v : V, (1 : ℚ) / ((G.degree v : ℚ) + 1)) ≤ (I.card : ℚ)
import LeanFrontier.Combinatorics.CaroWeia65e555e6bb02438c8f4f69e624f316edee01ce1 · downstream import passpropext, Classical.choice, Quot.soundedc1400edd39a6b5b1811b120d841ccdc90c54a860a0051b1299b5e0ccbe3796**Caro-Wei theorem.** Every finite simple graph has an independent set whose cardinality is at least `∑ v, 1 / (degree v + 1)`. The bound is stated over `ℚ`, so no rounding or floor operation obscures the sharp degree-dependent estimate.
LeanFrontier.Nat.mem_circularOneTwoTilings_add_two{n : ℕ} {crosses : Bool} {l : List ℕ} : (crosses, l) ∈ circularOneTwoTilings (n + 2) ↔ (crosses = false ∧ l ∈ oneTwoCompositions (n + 2)) ∨ (crosses = true ∧ l ∈ oneTwoCompositions n)
import LeanFrontier.Combinatorics.CircularDominoTilings1c6bcaa3eff6b2212a939e70948a07003d4313c3 · downstream import passpropext, Classical.choice, Quot.sound65695fe4ea64d79c8b4303513fd2aeb9d2aa0ca2c2689cb829ecf9f031ed2059For a circle of `n + 2` labelled cells, membership splits exactly into the no-crossing strip tilings of all cells and the crossing tilings of the remaining `n` cells.
LeanFrontier.Nat.card_circularOneTwoTilings_add_two(n : ℕ) : (circularOneTwoTilings (n + 2)).card = lucas (n + 2)
import LeanFrontier.Combinatorics.CircularDominoTilings1c6bcaa3eff6b2212a939e70948a07003d4313c3 · downstream import passpropext, Classical.choice, Quot.soundd26b3a040f0d0d552d3f336f676c7511eb5063671ef5abd024194a76a0ee1ffbCircular square-and-domino tilings of `n + 2` labelled cells are counted by the Lucas number `L (n + 2)`. The two tagged cases contribute `F (n + 3)` and `F (n + 1)` respectively.
LeanFrontier.Nat.mem_oneTwoCompositions{n : ℕ} {l : List ℕ} : l ∈ oneTwoCompositions n ↔ l.sum = n ∧ ∀ x ∈ l, x = 1 ∨ x = 2
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.sounda1d2e6cf0573257126542310990cc7482d85ed13bdbc7bf7e7acb8ad89daf313Membership in `oneTwoCompositions n` is exactly the a priori description: the list sums to `n` and every part is `1` or `2`.
LeanFrontier.Nat.card_oneTwoCompositions: ∀ n, (oneTwoCompositions n).card = Nat.fib (n + 1) | 0 => by simp | 1 => by simp | n + 2 => by have ih1
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.sound035d0182ec4c058222b429ee2cbd933067074263f4383791dbf26cf71c0f9e9aThe compositions of `n` into parts `1` and `2` are counted by the Fibonacci numbers: there are `fib (n + 1)` of them.
LeanFrontier.Nat.length_le_of_mem_oneTwoCompositions{n : ℕ} {l : List ℕ} (h : l ∈ oneTwoCompositions n) : l.length ≤ n
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.sound4ffd93a4ead03a02f0f74291db938abb065e9301124abd78c5cd8b7bf5792054A composition of `n` into parts `1` and `2` has at most `n` parts.
LeanFrontier.Nat.le_two_mul_length_of_mem_oneTwoCompositions{n : ℕ} {l : List ℕ} (h : l ∈ oneTwoCompositions n) : n ≤ 2 * l.length
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.soundb17b89b58c4f503e19462d6f8fce12166ae7c10773e255616960223ad8bb945fA composition of `n` into parts `1` and `2` has at least `n / 2` parts, in the subtraction-free form `n ≤ 2 * length`.
LeanFrontier.Nat.reverse_mem_oneTwoCompositions{n : ℕ} {l : List ℕ} (h : l ∈ oneTwoCompositions n) : l.reverse ∈ oneTwoCompositions n
import LeanFrontier.Combinatorics.FibonacciComposition2a5fd3af9b1cfda404b6aeb7f82ee1a55f425ff8 · downstream import passpropext, Classical.choice, Quot.soundd7932629d1386f62c36555ff7fbfcbd1983b56e559859e8d857701d59f153660Reading a composition of `n` into parts `1` and `2` right to left gives another one: the set is closed under list reversal.
LeanFrontier.Finset.laguerre_samuelson{ι : Type*} (s : Finset ι) (f : ι → ℝ) {x : ι} (hx : x ∈ s) : ((s.card : ℝ) * f x - ∑ y ∈ s, f y) ^ 2 ≤ ((s.card : ℝ) - 1) * ((s.card : ℝ) * ∑ y ∈ s, f y ^ 2 - (∑ y ∈ s, f y) ^ 2)
import LeanFrontier.Combinatorics.FiniteVariance.LaguerreSamuelson0f77b33fe7ba7d353065ef83b4d529fb12e4f332 · downstream import passpropext, Classical.choice, Quot.sounde61ee16a61b9b77d3ba2f34bba88720733f047f9a7ba2d39661b19b22e32e2e8**Laguerre-Samuelson inequality**, in a division-free finite-family form. For any member `x` of a finite real family `s`, its squared deviation from the mean is at most `|s| - 1` times the population variance. The displayed form avoids division and remains meaningful for the singleton case.
LeanFrontier.Finset.sum_pairwise_sq_sub(s : Finset ι) (f : ι → R) : ∑ x ∈ s, ∑ y ∈ s, (f x - f y) ^ 2 = 2 * (s.card : R) * ∑ x ∈ s, f x ^ 2 - 2 * (∑ x ∈ s, f x) ^ 2
import LeanFrontier.Combinatorics.FiniteVariance47c45b2e214d2fdfea7dd4d9985eb68955be3549 · downstream import passpropext, Classical.choice, Quot.sound70f317af42b1e7900f79b5ac2fff5be545386ed9e593ce094d15932ab787f6a4The total squared difference over all ordered pairs in a finite family is twice its unnormalized variance.
LeanFrontier.Josephus.josephus_pos{n : ℕ} (hn : n ≠ 0) : 0 < josephus n
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.soundd7d6133cc1bf02d0855ac5d9d8a1ac359958eb74d86c9645fe97dbac49c43d9fThe survivor's number is positive as soon as anybody is standing in the circle.
LeanFrontier.Josephus.josephus_two_pow(m : ℕ) : josephus (2 ^ m) = 1
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.sound55b8ee1544c421f762dde5e25e7abaf4d19d264d8a1547352ebc39fde40b6c08Among `2 ^ m` people, the survivor is person `1`.
LeanFrontier.Josephus.josephus_eq_survivor_add_one{n : ℕ} (hn : n ≠ 0) : josephus n = survivor n + 1
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.sound743913e60d6416a31fed9e2c06878dc320557c9e267f8d4b47af7b929d7936cbThe bridge between the two conventions: the one-indexed survivor is the zero-indexed survivor shifted by one. Both functions are defined by independent recursions - `survivor` steps the circle size by one, `josephus` halves it - so this identity cross-validates the two formalizations.
LeanFrontier.Josephus.odd_josephus{n : ℕ} (hn : n ≠ 0) : Odd (josephus n)
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.sound1e52e9b5b685f3ab82ecfcd1496eafdc711926af80f51b093ad717bd91f50376The survivor's number is odd: the first pass around the circle eliminates everyone whose number is even.
LeanFrontier.Josephus.josephus_le(n : ℕ) : josephus n ≤ n
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.sound9fc4d177837f8d040bbd6af4a58a8cc1c90abca9960041b04d0018d0bb1e8ffcThe survivor's number is at most `n`.
LeanFrontier.Josephus.josephus_eq_self_iff{n : ℕ} : josephus n = n ↔ ∃ m, n = 2 ^ m - 1
import LeanFrontier.Combinatorics.Josephus.OneIndexed749994bdabd865b56568789d00cf3ae4b9f5146e · downstream import passpropext, Classical.choice, Quot.soundd18a3b866f71a620ceaf5d28538852e6baf9dd8414d2e831ecbfb419e4d40f34Person `n` survives if and only if `n + 1` is a power of two: the survivor equals `n` exactly when `n = 2 ^ m - 1`, i.e. when the binary expansion of `n` is all ones.
LeanFrontier.Josephus.survivor_lt_self(n : ℕ) (hn : n ≠ 0) : survivor n < n
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import pass238ae38b1378919d741ce8c78903eec3a859918b8baaa87c444435055370fc24The survivor of a nonempty circle is one of its positions.
LeanFrontier.Josephus.survivor_eq_two_mul_sub_two_pow_log(n : ℕ) (hn : n ≠ 0) : survivor n = 2 * (n - 2 ^ Nat.log 2 n)
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.soundc920e0d923688b6c55e5088169aad76b0262b78b3d113ebab0ae0270756ff1a8The survivor of a circle of `n` people is `2 * (n - 2 ^ ⌊log₂ n⌋)`.
LeanFrontier.Josephus.survivor_two_pow_add(m k : ℕ) (hk : k < 2 ^ m) : survivor (2 ^ m + k) = 2 * k
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.soundbd21f35278497967b1fb4143c21eeac0bf89253ef567e588cacbc6bec2caf9e2Writing the size of the circle as `2 ^ m + k` with `k < 2 ^ m`, the survivor is `2 * k`: in binary, the leading one of `n` is deleted and a zero is appended.
LeanFrontier.Josephus.survivor_two_mul(n : ℕ) (hn : n ≠ 0) : survivor (2 * n) = 2 * survivor n
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.sound97ca93a26b9251a0e7826b4f3ad5580d0202065b1bf40fedae682b34856ea93aDoubling the circle doubles the survivor.
LeanFrontier.Josephus.survivor_two_mul_add_one(n : ℕ) (hn : n ≠ 0) : survivor (2 * n + 1) = 2 * survivor n + 2
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.sound41bfc9ba1853413e547637b009f2491eb870529eb1bb6e1bb4d2df1492dc1c75Doubling the circle and adding one person moves the survivor two places on.
LeanFrontier.Josephus.survivor_eq_zero_iff(n : ℕ) (hn : n ≠ 0) : survivor n = 0 ↔ ∃ m, n = 2 ^ m
import LeanFrontier.Combinatorics.Josephus2640351308f57c0d488f84d4d37cad41c806a6a4 · downstream import passpropext, Classical.choice, Quot.sound7f4af9e7df50272e1766792ed6dbb0b91455a373602f785ed5070fff0170e6e6The person who starts the count survives exactly when the circle has a power of two members.
LeanFrontier.Dynamics.ulamMapIcc_bijective: Function.Bijective ulamMapIcc
import LeanFrontier.Dynamics.LogisticConjugacyb946d0880f775673cf016d10e08b2a046b0f6a95 · downstream import passpropext, Classical.choice, Quot.sound38a5531e57da74e472a2b2d5735bc65bcf39f68d05327cc7c35081f13cdf532dThe Ulam map is a bijection of the closed unit interval.
LeanFrontier.Dynamics.ulamHomeomorph_apply(x : Icc (0 : ℝ) 1) : (ulamHomeomorph x : ℝ) = ulamMap (x : ℝ)
import LeanFrontier.Dynamics.LogisticConjugacyb946d0880f775673cf016d10e08b2a046b0f6a95 · downstream import passpropext, Classical.choice, Quot.soundac363a82649e9b35d5232dcb8fc9c774a5fd103340e4e20e661b7cb6baa85801LeanFrontier.Dynamics.ulamHomeomorph_semiconj_tentMap_logisticMap: Function.Semiconj (ulamHomeomorph : Icc (0 : ℝ) 1 → Icc (0 : ℝ) 1) tentMapIcc logisticMapIcc
import LeanFrontier.Dynamics.LogisticConjugacyb946d0880f775673cf016d10e08b2a046b0f6a95 · downstream import passpropext, Classical.choice, Quot.sound8b62c8e4292250ec28ce520f8c77907c50dbd3cc28c7eabc5dfd6e4013e6d2c1The Ulam homeomorphism gives a genuine topological conjugacy between the tent and logistic self-maps of the closed unit interval.
LeanFrontier.Dynamics.sin_sq_semiconj_tentMap_logisticMap: Function.Semiconj (fun x => sin (π * x / 2) ^ 2) tentMap logisticMap
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.soundabade14edd04a63275420d05bf939172ffb177f561688008fe196cd77a7a6fadThe Ulam-von Neumann semiconjugacy: `x ↦ sin (π * x / 2) ^ 2` intertwines the tent map and the logistic map.
LeanFrontier.Dynamics.sin_sq_tentMap_iterate(n : ℕ) (x : ℝ) : sin (π * tentMap^[n] x / 2) ^ 2 = logisticMap^[n] (sin (π * x / 2) ^ 2)
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound6f8f2decb9c627d69f4b46e2775113f4832039844e6fb16b000d4fb2cda2477aThe semiconjugacy transports every iterate of the tent map to the corresponding iterate of the logistic map.
LeanFrontier.Dynamics.tentMap_mem_Icc{x : ℝ} (hx : x ∈ Set.Icc (0 : ℝ) 1) : tentMap x ∈ Set.Icc (0 : ℝ) 1
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound08724dec514c51d4aba2af7d23bb1e2bdf9278cba63ed601fe4bc88b5ab247deThe tent map sends the unit interval into itself.
LeanFrontier.Dynamics.logisticMap_mem_Icc{x : ℝ} (hx : x ∈ Set.Icc (0 : ℝ) 1) : logisticMap x ∈ Set.Icc (0 : ℝ) 1
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound92f5da7bdc91643cb8ee8bf8cc4cc82f4bc071429203af92416a81b03c9f829eThe logistic map sends the unit interval into itself.
LeanFrontier.Dynamics.logisticMap_eq_self_iff{x : ℝ} : logisticMap x = x ↔ x = 0 ∨ x = 3 / 4
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.soundeb984d1597f2efff206cab2df6b3933168c427cc53144f4990fab5d99a4065d0The fixed points of the logistic map are exactly `0` and `3/4`.
LeanFrontier.Dynamics.isPeriodicPt_logisticMap_two: Function.IsPeriodicPt logisticMap 2 ((5 + Real.sqrt 5) / 8)
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound5434f354131f1014438da5afea1708334aa33b062e04c2f7a833acdf87dba142`(5 + √5)/8` is a periodic point of the logistic map of period two.
LeanFrontier.Dynamics.logisticMap_apply_ne_self_of_period_two: logisticMap ((5 + Real.sqrt 5) / 8) ≠ (5 + Real.sqrt 5) / 8
import LeanFrontier.Dynamics.LogisticMap2fda2715ee6290faa675941d7dbbbd8af0f19035 · downstream import passpropext, Classical.choice, Quot.sound55701b8085f7369aab21f504c5b3a08f020a4689b8f7a16046d7fb32e2992905The two-cycle is genuine: `(5 + √5)/8` is not a fixed point, so its period is exactly two.
LeanFrontier.Dynamics.dense_periodicPts_tentMapIcc: Dense (Function.periodicPts tentMapIcc)
import LeanFrontier.Dynamics.LogisticPeriodicDensity868f0b733c5de38a8805645385d1b8904f591272 · downstream import passpropext, Classical.choice, Quot.sound662980c816725006fbe2ad278b5eeebb192af7211369be6d46e1cfca7b85dcdaThe periodic points of the full tent map are dense in the closed unit interval.
LeanFrontier.Dynamics.dense_periodicPts_logisticMapIcc: Dense (Function.periodicPts logisticMapIcc)
import LeanFrontier.Dynamics.LogisticPeriodicDensity868f0b733c5de38a8805645385d1b8904f591272 · downstream import passpropext, Classical.choice, Quot.sounde26a61fa4f8ebb84bc6ea1713b450ea5d30c8eb2752b79bbc9f05fe36598e8d8The periodic points of the logistic map at parameter four are dense in the closed unit interval.
LeanFrontier.EuclideanGeometry.euler_quadrilateral(a b c d : P) : dist a b ^ 2 + dist b c ^ 2 + dist c d ^ 2 + dist d a ^ 2 = dist a c ^ 2 + dist b d ^ 2 + 4 * dist (midpoint ℝ a c) (midpoint ℝ b d) ^ 2
import LeanFrontier.Geometry.EulerQuadrilateral65031c82657fb39f31a6fff01849cd242a335744 · downstream import passpropext, Classical.choice, Quot.sound2d7cd482c41548873c8e10a015a27c4c476213037bab782747a103affd652172**Euler's quadrilateral theorem.** For any four points in a real Euclidean affine space, the sum of the squares of the four side lengths equals the sum of the squares of the diagonal lengths plus four times the square of the distance between the diagonal midpoints.
LeanFrontier.FordCircle.mediant_is_unique_largest_in_farey_gap{a b c d : ℤ} (hb : 0 < b) (hd : 0 < d) (hdet : Mediant.crossDet a b c d = 1) : Farey.IsStrictlyBetween a b (a + c) (b + d) c d ∧ ∀ {p q : ℤ}, Farey.IsStrictlyBetween a b p q c d → radius (q : ℝ) ≤ radius ((b + d : ℤ) : ℝ) ∧ (radius (q : ℝ) = radius ((b + d : ℤ) : ℝ) ↔ p = a + c ∧ q = b + d)
import LeanFrontier.Geometry.FareyFordCircle606524387e44207494e49f32886572a1bd771075 · downstream import passpropext, Classical.choice, Quot.sounde036783f594eb0e2768b499c2b143c9e578742acd93d16203826cc41fb526443Between positive-denominator Farey neighbours, the mediant lies in the open gap and its Ford-circle radius is maximal there. Equality of radii uniquely identifies the mediant numerator and denominator. Fractions are intentionally represented by integer numerator/denominator pairs, matching the accepted `Farey` and `Mediant` APIs. The strict-betweenness hypothesis forces every competing denominator to be at least `b + d > 0`, so non-reduced or negative-denominator representatives cannot create a spurious equality case.
LeanFrontier.FordCircle.farey_mediant_descartes_configuration{a b c d : ℝ} (hb : 0 < b) (hd : 0 < d) (hdet : Mediant.crossDet a b c d = 1) : (euclideanSphere a b).IsExtTangent (euclideanSphere c d) ∧ (euclideanSphere a b).IsExtTangent (euclideanSphere (a + c) (b + d)) ∧ (euclideanSphere (a + c) (b + d)).IsExtTangent (euclideanSphere c d) ∧ DescartesCircle.IsQuadruple (0 : ℝ) (radius b)⁻¹ (radius d)⁻¹ (radius (b + d))⁻¹
import LeanFrontier.Geometry.FordCircleDescartes5cfadeef4bf0262ea553633d0f72c0edd17c2391 · downstream import passpropext, Classical.choice, Quot.sound43d7d1a707d77915017106285019b9a6593b31baeef9ec863c1fc0784fca3144A positive-denominator unimodular pair and its mediant form a three-circle Ford configuration: the parent circles and mediant circle are pairwise externally tangent, and their actual curvatures (reciprocal radii), together with the horizontal tangent line of curvature zero, satisfy Descartes' circle relation.
LeanFrontier.FordCircle.isExtTangent_euclideanSphere_iff{p q r s : ℝ} (hq : q ≠ 0) (hs : s ≠ 0) : (euclideanSphere p q).IsExtTangent (euclideanSphere r s) ↔ Mediant.crossDet p q r s ^ 2 = 1
import LeanFrontier.Geometry.FordCircleTangencyede9830d7a7bd19c97cafe0a873256e7922cae3b · downstream import passpropext, Classical.choice, Quot.sounda1e1264d75c5a06f35511fc8d87b57fe2237e53fa3cefe5a59ef8f0959e96b5eTwo geometric Ford circles with nonzero denominators are externally tangent in Mathlib's `EuclideanGeometry.Sphere` sense exactly when their cross determinant has square `1`. This is the geometric form of the Farey-neighbour tangency criterion proved algebraically in `LeanFrontier.NumberTheory.FordCircle`.
LeanFrontier.InversiveGeometry.reflect_eq_self_iff(z : ℂ) (hden : (A : ℂ) * conj z + B ≠ 0) : reflect A C B z = z ↔ hermitianForm A C B z = 0
import LeanFrontier.Geometry.InversiveGeometry934a5220c5648b5135fceb1887d539b1b413f446 · downstream import passpropext, Classical.choice, Quot.sound749a005d18fd0cfc826ee214f1f4946998f77421e544457676d12c724faa7509The reflection fixes exactly the points of the generalized circle, away from its pole.
LeanFrontier.InversiveGeometry.reflect_reflect(z : ℂ) (hden1 : (A : ℂ) * conj z + B ≠ 0) (hden2 : (A : ℂ) * conj (reflect A C B z) + B ≠ 0) : reflect A C B (reflect A C B z) = z
import LeanFrontier.Geometry.InversiveGeometry934a5220c5648b5135fceb1887d539b1b413f446 · downstream import passpropext, Classical.choice, Quot.soundb38c06b1173934da0ab71d7b8cbb2cc5f1f984c96d70237d31cf622da7370e36The reflection is an involution, wherever both applications are defined.
LeanFrontier.AffineGeometry.varignon_theorem(a b c d : P) : (midpoint ℝ b c -ᵥ midpoint ℝ a b = midpoint ℝ c d -ᵥ midpoint ℝ d a) ∧ (midpoint ℝ c d -ᵥ midpoint ℝ b c = midpoint ℝ d a -ᵥ midpoint ℝ a b)
import LeanFrontier.Geometry.Varignonf9b9b0df44e8f95c50ac5026728113ec03c2a980 · downstream import passpropext, Classical.choice, Quot.sound75190a4e76e80f30105dae22610307f5438fc4cf93164f2e59619cb319aadb70**Varignon's theorem.** The four side midpoints of an arbitrary quadrilateral form a parallelogram, expressed by equality of both pairs of opposite side vectors.
LeanFrontier.EuclideanGeometry.weitzenbock_inequality(p₁ p₂ p₃ : P) : 4 * √(3 : ℝ) * (1 / 2 * dist p₁ p₂ * dist p₃ p₂ * sin (∠ p₁ p₂ p₃)) ≤ dist p₁ p₂ ^ 2 + dist p₃ p₂ ^ 2 + dist p₁ p₃ ^ 2
import LeanFrontier.Geometry.Weitzenbock0bcb8be77ae2fc0ae765e62d4301cdf459df73f7 · downstream import passpropext, Classical.choice, Quot.sounddba1ebf0dd968635821b34ed236b4257d2c7984de1adf7570271b82557f690cb**Weitzenböck's inequality.** For three points in a real Euclidean affine space, four times `√3` times the triangle area is at most the sum of the squares of its side lengths. The area is written as `(1/2)ab sin γ`, with `γ` the angle at the middle point.
LeanFrontier.ChangeRinging.length_rows(l : List α) : (rows l).length = Nat.factorial l.length
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext, Classical.choice, Quot.soundf0c151bdc16fea2c4504d9f88b1bdf9b534aece930dc78e90930779c858ff22dThe extent property, first part: the plain changes ring `(length l)!` rows.
LeanFrontier.ChangeRinging.mem_rows{s l : List α} : s ∈ rows l ↔ s ~ l
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext, Classical.choice, Quot.sound49d0c178677e3b25d3bfb050fe7c7c05ac07d43fbb3e3a759c472478f4951071The extent property, second part: a row is rung exactly when it is an ordering of the bells of the start row.
LeanFrontier.ChangeRinging.nodup_rows{l : List α} (hl : l.Nodup) : (rows l).Nodup
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext, Classical.choice, Quot.sound075f4a7cc21ba7bbf58c1455bb603473649d9596039d77bccb1a8facc06db0bbThe extent property, third part: when the bells are distinct, no row is rung twice.
LeanFrontier.ChangeRinging.isChain_adjSwap_rows(l : List α) : IsChain AdjSwap (rows l)
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext, Classical.choice, Quot.sound00829909654dc2b26db95b15a798cdfc3c3fa543d7e32293be718027989aff0bThe extent property, fourth part: consecutive rows differ by a single change of two adjacent bells. This is the statement that the plain changes can actually be rung.
LeanFrontier.ChangeRinging.head_rows(l : List α) : (rows l).head? = some l
import LeanFrontier.GroupTheory.ChangeRingingd06960bd185f218639de3f06964e47a20b811d31 · downstream import passpropext22524ccf0a83dd3d23eda2ecb316d8368f9cebc3ef310f206015e86fe3657076The ringing starts from the given row.
LeanFrontier.ChangeRinging.rows_append_pair_getLast(p : List α) (x y : α) : (rows (p ++ [x, y])).getLast? = some (p ++ [y, x])
import LeanFrontier.GroupTheory.ChangeRingingCyclicaafd215d680d5619d21287e94d09401221d8f1bc · downstream import passpropext, Classical.choice, Quot.sound2f83984a690922c18bf5d665543d362b26647e30b920433b65cc25c6a66e829dThe exact endpoint of the plain changes: if the starting row is written as a prefix followed by two final bells, the last row is obtained by swapping precisely those final two bells.
LeanFrontier.ChangeRinging.exists_last_adjSwap_first_of_two_le_length(l : List α) (h : 2 ≤ l.length) : ∃ last, (rows l).getLast? = some last ∧ AdjSwap last l
import LeanFrontier.GroupTheory.ChangeRingingCyclicaafd215d680d5619d21287e94d09401221d8f1bc · downstream import passpropext, Classical.choice, Quot.sound65cbf74b1b691e8b7f9828df790ba67ccda2364206f7fefcc9386f5ff94112eeFor every start row with at least two bells, the last row of the plain changes differs from the first by one adjacent transposition. Together with `head_rows` and `isChain_adjSwap_rows`, this is the cyclic-closing edge of the plain-changes Gray code.
LeanFrontier.Matrix.fibMatrix_pow_succ(n : ℕ) : fibMatrix ^ (n + 1) = !![(Nat.fib (n + 2) : ℤ), Nat.fib (n + 1); Nat.fib (n + 1), Nat.fib n]
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.sound09210f03f0e118abe5d852e6a6ea437ac0f66f04cf471fd2b461e5dee9ba2ea2The Q-matrix power formula: `Q ^ (n + 1) = !![F (n + 2), F (n + 1); F (n + 1), F n]`.
LeanFrontier.Matrix.det_fibMatrix: fibMatrix.det = -1
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.sound708dd0f746f9a5b64ecd1cb9a0fb633ba182f48d4ab48893997f85499b4198a4LeanFrontier.Matrix.det_fibMatrix_pow(n : ℕ) : (fibMatrix ^ n).det = (-1) ^ n
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.soundce13de3337d623eeaa9f0f24b3fb6b06396e08f9501b8aae9b197ae8313a77b6The powers of the Q-matrix alternate in determinant: `det (Q ^ n) = (-1) ^ n`. Expanding the left side with `fibMatrix_pow_succ` and `Matrix.det_fin_two` recovers Cassini's identity.
LeanFrontier.Matrix.trace_fibMatrix_pow_succ(n : ℕ) : (fibMatrix ^ (n + 1)).trace = Nat.fib n + Nat.fib (n + 2)
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.soundd418b327cd9747f3319f5f7c6cf58f61b8dc92083b1f4792ccf836c39aa321aaThe trace of `Q ^ (n + 1)` is `F n + F (n + 2)`, the Lucas number `L (n + 1)`.
LeanFrontier.Matrix.isUnit_fibMatrix: IsUnit fibMatrix
import LeanFrontier.LinearAlgebra.FibonacciMatrixe2940734f286f4da13d19d5e4771c21613f02798 · downstream import passpropext, Classical.choice, Quot.sound01fcf7e676d5a6a05f3791b0f3b0a3f72059275b404be0bea6f56f0fffa7a70aThe Q-matrix is a unit of the matrix ring: it lies in `GL₂(ℤ)`, since its determinant is the unit `-1`.
LeanFrontier.Horadam.W_isSolution_recurrence(P Q a b : R) : (recurrence P Q).IsSolution (W P Q a b)
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.sound7aaa5be91b309a627b841768d48a11350deb520ffea2ce0ebd4c7269a661dc45Every Horadam sequence is a solution of its associated Mathlib `LinearRecurrence`.
LeanFrontier.Horadam.recurrence_charPoly(P Q : R) : (recurrence P Q).charPoly = X ^ 2 - C P * X + C Q
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.sound1fe2d4ca638bfd8c0d539d4d36a83b44dce60fdfae86ab3504da9a344a750b0fThe characteristic polynomial of the Horadam recurrence is `X² - P X + Q`.
LeanFrontier.Horadam.companionMatrix_mulVec_W_state(P Q a b : R) (n : ℕ) : Matrix.mulVec (companionMatrix P Q) ![W P Q a b (n + 1), W P Q a b n] = ![W P Q a b (n + 2), W P Q a b (n + 1)]
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.sound5bc6de6d6e02c79cae66a8c92c81b7418cb2f33ecb64f9a3840658e59c1995deThe companion matrix advances the Horadam state vector by one recurrence step.
LeanFrontier.Horadam.companionMatrix_pow_mulVec_initial(P Q a b : R) (n : ℕ) : Matrix.mulVec (companionMatrix P Q ^ n) ![b, a] = ![W P Q a b (n + 1), W P Q a b n]
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.sound02d7bc0115958be744e5483dbb448dd85a91248a7da5ace04ede013978e277f8The `n`th power of the companion matrix sends the initial state `![b, a]` to the `n`th Horadam state `![W (n+1), W n]`. This is the state-space realization of the recurrence for arbitrary initial conditions.
LeanFrontier.Horadam.companionMatrix_pow_succ(P Q : R) (n : ℕ) : companionMatrix P Q ^ (n + 1) = companionPowerFormula P Q n
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.soundfbc6b0613e51847000228467992f48584edb46c14bec23f72e81e5ee56d30fa2Explicit powers of the Horadam companion matrix in terms of the fundamental sequence: `A^(n+1) = companionPowerFormula P Q n`.
LeanFrontier.Horadam.det_companionMatrix(P Q : R) : (companionMatrix P Q).det = Q
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.sound2fed3934a0602f5c9b52034e6b7ada4cedb46853b2e7b91c3b8480b036622d60LeanFrontier.Horadam.det_companionMatrix_pow(P Q : R) (n : ℕ) : (companionMatrix P Q ^ n).det = Q ^ n
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.soundfcf7ad4d6be0adb62d64fbfc6228675d997e37b6dfa361afe11c2e1a2e2a640fPowers of the companion matrix have determinant `Q^n`.
LeanFrontier.Horadam.trace_companionMatrix(P Q : R) : (companionMatrix P Q).trace = P
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.sound822b242ccc77e8aba01136a222ffe7a3840546d0a1d768b500e5662f80f7b9e1LeanFrontier.Horadam.trace_companionMatrix_pow_succ_fundamental(P Q : R) (n : ℕ) : (companionMatrix P Q ^ (n + 1)).trace = W P Q 0 1 (n + 2) - Q * W P Q 0 1 n
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.sound98992fd67d93a55b2d3d8c61a323f351b9db9cd9cee6f4a6b2dfcd99033e6287The trace of a positive companion-matrix power is the diagonal combination of the fundamental Horadam sequence appearing in the explicit power formula.
LeanFrontier.Horadam.charpoly_companionMatrix[Nontrivial R] (P Q : R) : (companionMatrix P Q).charpoly = (recurrence P Q).charPoly
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.sound0cd8f4f245c8f3ad02bfd882edbdf2ccc5fb518061c3e03fd12c48fdf806632cThe companion matrix and the scalar recurrence have the same characteristic polynomial.
LeanFrontier.Horadam.charpoly_companionMatrix_pow_succ_fundamental[Nontrivial R] (P Q : R) (n : ℕ) : (companionMatrix P Q ^ (n + 1)).charpoly = companionPowerCharPoly P Q n
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrix12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.soundb17d365239e74ffec1687a31c08c0ea00b7b199921db4056b1865d38f655db14The characteristic polynomial of a positive companion-matrix power is the polynomial specified by its fundamental Horadam trace and determinant.
LeanFrontier.Horadam.companionMatrix_fibonacci: companionMatrix (1 : ℤ) (-1) = LeanFrontier.Matrix.fibMatrix
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrixSpecializations12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.sound6fc1dff8ce224769d4f58df872930e8aebdae8c67d71477338fd36a1bdedf448The Horadam companion matrix for `P = 1`, `Q = -1` is LeanFrontier's Fibonacci Q-matrix.
LeanFrontier.Horadam.W_fibonacci_eq_fib(n : ℕ) : W (1 : ℤ) (-1) 0 1 n = (Nat.fib n : ℤ)
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrixSpecializations12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Quot.sound07ee0fd72c6329831fadd67d58ca572f2b5d3105ff27f77e49780f3f18ee93c6The fundamental Horadam sequence for `P = 1`, `Q = -1` is the Fibonacci sequence, viewed in `ℤ`.
LeanFrontier.Horadam.trace_fibMatrix_pow_succ_eq_lucas(n : ℕ) : (LeanFrontier.Matrix.fibMatrix ^ (n + 1)).trace = (LeanFrontier.Nat.lucas (n + 1) : ℤ)
import LeanFrontier.LinearAlgebra.HoradamCompanionMatrixSpecializations12e4f17436a6dc406329bfe80607d59c9881b0cc · downstream import passpropext, Classical.choice, Quot.soundcc4cb6ed5c1ca005727eaf681f01c09e08c3e444e017e2fc5d556695816e0eb7The trace of a positive Fibonacci Q-matrix power is the corresponding Lucas number. This is obtained by specializing the generic Horadam trace formula and then identifying the fundamental Horadam sequence with Fibonacci numbers.
LeanFrontier.A053067.exists_fixedWidth_residue_one_above(m B : ℕ) (hm : 0 < m) : ∃ d n : ℕ, B < n ∧ IsFixedWidthIndex d n ∧ natFixedA (10 ^ d) n ≡ 1 [MOD m]
import LeanFrontier.NumberTheory.A053067.ResidueOne76816cc5ea0b8c85838a17565ffe5798fcc77d35 · downstream import passpropext, Classical.choice, Quot.sounda932836b391c40d689635c796269c94a7dcdfc7594e830fc2f3d89c419248919Universal residue-one theorem for A053067, in an explicitly unbounded form. For every nonzero modulus m and every lower bound B, there is a genuine fixed-width A053067 index n > B whose fixed-width decimal concatenation is congruent to 1 modulo m.
LeanFrontier.CalkinWilf.pair_append(path : List Bool) (dir : Bool) : pair (path ++ [dir]) = if dir then ((pair path).1 + (pair path).2, (pair path).2) else ((pair path).1, (pair path).1 + (pair path).2)
import LeanFrontier.NumberTheory.CalkinWilf6b868e75a4c88873500d7ed276bfdd74e4c323dd · downstream import passpropextbc60674a9ae86f92db6da5a018205e554f5d996351bcc353ce2d401f7fb747bbAppending one root-to-leaf edge applies the corresponding Calkin-Wilf child operation to the pair already reached: `false` keeps the numerator and adds it to the denominator, while `true` keeps the denominator and adds it to the numerator.
LeanFrontier.CalkinWilf.fusc_pair_code(path : List Bool) : SternDiatomic.fusc (code path) = (pair path).1 ∧ SternDiatomic.fusc (code path + 1) = (pair path).2
import LeanFrontier.NumberTheory.CalkinWilf6b868e75a4c88873500d7ed276bfdd74e4c323dd · downstream import passpropext, Quot.soundf4a246e02fa718127cb7d7eead7176cfa4d9f9e4c5d0641315fd8a24869620bcThe pair reached by a path is exactly the consecutive Stern-diatomic pair at its binary code. This is the bridge between the path representation and the accepted arithmetic enumeration.
LeanFrontier.CalkinWilf.code_eq_iff(p q : List Bool) : code p = code q ↔ p = q
import LeanFrontier.NumberTheory.CalkinWilf6b868e75a4c88873500d7ed276bfdd74e4c323dd · downstream import passpropext, Classical.choice, Quot.sound87082d8a2518cb4c4716dc60175db3e5f146fd85d4af844d4a6b0861b82595afTwo root-to-leaf paths have the same binary code exactly when they are the same path.
LeanFrontier.CalkinWilf.exists_code_eq{n : ℕ} (hn : 0 < n) : ∃ path : List Bool, code path = n
import LeanFrontier.NumberTheory.CalkinWilf6b868e75a4c88873500d7ed276bfdd74e4c323dd · downstream import passpropext, Classical.choice, Quot.sound1c27c81bb0fcdc665683e16b57266cbad6ecabad206c763371ae17313a4440dfEvery positive natural number is the binary code of a unique-rooted Calkin-Wilf path.
LeanFrontier.CalkinWilf.pair_eq_iff(p q : List Bool) : pair p = pair q ↔ p = q
import LeanFrontier.NumberTheory.CalkinWilf6b868e75a4c88873500d7ed276bfdd74e4c323dd · downstream import passpropext, Classical.choice, Quot.sound1ad1e05bb1549c8dbc265761318f15b30069326ffedf0f79a53992b5e30cc57eTwo root-to-leaf paths reach the same Calkin-Wilf pair exactly when they are the same path. This uses the accepted theorem that a positive index is determined by its consecutive Stern-diatomic pair.
LeanFrontier.CalkinWilf.pair_positive_coprime(path : List Bool) : 0 < (pair path).1 ∧ 0 < (pair path).2 ∧ Nat.Coprime (pair path).1 (pair path).2
import LeanFrontier.NumberTheory.CalkinWilf6b868e75a4c88873500d7ed276bfdd74e4c323dd · downstream import passpropext, Classical.choice, Quot.sound30198e05a95cd629f26063914eae5ecad4300fcdaba8ab31c400e8a303a78ae8Every Calkin-Wilf path reaches a pair of positive coprime naturals.
LeanFrontier.CalkinWilf.existsUnique_pair_of_coprime{a b : ℕ} (ha : 0 < a) (hb : 0 < b) (hab : Nat.Coprime a b) : ∃! path : List Bool, pair path = (a, b)
import LeanFrontier.NumberTheory.CalkinWilf6b868e75a4c88873500d7ed276bfdd74e4c323dd · downstream import passpropext, Classical.choice, Quot.soundaeff5d431738e75c8c1712ffb9b0a69be3d5d241e95ba7aed857421146243ddeEvery positive coprime numerator-denominator pair occurs at exactly one root-to-leaf Calkin-Wilf path. This is the path-level form of the accepted Stern-diatomic enumeration.
LeanFrontier.CalkinWilf.pair_reverse_eq_sternBrocot(path : List Bool) : pair path.reverse = SternBrocot.pair path
import LeanFrontier.NumberTheory.CalkinWilfSternBrocot9fabb27175e4c1134484065834ae6828fdaf6844 · downstream import passpropext5443ada51e1effc87ddd47dbce43f0d153abdcb6ab28e86636d7bc4c0a2912d3Reversing a root-to-leaf path converts the Calkin-Wilf pair convention into the Stern-Brocot pair convention.
LeanFrontier.CalkinWilf.pair_eq_sternBrocot_iff_reverse(p q : List Bool) : pair p = SternBrocot.pair q ↔ p = q.reverse
import LeanFrontier.NumberTheory.CalkinWilfSternBrocot9fabb27175e4c1134484065834ae6828fdaf6844 · downstream import passpropext, Classical.choice, Quot.soundcf0c39da0443b2231a79c08735e6aa979e2716e746107d14f1b67ce04d02eac3A Calkin-Wilf path and a Stern-Brocot path reach the same numerator-denominator pair exactly when the two root-to-leaf paths are reverses of one another.
LeanFrontier.DescartesCircle.isQuadruple_reflect(h : IsQuadruple k₁ k₂ k₃ k₄) : IsQuadruple k₁ k₂ k₃ (reflect k₁ k₂ k₃ k₄)
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext, Quot.soundbd56b96239b5eae4e3a4f2f43fa1de8779060157976c095e2375511f26ba3630Reflection preserves Descartes' relation.
LeanFrontier.DescartesCircle.reflect_reflect(k₁ k₂ k₃ k₄ : R) : reflect k₁ k₂ k₃ (reflect k₁ k₂ k₃ k₄) = k₄
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext73aeae93da9e570671892ac868f5b57950f586950ad41f55fb60878ac01cae92Reflection is an involution, so the two completions of a mutually tangent triple are symmetric.
LeanFrontier.DescartesCircle.mul_reflect_eq(h : IsQuadruple k₁ k₂ k₃ k₄) : k₄ * reflect k₁ k₂ k₃ k₄ = 2 * (k₁ ^ 2 + k₂ ^ 2 + k₃ ^ 2) - (k₁ + k₂ + k₃) ^ 2
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext, Quot.soundd38269122512c7b9e7fc0df67cb8e2b86c3f93fa2bbb9dca15971ca156e7344cThe product of the two solutions for the fourth curvature, the second of Vieta's relations for Descartes' quadratic.
LeanFrontier.DescartesCircle.isQuadruple_neg_one_two_two_three: IsQuadruple (-1 : R) 2 2 3
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext, Quot.sounddd7171546080d17eab50383ece6c0140f87e28427dd6bb20e77ba0791498a50aThe curvatures `-1, 2, 2, 3` of the standard Apollonian gasket form a quadruple.
LeanFrontier.DescartesCircle.eq_or_eq_reflect(hx : IsQuadruple k₁ k₂ k₃ x) (hy : IsQuadruple k₁ k₂ k₃ y) : x = y ∨ x = reflect k₁ k₂ k₃ y
import LeanFrontier.NumberTheory.DescartesCircle1ca54a089a0fffcb507a2e594b30fbf7adccd367 · downstream import passpropext, Quot.soundbdf6fed07af317e992bcdf4d445edd5a84c769881597280ec936125f4ea338c6A mutually tangent triple has exactly two completions: any two fourth curvatures satisfying Descartes' relation with the same triple are equal, or are each other's reflection. This is what makes `reflect` the only way to continue an Apollonian gasket.
LeanFrontier.DiscriminantTower.loadBearing_of_witness(L : Type) [Field L] [NumberField L] (K₁ K₂ : IntermediateField ℚ L) (hsplit : Splits L K₁ K₂) (hL : (discr L).natAbs = 256) (h₁ : discrAbs K₁ = 8) (h₂ : discrAbs K₂ = 8) (n₁ : degree K₁ = 2) (n₂ : degree K₂ = 2) : CoprimalityIsLoadBearing
import LeanFrontier.NumberTheory.DiscriminantTowerd9c04f6fb2bebdaffe6f5821423b195299cd5c55 · downstream import passpropext, Classical.choice, Quot.sound03dc43f4a9ed20630d375544ec6ba7054e77e9bee62d24b9b02087247506756dA field of degree four over `ℚ` with discriminant of absolute value `256`, split into two linearly disjoint quadratic subfields each of discriminant absolute value `8`, resolves `CoprimalityIsLoadBearing`. The identity predicts `4096` where the hypothesis gives `256`.
LeanFrontier.NumberTheory.DiscriminantTower.sqrtTwoGen_sq: sqrtTwoGen ^ 2 = (2 : CyclotomicEight)
import LeanFrontier.NumberTheory.DiscriminantTowerWitnessd58090cebbf8e87129e8e392a1271acfb0fd9c25 · downstream import passpropext, Classical.choice, Quot.sound04780ca87d935c901197fb477e5ad1903c4d20971b4997a3c55711eea2d8da6dLeanFrontier.NumberTheory.DiscriminantTower.sqrtNegTwoGen_sq: sqrtNegTwoGen ^ 2 = (-2 : CyclotomicEight)
import LeanFrontier.NumberTheory.DiscriminantTowerWitnessd58090cebbf8e87129e8e392a1271acfb0fd9c25 · downstream import passpropext, Classical.choice, Quot.sound617214fbb5da236a9dc6e84cda533535e8aa4edabd95feb5bc61403a2c1cb874LeanFrontier.NumberTheory.DiscriminantTower.quadraticGenerator_minpolys: minpoly ℚ sqrtTwoGen = X ^ 2 - C 2 ∧ minpoly ℚ sqrtNegTwoGen = X ^ 2 + C 2
import LeanFrontier.NumberTheory.DiscriminantTowerWitnessd58090cebbf8e87129e8e392a1271acfb0fd9c25 · downstream import passpropext, Classical.choice, Quot.sound1b73e3a950f8608b8078d40c4d0d5c8b0bb7c789bccff3c42c57b76474538992The two explicit elements `ζ₈ + ζ₈^7` and `ζ₈ - ζ₈^7` have the expected quadratic minimal polynomials over `ℚ`. These are the generators of the real and imaginary quadratic subfields used in the discriminant-tower witness.
LeanFrontier.NumberTheory.DiscriminantTower.cyclotomicEight_ambient_invariants: Module.finrank ℚ CyclotomicEight = 4 ∧ (NumberField.discr CyclotomicEight).natAbs = 256
import LeanFrontier.NumberTheory.DiscriminantTowerWitnessd58090cebbf8e87129e8e392a1271acfb0fd9c25 · downstream import passpropext, Classical.choice, Quot.sound45302f4f6be7a22f5290788cf1820290d9cd8dd840385432a6ca8a77d04b9d66The ambient eighth cyclotomic field already has the degree and discriminant required by the load-bearing witness.
LeanFrontier.NumberTheory.DiscriminantTower.quadraticFields_discr_abs: (NumberField.discr sqrtTwoField).natAbs = 8 ∧ (NumberField.discr sqrtNegTwoField).natAbs = 8
import LeanFrontier.NumberTheory.DiscriminantTowerWitnessd58090cebbf8e87129e8e392a1271acfb0fd9c25 · downstream import passpropext, Classical.choice, Quot.sound9fb5ac70fd1ed61f3977ee3aa6e64a09c86b808b88a79433c3f80de0353ac430The two quadratic subfields in the eighth cyclotomic field both have absolute discriminant 8. The proof identifies the Eisenstein orders ℤ[√2] and ℤ[√-2] with the full rings of integers before transporting their power-basis discriminants.
LeanFrontier.NumberTheory.DiscriminantTower.coprimalityIsLoadBearing: LeanFrontier.DiscriminantTower.CoprimalityIsLoadBearing
import LeanFrontier.NumberTheory.DiscriminantTowerWitnessd58090cebbf8e87129e8e392a1271acfb0fd9c25 · downstream import passpropext, Classical.choice, Quot.sound4f7689930eb80353d2d79f4ce33063d223f92de09abe8f196f7f26e7156aaca8The explicit quadratic subfields of the eighth cyclotomic field witness that the coprimality hypothesis in the compositum discriminant identity is load-bearing.
LeanFrontier.Farey.add_le_of_isStrictlyBetween(hb : 0 < b) (hd : 0 < d) (hdet : Mediant.crossDet a b c d = 1) (h : IsStrictlyBetween a b p q c d) : b + d ≤ q
import LeanFrontier.NumberTheory.Fareyfa231df468ec55465a72c296174cbadb0fa7c546 · downstream import passpropext, Classical.choice, Quot.sounde48639db6bf6fca315c127f9aaede0eef65159c7d1775a03f43d49eab5a56976A fraction strictly between two Farey neighbours has denominator at least the sum of their denominators.
LeanFrontier.Farey.eq_add_of_denom_eq_add(hb : 0 < b) (hd : 0 < d) (hdet : Mediant.crossDet a b c d = 1) (h : IsStrictlyBetween a b p q c d) (hq : q = b + d) : p = a + c
import LeanFrontier.NumberTheory.Fareyfa231df468ec55465a72c296174cbadb0fa7c546 · downstream import passpropext, Classical.choice, Quot.sound11cbb6b6cd361834c84a5c71f4df6b143699a3e20a80bd62c6dcdd4c607b17e7If a fraction strictly between two Farey neighbours attains the least possible denominator, it is the mediant: its numerator is forced to be the sum of the numerators.
LeanFrontier.FordCircle.centerDistSq_sub_sq_radius_add(hq : q ≠ 0) (hs : s ≠ 0) : centerDistSq p q r s - (radius q + radius s) ^ 2 = (Mediant.crossDet p q r s ^ 2 - 1) / (q ^ 2 * s ^ 2)
import LeanFrontier.NumberTheory.FordCircle3deca15d57889a8acb84e778204872c814099284 · downstream import passpropext, Classical.choice, Quot.soundb8e0d4d2188f09ec1a3d506ef896992f4e2af1e2be23212d00d096c677017535The exact defect of the tangency relation between two Ford circles: the squared distance between the centres, minus the squared sum of the radii, is governed entirely by the cross determinant of the two numerator/denominator pairs.
LeanFrontier.FordCircle.centerDistSq_eq_iff(hq : q ≠ 0) (hs : s ≠ 0) : centerDistSq p q r s = (radius q + radius s) ^ 2 ↔ Mediant.crossDet p q r s ^ 2 = 1
import LeanFrontier.NumberTheory.FordCircle3deca15d57889a8acb84e778204872c814099284 · downstream import passpropext, Classical.choice, Quot.sound1ec415b10cf5756f8560a868548754875ac11a4cb7fb16261627932f7487549cTwo Ford circles have centres exactly the sum of their radii apart precisely when their fractions are Farey neighbours, that is when the cross determinant is `1` or `-1`.
LeanFrontier.FordCircle.sq_radius_add_le_centerDistSq(hq : q ≠ 0) (hs : s ≠ 0) (h : 1 ≤ Mediant.crossDet p q r s ^ 2) : (radius q + radius s) ^ 2 ≤ centerDistSq p q r s
import LeanFrontier.NumberTheory.FordCircle3deca15d57889a8acb84e778204872c814099284 · downstream import passpropext, Classical.choice, Quot.sounda5f9df6a37732cacbbb6b0259f3171d1cf70e1ba4dab637bfe82db2e8d52025cFord circles never overlap: once the cross determinant is at least `1` in absolute value, the centres are at least the sum of the radii apart.
LeanFrontier.Horadam.W_addition_formula(P Q a b : R) (m n : ℕ) : W P Q a b (m + n + 1) = W P Q 0 1 (m + 1) * W P Q a b (n + 1) - Q * W P Q 0 1 m * W P Q a b n
import LeanFrontier.NumberTheory.HoradamSequence.AdditionFormula7f89071cd9d8733b7cad1e69146a4492a96c2417 · downstream import passpropext, Classical.choice, Quot.sound381a89806b87c1bb8c879a7720d42bf78efaa66caffbbc6213e7c26ff500f73d**Horadam addition formula.** Let `U k = W P Q 0 1 k` be the fundamental sequence for the recurrence `W (n+2) = P W (n+1) - Q W n`. Then every solution with initial data `a, b` satisfies `W (m+n+1) = U (m+1) W (n+1) - Q U m W n`. The proof factors the state evolution at time `m+n+1` into `n` steps followed by `m+1` steps, then evaluates the latter power using the accepted explicit companion-matrix formula.
LeanFrontier.Horadam.W_add_two(n : ℕ) : W P Q a b (n + 2) = P * W P Q a b (n + 1) - Q * W P Q a b n
import LeanFrontier.NumberTheory.HoradamSequence6b8535c26f3771bc559843317bf188d432747b4f · downstream import passpropext9d305c5886979d6375a0ebcecb872bca153d2b6a4d2ebd99e8cd1a41d061e351The defining recurrence of a Horadam sequence.
LeanFrontier.Horadam.W_mul_W_add_two_sub_sq(n : ℕ) : W P Q a b n * W P Q a b (n + 2) - W P Q a b (n + 1) ^ 2 = Q ^ n * (W P Q a b 0 * W P Q a b 2 - W P Q a b 1 ^ 2)
import LeanFrontier.NumberTheory.HoradamSequence6b8535c26f3771bc559843317bf188d432747b4f · downstream import passpropext, Quot.soundd025852fe3baaee6d91b386af061b8ff63aa99ec7b324641a322b9e32774980bThe **Cassini identity** for a Horadam sequence: the determinant `W n * W (n + 2) - W (n + 1) ^ 2` is its initial value scaled by `Q ^ n`. For the Fibonacci numbers `Q = -1`, which is why the classical statement alternates in sign.
LeanFrontier.Horadam.W_add_initial(a₁ a₂ b₁ b₂ : R) (n : ℕ) : W P Q (a₁ + a₂) (b₁ + b₂) n = W P Q a₁ b₁ n + W P Q a₂ b₂ n
import LeanFrontier.NumberTheory.HoradamSequence6b8535c26f3771bc559843317bf188d432747b4f · downstream import passpropext710d1b25fbaf846ba9432930d011336fb2e15dbb194dbef3d58be7f7995381a1A Horadam sequence is additive in its initial values: the solutions of one recurrence are closed under addition, hence form a module over the coefficient ring.
LeanFrontier.Nat.lucas_pos: ∀ n, 0 < lucas n | 0 => by simp | 1 => by simp | n + 2 => by have h1
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Classical.choice, Quot.sound04edf8a7bbe09fc446fc5cbe608c4ed8a10fa9e8328fcdae5258a81ae19e72f6Lucas numbers are positive.
LeanFrontier.Nat.lucas_succ_eq_fib_add_fib: ∀ n, lucas (n + 1) = Nat.fib n + Nat.fib (n + 2) | 0 => by decide | 1 => by decide | n + 2 => by have h1
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Quot.sound142bf65394109070392499d61ad65fe7e96983c1e8d00194758432c4ef2e504cThe bridge to the Fibonacci numbers: `L (n + 1) = F n + F (n + 2)`. The index is shifted by one so that the statement needs no natural subtraction.
LeanFrontier.Nat.fib_two_mul_eq_fib_mul_lucas(n : ℕ) : Nat.fib (2 * n) = Nat.fib n * lucas n
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Quot.soundc6bb398f74ad93e80981ffb61aa8e8a31b3c788e0101faa7bff8c4f7c2b6053bThe doubling identity `F (2 * n) = F n * L n`: a Fibonacci number at an even index factors through the Lucas number at half the index.
LeanFrontier.Nat.fib_succ_sq_sub_fib_mul_fib_add_two(n : ℕ) : (Nat.fib (n + 1) : ℤ) ^ 2 - Nat.fib n * Nat.fib (n + 2) = (-1) ^ n
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Classical.choice, Quot.sound441418abdf4a237289301f90ea6173ad19b83d8d87da40aba33e9992b5dd620eThe Cassini-type identity in the subtraction-free index form: `(F (n + 1))² - F n * F (n + 2) = (-1) ^ n` over `ℤ`.
LeanFrontier.Nat.lucas_sq_eq_five_mul_fib_sq_add(n : ℕ) : (lucas n : ℤ) ^ 2 = 5 * (Nat.fib n : ℤ) ^ 2 + 4 * (-1) ^ n
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Classical.choice, Quot.soundec5bf34439a556ab9ea9e60b34d0d640005b1145a99828e18823b97779f76f67The Pell-type identity `(L n)² = 5 (F n)² + 4 * (-1) ^ n`: the pair `(L n, F n)` lies on one of the two conics `x² - 5 y² = ± 4`, which is why `(L n + √5 F n) / 2 = φ ^ n`.
LeanFrontier.Nat.sum_range_lucas(n : ℕ) : ∑ i ∈ Finset.range n, lucas i = lucas (n + 1) - 1
import LeanFrontier.NumberTheory.LucasNumber77b9a30910c2b63eed7747df9a42d2a2f60468b5 · downstream import passpropext, Classical.choice, Quot.sound08125a2ee4f940c6bad599f32742bb7d0c01fba6873596a8cd6db4f53f83a06bThe partial sums of the Lucas numbers: `∑ i < n, L i = L (n + 1) - 1`.
LeanFrontier.MarkovEquation.collision_factorization{a₁ b₁ a₂ b₂ c : ℤ} (h₁ : IsSolution a₁ b₁ c) (h₂ : IsSolution a₂ b₂ c) : (a₁ * a₂ - b₁ * b₂) * (a₁ * b₂ - b₁ * a₂) = c ^ 2 * (a₁ * b₁ - a₂ * b₂)
import LeanFrontier.NumberTheory.MarkovEquation.Collision88d03678ae2c88890916b222155f8fa3b1c8b2bc · downstream import passpropext, Classical.choice, Quot.sound44a102cba6bfbd54bfa50b12278f641055d2543d234c3cfdbc9742af68907687If two Markov triples share their third coordinate, their two remaining coordinate pairs satisfy Srinivasan's collision factorization.
LeanFrontier.MarkovEquation.odd_prime_not_dvd_both_collision_factors{a₁ b₁ a₂ b₂ c : ℤ} {p : ℕ} (h₂ : IsSolution a₂ b₂ c) (hc₁ : IsCoprime a₁ c) (hc₂ : IsCoprime a₂ c) (hp : p.Prime) (hp2 : p ≠ 2) (hpc : (p : ℤ) ∣ c) : ¬((p : ℤ) ∣ (a₁ * a₂ - b₁ * b₂) ∧ (p : ℤ) ∣ (a₁ * b₂ - b₁ * a₂))
import LeanFrontier.NumberTheory.MarkovEquation.CollisionPrimeSplit8890bd043dd27114e23d0805a6c1e752106aafa9 · downstream import passpropext, Classical.choice, Quot.sound1bc5565888fd28d06b0fda25a9cc946386d863d07d47e3ed5c985ecf84dd3cf0Let `p` be an odd prime dividing the common coordinate `c`. If `a₁` and `a₂` are coprime to `c`, then `p` cannot divide both collision factors. The hypotheses are stated only with the two coprimality facts actually needed by the elementary argument. Pairwise coprimality of positive Markov triples supplies them in the intended application.
LeanFrontier.MarkovEquation.odd_prime_power_collision_factor_split{a₁ b₁ a₂ b₂ c : ℤ} {p k : ℕ} (h₁ : IsSolution a₁ b₁ c) (h₂ : IsSolution a₂ b₂ c) (hc₁ : IsCoprime a₁ c) (hc₂ : IsCoprime a₂ c) (hp : p.Prime) (hp2 : p ≠ 2) (hk : 0 < k) (hpkc : ((p : ℤ) ^ k) ∣ c) : ((((p : ℤ) ^ k) ^ 2 ∣ (a₁ * a₂ - b₁ * b₂)) ∨ (((p : ℤ) ^ k) ^ 2 ∣ (a₁ * b₂ - b₁ * a₂))) ∧ ¬((p : ℤ) ∣ (a₁ * a₂ - b₁ * b₂) ∧ (p : ℤ) ∣ (a₁ * b₂ - b₁ * a₂))
import LeanFrontier.NumberTheory.MarkovEquation.CollisionPrimeSplit8890bd043dd27114e23d0805a6c1e752106aafa9 · downstream import passpropext, Classical.choice, Quot.sound250419670f87230d69e3542e5517fec548afbea743e3413a4d2b1f01d9cc1831If a positive power of an odd prime divides the shared coordinate of two Markov triples, then the square of that prime power divides one entire collision factor, and the prime itself does not divide both factors. This is the arithmetic prime-power split behind the same-root/opposite-root decomposition used in classical partial proofs of Markov uniqueness.
LeanFrontier.MarkovEquation.slope_scale_common_divisors_iff{M x y q : ℤ} (hxy : IsCoprime x y) (hM : Odd M) : (q ∣ x ^ 2 + y ^ 2 + 3 * M * x * y ∧ q ∣ y ^ 2 - x ^ 2) ↔ (q ∣ 3 * M * x + 2 * y ∧ q ∣ 3 * M * y + 2 * x)
import LeanFrontier.NumberTheory.MarkovEquation.SlopeScaleGCD8a7e7f5a0a2ed11ff0b35a6cb7e32ddb66e64176 · downstream import passpropext, Classical.choice, Quot.sounddc4f27453fac1ad7d7ac8af4cc61df9cf0b69dd9ac2e485eb58c499b34ff8e14For primitive `x,y` and odd `M`, the quadratic slope-scale pair and its associated linear pair have exactly the same integer common divisors.
LeanFrontier.MarkovEquation.slope_scale_gcd_eq{M x y : ℤ} (hxy : IsCoprime x y) (hM : Odd M) : Int.gcd (x ^ 2 + y ^ 2 + 3 * M * x * y) (y ^ 2 - x ^ 2) = Int.gcd (3 * M * x + 2 * y) (3 * M * y + 2 * x)
import LeanFrontier.NumberTheory.MarkovEquation.SlopeScaleGCD8a7e7f5a0a2ed11ff0b35a6cb7e32ddb66e64176 · downstream import passpropext, Classical.choice, Quot.sound19674d77eb3f7dee11b1636d1c151c2e504692b7be786bd14965e6dc2bd0c1efThe gcd form of `slope_scale_common_divisors_iff`.
LeanFrontier.MarkovEquation.slope_scale_primitive_quotient_gcd{M x y Q A B C D : ℤ} (hxy : IsCoprime x y) (hQ : Q ≠ 0) (hL : x ^ 2 + y ^ 2 + 3 * M * x * y = Q * A) (hT : y ^ 2 - x ^ 2 = Q * B) (hU : 3 * M * x + 2 * y = Q * C) (hV : 3 * M * y + 2 * x = Q * D) : Int.gcd (x * C) (A + B) = C.natAbs ∧ Int.gcd (A - B) (y * D) = D.natAbs
import LeanFrontier.NumberTheory.MarkovEquation.SlopeScaleGCD8a7e7f5a0a2ed11ff0b35a6cb7e32ddb66e64176 · downstream import passpropext, Classical.choice, Quot.sound58965ac2e88fb81d90ffb82be09c4d10716a067cc31ffcce90492444364829f4If a common factor `Q` is removed from the slope-scale expressions, the remaining linear quotient factors are recoverable as gcds when `x,y` are primitive. This packages the identities `L + T = y U` and `L - T = x V`: if `L = Q*A`, `T = Q*B`, `U = Q*C`, and `V = Q*D`, then `A+B = y*C` and `A-B = x*D`. Primitivity of `x,y` then gives the two displayed gcds.
LeanFrontier.MarkovEquation.mul_jump_eq(h : IsSolution x y z) : z * jump x y z = x ^ 2 + y ^ 2
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropext, Classical.choice, Quot.sound21d6f0eff5603f9434ad2147bec045ced69a02444077d69e705425a9fcf1ea93Vieta's product relation for the two roots of the Markov equation in its last coordinate.
LeanFrontier.MarkovEquation.isSolution_jump(h : IsSolution x y z) : IsSolution x y (jump x y z)
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropext, Classical.choice, Quot.sound4e287e7be84dd9cd839a78aa1cb82724cc57676363a29b571ed3a74fcd9b0e49The Vieta jump sends Markov triples to Markov triples.
LeanFrontier.MarkovEquation.jump_jump(x y z : ℤ) : jump x y (jump x y z) = z
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropextd7ea0657139973611ce13469b827246bf864eda304827fab1e2755dc4a4bb645The Vieta jump is an involution, so each edge of the Markov tree can be traversed in both directions.
LeanFrontier.MarkovEquation.jump_pos(hx : 0 < x) (hz : 0 < z) (h : IsSolution x y z) : 0 < jump x y z
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropext, Classical.choice, Quot.sound47820078e476211b9dfdeb062aa9c8334fc464bab1ee0081b44118ccc99565e5A Markov triple with positive first and last coordinate has a positive jump: the second root of a positive triple is again positive.
LeanFrontier.MarkovEquation.isSolution_one_one_one: IsSolution 1 1 1
import LeanFrontier.NumberTheory.MarkovEquation01f90b127abc05535dc14d45b05ca8d687097312 · downstream import passpropexte57980699c4cfa37549f600b273029c783ed824ab01e3192e0ad2a5c723e27b1`(1, 1, 1)` is a Markov triple; it is the root from which the Vieta jumps generate the Markov tree.
LeanFrontier.MarkovTree.divergesBelow_commonAncestor_of_incomparable{p q : List Bool} (h : PathsIncomparable p q) : DivergesBelow (commonAncestor p q) p q
import LeanFrontier.NumberTheory.MarkovTree.BranchDivergence65832dae7bfc674358a7a73fe13953bd2a42c322 · downstream import passpropext, Classical.choice, Quot.sound057a2a8281d527b6d11194e6add1e8e03773ec9420e62972b20b18880c0d7288Incomparable paths leave their deepest common ancestor through distinct immediate children.
LeanFrontier.MarkovTree.incomparable_of_divergesBelow_commonAncestor{p q : List Bool} (h : DivergesBelow (commonAncestor p q) p q) : PathsIncomparable p q
import LeanFrontier.NumberTheory.MarkovTree.BranchDivergence65832dae7bfc674358a7a73fe13953bd2a42c322 · downstream import passpropext, Quot.sound2a7ca1869a980d96c69bb1f18e2c4a6f3d55d5432ce5167d4f16a13e0471401aA divergence decomposition below the deepest common ancestor forces path incomparability.
LeanFrontier.MarkovTree.pathsIncomparable_iff_divergesBelow_commonAncestor(p q : List Bool) : PathsIncomparable p q ↔ DivergesBelow (commonAncestor p q) p q
import LeanFrontier.NumberTheory.MarkovTree.BranchDivergence65832dae7bfc674358a7a73fe13953bd2a42c322 · downstream import passpropext, Classical.choice, Quot.sound4482d3ab304e401038b23b7bd2d9fb3ac0c548a8694e96a51711804b4839ddf7Exact first-divergence characterization for canonical Markov/Stern-Brocot paths. Two paths are incomparable exactly when, below their deepest common ancestor, they enter different immediate child subtrees.
LeanFrontier.MarkovTree.exists_opposite_child_decomposition_of_incomparable{p q : List Bool} (h : PathsIncomparable p q) : ∃ left right : List Bool, (p = left ++ false :: commonAncestor p q ∧ q = right ++ true :: commonAncestor p q) ∨ (p = left ++ true :: commonAncestor p q ∧ q = right ++ false :: commonAncestor p q)
import LeanFrontier.NumberTheory.MarkovTree.BranchDivergence65832dae7bfc674358a7a73fe13953bd2a42c322 · downstream import passpropext, Classical.choice, Quot.sound9013e757695995eba0b65aa0d43eaa61521555683357adecf1a45fc16c02d789Incomparable Boolean paths can be normalized to the two concrete opposite-child cases. Thus every incomparable pair is obtained by descending below its deepest common ancestor through `false` on one side and `true` on the other, in one of the two possible orders.
LeanFrontier.MarkovTree.commonAncestor_length_lt_both_of_incomparable{p q : List Bool} (h : PathsIncomparable p q) : (commonAncestor p q).length < p.length ∧ (commonAncestor p q).length < q.length
import LeanFrontier.NumberTheory.MarkovTree.BranchDivergence65832dae7bfc674358a7a73fe13953bd2a42c322 · downstream import passpropext, Classical.choice, Quot.sounde24c23a63b3885a23d41e2fc6c44241094fdaa7cf831fe9ae151e7808ddfeb09Incomparable paths have a strictly shorter common ancestor than both paths.
LeanFrontier.MarkovTree.commonPrefix_isPrefix_left(p q : List Bool) : commonPrefix p q <+: p
import LeanFrontier.NumberTheory.MarkovTree.BranchStructure229498f70b101dd67354112476a77106f4a99fbc · downstream import passpropext, Quot.sound586ae888913bc876581ea36630c60b5dc7e88f22b019746c604de69b952cf29eThe longest common prefix is a prefix of its left input.
LeanFrontier.MarkovTree.commonPrefix_isPrefix_right(p q : List Bool) : commonPrefix p q <+: q
import LeanFrontier.NumberTheory.MarkovTree.BranchStructure229498f70b101dd67354112476a77106f4a99fbc · downstream import passpropext, Quot.soundd701f3d96ee1cc4c0ecb3a122b2a555fe7e0cd7bdf450ba9c8bde48511216e49The longest common prefix is a prefix of its right input.
LeanFrontier.MarkovTree.isPrefix_commonPrefix{r p q : List Bool} (hp : r <+: p) (hq : r <+: q) : r <+: commonPrefix p q
import LeanFrontier.NumberTheory.MarkovTree.BranchStructure229498f70b101dd67354112476a77106f4a99fbc · downstream import passpropext, Quot.sound4a510ca6c2ea5ad7388f2c79dce125b12cde8c751fcebe83680e1c0d69da18c5Universal property of `commonPrefix`: every list which is a prefix of both inputs is itself a prefix of their longest common prefix.
LeanFrontier.MarkovTree.commonAncestor_isSuffix_left(p q : List Bool) : commonAncestor p q <:+ p
import LeanFrontier.NumberTheory.MarkovTree.BranchStructure229498f70b101dd67354112476a77106f4a99fbc · downstream import passpropext, Quot.soundf6d79e2ee466bda4f098036cca660cd17e31e877cf460998414f6408ec473fa7The common ancestor lies on the ancestor chain of the left path.
LeanFrontier.MarkovTree.commonAncestor_isSuffix_right(p q : List Bool) : commonAncestor p q <:+ q
import LeanFrontier.NumberTheory.MarkovTree.BranchStructure229498f70b101dd67354112476a77106f4a99fbc · downstream import passpropext, Quot.sounda55b32ded6e25bf296abc0c7f853a036ef9f3a238e52e35f18042794fb6d3a4dThe common ancestor lies on the ancestor chain of the right path.
LeanFrontier.MarkovTree.isSuffix_commonAncestor{r p q : List Bool} (hp : r <:+ p) (hq : r <:+ q) : r <:+ commonAncestor p q
import LeanFrontier.NumberTheory.MarkovTree.BranchStructure229498f70b101dd67354112476a77106f4a99fbc · downstream import passpropext, Quot.sound1ecae49a3aaf7fcb29c1ec7ae515270ef95cc588a30c1a9f45c18986a4a035b6Universal property of the canonical common ancestor: every path which is an ancestor of both `p` and `q` is itself an ancestor of `commonAncestor p q`. Thus `commonAncestor p q` is the greatest common ancestor in the tree order.
LeanFrontier.MarkovTree.commonAncestor_eq_left_iff(p q : List Bool) : commonAncestor p q = p ↔ p <:+ q
import LeanFrontier.NumberTheory.MarkovTree.BranchStructure229498f70b101dd67354112476a77106f4a99fbc · downstream import passpropext, Quot.sound63f2e82164dec281b8bebcc9c7c41d5eefd30cfc25c6514935a002c593b5e88bA path is its own common ancestor with `q` exactly when it is an ancestor of `q`.
LeanFrontier.MarkovTree.commonAncestor_eq_right_iff(p q : List Bool) : commonAncestor p q = q ↔ q <:+ p
import LeanFrontier.NumberTheory.MarkovTree.BranchStructure229498f70b101dd67354112476a77106f4a99fbc · downstream import passpropext, Quot.sound08a90b4ebafbde9d716cb45672e2037e27abaa49a0ae329a444adf914ca6861dSymmetrically, a path is its own common ancestor with `p` exactly when it is an ancestor of `p`.
LeanFrontier.MarkovTree.commonAncestor_comm(p q : List Bool) : commonAncestor p q = commonAncestor q p
import LeanFrontier.NumberTheory.MarkovTree.BranchStructure229498f70b101dd67354112476a77106f4a99fbc · downstream import passpropext, Quot.sound440970de6e603df5e7759d4e3dfba707a4bb39c2e932aad604a23408d468582bThe canonical common ancestor is symmetric in its two arguments.
LeanFrontier.MarkovTree.markovNumber_pos(n : OrientedNode) : 0 < n.markovNumber
import LeanFrontier.NumberTheory.MarkovTree.ChildLabelsca8b06882d1bb98ec03309430b7e4574e3ea2653 · downstream import passpropextff73c286e1c1117ebc37b89c39934799ad9748aeb246ca260f1def2ff08379f1The Markov-number coordinate of every oriented node is positive.
LeanFrontier.MarkovTree.forwardCoordinate_pos(n : OrientedNode) (dir : Bool) : 0 < n.forwardCoordinate dir
import LeanFrontier.NumberTheory.MarkovTree.ChildLabelsca8b06882d1bb98ec03309430b7e4574e3ea2653 · downstream import passpropext6f304fcfc2c0f8fb2ec6456b6a7b9d9b0444475645271e7a843e7ca717efe95bEither non-back coordinate of an oriented node is positive.
LeanFrontier.MarkovTree.child_markovNumber_formula(n : OrientedNode) (dir : Bool) : (child n dir).markovNumber = 3 * n.markovNumber * n.forwardCoordinate (!dir) - n.forwardCoordinate dir
import LeanFrontier.NumberTheory.MarkovTree.ChildLabelsca8b06882d1bb98ec03309430b7e4574e3ea2653 · downstream import passpropext, Classical.choice, Quot.sounddf67f8e3ac9a01bf69ef14d63ab1e2fe760cef11d973d3a723f5d11b8b66a8fcExact formula for the Markov-number label of either forward child. The coordinate being jumped is `forwardCoordinate dir`; the other non-back coordinate is `forwardCoordinate (!dir)`.
LeanFrontier.MarkovTree.child_markovNumber_sub_child_markovNumber(n : OrientedNode) : (child n false).markovNumber - (child n true).markovNumber = (3 * n.markovNumber + 1) * (n.forwardCoordinate true - n.forwardCoordinate false)
import LeanFrontier.NumberTheory.MarkovTree.ChildLabelsca8b06882d1bb98ec03309430b7e4574e3ea2653 · downstream import passpropext, Classical.choice, Quot.soundc05a58b6e4af7eb0abddd7d01bc047ed367f6ea1eb6d2a2d6cbba6834048a1edThe difference of the two child Markov-number labels factors through the difference of the two non-back parent coordinates.
LeanFrontier.MarkovTree.child_false_markovNumber_lt_child_true_iff(n : OrientedNode) : (child n false).markovNumber < (child n true).markovNumber ↔ n.forwardCoordinate true < n.forwardCoordinate false
import LeanFrontier.NumberTheory.MarkovTree.ChildLabelsca8b06882d1bb98ec03309430b7e4574e3ea2653 · downstream import passpropext, Classical.choice, Quot.sound029780be23604abac44c8ba455d3071e32320321cafce158de6e3674dd4991a7The child reached by `false` has the smaller Markov-number label exactly when the parent coordinate selected by `true` is smaller. Equivalently, among the two forward Vieta moves, jumping the larger current coordinate produces the smaller child label.
LeanFrontier.MarkovTree.child_markovNumber_eq_iff_forwardCoordinate_eq(n : OrientedNode) : (child n false).markovNumber = (child n true).markovNumber ↔ n.forwardCoordinate false = n.forwardCoordinate true
import LeanFrontier.NumberTheory.MarkovTree.ChildLabelsca8b06882d1bb98ec03309430b7e4574e3ea2653 · downstream import passpropext, Classical.choice, Quot.soundeb4c5ec850fe17de7bcae8d5a1d7ff6e8e88a2d749c3fe93ca727d5efbc840b5The two immediate child Markov numbers coincide exactly when the two non-back parent coordinates coincide.
LeanFrontier.MarkovTree.pairwiseCoprime_move(m : Move) {s : State} (h : s.PairwiseCoprime) : (move m s).PairwiseCoprime
import LeanFrontier.NumberTheory.MarkovTree.Coprime998b357fdc1ce0e81d2e2a5698305c78ee3cb92b · downstream import passpropext814464e968ad3a16a7f3ec0088f7adae5e7b9d2c6c39f5578a63a2d9b606c86eA single Vieta coordinate move preserves pairwise coprimality. This statement is purely algebraic and does not require the Markov equation: replacing one coordinate by `3` times the product of the other two minus that coordinate leaves its gcd with either untouched coordinate unchanged.
LeanFrontier.MarkovTree.pairwiseCoprime_walk(path : List Move) {s : State} (h : s.PairwiseCoprime) : (walk path s).PairwiseCoprime
import LeanFrontier.NumberTheory.MarkovTree.Coprime998b357fdc1ce0e81d2e2a5698305c78ee3cb92b · downstream import passpropextf8f1bd8b8dd6bee04d04c54ce2ebd48eba7215b1b30833c4830dfe96da8bd84aPairwise coprimality is preserved by every finite Markov-tree walk.
LeanFrontier.MarkovTree.pairwiseCoprime_of_positive_solution(s : State) (hx : 0 < s.x) (hy : 0 < s.y) (hz : 0 < s.z) (hsol : s.IsSolution) : s.PairwiseCoprime
import LeanFrontier.NumberTheory.MarkovTree.Coprime998b357fdc1ce0e81d2e2a5698305c78ee3cb92b · downstream import passpropext, Classical.choice, Quot.sound510a000927d77f3c07e84b60d01f907bb5249beb09862ce7c18c4f77d443ad6dEvery positive integer solution of the Markov equation has pairwise coprime coordinates.
LeanFrontier.MarkovTree.existsUnique_pathMoves_of_nonBacktracking(n : OrientedNode) {moves : List Move} (h : NonBacktrackingFrom n.back moves) : ∃! path : List Bool, pathMoves n path = moves
import LeanFrontier.NumberTheory.MarkovTree.Coverage59fc3f26ee411a54e2f9d3f41e45bffc6ebfd4ee · downstream import passpropext, Classical.choice, Quot.sound7a096985935d1af8e1b122ea626ff920eb91fd66bc45edfb3b4f03caa83af797Every non-backtracking coordinate-move list from an oriented node has a unique Boolean path encoding.
LeanFrontier.MarkovTree.branchNode_third(path : List Bool) : branchNode .third path = sternNode path
import LeanFrontier.NumberTheory.MarkovTree.Coverage59fc3f26ee411a54e2f9d3f41e45bffc6ebfd4ee · downstream import passpropext, Classical.choice, Quot.soundf8b4ae371fa5923e2fa7fc600c228aa10dfe796ad48983a42a32d1c84f1b80ecThe third labelled root branch is exactly the accepted `sternNode` representation.
LeanFrontier.MarkovTree.exists_branchNode_state_of_positive_solution(s : State) (hx : 0 < s.x) (hy : 0 < s.y) (hz : 0 < s.z) (hsol : s.IsSolution) (hne : s ≠ ⟨1, 1, 1⟩) : ∃ initial : Move, ∃ path : List Bool, (branchNode initial path).state = s
import LeanFrontier.NumberTheory.MarkovTree.Coverage59fc3f26ee411a54e2f9d3f41e45bffc6ebfd4ee · downstream import passpropext, Classical.choice, Quot.sound164cf2b349778e1064f98d8ce10d9170809e21cbe3441c729c08fc455e7747fbEvery positive Markov solution other than `(1,1,1)` belongs to one of the three oriented binary branches obtained by choosing its first coordinate move from the root. The Boolean path is written in the same convention as the accepted Stern-Brocot representation. No uniqueness of `first` or of the resulting numerical state representation is asserted.
LeanFrontier.MarkovTree.markovFib_vieta_recurrence(n : ℕ) : markovFib (n + 2) = 3 * markovFib (n + 1) - markovFib n
import LeanFrontier.NumberTheory.MarkovTree.FibonacciSpine3f8367ee4aa809b304a5a8cf1bfae82cfd69ddb4 · downstream import passpropext, Classical.choice, Quot.soundeb6ca9a03b8fe8afc97923c32b07db2e72c19d6bd8893573b983aa1e340820d2Consecutive odd-index Fibonacci numbers satisfy the same second-order recurrence as successive Vieta jumps along the Markov branch.
LeanFrontier.MarkovTree.sternNode_fibonacciSpine_even(n : ℕ) : (sternNode (List.replicate (2 * n) true)).state = ⟨1, markovFib (2 * n), markovFib (2 * n + 1)⟩
import LeanFrontier.NumberTheory.MarkovTree.FibonacciSpine3f8367ee4aa809b304a5a8cf1bfae82cfd69ddb4 · downstream import passpropext, Classical.choice, Quot.sound36d0638bb50d4856c86503313a2f01a4a904ba0d5147c946104131f22fbe3a26At every even depth on the all-right Stern-Brocot path, the Markov state is `(1, F_(4n+1), F_(4n+3))`, expressed through `markovFib`.
LeanFrontier.MarkovTree.sternNode_fibonacciSpine_odd(n : ℕ) : (sternNode (List.replicate (2 * n + 1) true)).state = ⟨1, markovFib (2 * n + 2), markovFib (2 * n + 1)⟩
import LeanFrontier.NumberTheory.MarkovTree.FibonacciSpine3f8367ee4aa809b304a5a8cf1bfae82cfd69ddb4 · downstream import passpropext, Classical.choice, Quot.soundf0e1f2ab1b0e817f8b0d549c8f6e5ea0562efc077bf85e34c37ad54ca75abd74At every odd depth on the all-right Stern-Brocot path, the same two consecutive odd-index Fibonacci numbers occur in the opposite coordinate order: `(1, F_(4n+5), F_(4n+3))`.
LeanFrontier.MarkovTree.state_mass_lt_child(n : OrientedNode) (dir : Bool) : n.state.mass < (child n dir).state.mass
import LeanFrontier.NumberTheory.MarkovTree.Injectivity132f58d6ac00587a689e10a9b994f07b77668fee · downstream import passpropext, Classical.choice, Quot.sound586e781c138202a4db015000a9af65f069305fd5d672071cb7fdce08e19cc460Moving to either forward child strictly increases coordinate mass.
LeanFrontier.MarkovTree.orientedNode_eq_of_state_eq{a b : OrientedNode} (hstate : a.state = b.state) : a = b
import LeanFrontier.NumberTheory.MarkovTree.Injectivity132f58d6ac00587a689e10a9b994f07b77668fee · downstream import passpropext, Classical.choice, Quot.sound71838bd56bff44da4c5a0332f9a2322ab7a744c6f078b9146603714a3eb01e97The underlying labelled Markov state uniquely determines an oriented node. In particular, the descending parent edge is not extra ambiguity: it is forced by the state.
LeanFrontier.MarkovTree.sternNode_state_injective: Function.Injective (fun path : List Bool => (sternNode path).state)
import LeanFrontier.NumberTheory.MarkovTree.Injectivity132f58d6ac00587a689e10a9b994f07b77668fee · downstream import passpropext, Classical.choice, Quot.sound91844c2dd446ca89ce1951b5ee5b02374caad1b08c7fc8043d3997732ae0d790Distinct Stern-Brocot path positions reach distinct full labelled Markov states in the canonical oriented branch. This is injectivity of the complete triple-valued tree embedding, not injectivity of the maximum-coordinate Markov-number label.
LeanFrontier.MarkovTree.sternBrocot_pair_eq_iff_sternNode_state_eq(p q : List Bool) : SternBrocot.pair p = SternBrocot.pair q ↔ (sternNode p).state = (sternNode q).state
import LeanFrontier.NumberTheory.MarkovTree.Injectivity132f58d6ac00587a689e10a9b994f07b77668fee · downstream import passpropext, Classical.choice, Quot.sound4c4f86391ae839db95265e2d03b0c5c6b3281017277ad0ef050e703ca1cc0d1eEquality of Stern-Brocot nodes is equivalent to equality of the full labelled Markov states attached to the same path positions. This upgrades the accepted move-word correspondence to the actual triple-valued tree embedding, without making any claim about injectivity of a single Markov-number coordinate.
LeanFrontier.MarkovTree.coordinate_lt_markovNumber_of_ne_back(n : OrientedNode) {m : Move} (hne : m ≠ n.back) : n.state.coordinate m < n.markovNumber
import LeanFrontier.NumberTheory.MarkovTree.MarkovNumberb282fc2656d74a54f8b4ba4558789d4955722931 · downstream import passpropext, Classical.choice, Quot.sound0ac2842742fa807531215f34c7974bf56cf47b90861c19528be50c891503c847At an oriented Markov node, the coordinate selected by any move other than `back` is strictly smaller than the Markov-number coordinate selected by `back`. Thus the orientation invariant already singles out a unique largest coordinate.
LeanFrontier.MarkovTree.markovNumber_eq_max(n : OrientedNode) : n.markovNumber = max n.state.x (max n.state.y n.state.z)
import LeanFrontier.NumberTheory.MarkovTree.MarkovNumberb282fc2656d74a54f8b4ba4558789d4955722931 · downstream import passpropext, Classical.choice, Quot.sound1446ea6d757a07b041119f652a7f87d6f8eee78186d2af81634c12b07c976840The oriented-node Markov-number label is exactly the maximum of its three coordinates. In particular, the `back` field does not introduce an arbitrary choice of numerical label: its coordinate is forced by the underlying positive Markov state.
LeanFrontier.MarkovTree.markovNumber_lt_child(n : OrientedNode) (dir : Bool) : n.markovNumber < (child n dir).markovNumber
import LeanFrontier.NumberTheory.MarkovTree.MarkovNumberb282fc2656d74a54f8b4ba4558789d4955722931 · downstream import passpropext, Classical.choice, Quot.sounde87a5164e706c66b865d5c06c27f6148accecbcf08358161ab8d3b0340ef39ebThe Markov-number label strictly increases along either forward edge of the oriented tree. This proves ancestor-chain injectivity of the numerical label. Possible collisions are therefore confined to incomparable branches.
LeanFrontier.MarkovTree.sternMarkovNumber_lt_cons(dir : Bool) (path : List Bool) : sternMarkovNumber path < sternMarkovNumber (dir :: path)
import LeanFrontier.NumberTheory.MarkovTree.MarkovNumberb282fc2656d74a54f8b4ba4558789d4955722931 · downstream import passpropext, Classical.choice, Quot.sound5f79f92ff0d984728d86a13ed1bcf8921ac868bdaad3d242eff19ef80a695738Prepending either Stern-Brocot direction moves to a child with strictly larger Markov number.
LeanFrontier.MarkovTree.pathLength_add_two_le_sternMarkovNumber(path : List Bool) : (path.length : ℤ) + 2 ≤ sternMarkovNumber path
import LeanFrontier.NumberTheory.MarkovTree.MarkovNumberb282fc2656d74a54f8b4ba4558789d4955722931 · downstream import passpropext, Classical.choice, Quot.sound31142cb09816879182cb6007e1befd7e1c529c31a03d37976ae88bc7310922a8A canonical path of length `d` has Markov number at least `d + 2`. The bound is deliberately elementary; its useful consequence is finiteness of the tree depth that must be inspected below any fixed candidate Markov number.
LeanFrontier.MarkovTree.modFourPattern_of_positive_solution(s : State) (hx : 0 < s.x) (hy : 0 < s.y) (hz : 0 < s.z) (hsol : s.IsSolution) : ModFourPattern s
import LeanFrontier.NumberTheory.MarkovTree.ModFourf80a60874b9d3d6183852d82349aa6699503d9f4 · downstream import passpropext, Classical.choice, Quot.sound0af91170bd43b5869228f2f0daba712a21dcf822a6c89e6d7b5a8e4b3e019a96Every positive integer Markov triple has, modulo four, either residue pattern `(1,1,1)` or a permutation of `(2,1,1)`.
LeanFrontier.MarkovTree.modFour_of_even_third_coordinate{x y z : ℤ} (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (hsol : MarkovEquation.IsSolution x y z) (heven : (2 : ℤ) ∣ z) : (x : ZMod 4) = 1 ∧ (y : ZMod 4) = 1 ∧ (z : ZMod 4) = 2
import LeanFrontier.NumberTheory.MarkovTree.ModFourf80a60874b9d3d6183852d82349aa6699503d9f4 · downstream import passpropext, Classical.choice, Quot.soundbbd236c2c6ea67284e7bb558a1fe31de2b1519e780b2e464a3c9428979bdf083If the third coordinate of a positive Markov triple is even, then it is `2 mod 4`, while the other two coordinates are both `1 mod 4`.
LeanFrontier.MarkovTree.markovNumber_isCoprime_forwardCoordinate(n : OrientedNode) (dir : Bool) : IsCoprime n.markovNumber (n.forwardCoordinate dir)
import LeanFrontier.NumberTheory.MarkovTree.ModularRoot1f3e8fae49d71521079cb17ea2cf18341072ac2d · downstream import passpropext, Classical.choice, Quot.sound293503919611dded27b52d7e16d54c3ec2180d1f51045ad93ecaa35a8c9b3893The Markov-number coordinate is coprime to either of the two non-back coordinates selected by a Boolean forward direction.
LeanFrontier.MarkovTree.otherSquareSum_back_eq_forwardCoordinate_squares(n : OrientedNode) : n.state.otherSquareSum n.back = n.forwardCoordinate false ^ 2 + n.forwardCoordinate true ^ 2
import LeanFrontier.NumberTheory.MarkovTree.ModularRoot1f3e8fae49d71521079cb17ea2cf18341072ac2d · downstream import passpropextd2231b3204da32eb3a52d08f752a76e83adc8b443f9bd1b78fcb4aca5b2d789dThe complementary square sum at the back coordinate is exactly the sum of squares of the two Boolean forward coordinates.
LeanFrontier.MarkovTree.exists_sq_modEq_neg_one_markovNumber(n : OrientedNode) : ∃ r : ℤ, r ^ 2 ≡ -1 [ZMOD n.markovNumber]
import LeanFrontier.NumberTheory.MarkovTree.ModularRoot1f3e8fae49d71521079cb17ea2cf18341072ac2d · downstream import passpropext, Classical.choice, Quot.sound8d9e5b57b0881bd469b7d5a8af6297a7c1171330769229ba10c71177d72b4ab8Every accepted oriented Markov number admits an integer square root of `-1` modulo itself.
LeanFrontier.MarkovTree.pathMoves_nonBacktracking(n : OrientedNode) (path : List Bool) : NonBacktrackingFrom n.back (pathMoves n path)
import LeanFrontier.NumberTheory.MarkovTree.Orientedcbde55d511254764cb1496e27f719dc34bcb530e · downstream import passpropext, Classical.choice, Quot.soundfb0605229caebfeedd89029054039e3dc66517980f5bd87364b67ff5ab2f8307Boolean paths erase to non-backtracking move lists in the accepted three-move Markov graph.
LeanFrontier.MarkovTree.follow_state_eq_walk(n : OrientedNode) (path : List Bool) : (follow n path).state = walk (pathMoves n path) n.state
import LeanFrontier.NumberTheory.MarkovTree.Orientedcbde55d511254764cb1496e27f719dc34bcb530e · downstream import passpropext, Classical.choice, Quot.sound78a6d13cfe0f403e7934ad4a54a77e71137dd06626b3b36b33bde724d0bf49c9The state reached by the oriented binary path is exactly the state reached by erasing it to the accepted `MarkovTree.walk` representation.
LeanFrontier.MarkovTree.pathMoves_injective(n : OrientedNode) : Function.Injective (pathMoves n)
import LeanFrontier.NumberTheory.MarkovTree.Orientedcbde55d511254764cb1496e27f719dc34bcb530e · downstream import passpropext, Classical.choice, Quot.soundff41d09c7a42ac9c091c87782b716d37aef2b902b258fc65ce54971d1ccde1ebDistinct Boolean paths have distinct erased move sequences. This is injectivity of the *path representation*, not injectivity of the resulting Markov state or of any numerical Markov label.
LeanFrontier.MarkovTree.move_isSolution(m : Move) {s : State} (h : s.IsSolution) : (move m s).IsSolution
import LeanFrontier.NumberTheory.MarkovTree.Pathsf36bbf2eab4158012a4fac0308a56de67f6a6f61 · downstream import passpropext, Classical.choice, Quot.sound842ae64f2e316b8e5d24ca3e492e47ace919595743ec7cc08ea555bb53df2726Every coordinate Vieta move preserves the Markov equation.
LeanFrontier.MarkovTree.move_involutive(m : Move) (s : State) : move m (move m s) = s
import LeanFrontier.NumberTheory.MarkovTree.Pathsf36bbf2eab4158012a4fac0308a56de67f6a6f61 · downstream import passpropextd5ca2aad8073010f64ea05f01e8cde3d2f8229e0905c30af20050a044dcab6e5Each coordinate Vieta move is an involution.
LeanFrontier.MarkovTree.walk_isSolution(path : List Move) {s : State} (h : s.IsSolution) : (walk path s).IsSolution
import LeanFrontier.NumberTheory.MarkovTree.Pathsf36bbf2eab4158012a4fac0308a56de67f6a6f61 · downstream import passpropext, Classical.choice, Quot.soundaf89abf2e584bca0120124216fd1d074933bcfa83e9a87afa9812a59ab8d4498Every finite Markov-tree walk preserves the Markov equation.
LeanFrontier.MarkovTree.walk_reverse(path : List Move) (s : State) : walk path.reverse (walk path s) = s
import LeanFrontier.NumberTheory.MarkovTree.Pathsf36bbf2eab4158012a4fac0308a56de67f6a6f61 · downstream import passpropext69c39e9468a33f32e3374931ffa745f0771ef79e95a2c8e9ba877189d0a4a817Reversing a move list exactly reverses the corresponding Markov-tree walk.
LeanFrontier.MarkovTree.isSquare_neg_one_mod_markovNumber(n : OrientedNode) : IsSquare (-1 : ZMod n.markovNumber.natAbs)
import LeanFrontier.NumberTheory.MarkovTree.QuadraticResidue7a635e595d7d34d5ad7372a77e3dec4d787de8f3 · downstream import passpropext, Classical.choice, Quot.sound5ba70600209ab46e02a339dc1bb79d204f7096ae792875ffcef83687cb5c4b58Every oriented Markov-number label carries a square root of `-1` modulo its absolute value. The complementary coordinates are coprime, their squares sum to a multiple of the Markov number, and the primitive sum-of-two-squares theorem supplies the modular square root.
LeanFrontier.MarkovTree.prime_dvd_markovNumber_mod_four_ne_three(n : OrientedNode) {p : ℕ} (hp : p.Prime) (hd : p ∣ n.markovNumber.natAbs) : p % 4 ≠ 3
import LeanFrontier.NumberTheory.MarkovTree.QuadraticResidue7a635e595d7d34d5ad7372a77e3dec4d787de8f3 · downstream import passpropext, Classical.choice, Quot.sound7afad2b9ee3fa7a9edceea01538fb8d4382e108a6a201874d6e0071f2572be33No prime divisor of an oriented Markov-number label is congruent to three modulo four.
LeanFrontier.MarkovTree.sternNode_append_eq_descendFrom(tail base : List Bool) : sternNode (tail ++ base) = descendFrom (sternNode base) tail
import LeanFrontier.NumberTheory.MarkovTree.ReRootedSubtree036dcff2e266b00e74e80d3fe46897919884572e · downstream import passpropext, Classical.choice, Quot.sound74adfa4d37ca2c711b84c669679557281cb1a54de436958d57b4755146ea410bAppending a local descendant tail to a canonical base path is exactly the same as re-rooting at `sternNode base` and applying `descendFrom`.
LeanFrontier.MarkovTree.sternNode_childSubtree_eq_descendFrom(base tail : List Bool) (dir : Bool) : sternNode (tail ++ dir :: base) = descendFrom (child (sternNode base) dir) tail
import LeanFrontier.NumberTheory.MarkovTree.ReRootedSubtree036dcff2e266b00e74e80d3fe46897919884572e · downstream import passpropext, Classical.choice, Quot.sound907af8d97fe916e6289e4fcc623eda3d476090ed410b20b0e41bac69be8f5821A descendant of the immediate `dir` child of `base` can be computed entirely inside the re-rooted subtree at that child.
LeanFrontier.MarkovTree.sternMarkovNumber_append_eq_descendFrom(tail base : List Bool) : sternMarkovNumber (tail ++ base) = (descendFrom (sternNode base) tail).markovNumber
import LeanFrontier.NumberTheory.MarkovTree.ReRootedSubtree036dcff2e266b00e74e80d3fe46897919884572e · downstream import passpropext, Classical.choice, Quot.sound1bc843ad3c53f0cc5f1be990758990c76192ca63864a3d67371547a3f34ab154The canonical Markov-number label of an appended descendant path is the local label obtained by re-rooting at the base node.
LeanFrontier.MarkovTree.markovNumber_le_descendFrom(n : OrientedNode) (tail : List Bool) : n.markovNumber ≤ (descendFrom n tail).markovNumber
import LeanFrontier.NumberTheory.MarkovTree.ReRootedSubtree036dcff2e266b00e74e80d3fe46897919884572e · downstream import passpropext, Classical.choice, Quot.sound7aa15cbf84d67d281e7dfa9ff36a91c441718f991f200f29b9f84456d707c5c3Re-rooted descent never decreases the Markov-number label.
LeanFrontier.MarkovTree.markovNumber_lt_descendFrom_of_ne_nil(n : OrientedNode) {tail : List Bool} (hne : tail ≠ []) : n.markovNumber < (descendFrom n tail).markovNumber
import LeanFrontier.NumberTheory.MarkovTree.ReRootedSubtree036dcff2e266b00e74e80d3fe46897919884572e · downstream import passpropext, Classical.choice, Quot.sound6bda986da8dfcc84c25128d9f5a9981e47265e959671b2851e8c240f54a65e5bEvery nontrivial re-rooted descent strictly increases the Markov-number label.
LeanFrontier.MarkovTree.descendFrom_sternNode_state_injective(base : List Bool) : Function.Injective (fun tail : List Bool => (descendFrom (sternNode base) tail).state)
import LeanFrontier.NumberTheory.MarkovTree.ReRootedSubtree036dcff2e266b00e74e80d3fe46897919884572e · downstream import passpropext, Classical.choice, Quot.sound3687933d043f5204442772f5fb19ca254c63313cd8674e06c4ec8d2dab0cf70fWithin a subtree re-rooted at a canonical `sternNode`, the full labelled Markov state still determines the local descendant tail. Thus re-rooting does not create any collisions in the already-proved full-state tree embedding.
LeanFrontier.MarkovTree.exists_walk_from_root_of_positive_solution(s : State) (hx : 0 < s.x) (hy : 0 < s.y) (hz : 0 < s.z) (hsol : s.IsSolution) : ∃ path : List Move, walk path ⟨1, 1, 1⟩ = s
import LeanFrontier.NumberTheory.MarkovTree.Reachabilityf14fad76dc25ce37dc7a908424430a556ede1197 · downstream import passpropext, Classical.choice, Quot.soundcddae09046bf5de7f994391fd43c67900a1a8330c241cda13b421e8fa97a77f6Every positive integer solution of the Markov equation is reachable from the root `(1,1,1)` by a finite sequence of coordinate Vieta moves. This is an existence/normalization theorem only: it does not assert uniqueness of the path, nor injectivity of any coordinate or Markov-number label.
LeanFrontier.MarkovTree.sternNode_cons(dir : Bool) (path : List Bool) : sternNode (dir :: path) = child (sternNode path) dir
import LeanFrontier.NumberTheory.MarkovTree.SternBrocot12539aa0d323d1eb02574ecf8d41c7bcc44c0a92 · downstream import passpropext, Classical.choice, Quot.sound520eab05332c9ea7973f6be862d363e8f66f407d93354c7c8a94662e8fcc1f99Prepending a Stern-Brocot direction is exactly one forward child step in the oriented Markov tree. Thus the two accepted path representations have the same rooted binary recursion after the path-convention reversal.
LeanFrontier.MarkovTree.sternMoves_cons(dir : Bool) (path : List Bool) : sternMoves (dir :: path) = sternMoves path ++ [forwardMove (sternNode path).back dir]
import LeanFrontier.NumberTheory.MarkovTree.SternBrocot12539aa0d323d1eb02574ecf8d41c7bcc44c0a92 · downstream import passpropext, Classical.choice, Quot.sounda2174e5ddeb754da2c84980ddbb3794ddae755fcb5c92d8cecb981eec21e8ac7Under the same path convention, prepending a Stern-Brocot direction appends exactly the corresponding forward coordinate move to the non-backtracking Markov walk.
LeanFrontier.MarkovTree.sternBrocot_pair_eq_iff_sternMoves_eq(p q : List Bool) : SternBrocot.pair p = SternBrocot.pair q ↔ sternMoves p = sternMoves q
import LeanFrontier.NumberTheory.MarkovTree.SternBrocot12539aa0d323d1eb02574ecf8d41c7bcc44c0a92 · downstream import passpropext, Classical.choice, Quot.soundd09a4f59c53cc0e863237ca15ef6e39961867bf37f3f60d3af07f9d95b0bc4e0Two Stern-Brocot nodes are equal exactly when their corresponding oriented Markov non-backtracking move encodings are equal. This is the tree-position correspondence between the accepted Stern-Brocot and oriented Markov representations. It intentionally stops before any assertion about injectivity of numerical Markov triples or Markov-number labels.
LeanFrontier.MarkovTree.coordinate_dvd_otherSquareSum(s : State) (m : Move) (h : s.IsSolution) : s.coordinate m ∣ s.otherSquareSum m
import LeanFrontier.NumberTheory.MarkovTree.SumSquaresDivisibility7d312dd2fe0ddf4eb1b6b8739e1c7c1a56c4c98c · downstream import passpropext, Classical.choice, Quot.sound30b42dd056392958dfed2526ea869ff78d092cbec0cee5628036d59b82a5315eIn any bundled Markov solution, each coordinate divides the sum of squares of the other two coordinates.
LeanFrontier.MarkovTree.markovNumber_dvd_otherSquareSum(n : OrientedNode) : n.markovNumber ∣ n.state.otherSquareSum n.back
import LeanFrontier.NumberTheory.MarkovTree.SumSquaresDivisibility7d312dd2fe0ddf4eb1b6b8739e1c7c1a56c4c98c · downstream import passpropext, Classical.choice, Quot.sounde037fd2d17fd77d7f6bbdf38c9b5fb8a5d8344ef1821f2580db37f43e89b9cf5The Markov-number coordinate of an oriented node divides the sum of squares of its two non-back coordinates.
LeanFrontier.MarkovTree.branchPermState_move(initial m : Move) (s : State) : branchPermState initial (move m s) = move (branchPermMove initial m) (branchPermState initial s)
import LeanFrontier.NumberTheory.MarkovTree.Symmetryc9aa9dab007a016606d15b96ad1be6e3d09cfc47 · downstream import passpropextdeec79814cde2d4e7b0837ec92d998efb7399f16f9e33763b7da528f87e91a11The cyclic coordinate permutation commutes with the corresponding permutation of a single Vieta coordinate move.
LeanFrontier.MarkovTree.exists_permuted_sternNode_of_branchNode(initial : Move) (path : List Bool) : ∃ sternPath : List Bool, branchPermState initial (sternNode sternPath).state = (branchNode initial path).state
import LeanFrontier.NumberTheory.MarkovTree.Symmetryc9aa9dab007a016606d15b96ad1be6e3d09cfc47 · downstream import passpropext, Classical.choice, Quot.sound891cdfdb15a70d414a9789398b3ea1d27f816ce08e37cd8ee0f2fa1696fb017eEvery node in any of the three labelled oriented branches is a cyclic coordinate permutation of a node in the canonical third branch, hence of a `sternNode`. The Boolean path on the canonical branch is reconstructed by transporting the erased non-backtracking move word through the inverse coordinate permutation and invoking the accepted unique decoder.
LeanFrontier.MarkovTree.exists_permuted_sternNode_of_positive_solution(s : State) (hx : 0 < s.x) (hy : 0 < s.y) (hz : 0 < s.z) (hsol : s.IsSolution) (hne : s ≠ ⟨1, 1, 1⟩) : ∃ initial : Move, ∃ path : List Bool, branchPermState initial (sternNode path).state = s
import LeanFrontier.NumberTheory.MarkovTree.Symmetryc9aa9dab007a016606d15b96ad1be6e3d09cfc47 · downstream import passpropext, Classical.choice, Quot.sound74f92fd63e3adbda9560313ad4fd8769fe4fbf46ea33c30c814bb95a5f1dfd7aEvery positive integer Markov solution other than the exceptional root is a cyclic coordinate permutation of the Markov state attached to some Stern-Brocot path. This collapses the accepted three-branch labelled coverage theorem to the single canonical Stern-Brocot branch modulo cyclic coordinate symmetry. It remains purely a representation statement: no uniqueness of the Stern-Brocot path after forgetting coordinate order, and no injectivity of any numerical Markov label, is asserted.
LeanFrontier.MarkovTree.uniquenessConjecture_iff_sternNode: UniquenessConjecture ↔ ∀ p q : List Bool, (sternNode p).state.maxCoord = (sternNode q).state.maxCoord → (sternNode p).state.Permutes (sternNode q).state
import LeanFrontier.NumberTheory.MarkovTree.UniquenessConjecture6d228f4731647094b6fbe243466d65484fe491dd · downstream import passpropext, Classical.choice, Quot.sound0c1558e8539aa9a57dd441797ff14352e09004b4b7dddf722d026814611c490cThe classical global Markov uniqueness conjecture is equivalent to its restriction to the accepted canonical Stern-Brocot branch. The forward direction is immediate because every `sternNode` is a positive Markov solution. For the converse, the accepted cyclic-symmetry coverage theorem writes every non-root positive solution as a cyclic coordinate permutation of some `sternNode`. Cyclic permutation preserves both the maximum coordinate and the unordered coordinate multiset, so a canonical-branch uniqueness statement transports back to arbitrary positive Markov triples. The exceptional root `(1,1,1)` is handled directly from positivity and maximum coordinate one.
LeanFrontier.MarkovTree.jump_descends_ordered_positive{x y z : ℤ} (hx : 0 < x) (hxy : x ≤ y) (hyz : y ≤ z) (h : MarkovEquation.IsSolution x y z) (hne : ¬ (x = 1 ∧ y = 1 ∧ z = 1)) : 0 < MarkovEquation.jump x y z ∧ MarkovEquation.jump x y z ≤ y ∧ MarkovEquation.jump x y z < z
import LeanFrontier.NumberTheory.MarkovTree294a1aab198bae904a0a00b3dbe1bc866949974b · downstream import passpropext, Classical.choice, Quot.sound938bf7108be9385ad9e5d917a85ed5e4d51f3635b565c601fed94a664dfe3429For a positive ordered Markov triple other than `(1, 1, 1)`, the Vieta jump in the largest coordinate is again positive, lies at or below the middle coordinate, and therefore strictly decreases the largest coordinate.
LeanFrontier.Mediant.crossDet_left_mediant(a b c d : R) : crossDet a b (a + c) (b + d) = crossDet a b c d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropextbae55606efcfc7ae247cc8b3bdefc34239dc5217fe22aeedf35cfc3c11e17f39Replacing the second pair by the mediant pair leaves the cross determinant unchanged.
LeanFrontier.Mediant.crossDet_mediant_right(a b c d : R) : crossDet (a + c) (b + d) c d = crossDet a b c d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext4bb5c50f0e07bace5f8b2a722208a89ff40b7ea0656a37f4d372fdc6ad8d95c1Replacing the first pair by the mediant pair leaves the cross determinant unchanged.
LeanFrontier.Mediant.isCoprime_mediant(a b c d : R) (h : crossDet a b c d = 1) : IsCoprime (a + c) (b + d)
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext, Quot.soundf92c71194fc090c9265920e1a49d0a344d9532dd936c7f57e4fac550ae14f880The numerator and denominator of the mediant of a unimodular pair are coprime: the mediant of two Farey neighbours is already in lowest terms.
LeanFrontier.Mediant.div_lt_div_iff_crossDet_pos{a b c d : K} (hb : 0 < b) (hd : 0 < d) : a / b < c / d ↔ 0 < crossDet a b c d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext, Classical.choice, Quot.sound6a14834d17f770e7e0baebac95fb6c8e1c625e987cef9bc9527b5d4ae550b2cdOver a linearly ordered field, two fractions with positive denominators are in increasing order exactly when their cross determinant is positive.
LeanFrontier.Mediant.div_lt_mediant{a b c d : K} (hb : 0 < b) (hd : 0 < d) (h : a / b < c / d) : a / b < mediant a b c d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext, Classical.choice, Quot.sounddfcd538c9ad0865d744d81d02ffd0e07028e02db0ca89401d7aa1cc66c8a0a35The mediant is strictly larger than the smaller of the two fractions.
LeanFrontier.Mediant.mediant_lt_div{a b c d : K} (hb : 0 < b) (hd : 0 < d) (h : a / b < c / d) : mediant a b c d < c / d
import LeanFrontier.NumberTheory.Mediantc6e5dbc7bff6d829b9be140bc8ec91452908eb23 · downstream import passpropext, Classical.choice, Quot.sound2a79fa0e5c8520f3d2fa6b2fc5ee8ac23db94bc9053cb22024645311e40dc13bThe mediant is strictly smaller than the larger of the two fractions.
LeanFrontier.Padovan.padovan_pos(n : ℕ) : 1 ≤ padovan n
import LeanFrontier.NumberTheory.Padovan7863e1ceb4652b578a4e08d70cc08cecb7730090 · downstream import passpropext, Quot.sound1ff3ff0bfba85c688f4576ed13cea8bce9b7bcf18b20a753ec8c1e8b979eba20Every term of the Padovan sequence is at least `1`.
LeanFrontier.Padovan.padovan_sum_add_two(n : ℕ) : (∑ i ∈ Finset.range (n + 1), padovan i) + 2 = padovan (n + 2) + padovan (n + 3)
import LeanFrontier.NumberTheory.Padovan7863e1ceb4652b578a4e08d70cc08cecb7730090 · downstream import passpropext, Classical.choice, Quot.sound971c512602dc3d59f7e35ef5e13a112e7c75ce2360d4bf95855fe25badc865b7The partial sums of the Padovan sequence telescope against two later terms: `(∑ i ∈ range (n + 1), P i) + 2 = P (n + 2) + P (n + 3)`.
LeanFrontier.PowerSums.sum_odd_eq_sq(n : ℕ) : ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2
import LeanFrontier.NumberTheory.PowerSums2636907985e7cc99ab78b2f099b0ddfa006bd4bb · downstream import passpropext, Classical.choice, Quot.sound34476c59800c620441c08612dc96771afcd1fad3e181d430558072b16fa1eddcThe first `n` odd natural numbers sum to `n²`.
LeanFrontier.PowerSums.sum_cubes_eq_sum_sq(n : ℕ) : (∑ i ∈ Finset.range n, i) ^ 2 = ∑ i ∈ Finset.range n, i ^ 3
import LeanFrontier.NumberTheory.PowerSums2636907985e7cc99ab78b2f099b0ddfa006bd4bb · downstream import passpropext, Classical.choice, Quot.sounde90e64d3c4716c9b63f002157e3f77539368a0cce94a4e9bfa0bd7daa79175b1Nicomachus's theorem: the sum of the first `n` cubes equals the square of the sum of the first `n` natural numbers.
LeanFrontier.Int.exists_sq_modEq_neg_one_of_isCoprime_of_dvd_sq_add_sq{m u v : ℤ} (hcop : IsCoprime m v) (hdiv : m ∣ u ^ 2 + v ^ 2) : ∃ r : ℤ, r ^ 2 ≡ -1 [ZMOD m]
import LeanFrontier.NumberTheory.SquareRootNegOnef3829d21aede7bd4033f96b619124a3abe6d6f07 · downstream import passpropextacb96b1358222ddfde543b29834e09d9c291d02337f7ad2250bfcb73c4d8f2deIf `m ∣ u² + v²` and `m` is coprime to `v`, then `-1` has a square root modulo `m`.
LeanFrontier.SternBrocot.mediant_isStrictlyBetween_bounds(path : List Bool) : Farey.IsStrictlyBetween (bounds path).1.1 (bounds path).1.2 ((bounds path).1.1 + (bounds path).2.1) ((bounds path).1.2 + (bounds path).2.2) (bounds path).2.1 (bounds path).2.2
import LeanFrontier.NumberTheory.SternBrocot.Extremala975bf622289d45ff85acd51828218841bb257a4 · downstream import passpropext, Classical.choice, Quot.sound5ac3c51f75362d705fb0d8cabbfb98cf644e1e25869980f5f3359c587a2a49a6The mediant of the two boundary pairs at every Stern-Brocot path lies strictly between the boundaries in the integer cross-multiplication sense. This remains meaningful on the outer spines, where one boundary denominator may still be zero.
LeanFrontier.SternBrocot.mediant_leastDenominator_bounds(path : List Bool) (hleft : 0 < (bounds path).1.2) (hright : 0 < (bounds path).2.2) {p q : ℤ} (hbetween : Farey.IsStrictlyBetween (bounds path).1.1 (bounds path).1.2 p q (bounds path).2.1 (bounds path).2.2) : (bounds path).1.2 + (bounds path).2.2 ≤ q ∧ (q = (bounds path).1.2 + (bounds path).2.2 → p = (bounds path).1.1 + (bounds path).2.1)
import LeanFrontier.NumberTheory.SternBrocot.Extremala975bf622289d45ff85acd51828218841bb257a4 · downstream import passpropext, Classical.choice, Quot.sound955ce58db6aaece9e19a80ba9302b65fa54a15ae21437f4019c11394be54935aIf both boundary denominators of a Stern-Brocot interval are positive, every interior fraction has denominator at least the mediant denominator. Equality of denominators forces the interior numerator to be the mediant numerator, so the mediant is the unique least-denominator interior representative.
LeanFrontier.SternBrocot.bounds_append(path : List Bool) (dir : Bool) : bounds (path ++ [dir]) = if dir then (((bounds path).1.1 + (bounds path).2.1, (bounds path).1.2 + (bounds path).2.2), (bounds path).2) else ((bounds path).1, ((bounds path).1.1 + (bounds path).2.1, (bounds path).1.2 + (bounds path).2.2))
import LeanFrontier.NumberTheory.SternBrocot.Intervals45d75e52229002d285d487c3f0f0c00c63784173 · downstream import passpropext6f9ffacc2abae848f1008fd29487823d15f0a77e675a9d8c0cc6f1cfbd869701Appending one root-to-leaf edge updates exactly one boundary by the mediant of the current boundaries: `false` replaces the right boundary and `true` replaces the left boundary.
LeanFrontier.SternBrocot.crossDet_bounds(path : List Bool) : Mediant.crossDet (bounds path).1.1 (bounds path).1.2 (bounds path).2.1 (bounds path).2.2 = 1
import LeanFrontier.NumberTheory.SternBrocot.Intervals45d75e52229002d285d487c3f0f0c00c63784173 · downstream import passpropextaee62da93a75fa39b94708f1c72bdaf5d26547a4d5e96b7ca06cf97db10f750eThe two boundary pairs of every Stern-Brocot interval are unimodular: their cross determinant is exactly `1`.
LeanFrontier.SternBrocot.mediantDen_pos(path : List Bool) : 0 < (bounds path).1.2 + (bounds path).2.2
import LeanFrontier.NumberTheory.SternBrocot.Intervals45d75e52229002d285d487c3f0f0c00c63784173 · downstream import passpropext, Classical.choice, Quot.soundd046d9a081924211234e28e495a95421d865248174e46bfeb0ff636a3aa2f633The denominator of the mediant of every Stern-Brocot interval is positive. This includes the outer spines where one of the two boundary denominators is still zero.
LeanFrontier.SternBrocot.mediant_isCoprime(path : List Bool) : IsCoprime ((bounds path).1.1 + (bounds path).2.1) ((bounds path).1.2 + (bounds path).2.2)
import LeanFrontier.NumberTheory.SternBrocot.Intervals45d75e52229002d285d487c3f0f0c00c63784173 · downstream import passpropext, Quot.sounde7b5af69a7b7456ddd5571ce133bf033c78d2afc0803e45f30393b5e48d6c4c3The mediant numerator and denominator of every Stern-Brocot interval are coprime. Thus every node produced by the interval construction is already a reduced fraction.
LeanFrontier.SternBrocot.mediant_bounds_eq_pair(path : List Bool) : (bounds path).1.1 + (bounds path).2.1 = ((pair path).1 : ℤ) ∧ (bounds path).1.2 + (bounds path).2.2 = ((pair path).2 : ℤ)
import LeanFrontier.NumberTheory.SternBrocot.NodeInterval83a28981e6863e0f54e15227b65d834256a65123 · downstream import passpropext, Quot.sound6cd6373ff4ee4ce6ff9c210ec57df15cdc4a3b81c602644ab2c32f77702dec1dThe direct Stern-Brocot node represented by a path is exactly the mediant of the two boundary pairs of the interval represented by the same path. The interval uses integers, so the natural numerator and denominator of `pair path` are cast to `ℤ`.
LeanFrontier.SternBrocot.pair_positive_coprime(path : List Bool) : 0 < (pair path).1 ∧ 0 < (pair path).2 ∧ Nat.Coprime (pair path).1 (pair path).2
import LeanFrontier.NumberTheory.SternBrocot1bacfad752c35f0133d4311550543b2b6044ddfe · downstream import passpropext, Quot.sound0def422f8307687347e698908d413aba50fc1209365e29e5da676d919d4d9152Every Stern-Brocot path reaches a pair of positive coprime naturals.
LeanFrontier.SternBrocot.existsUnique_pair_of_coprime{a b : ℕ} (ha : 0 < a) (hb : 0 < b) (hab : Nat.Coprime a b) : ∃! path : List Bool, pair path = (a, b)
import LeanFrontier.NumberTheory.SternBrocot1bacfad752c35f0133d4311550543b2b6044ddfe · downstream import passpropext, Classical.choice, Quot.sound2d51641f6d39e00ed4d94bbfdb0025554dda64523e1b4379f7ecc151e032d190Every positive coprime numerator-denominator pair occurs at exactly one root-to-leaf path in the Stern-Brocot tree.
LeanFrontier.SternBrocot.initial_run_euclidean_quotient(dir : Bool) (k : ℕ) (path : List Bool) : let p
import LeanFrontier.NumberTheory.SternBrocotEuclidean75f2d19582ff80f6fab133b79615739024c14f5f · downstream import passpropext, Quot.sound16648d83440a4e6e43d301af7980cb37ce8941e226feb136f3f8c61bb046e964An initial nonterminal Stern-Brocot run records one Euclidean quotient. A run of `k` left moves followed by a right move gives denominator/numerator quotient `k`; a run of `k` right moves followed by a left move gives numerator/denominator quotient `k`. The theorem is stated uniformly in the run direction.
LeanFrontier.SternBrocot.terminal_run_euclidean_quotient(dir : Bool) (k : ℕ) : let p
import LeanFrontier.NumberTheory.SternBrocotEuclidean75f2d19582ff80f6fab133b79615739024c14f5f · downstream import passpropextfaa71f1530720a5b27b26ebd679ebfb4d38a390f1272ec3d6409511195ea834cA terminal Stern-Brocot run has Euclidean quotient one larger than its run length. This is the endpoint case complementary to `initial_run_euclidean_quotient`: starting from the root pair `(1,1)`, a path consisting entirely of `k` copies of one direction has quotient `k + 1` in that direction.
LeanFrontier.SternDiatomic.fusc_eq_fusc_succ_iff{n : ℕ} (hn : 0 < n) : fusc n = fusc (n + 1) ↔ n = 1
import LeanFrontier.NumberTheory.SternDiatomic.Enumeration2818ce0711712006c2d95498db5503627723f72c · downstream import passpropext, Classical.choice, Quot.sound599db82c519ba724c2cf1991f67ee870480d60078ad28140427ddd9149a7229cA value of Stern's diatomic sequence equals the next one exactly at index `1`, where the pair is `(1, 1)`. Everywhere else the pair is strictly monotone in a direction that records the parity of the index, which is what makes the enumeration injective.
LeanFrontier.SternDiatomic.exists_fusc_eq_of_coprime{a b : ℕ} (ha : 0 < a) (hb : 0 < b) (hab : Nat.Coprime a b) : ∃ n, 0 < n ∧ fusc n = a ∧ fusc (n + 1) = b
import LeanFrontier.NumberTheory.SternDiatomic.Enumeration2818ce0711712006c2d95498db5503627723f72c · downstream import passpropext, Classical.choice, Quot.sounddedfdfa4ed032a2df487b80b5d6e90e568060789453c51562fdead15d20b6fcaEvery pair of coprime positive naturals occurs as a pair of consecutive values of Stern's diatomic sequence. Together with `LeanFrontier.SternDiatomic.coprime_fusc_fusc_succ` this says that the fractions `fusc n / fusc (n + 1)` are exactly the positive rationals in lowest terms.
LeanFrontier.SternDiatomic.eq_of_fusc_pair_eq{m n : ℕ} (hm : 0 < m) (hn : 0 < n) (h₀ : fusc m = fusc n) (h₁ : fusc (m + 1) = fusc (n + 1)) : m = n
import LeanFrontier.NumberTheory.SternDiatomic.Enumeration2818ce0711712006c2d95498db5503627723f72c · downstream import passpropext, Classical.choice, Quot.sound0c525267c568aa3a74139b9c8c9cfefa1156e0830f3666cfed6238a4c3fc88ceAn index above `0` is determined by its pair of consecutive values: the map `n ↦ (fusc n, fusc (n + 1))` is injective on the positive naturals.
LeanFrontier.SternDiatomic.existsUnique_fusc_eq_of_coprime{a b : ℕ} (ha : 0 < a) (hb : 0 < b) (hab : Nat.Coprime a b) : ∃! n : ℕ, 0 < n ∧ fusc n = a ∧ fusc (n + 1) = b
import LeanFrontier.NumberTheory.SternDiatomic.Enumeration2818ce0711712006c2d95498db5503627723f72c · downstream import passpropext, Classical.choice, Quot.soundbf770f49cba437b1d88c15a7e92eba9f0363657f28ebf127a0178a0a2909a392The Stern-Brocot enumeration: the consecutive pairs of Stern's diatomic sequence run through every pair of coprime positive naturals exactly once.
LeanFrontier.SternDiatomic.fusc_surjective: Function.Surjective fusc
import LeanFrontier.NumberTheory.SternDiatomic.Enumeration2818ce0711712006c2d95498db5503627723f72c · downstream import passpropext, Classical.choice, Quot.sound4edf2c74a3409d2e6dc33d7d32150276d639878f181cb4e2b7375d6296806b9dStern's diatomic sequence is surjective: every natural number occurs as a value, since `(a, 1)` is a coprime pair for every positive `a`.
LeanFrontier.SternDiatomic.fib_is_max_on_dyadic_row(n : ℕ) : (∀ k : ℕ, ((2 : ℕ) ^ n ≤ k ∧ k < (2 : ℕ) ^ (n + 1)) → fusc k ≤ Nat.fib (n + 2)) ∧ ∃ k : ℕ, (2 : ℕ) ^ n ≤ k ∧ k < (2 : ℕ) ^ (n + 1) ∧ fusc k = Nat.fib (n + 2)
import LeanFrontier.NumberTheory.SternDiatomic.RowMaximumaf928552d6ec1dac459b2c028df88d75cdaf8d25 · downstream import passpropext, Classical.choice, Quot.sound3fe5a78cb4abfc7991446469771a062c2623022220a9ef39e75a8f1331b04dfcOn every dyadic row of Stern's diatomic sequence, the largest value is the corresponding Fibonacci number. More precisely, every value with `2^n ≤ k < 2^(n+1)` is at most `fib (n + 2)`, and some index in that same row attains equality.
LeanFrontier.SternDiatomic.fusc_two_mul(n : ℕ) : fusc (2 * n) = fusc n
import LeanFrontier.NumberTheory.SternDiatomicee51b67eda84ead788d67f6b3a4ecde0709eecdd · downstream import passpropext, Quot.soundc1f244e0834d3809d7e960fd9a730b47c3d459e1062ef2e910d00b4722c99f15Halving an even index leaves the value unchanged.
LeanFrontier.SternDiatomic.fusc_two_mul_add_one(n : ℕ) : fusc (2 * n + 1) = fusc n + fusc (n + 1)
import LeanFrontier.NumberTheory.SternDiatomicee51b67eda84ead788d67f6b3a4ecde0709eecdd · downstream import passpropext, Quot.sounda44f0f6d20e948e023b4bc8480843bb93612a1f6a8d5882c8e5cb8342cc2db70An odd index splits into the two neighbouring values at half the index.
LeanFrontier.SternDiatomic.coprime_fusc_fusc_succ(n : ℕ) : Nat.Coprime (fusc n) (fusc (n + 1))
import LeanFrontier.NumberTheory.SternDiatomicee51b67eda84ead788d67f6b3a4ecde0709eecdd · downstream import passpropext, Classical.choice, Quot.sounda959969f48c0e19a8ae259e56cfa7e2d3683f98ce2a17e4ff300870f909b3effConsecutive values of Stern's diatomic sequence are coprime, so the fraction `fusc n / fusc (n + 1)` is always in lowest terms.
LeanFrontier.SternDiatomic.fusc_pos{n : ℕ} (hn : n ≠ 0) : 0 < fusc n
import LeanFrontier.NumberTheory.SternDiatomicee51b67eda84ead788d67f6b3a4ecde0709eecdd · downstream import passpropext, Classical.choice, Quot.sound1a38f1af66849b7b793296a9ff6c9ee8285c771949d9056ba259925898f3004fEvery value of Stern's diatomic sequence after the initial one is positive.
LeanFrontier.Nat.hasSum_inv_sylvesterNumber: HasSum (fun n : ℕ => (1 : ℝ) / sylvesterNumber n) 1
import LeanFrontier.NumberTheory.SylvesterSequence.ReciprocalSeries844687c308e67ece9fd13e72e3de4aaca53b4ce3 · downstream import passpropext, Classical.choice, Quot.sound4f09bf8695d7cd0e573663e5e2280b29d856eb6edc5ad49073ae10efe006a938The reciprocals of Sylvester's sequence sum to one: `1/2 + 1/3 + 1/7 + 1/43 + ⋯ = 1`. This is the infinite-series completion of `sum_range_inv_sylvesterNumber`.
LeanFrontier.Nat.two_le_sylvesterNumber(n : ℕ) : 2 ≤ sylvesterNumber n
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Quot.sound6948b3ebe1e937cca79ec29770e4953ea8633369b93826428efaf20bdcf7867cEvery term is at least `2`; in particular no term is `0` or `1`.
LeanFrontier.Nat.sylvesterNumber_succ_eq_sq_sub_add_one(n : ℕ) : sylvesterNumber (n + 1) = sylvesterNumber n ^ 2 - sylvesterNumber n + 1
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Quot.soundcf37838bb578357f9607c7e765fc6cdbf44b92a8d32004b01a9c9bc3db611835The defining recurrence in its classical form.
LeanFrontier.Nat.sylvesterNumber_eq_prod_add_one(n : ℕ) : sylvesterNumber n = (∏ i ∈ Finset.range n, sylvesterNumber i) + 1
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Classical.choice, Quot.sound51032bbf0bb61849a926ad476ae3f82efafe4c38efa7aac8f0f0906b8ad5d3b6Each term is one more than the product of all the earlier ones.
LeanFrontier.Nat.coprime_sylvesterNumber_sylvesterNumber{m n : ℕ} (h : m ≠ n) : Nat.Coprime (sylvesterNumber m) (sylvesterNumber n)
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Classical.choice, Quot.sound204ad1c3614d13c4c9ebaa3fde114b0c7bb5276c157fd7f3db57c9db85e259edDistinct terms of Sylvester's sequence are coprime.
LeanFrontier.Nat.strictMono_sylvesterNumber: StrictMono sylvesterNumber
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Quot.sound9db6a46f259be074e5039c727b708e129a21c4578b9c18b24795b3964764e536Sylvester's sequence is strictly increasing.
LeanFrontier.Nat.sum_range_inv_sylvesterNumber(n : ℕ) : ∑ i ∈ Finset.range n, (1 : K) / sylvesterNumber i = 1 - 1 / ((sylvesterNumber n : K) - 1)
import LeanFrontier.NumberTheory.SylvesterSequencea93c2e393ef2fa763197c6ce7a700e723868b71d · downstream import passpropext, Classical.choice, Quot.sound7e3e2c3f07fc325b36056364777ce1bf31e62aae77931328950986947aea6469The reciprocals of Sylvester's sequence telescope: the partial sums of `1 / S i` are `1 - 1 / (S n - 1)`, so the greedy unit fraction expansion of `1` never overshoots.
LeanFrontier.Nat.sum_cubes_thueMorse_partition(k : ℕ) : (∑ n ∈ (range (2 ^ (k + 4))).filter (fun n => thueMorse n = false), n ^ 3) = 32 * (2 ^ k) ^ 2 * (2 ^ (k + 4) - 1) ^ 2 ∧ (∑ n ∈ (range (2 ^ (k + 4))).filter (fun n => thueMorse n = true), n ^ 3) = 32 * (2 ^ k) ^ 2 * (2 ^ (k + 4) - 1) ^ 2
import LeanFrontier.NumberTheory.ThueMorse.ExplicitPowerSumsd038488b4c3606df6819b69a9ec3a440ff22652b · downstream import passpropext, Classical.choice, Quot.soundbc43d748db06ee88952e951f0590565c6b3edb1148f6257ee6ecc06e5e9a466eEach Thue-Morse parity class in `{0, ..., 2^(k+4)-1}` has cube sum `32 * (2^k)^2 * (2^(k+4)-1)^2`. This composes Prouhet's equal-power-sum partition with Nicomachus's closed form for the total sum of cubes.
LeanFrontier.Nat.thueMorse_two_mul(n : ℕ) : thueMorse (2 * n) = thueMorse n
import LeanFrontier.NumberTheory.ThueMorse9c79bc66909d6fbee722edc485b08a3952fb6df3 · downstream import passpropext, Classical.choice, Quot.sound57a890306872a5e28e4e232767fdd68c6286347706c7cc73907906b8392a4911Doubling leaves the Thue-Morse value unchanged: a trailing binary zero adds no one.
LeanFrontier.Nat.thueMorse_two_mul_add_one(n : ℕ) : thueMorse (2 * n + 1) = !thueMorse n
import LeanFrontier.NumberTheory.ThueMorse9c79bc66909d6fbee722edc485b08a3952fb6df3 · downstream import passpropext, Classical.choice, Quot.soundf15d4d556f71fc232c69fcde74570bad22d0db58386d7cb6630823447d7c5b0eA trailing binary one flips the Thue-Morse value.
LeanFrontier.Nat.thueMorseSign_eq_ite(n : ℕ) : thueMorseSign n = if thueMorse n then -1 else 1
import LeanFrontier.NumberTheory.ThueMorse9c79bc66909d6fbee722edc485b08a3952fb6df3 · downstream import passpropext, Classical.choice, Quot.sound2175d0a457d98edd061e8565864ee16280ab74b1c2174d67f54546d113075af6The `±1`-valued sequence is the `Bool`-valued one read as a sign.
LeanFrontier.Nat.sum_range_thueMorseSign_mul_pow{j k : ℕ} (hjk : j < k) : ∑ n ∈ range (2 ^ k), thueMorseSign n * (n : ℤ) ^ j = 0
import LeanFrontier.NumberTheory.ThueMorse9c79bc66909d6fbee722edc485b08a3952fb6df3 · downstream import passpropext, Classical.choice, Quot.sound360a65d7379c724bdfb927419fb17a97556b223928899784ef0e34eec94ded9aThe signed power sums of the Thue-Morse sequence vanish: for every exponent `j` below `k`, `∑ n < 2 ^ k, (-1) ^ s₂ n * n ^ j = 0`.
LeanFrontier.Nat.sum_pow_eq_sum_pow_thueMorse{j k : ℕ} (hjk : j < k) : ∑ n ∈ (range (2 ^ k)).filter (fun n => thueMorse n = false), n ^ j = ∑ n ∈ (range (2 ^ k)).filter (fun n => thueMorse n = true), n ^ j
import LeanFrontier.NumberTheory.ThueMorse9c79bc66909d6fbee722edc485b08a3952fb6df3 · downstream import passpropext, Classical.choice, Quot.sound900987a5e9a5bab392aee3da1fe236557b91f27337a858b81f109c991ac1a52e**Prouhet's theorem**: splitting `{0, 1, ..., 2 ^ k - 1}` by the Thue-Morse parity of its elements gives two blocks with the same sum of `j`-th powers for every exponent `j < k`.
LeanFrontier.HermiteLindemann.exp_injOn_isAlgebraic(hermiteLindemann : ∀ {z : ℂ}, z ≠ 0 → IsAlgebraic ℤ z → Transcendental ℤ (Complex.exp z)) : Set.InjOn Complex.exp {z : ℂ | IsAlgebraic ℤ z}
import LeanFrontier.NumberTheory.Transcendental.HermiteLindemann67f6771a4abe7dd5610f4d4a32c5abccd652a24a · downstream import passpropext, Classical.choice, Quot.sound3420106adbec770426cf0b8492918c4bedcb2e71b56ed9fdde9f4a988a30a46fHermite--Lindemann implies that complex exponentiation is injective when restricted to algebraic numbers.
LeanFrontier.Tribonacci.tribonacci_succ_pos(n : ℕ) : 1 ≤ tribonacci (n + 1)
import LeanFrontier.NumberTheory.Tribonaccibec236503c0bca9b3ce8e4c6e969fe3d30b40a9b · downstream import passpropext, Quot.sound958af4578aa35eb9e57020ae66c58d03fb14b15d905d54dadf4392605a2ed085Every Tribonacci term from index `1` onward is at least `1`.
LeanFrontier.Tribonacci.tribonacci_two_mul_sum_add_one(n : ℕ) : 2 * (∑ i ∈ Finset.range (n + 1), tribonacci i) + 1 = tribonacci (n + 2) + tribonacci n
import LeanFrontier.NumberTheory.Tribonaccibec236503c0bca9b3ce8e4c6e969fe3d30b40a9b · downstream import passpropext, Classical.choice, Quot.sounde3ad41e30f6df12a21d6280ab37f7a8502b77d9b9dd6ddd5c2ecfc7be41225bdThe partial sums of the Tribonacci sequence satisfy `2 * (∑ i ∈ range (n + 1), T i) + 1 = T (n + 2) + T n`.
LeanFrontier.ProbabilityTheory.cantelli(μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) (hX : MemLp X 2 μ) {a : ℝ} (ha : 0 < a) : μ {ω | a ≤ X ω - μ[X]} ≤ ENNReal.ofReal (Var[X; μ] / (Var[X; μ] + a ^ 2))
import LeanFrontier.Probability.Cantelli8bd0fbd4e8445a75e24cdaaa4e18ee3c988c717f · downstream import passpropext, Classical.choice, Quot.sounddd02df95054295f42d618454313d17102c820cd5c1e38b44e7f1cac823e8c4d9**Cantelli's inequality (one-sided Chebyshev inequality).** For a square-integrable real random variable `X` and `a > 0`, the upper-tail probability is bounded by `P(X - E[X] ≥ a) ≤ Var(X) / (Var(X) + a²)`. This is sharper than applying the ordinary two-sided Chebyshev inequality to the same event.
LeanFrontier.ProbabilityTheory.chungErdos(μ : Measure Ω) [IsProbabilityMeasure μ] (s : Finset ι) (A : ι → Set Ω) (hA : ∀ i ∈ s, MeasurableSet (A i)) (hsecond : 0 < ∑ i ∈ s, ∑ j ∈ s, μ.real (A i ∩ A j)) : ((∑ i ∈ s, μ.real (A i)) ^ 2) / (∑ i ∈ s, ∑ j ∈ s, μ.real (A i ∩ A j)) ≤ μ.real (⋃ i ∈ s, A i)
import LeanFrontier.Probability.ChungErdos1517a077bebaf42e4246a154855451b6a97e33fa · downstream import passpropext, Classical.choice, Quot.soundb531b36156cb1d93b4d8d29da71979f30966eebec1eeff2e67e479b687490be6**Chung-Erdős inequality.** For a finite family of measurable events, the probability of their union is bounded below by the square of the sum of their probabilities divided by the sum of all pairwise-intersection probabilities. The denominator positivity assumption is exactly the nondegenerate condition needed for the divided form.
LeanFrontier.ProbabilityTheory.kochenStone(μ : Measure Ω) [IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ n, MeasurableSet (A n)) (hdiv : Tendsto (fun N => ∑ i ∈ Finset.range N, μ.real (A i)) atTop atTop) : Filter.limsup (fun N => ((∑ i ∈ Finset.range N, μ.real (A i)) ^ 2) / (∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N, μ.real (A i ∩ A j))) atTop ≤ μ.real (Filter.limsup A atTop)
import LeanFrontier.Probability.KochenStonedcdf3d1c777552d0bc0a89d901bc39fc515f4502 · downstream import passpropext, Classical.choice, Quot.soundad071eaf1ebd4eeadc64a10ab9aa092a80b6ed2971d5fcbf6c531d5a786d63b9**Kochen-Stone inequality.** Let `A n` be measurable events in a probability space and suppose their probability partial sums diverge. Then the probability that infinitely many `A n` occur is bounded below by the limsup of the Chung-Erdős prefix ratios. No independence assumption is required.
LeanFrontier.ProbabilityTheory.paleyZygmund(μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) (hXmeas : Measurable X) (hXnonneg : ∀ ω, 0 ≤ X ω) (hX2 : MemLp X 2 μ) {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) (hsecond : 0 < ∫ ω, X ω ^ 2 ∂μ) : (((1 - θ) * ∫ ω, X ω ∂μ) ^ 2) / (∫ ω, X ω ^ 2 ∂μ) ≤ μ.real {ω | θ * (∫ x, X x ∂μ) < X ω}
import LeanFrontier.Probability.MeasurePaleyZygmund751140fbf0a50784cab31c1f70310473c9df2592 · downstream import passpropext, Classical.choice, Quot.sounddd0479a25f1aca57b6e01aa98357ab92d6ce1a2683dbc2911ed722b59c83011a**Paley-Zygmund inequality on an arbitrary probability space.** Let `X` be a measurable nonnegative real random variable with finite second moment. For `0 ≤ θ ≤ 1`, if `E[X²]` is positive, then `((1 - θ) * E[X])² / E[X²] ≤ P(X > θ * E[X])`. The probability on the right is represented by `μ.real`, the real-valued measure of the strict superlevel event.
LeanFrontier.ProbabilityTheory.pmf_paleyZygmund(p : PMF α) (X : α → ℝ) (hX : ∀ i, 0 ≤ X i) {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) (hsecond : 0 < ∫ i, X i ^ 2 ∂p.toMeasure) : (((1 - θ) * ∫ i, X i ∂p.toMeasure) ^ 2) / (∫ i, X i ^ 2 ∂p.toMeasure) ≤ (p.toMeasure {i | θ * (∫ j, X j ∂p.toMeasure) < X i}).toReal
import LeanFrontier.Probability.PMFPaleyZygmundc3f89ffdbdc46cba31bcb07797b548c7df9314e3 · downstream import passpropext, Classical.choice, Quot.sound155b427ca7037e8ebb84d9033c4702af4aa445a793e23f0a34f9cfd7f1d4aa40**Paley-Zygmund inequality for a finite probability mass function.** If `X` is nonnegative, `0 ≤ θ ≤ 1`, and the second moment is positive, then the probability that `X` exceeds `θ` times its expectation is at least `((1 - θ) E[X])² / E[X²]`. This is the standard probability-facing specialization of `LeanFrontier.FiniteProbability.paleyZygmund`.
LeanFrontier.ProbabilityTheory.measure_limsup_eq_one_of_pairwise_indep(μ : Measure Ω) [IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ n, MeasurableSet (A n)) (hpair : ∀ ⦃i j : ℕ⦄, i ≠ j → ProbabilityTheory.IndepSet (A i) (A j) μ) (hdiv : Tendsto (fun N => ∑ i ∈ Finset.range N, μ.real (A i)) atTop atTop) : μ (Filter.limsup A atTop) = 1
import LeanFrontier.Probability.PairwiseBorelCantellib2858db72f22549bb95fb9e54320ea311b8759ed · downstream import passpropext, Classical.choice, Quot.sound26b2df8bcad1368cf06226d9961b86f63ffde2446638a5d245f90547ad488c0d**Second Borel-Cantelli under pairwise independence.** Let `A n` be measurable events in a probability space. If distinct events are pairwise independent and the partial sums of their probabilities diverge to `+∞`, then infinitely many of the events occur with probability one. The hypothesis is only pairwise independence; mutual independence is not assumed.
LeanFrontier.FiniteProbability.paleyZygmund(s : Finset ι) (w X : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hX : ∀ i ∈ s, 0 ≤ X i) (hnorm : ∑ i ∈ s, w i = 1) {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) : ((1 - θ) * ∑ i ∈ s, w i * X i) ^ 2 ≤ (∑ i ∈ s.filter (fun i => θ * (∑ j ∈ s, w j * X j) < X i), w i) * ∑ i ∈ s, w i * X i ^ 2
import LeanFrontier.Probability.PaleyZygmund5ac887f79b68b50da0201f0112f98a227325b2ca · downstream import passpropext, Classical.choice, Quot.sound51732e88af0738f451b0ae267a758557a5d0d7303901303a91873bc5a19abeab**Finite weighted Paley-Zygmund inequality.** Let `w` be nonnegative weights on a finite set `s` with total weight one, and let `X` be nonnegative on `s`. For `0 ≤ θ ≤ 1`, the square of `(1 - θ) * E[X]` is at most the weight of the strict superlevel set `{i ∈ s | θ * E[X] < X i}` times the second weighted moment. Equivalently, whenever the second moment is positive, division yields the usual lower bound for the probability of exceeding a fraction `θ` of the mean.
LeanFrontier.FiniteGroupCharacter.sum_div_eq_zero_of_ne(chi psi : G →* K) (hchi : chi ≠ psi) : ∑ g : G, chi g / psi g = 0
import LeanFrontier.RepresentationTheory.FiniteGroupCharacter.Orthogonality01e225d32be7f7713cd0a652dd699c26efd64f72 · downstream import passpropext, Classical.choice, Quot.sound078811217712d84d05ddaa2e792f9ce42d27a55695898e3eb3d05b97abfc7561The pointwise quotient of two distinct multiplicative characters of a finite group has sum zero.
LeanFrontier.FiniteGroupCharacter.sum_monoidHom_eq_zero_of_ne_one(chi : G →* R) (hchi : chi ≠ 1) : ∑ g : G, chi g = 0
import LeanFrontier.RepresentationTheory.FiniteGroupCharacter9d12a280a0722da3e56aac50f1bf413081a651c6 · downstream import passpropext, Classical.choice, Quot.sounda07f2b1c2d5e16305608cf860e2714c3ce04920cf59ce92a4bdfc415d49a1addA nontrivial monoid homomorphism from a finite group into a ring without zero divisors has sum zero.
LeanFrontier.Int.totallySeparatedSpace_furstenberg: @TotallySeparatedSpace ℤ furstenbergTopology
import LeanFrontier.Topology.Furstenberg.Separation2941b50d1a8d247a2df09ef06854bf1c0199ee73 · downstream import passpropext, Classical.choice, Quot.sounde9d8e867e7fd0ece4a3d2a84b14864c64b89b7b861245d61f12c34d2ab64370bThe Furstenberg topology on the integers is totally separated: any two distinct integers can be separated by a clopen arithmetic progression.
LeanFrontier.Int.not_isOpen_singleton_furstenberg(x : ℤ) : ¬ IsOpen[furstenbergTopology] ({x} : Set ℤ)
import LeanFrontier.Topology.Furstenberg.Separation2941b50d1a8d247a2df09ef06854bf1c0199ee73 · downstream import passpropext, Classical.choice, Quot.sound5d5f647018c0420e982b57b16a3f94ac2bbf593a3f53d65df616e5d8922d5621No point is isolated in the Furstenberg topology: a singleton cannot be open because every nonempty open set is infinite. In particular, the Furstenberg topology is not discrete.
LeanFrontier.Int.isTopologicalBasis_arithProgression: @IsTopologicalBasis ℤ furstenbergTopology {S : Set ℤ | ∃ a b, b ≠ 0 ∧ S = arithProgression a b}
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.soundcd6fe9610173e1fde1db2a1e99140ba3a9d0b2314444484aa66991f033be7d38The arithmetic progressions with nonzero step are a basis of the Furstenberg topology.
LeanFrontier.Int.isOpen_arithProgression(a b : ℤ) (hb : b ≠ 0) : IsOpen[furstenbergTopology] (arithProgression a b)
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.sounddf75e75c08639fa35d3742c0eec46abe896ff20ae635d06c40831dfff88bf0deArithmetic progressions with nonzero step are open.
LeanFrontier.Int.isClosed_arithProgression(a : ℤ) {b : ℤ} (hb : b ≠ 0) : IsClosed[furstenbergTopology] (arithProgression a b)
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.soundfa74aaa726bab690656f9228808873c127b6dc34a024ddbe26da4ad629645fe6Arithmetic progressions with nonzero step are closed: after reducing to a positive step via `abs_dvd`, the complement is the union of the progressions shifted by the nonzero residues. Together with `isOpen_arithProgression`, the basic sets of the Furstenberg topology are clopen.
LeanFrontier.Int.infinite_arithProgression(a : ℤ) {b : ℤ} (hb : b ≠ 0) : (arithProgression a b).Infinite
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.sound300240412febcfb60f08ca96cad0504a80c523c4eeaa5d929b4544ae1254b3a6An arithmetic progression with nonzero step is infinite.
LeanFrontier.Int.infinite_of_isOpen{U : Set ℤ} (hU : IsOpen[furstenbergTopology] U) (hne : U.Nonempty) : U.Infinite
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.soundd10a7b29b25c414cf49efa33d04a676b83ed60274b8626a0dff0d0ed0234b247Every nonempty open set of the Furstenberg topology is infinite: it contains a whole arithmetic progression around each of its points.
LeanFrontier.Int.iUnion_prime_arithProgression: ⋃ p ∈ {p : ℕ | p.Prime}, arithProgression 0 (p : ℤ) = ({1, -1} : Set ℤ)ᶜ
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.sound47f380ba47d198cb18e10c545f39eff5c6f2b9156ea805ffc0ccbf235b22f552Furstenberg's covering identity: the progressions `pℤ` over all primes cover exactly the integers other than `1` and `-1`.
LeanFrontier.Int.infinite_of_iUnion_eq_compl{S : Set ℕ} (h0 : 0 ∉ S) (hcov : ⋃ p ∈ S, arithProgression 0 (p : ℤ) = ({1, -1} : Set ℤ)ᶜ) : S.Infinite
import LeanFrontier.Topology.Furstenbergf1f62321057c2d6d836f4a0e032c45555605b6ae · downstream import passpropext, Classical.choice, Quot.sound52d6d8ff6b3f3963b7a91b2d5138ff4fbc011f85205aa4dc379b1947607636aeThe engine of Furstenberg's proof: a set of nonzero naturals whose progressions cover all of `ℤ \ {1, -1}` cannot be finite, since a finite union of closed progressions is closed, and `{1, -1}` cannot be open, being finite and nonempty. Applied to the set of primes via `iUnion_prime_arithProgression`, this yields the infinitude of primes, which Mathlib already states as `Nat.infinite_setOf_prime`.
LeanFrontier.Int.continuous_neg_furstenberg: Continuous[furstenbergTopology, furstenbergTopology] (fun x : ℤ => -x)
import LeanFrontier.Topology.FurstenbergAlgebraa2cfb113a19f249c0ed9eb677491644778ee62ab · downstream import passpropext, Classical.choice, Quot.soundff5b6b5d3a8dfaf3c12667c039e15de828cb65f6b50536a59c8dbf63b25b0d98Negation is continuous for the named Furstenberg topology on `ℤ`. The topology is installed only locally by the theorem statement; this does not alter the ordinary global topology instance on the integers.
LeanFrontier.Int.continuous_add_furstenberg: Continuous[ @instTopologicalSpaceProd ℤ ℤ furstenbergTopology furstenbergTopology, furstenbergTopology] (fun p : ℤ × ℤ => p.1 + p.2)
import LeanFrontier.Topology.FurstenbergAlgebraa2cfb113a19f249c0ed9eb677491644778ee62ab · downstream import passpropext, Classical.choice, Quot.sounde71a39cd41a52fa959298bf2d7d0efd645cad576ebf2b670424ac9b53009ab9bAddition is continuous for the named Furstenberg topology on `ℤ`. Again, the Furstenberg topology is local to the statement; the product topology on `ℤ × ℤ` is therefore the product of two copies of `furstenbergTopology`.
LeanFrontier.Int.arithProgression_eq_zmodReduction_fiber(a : ℤ) (n : ℕ) : arithProgression a (n : ℤ) = zmodReduction n ⁻¹' ({zmodReduction n a} : Set (ZMod n))
import LeanFrontier.Topology.FurstenbergQuotients3293c670467938f1e89bf7f106fb1b53a0f61d80 · downstream import passpropext, Classical.choice, Quot.sound0c5431bc2fc6986b498574f8bddf1973b1b316773c552d734f78e592b66e7fb4An arithmetic progression with natural step `n` is exactly a fiber of reduction modulo `n`. This identity also holds at `n = 0`.
LeanFrontier.Int.continuous_zmodReduction{n : ℕ} (hn : n ≠ 0) : Continuous[furstenbergTopology, (⊥ : TopologicalSpace (ZMod n))] (zmodReduction n)
import LeanFrontier.Topology.FurstenbergQuotients3293c670467938f1e89bf7f106fb1b53a0f61d80 · downstream import passpropext, Classical.choice, Quot.sounde8b56aedca5a06f10b9a1c6155a845a4599fc895de8bf21ba64d51bd94a494d0Every nonzero reduction map is continuous from the Furstenberg topology to the discrete topology on the finite cyclic quotient.
LeanFrontier.Int.furstenbergTopology_eq_finiteQuotientTopology: furstenbergTopology = finiteQuotientTopology
import LeanFrontier.Topology.FurstenbergQuotients3293c670467938f1e89bf7f106fb1b53a0f61d80 · downstream import passpropext, Classical.choice, Quot.sound56634780bf261d2bed1d5d8b9c843dce8baaf53554ae72a0c66e777b4368926eThe Furstenberg topology is exactly the topology induced jointly by all nonzero reduction maps `ℤ → ZMod n` when the finite quotients are discrete. Thus the clopen arithmetic-progressions basis is precisely the finite-congruence quotient topology.