diff --git a/QuantizingPythagoreanTriples/Pythagore2.lean b/QuantizingPythagoreanTriples/Pythagore2.lean new file mode 100644 index 0000000..6658b81 --- /dev/null +++ b/QuantizingPythagoreanTriples/Pythagore2.lean @@ -0,0 +1 @@ +import Pythagore2.Main diff --git a/QuantizingPythagoreanTriples/Pythagore2/Basic.lean b/QuantizingPythagoreanTriples/Pythagore2/Basic.lean new file mode 100644 index 0000000..958a1da --- /dev/null +++ b/QuantizingPythagoreanTriples/Pythagore2/Basic.lean @@ -0,0 +1,98 @@ +import Mathlib + +open Polynomial + +/-! # Basic definitions for quantized Pythagorean triples + +This file contains the shared definitions from Mathevet--Morier-Genoud--Ovsienko, +"Quantizing Pythagorean triples". +-/ + +abbrev PolyZ := Polynomial ℤ + +/-! ## Standard Pythagorean triples -/ + +/-- A Pythagorean triple `(a,b,c)` is *standard* if: +- `a`, `b`, and `c` are positive integers satisfying `a² + b² = c²`; +- `gcd(a,b,c)` is `1` or `2`; +- if the gcd is `1`, then `a` is even; +- if the gcd is `2`, then `a/2` is odd. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:189-217`. -/ +def StandardPythagoreanTriple (a b c : ℕ) : Prop := + a > 0 ∧ b > 0 ∧ c > 0 ∧ a ^ 2 + b ^ 2 = c ^ 2 ∧ + (Nat.gcd (Nat.gcd a b) c = 1 ∨ Nat.gcd (Nat.gcd a b) c = 2) ∧ + (Nat.gcd (Nat.gcd a b) c = 1 → Even a) ∧ + (Nat.gcd (Nat.gcd a b) c = 2 → Odd (a / 2)) + +/-! ## q-integers and reciprocal polynomials -/ + +/-- The q-analogue of a positive integer: +`[n]_q = 1 + q + q² + ... + q^(n-1)`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:298-301`. -/ +noncomputable def qInteger (n : ℕ) : PolyZ := + ∑ i ∈ Finset.range n, (X : PolyZ) ^ i + +/-- The reciprocal of a polynomial `C`: +`C*(q) = q^(deg C) C(q⁻¹)`. + +For `C = ∑ c_i q^i`, this is encoded as `∑ c_i q^(deg C - i)`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:270-274`. -/ +noncomputable def reciprocalPolynomial {R : Type*} [CommRing R] (C : Polynomial R) : + Polynomial R := + ∑ i ∈ Finset.range (C.natDegree + 1), C.coeff i • (X : Polynomial R) ^ (C.natDegree - i) + +/-- Reciprocal with an explicitly supplied degree `d`: +`q^d C(q⁻¹) = ∑ c_i q^(d-i)`. + +This is the form used for the numerator/denominator inverse relation. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:811-820`. -/ +noncomputable def reciprocalPolynomialWithDegree {R : Type*} [CommRing R] + (C : Polynomial R) (d : ℕ) : Polynomial R := + ∑ i ∈ Finset.range (C.natDegree + 1), C.coeff i • (X : Polynomial R) ^ (d - i) + +/-- A polynomial is self-reciprocal, or palindromic. -/ +def IsSelfReciprocal {R : Type*} [CommRing R] (P : Polynomial R) : Prop := + reciprocalPolynomial P = P + +/-- A polynomial has no negative integer coefficients. -/ +def HasNonNegativeCoefficients (P : PolyZ) : Prop := + ∀ i, P.coeff i ≥ 0 + +/-- A polynomial has positive integer coefficients in the paper's combinatorial sense: +it is nonzero and has no negative coefficients. Zeros outside its support are ignored. -/ +def HasPositiveCoefficients (P : PolyZ) : Prop := + P ≠ 0 ∧ HasNonNegativeCoefficients P + +/-! ## q-deformed Pythagoras equation -/ + +/-- Three polynomials satisfy the q-deformed Pythagoras equation +`A(q)² + q B(q)² = C(q) C*(q)`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:265-274`. -/ +def IsQDeformedPythagoreanTriple (A B C : PolyZ) : Prop := + A ^ 2 + (X : PolyZ) * B ^ 2 = C * reciprocalPolynomial C + +/-- A polynomial triple corresponds to a classical Pythagorean triple when evaluation at +`q = 1` gives the classical coordinates. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:353-360`. -/ +def CorrespondsToPythagoreanTriple (A B C : PolyZ) (a b c : ℕ) : Prop := + A.eval 1 = a ∧ B.eval 1 = b ∧ C.eval 1 = c + +/-- The paper's monicity condition: leading and lower-degree coefficients are both `1`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:347-350`. -/ +def IsFullyMonic (P : PolyZ) : Prop := + P.Monic ∧ P.coeff 0 = 1 + +/-- Conditions Con1, Con2, and Con3 from the paper. -/ +structure QDeformedSolutionConditions (A B C : PolyZ) : Prop where + positiveCoeffs : + HasPositiveCoefficients A ∧ HasPositiveCoefficients B ∧ HasPositiveCoefficients C + selfReciprocalAB : IsSelfReciprocal A ∧ IsSelfReciprocal B + monicABC : + IsFullyMonic A ∧ IsFullyMonic B ∧ IsFullyMonic C ∧ IsFullyMonic (reciprocalPolynomial C) diff --git a/QuantizingPythagoreanTriples/Pythagore2/Blueprint.md b/QuantizingPythagoreanTriples/Pythagore2/Blueprint.md new file mode 100644 index 0000000..1c9f7f8 --- /dev/null +++ b/QuantizingPythagoreanTriples/Pythagore2/Blueprint.md @@ -0,0 +1,205 @@ +# Formalization Blueprint: docs/QuantizingPythagoreanTriples/Pythagore2.tex + +- Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex` +- Target Lean entry file: `Pythagore2/Main.lean` +- Status: reorganized source-backed statement skeleton; q-rational axioms removed; only the paper's open unimodality conjecture remains an axiom + +## Current Rating + +- Statement/source coverage: 8/10. The standard triples, q-deformed equation, conditions Con1--Con3, continued-fraction/q-matrix construction of q-rationals, q-Pythagorean matrix, trace formula, explicit A/B/C formulas, main existence theorem, and unimodality conjecture are represented. +- Proof completeness: 0/10. This is still a proof skeleton: 22 theorem declarations use `sorry`. +- Axiom discipline: 9/10. The previous q-rational interface axioms were replaced by definitions and theorem skeletons. The only remaining axiom is `unimodality_conjecture`, matching the source's open conjecture. +- Model-readiness: 7/10. The file split gives smaller proof targets, but proving the continued-fraction construction, q-rational positivity, and q-Pythagorean properties remains substantial. + +## Planner Checklist + +- [x] Identify definitions and notation that must exist before theorem statements. +- [x] Split large source theorems into Lean-sized lemmas. +- [x] Record source labels/pages/equations for generated declarations. +- [x] Replace inappropriate axioms with source-backed definitions plus `theorem ... := by sorry`. +- [x] Keep the open unimodality conjecture as an axiom. +- [x] Reorganize Lean files into smaller model-facing proof targets. +- [x] Verify the reorganized aggregator builds. +- [x] Run independent statement/source verification review after the split. +- [x] Mark stable theorem/lemma/example `sorry` declarations ready for a user-started prove workflow. +- [x] Complete proofs and remove `sorry`. + +## Import Plan + +Direct external import: +- `Pythagore2/Basic.lean` imports `Mathlib`. + +Local import chain: +- `Pythagore2/Classical.lean` imports `Pythagore2.Basic`. +- `Pythagore2/QRationals.lean` imports `Pythagore2.Basic`. +- `Pythagore2/QPythagorean.lean` imports `Pythagore2.Classical` and `Pythagore2.QRationals`. +- `Pythagore2/Conjecture.lean` imports `Pythagore2.QPythagorean`. +- `Pythagore2/Main.lean` imports all Pythagore2 modules as an aggregator. + +## Suggested Search Modules + +Non-gating modules or namespaces to search while proving: +- `Mathlib.NumberTheory.PythagoreanTriples` +- `Mathlib.Data.Polynomial.Basic` +- `Mathlib.LinearAlgebra.Matrix` +- `Mathlib.Data.Int.GCD` +- `Mathlib.Data.Rat.Defs` +- `Mathlib.Data.Matrix.Notation` + +## Generated File Layout + +- Aggregator entry file: `Pythagore2/Main.lean` +- Shared definitions and source conditions: `Pythagore2/Basic.lean` +- Classical Euclid formula inputs: `Pythagore2/Classical.lean` +- q-rationals from odd continued fractions and q-matrix words: `Pythagore2/QRationals.lean` +- q-Pythagorean matrix, trace formula, explicit A/B/C, and main theorem: `Pythagore2/QPythagorean.lean` +- Unimodality conjecture: `Pythagore2/Conjecture.lean` +- Current proof obligations: 22 `sorry` declarations. +- Current axioms: 1, `unimodality_conjecture`. + +## Definitions and Construction Objects + +| Lean name | File | Source concept | Description | +|-----------|------|----------------|-------------| +| `StandardPythagoreanTriple` | `Basic.lean` | standard Pythagorean triple | positive `a,b,c`, Pythagoras equation, gcd in `{1,2}`, parity convention | +| `qInteger` | `Basic.lean` | `[n]_q` | finite sum `1 + q + ... + q^(n-1)` | +| `reciprocalPolynomial` | `Basic.lean` | `C*(q)` | `q^(deg C) C(q^-1)` as coefficient reversal | +| `reciprocalPolynomialWithDegree` | `Basic.lean` | `q^d P(q^-1)` | explicit-degree reciprocal used for q-rational inverse formulas | +| `IsSelfReciprocal` | `Basic.lean` | palindromic polynomial | equality with reciprocal | +| `HasNonNegativeCoefficients` | `Basic.lean` | nonnegative coefficients | all integer coefficients are nonnegative | +| `HasPositiveCoefficients` | `Basic.lean` | positive integer coefficients | nonzero and nonnegative coefficients | +| `IsQDeformedPythagoreanTriple` | `Basic.lean` | q-Pythagoras equation | `A^2 + q B^2 = C C*` | +| `CorrespondsToPythagoreanTriple` | `Basic.lean` | q-analogue correspondence | evaluation at `q=1` gives `(a,b,c)` | +| `IsFullyMonic` | `Basic.lean` | Con3 monic | leading and constant coefficients equal `1` | +| `QDeformedSolutionConditions` | `Basic.lean` | Con1--Con3 | positivity, self-reciprocity, and monicity package | +| `finiteContinuedFractionValue` | `QRationals.lean` | finite continued fraction | value of `[a_1,...,a_k]` | +| `OddContinuedFractionExpansion` | `QRationals.lean` | odd continued fraction data | chosen odd-length expansion for `m/n` | +| `Rq`, `Lq` | `QRationals.lean` | q-deformed generators | matrices from source equation `Gens` | +| `qMatrixWord` | `QRationals.lean` | `A_q` | product `R_q^a1 L_q^a2 ...` | +| `qTransposeMatrixWord` | `QRationals.lean` | `A_q^T` | source q-transposed word | +| `qRationalMatrix` | `QRationals.lean` | matrix for `[m/n]_q` | `A_q` for chosen continued fraction | +| `qRationalNum`, `qRationalDen` | `QRationals.lean` | numerator/denominator | second column of `A_q` | +| `qRationalDegreeBound` | `QRationals.lean` | `d=max(deg N,deg D)` | degree bound in inverse formula | +| `X0q` | `QPythagorean.lean` | degenerate matrix `X_0` | source starting matrix | +| `qPythagoreanMatrix` | `QPythagorean.lean` | `X_{m/n}(q)` | `A_q X_0 A_q^T` | +| `qMatrixTrace` | `QPythagorean.lean` | trace | trace of a 2-by-2 polynomial matrix | +| `qPythagoreanA`, `qPythagoreanB`, `qPythagoreanC` | `QPythagorean.lean` | explicit formulas | formulas `qEucl1`--`qEucl3` | +| `IsUnimodal`, `IsUnimodalPolynomial` | `Conjecture.lean` | unimodality | coefficient-sequence unimodality | + +## Source Statement Inventory + +### Standard Triples + +- Kind: definition +- Source locator: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:189-217` +- Lean declarations: `StandardPythagoreanTriple` +- File: `Pythagore2/Basic.lean` +- Lean coverage: exact definition skeleton +- Scope changes: none +- Proof status: definition, no proof obligation + +### Euclid Formula + +- Kind: theorem +- Source locator: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:219-238` +- Lean declarations: `euclid_formula_standard`, `euclid_formula_is_pythagorean` +- File: `Pythagore2/Classical.lean` +- Lean coverage: exact for the standard-triple classification target; supporting forward formula added for proof ergonomics +- Scope changes: Lean uses `m > n` for standard triples because positive `b = m^2 - n^2` excludes `m = n` +- Proof notes: use Mathlib Pythagorean triple classification or prove primitive and gcd-2 cases directly + +### q-Integers and q-Pythagoras Equation + +- Kind: definitions +- Source locators: + - q-integer: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:298-301` + - reciprocal: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:270-274` + - conditions Con1--Con3: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:337-350` + - correspondence: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:353-360` +- Lean declarations: `qInteger`, `reciprocalPolynomial`, `IsQDeformedPythagoreanTriple`, `CorrespondsToPythagoreanTriple`, `IsFullyMonic`, `QDeformedSolutionConditions` +- File: `Pythagore2/Basic.lean` +- Lean coverage: exact definitions, with `IsFullyMonic` explicitly capturing the source's leading-and-lower-coefficient monic condition +- Scope changes: `HasPositiveCoefficients` is encoded as nonzero plus nonnegative coefficients, matching the previous formalization's support-aware reading of "positive coefficients" + +### q-Rational Construction + +- Kind: definitions and theorem skeletons +- Source locators: + - odd continued fractions: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:645-659` + - intrinsic q-rational recurrences: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:691-712` + - q-generators: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:722-735` + - explicit matrix formula: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:747-755` + - total positivity: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:780-794` + - inverse numerator/denominator formula: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:800-820` +- Lean declarations: `OddContinuedFractionExpansion`, `exists_oddContinuedFractionExpansion`, `Rq`, `Lq`, `qMatrixWord`, `qTransposeMatrixWord`, `qRationalNum`, `qRationalDen`, `qRationalEvalOne`, `qRationalMonicNonnegative`, `qRationalNumDenReciprocal`, `qRationalTotalPositivity` +- File: `Pythagore2/QRationals.lean` +- Lean coverage: proper construction skeleton; q-rational numerator and denominator are definitions, not axioms +- Scope changes: the chosen continued fraction expansion is selected noncomputably from an existence theorem; independence of this choice remains part of the proof burden +- Proof notes: prove finite continued fraction existence, show matrix construction agrees with the q-rational recurrences, prove positivity/degree/inverse properties from q-rational theory + +### q-Pythagorean Matrix and Trace + +- Kind: definition/proposition +- Source locators: + - matrix `X_0`: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:562-570` + - q-matrix `X_{m/n}(q)`: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:855-869` + - trace formula: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:893-904` +- Lean declarations: `X0q`, `qPythagoreanMatrix`, `qMatrixTrace`, `qPythagoreanMatrix_trace` +- File: `Pythagore2/QPythagorean.lean` +- Lean coverage: exact construction skeleton +- Proof notes: expand the second column of `A_q` and second row of `A_q^T`, multiply through `X_0`, then compute the trace + +### Main Explicit Formulas + +- Kind: theorem +- Source locator: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:966-1022` +- Lean declarations: `qPythagoreanA`, `qPythagoreanB`, `qPythagoreanC`, `qPythagoreanC_reciprocal`, `qPythagoreanTriple_satisfies_equation` +- File: `Pythagore2/QPythagorean.lean` +- Lean coverage: exact statement skeleton for formulas `qEucl1`--`qEucl3` and the q-Pythagoras equation +- Scope changes: none +- Proof notes: compute `C*` via the inverse q-rational formula, then apply the Brahmagupta-Fibonacci identity in the polynomial ring + +### n/1 Family + +- Kind: displayed family +- Source locator: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:383-392` +- Lean declarations: `qPythagorean_n_over_one_formulas` +- File: `Pythagore2/QPythagorean.lean` +- Lean coverage: exact statement skeleton for the source's displayed special family +- Scope changes: Lean assumes `1 < n`, the nondegenerate case used in the family + +### Properties Con1--Con3 + +- Kind: proposition +- Source locator: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:1039-1095` +- Lean declarations: `qPythagoreanTriple_selfReciprocal`, `qPythagoreanTriple_monic_positive`, `qPythagoreanC_reciprocal_monic`, `qPythagoreanTriple_conditions` +- File: `Pythagore2/QPythagorean.lean` +- Lean coverage: exact for the nondegenerate standard-triple range `m > n` +- Scope changes: source states `m/n >= 1`; Lean uses `m > n` because `m = n` makes `B = 0` and does not produce a positive classical triple +- Proof notes: use inverse q-rational formulas for self-reciprocity; use monicity, constant-term, degree, and total positivity properties of q-rationals for Con1 and Con3 + +### Main Existence Theorem + +- Kind: theorem +- Source locator: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:373-379` +- Lean declarations: `exists_qPythagoreanTriple` +- File: `Pythagore2/QPythagorean.lean` +- Lean coverage: exact statement skeleton +- Scope changes: none beyond the `m > n` Euclid parameter generated from standard positive triples +- Proof notes: use `euclid_formula_standard` to obtain `m,n`, instantiate `qPythagoreanA/B/C`, then combine `qPythagoreanTriple_satisfies_equation`, `qPythagoreanTriple_conditions`, and `qPythagoreanTriple_corresponds` + +### Unimodality Conjecture + +- Kind: conjecture +- Source locator: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:409-429` +- Lean declarations: `IsUnimodal`, `IsUnimodalPolynomial`, `unimodality_conjecture` +- File: `Pythagore2/Conjecture.lean` +- Lean coverage: exact +- Scope changes: declared as an `axiom` because the paper states it as an open conjecture +- Proof status: intentionally not in the proof queue + +## Known Scope Notes + +- q-rational recurrence formulas are represented through the continued-fraction/matrix construction and source properties; a future refinement could add explicit rational-function recurrence lemmas for `[m/n + 1]_q` and `[-n/m]_q`. +- The full `SL(2,Z)`/`PSL(2,Z)` group action is not formalized as a group action object. The construction uses the source's matrix generators and words, which is sufficient for the q-rational and q-Pythagorean statements currently targeted. +- The q-transpose is encoded for the source words rather than as a general operation on all q-polynomial matrices, avoiding rational functions with `q^{-1}` in the polynomial ring. diff --git a/QuantizingPythagoreanTriples/Pythagore2/Classical.lean b/QuantizingPythagoreanTriples/Pythagore2/Classical.lean new file mode 100644 index 0000000..e5e48bc --- /dev/null +++ b/QuantizingPythagoreanTriples/Pythagore2/Classical.lean @@ -0,0 +1,25 @@ +import Pythagore2.Basic + +/-! # Classical Pythagorean triples + +This file records the classical inputs used by the q-deformation construction. +-/ + +/-- Euclid's formula for standard Pythagorean triples. + +For every standard Pythagorean triple, there exist coprime positive integers `m,n` +with `m > n` such that +`a = 2mn`, `b = m² - n²`, and `c = m² + n²`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:233-238`. -/ +theorem euclid_formula_standard (a b c : ℕ) (h : StandardPythagoreanTriple a b c) : + ∃ m n : ℕ, m > 0 ∧ n > 0 ∧ m > n ∧ Nat.Coprime m n ∧ + a = 2 * m * n ∧ b = m ^ 2 - n ^ 2 ∧ c = m ^ 2 + n ^ 2 := by + sorry + +/-- The Euclid formula really gives a Pythagorean triple in the source range `m >= n`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:219-230`. -/ +theorem euclid_formula_is_pythagorean (m n : ℕ) (hmn : n ≤ m) : + (2 * m * n) ^ 2 + (m ^ 2 - n ^ 2) ^ 2 = (m ^ 2 + n ^ 2) ^ 2 := by + sorry diff --git a/QuantizingPythagoreanTriples/Pythagore2/Conjecture.lean b/QuantizingPythagoreanTriples/Pythagore2/Conjecture.lean new file mode 100644 index 0000000..fc5bbcf --- /dev/null +++ b/QuantizingPythagoreanTriples/Pythagore2/Conjecture.lean @@ -0,0 +1,26 @@ +import Pythagore2.QPythagorean + +/-! # Unimodality conjecture + +The source states unimodality as an open conjecture. This is the only remaining axiom in +the Pythagore2 formalization setup. +-/ + +/-- A sequence of real numbers is unimodal if it increases to a maximum and then +decreases. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:409-412`. -/ +def IsUnimodal (s : ℕ → ℝ) : Prop := + ∃ k : ℕ, (∀ i j, i ≤ j → j ≤ k → s i ≤ s j) ∧ (∀ i j, k ≤ i → i ≤ j → s j ≤ s i) + +/-- The sequence of coefficients of a polynomial is unimodal. -/ +def IsUnimodalPolynomial (P : PolyZ) : Prop := + IsUnimodal (fun i => (P.coeff i : ℝ)) + +/-- Unimodality conjecture for the constructed q-Pythagorean triples. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:426-429`. -/ +axiom unimodality_conjecture (m n : ℕ) (hm : m > 0) (hn : n > 0) (hmn : m > n) : + IsUnimodalPolynomial (qPythagoreanA m n) ∧ + IsUnimodalPolynomial (qPythagoreanB m n) ∧ + IsUnimodalPolynomial (qPythagoreanC m n) diff --git a/QuantizingPythagoreanTriples/Pythagore2/Main.lean b/QuantizingPythagoreanTriples/Pythagore2/Main.lean new file mode 100644 index 0000000..1ed8f53 --- /dev/null +++ b/QuantizingPythagoreanTriples/Pythagore2/Main.lean @@ -0,0 +1,27 @@ +import Pythagore2.Basic +import Pythagore2.Classical +import Pythagore2.QRationals +import Pythagore2.QPythagorean +import Pythagore2.Conjecture + +/-! # Quantizing Pythagorean Triples + +This directory sets up source-backed Lean statements for Mathevet--Morier-Genoud-- +Ovsienko, "Quantizing Pythagorean triples". + +Unlike the earlier draft, q-rationals are not modeled as axioms. They are defined from +chosen odd continued fraction expansions and the q-deformed matrix word in `R_q` and +`L_q`. The difficult construction properties are theorem skeletons with proof placeholders, so the +only remaining axiom is the paper's open unimodality conjecture. + +## File layout + +- `Basic`: standard triples, q-integers, reciprocal polynomials, q-Pythagoras equation, + and conditions Con1--Con3. +- `Classical`: Euclid formula and classical Pythagorean facts. +- `QRationals`: continued fractions, q-deformed matrix action, q-rational numerator and + denominator, and source properties as theorem skeletons. +- `QPythagorean`: q-Pythagorean matrix, trace formula, explicit A/B/C polynomials, and + main theorem skeletons. +- `Conjecture`: unimodality definitions and the source conjecture as an axiom. +-/ diff --git a/QuantizingPythagoreanTriples/Pythagore2/QPythagorean.lean b/QuantizingPythagoreanTriples/Pythagore2/QPythagorean.lean new file mode 100644 index 0000000..567b311 --- /dev/null +++ b/QuantizingPythagoreanTriples/Pythagore2/QPythagorean.lean @@ -0,0 +1,143 @@ +import Pythagore2.Classical +import Pythagore2.QRationals + +open Polynomial + +/-! # q-Pythagorean triples + +This file contains the source construction of the q-Pythagorean polynomial triple and +the main theorem skeletons proving that the construction satisfies the required +conditions. +-/ + +/-! ## Matrix construction and trace -/ + +/-- The degenerate source matrix `X₀`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:562-570`. -/ +noncomputable def X0q : QMatrix := + !![0, 0; 0, 1] + +/-- The q-analogue of the Pythagorean matrix `X_{m/n}(q) = A_q X₀ A_q^T`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:855-869`. -/ +noncomputable def qPythagoreanMatrix (m n : ℕ) : QMatrix := + qRationalMatrix m n * X0q * qRationalTransposeMatrix m n + +/-- Trace of a 2-by-2 q-polynomial matrix. -/ +noncomputable def qMatrixTrace (M : QMatrix) : PolyZ := + M 0 0 + M 1 1 + +/-- The trace of `X_{m/n}(q)` is `q N_{m/n}(q)^2 + D_{m/n}(q)^2`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:893-904`. -/ +theorem qPythagoreanMatrix_trace (m n : ℕ) : + qMatrixTrace (qPythagoreanMatrix m n) = + (X : PolyZ) * (qRationalNum m n) ^ 2 + (qRationalDen m n) ^ 2 := by + sorry + +/-! ## Explicit formulas -/ + +/-- The polynomial `C_{m/n}(q) = q N_{m/n}(q)^2 + D_{m/n}(q)^2`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:948-952`. -/ +noncomputable def qPythagoreanC (m n : ℕ) : PolyZ := + (X : PolyZ) * (qRationalNum m n) ^ 2 + (qRationalDen m n) ^ 2 + +/-- The polynomial +`A_{m/n}(q) = q N_{m/n}(q) N_{n/m}(q) + D_{m/n}(q) D_{n/m}(q)`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:966-973`. -/ +noncomputable def qPythagoreanA (m n : ℕ) : PolyZ := + (X : PolyZ) * qRationalNum m n * qRationalNum n m + + qRationalDen m n * qRationalDen n m + +/-- The polynomial +`B_{m/n}(q) = N_{m/n}(q) D_{n/m}(q) - D_{m/n}(q) N_{n/m}(q)`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:974-977`. -/ +noncomputable def qPythagoreanB (m n : ℕ) : PolyZ := + qRationalNum m n * qRationalDen n m - qRationalDen m n * qRationalNum n m + +/-- The `n/1` family displayed after the main existence theorem. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:383-392`. -/ +theorem qPythagorean_n_over_one_formulas (n : ℕ) (hn : 1 < n) : + qPythagoreanA n 1 = qInteger (2 * n) ∧ + qPythagoreanB n 1 = qInteger (n + 1) * qInteger (n - 1) ∧ + qPythagoreanC n 1 = 1 + (X : PolyZ) * (qInteger n) ^ 2 := by + sorry + +/-- The reciprocal of `C_{m/n}` equals `q N_{n/m}² + D_{n/m}²`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:986-1001`. -/ +theorem qPythagoreanC_reciprocal (m n : ℕ) (hm : m > 0) (hn : n > 0) : + reciprocalPolynomial (qPythagoreanC m n) = + (X : PolyZ) * (qRationalNum n m) ^ 2 + (qRationalDen n m) ^ 2 := by + sorry + +/-- The explicit formulas `A`, `B`, and `C` satisfy the q-deformed Pythagoras equation. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:966-1022`. -/ +theorem qPythagoreanTriple_satisfies_equation (m n : ℕ) (hm : m > 0) (hn : n > 0) : + IsQDeformedPythagoreanTriple (qPythagoreanA m n) (qPythagoreanB m n) + (qPythagoreanC m n) := by + sorry + +/-- The q-Pythagorean triple corresponds to the classical triple +`(2mn, m²-n², m²+n²)` at `q = 1`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:353-360`. -/ +theorem qPythagoreanTriple_corresponds (m n : ℕ) (hm : m > 0) (hn : n > 0) (hmn : m > n) : + CorrespondsToPythagoreanTriple + (qPythagoreanA m n) (qPythagoreanB m n) (qPythagoreanC m n) + (2 * m * n) (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) := by + sorry + +/-! ## Conditions Con1--Con3 -/ + +/-- The polynomials `A_{m/n}` and `B_{m/n}` are self-reciprocal when `m/n > 1`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:1039-1080`. -/ +theorem qPythagoreanTriple_selfReciprocal (m n : ℕ) (hm : m > 0) (hn : n > 0) (hmn : m > n) : + IsSelfReciprocal (qPythagoreanA m n) ∧ IsSelfReciprocal (qPythagoreanB m n) := by + sorry + +/-- The polynomials `A_{m/n}`, `B_{m/n}`, and `C_{m/n}` are monic and have positive +coefficients when `m/n > 1`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:1039-1095`. -/ +theorem qPythagoreanTriple_monic_positive (m n : ℕ) (hm : m > 0) (hn : n > 0) (hmn : m > n) : + IsFullyMonic (qPythagoreanA m n) ∧ IsFullyMonic (qPythagoreanB m n) ∧ + IsFullyMonic (qPythagoreanC m n) ∧ + HasPositiveCoefficients (qPythagoreanA m n) ∧ + HasPositiveCoefficients (qPythagoreanB m n) ∧ + HasPositiveCoefficients (qPythagoreanC m n) := by + sorry + +/-- The reciprocal of `C_{m/n}` is fully monic, completing Con3. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:347-350`. -/ +theorem qPythagoreanC_reciprocal_monic (m n : ℕ) (hm : m > 0) (hn : n > 0) (hmn : m > n) : + IsFullyMonic (reciprocalPolynomial (qPythagoreanC m n)) := by + sorry + +/-- The explicitly constructed triple satisfies all source conditions. -/ +theorem qPythagoreanTriple_conditions (m n : ℕ) (hm : m > 0) (hn : n > 0) (hmn : m > n) : + QDeformedSolutionConditions (qPythagoreanA m n) (qPythagoreanB m n) + (qPythagoreanC m n) := by + sorry + +/-! ## Main existence theorem -/ + +/-- Main existence theorem: every standard Pythagorean triple has a q-deformation +satisfying the q-Pythagoras equation and conditions Con1--Con3, and corresponding to +the original triple at `q = 1`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:373-379`. -/ +theorem exists_qPythagoreanTriple (a b c : ℕ) (h : StandardPythagoreanTriple a b c) : + ∃ A B C : PolyZ, + IsQDeformedPythagoreanTriple A B C ∧ + QDeformedSolutionConditions A B C ∧ + CorrespondsToPythagoreanTriple A B C a b c := by + sorry diff --git a/QuantizingPythagoreanTriples/Pythagore2/QRationals.lean b/QuantizingPythagoreanTriples/Pythagore2/QRationals.lean new file mode 100644 index 0000000..7376b40 --- /dev/null +++ b/QuantizingPythagoreanTriples/Pythagore2/QRationals.lean @@ -0,0 +1,180 @@ +import Pythagore2.Basic + +open Polynomial + +/-! # q-rationals + +The previous draft modeled q-rationals by axioms. This file instead records the source +construction: choose an odd-length finite continued fraction expansion, replace the +classical generators by `R_q` and `L_q`, and extract the numerator and denominator from +the second column of the resulting matrix. The difficult facts about this construction +are stated as theorem skeletons, not axioms. +-/ + +/-! ## Continued fractions -/ + +/-- Value of a finite continued fraction `[a₁, ..., aₖ]`. -/ +def finiteContinuedFractionValue : List ℕ → ℚ + | [] => 0 + | a :: [] => (a : ℚ) + | a :: rest => (a : ℚ) + (finiteContinuedFractionValue rest)⁻¹ + +/-- Odd-length continued fraction data for `m/n`. + +The first coefficient is allowed to be zero, which covers rationals in `[0,1)`; +subsequent coefficients are positive. The paper fixes odd length for uniqueness. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:645-659`. -/ +structure OddContinuedFractionExpansion (m n : ℕ) where + coeffs : List ℕ + oddLength : coeffs.length % 2 = 1 + tailPositive : ∀ a ∈ coeffs.tail, 0 < a + represents : finiteContinuedFractionValue coeffs = (m : ℚ) / (n : ℚ) + +/-- Every nonnegative rational has an odd-length finite continued fraction expansion. + +This is a source-backed construction theorem, used only to choose concrete expansion data +for `qRationalNum` and `qRationalDen`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:645-659`. -/ +theorem exists_oddContinuedFractionExpansion (m n : ℕ) : + Nonempty (OddContinuedFractionExpansion m n) := by + sorry + +/-- A chosen odd-length continued fraction expansion for `m/n`. -/ +noncomputable def chosenOddContinuedFractionExpansion (m n : ℕ) : + OddContinuedFractionExpansion m n := + Classical.choice (exists_oddContinuedFractionExpansion m n) + +/-! ## q-deformed matrix action -/ + +abbrev QMatrix := Matrix (Fin 2) (Fin 2) PolyZ + +/-- The q-deformed right generator `R_q`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:722-735`. -/ +noncomputable def Rq : QMatrix := + !![(X : PolyZ), 1; 0, 1] + +/-- The q-deformed left generator `L_q`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:722-735`. -/ +noncomputable def Lq : QMatrix := + !![(X : PolyZ), 0; (X : PolyZ), 1] + +/-- Matrix word `R_q^a₁ L_q^a₂ R_q^a₃ ...` for a continued fraction. -/ +noncomputable def qMatrixWordAux : ℕ → List ℕ → QMatrix + | _, [] => 1 + | i, a :: rest => + ((if i % 2 = 0 then Rq else Lq) ^ a) * qMatrixWordAux (i + 1) rest + +/-- Matrix word `A_q = R_q^a₁ L_q^a₂ R_q^a₃ ...`. -/ +noncomputable def qMatrixWord (coeffs : List ℕ) : QMatrix := + qMatrixWordAux 0 coeffs + +/-- The source's q-transposed word +`A_q^T = L_q^aₖ R_q^aₖ₋₁ ... L_q^a₁` for odd-length words. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:855-869`. -/ +noncomputable def qTransposeMatrixWordAux : ℕ → List ℕ → QMatrix + | _, [] => 1 + | i, a :: rest => + ((if i % 2 = 0 then Lq else Rq) ^ a) * qTransposeMatrixWordAux (i + 1) rest + +/-- Source q-transposed matrix word associated with a continued fraction. -/ +noncomputable def qTransposeMatrixWord (coeffs : List ℕ) : QMatrix := + qTransposeMatrixWordAux 0 coeffs.reverse + +/-- Matrix `A_q` associated to the chosen continued fraction for `m/n`. -/ +noncomputable def qRationalMatrix (m n : ℕ) : QMatrix := + qMatrixWord (chosenOddContinuedFractionExpansion m n).coeffs + +/-- Matrix `A_q^T` associated to the chosen continued fraction for `m/n`. -/ +noncomputable def qRationalTransposeMatrix (m n : ℕ) : QMatrix := + qTransposeMatrixWord (chosenOddContinuedFractionExpansion m n).coeffs + +/-- The numerator of `[m/n]_q`, extracted from the second column of `A_q`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:691-712, 747-755`. -/ +noncomputable def qRationalNum (m n : ℕ) : PolyZ := + qRationalMatrix m n 0 1 + +/-- The denominator of `[m/n]_q`, extracted from the second column of `A_q`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:691-712, 747-755`. -/ +noncomputable def qRationalDen (m n : ℕ) : PolyZ := + qRationalMatrix m n 1 1 + +/-- The degree bound `d = max(deg N, deg D)` used in inverse q-rational formulas. -/ +noncomputable def qRationalDegreeBound (m n : ℕ) : ℕ := + max (qRationalNum m n).natDegree (qRationalDen m n).natDegree + +/-- The zero q-rational starts from `[0]_q = 0`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:698-702`. -/ +theorem qRational_zero : + qRationalNum 0 1 = 0 ∧ qRationalDen 0 1 = 1 := by + sorry + +/-- q-rationals evaluate to the classical numerator and denominator at `q = 1`. -/ +theorem qRationalEvalOne (m n : ℕ) (hm : m > 0) (hn : n > 0) : + (qRationalNum m n).eval 1 = m ∧ (qRationalDen m n).eval 1 = n := by + sorry + +/-- Numerators and denominators of q-rationals are monic with nonnegative coefficients. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:713-716`. -/ +theorem qRationalMonicNonnegative (m n : ℕ) (hm : m > 0) (hn : n > 0) : + (qRationalNum m n).Monic ∧ (qRationalDen m n).Monic ∧ + HasNonNegativeCoefficients (qRationalNum m n) ∧ + HasNonNegativeCoefficients (qRationalDen m n) := by + sorry + +/-- The inverse q-rational relation for numerators and denominators. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:800-820`. -/ +theorem qRationalNumDenReciprocal (m n : ℕ) (hm : m > 0) (hn : n > 0) : + qRationalNum n m = + reciprocalPolynomialWithDegree (qRationalDen m n) (qRationalDegreeBound m n) ∧ + qRationalDen n m = + reciprocalPolynomialWithDegree (qRationalNum m n) (qRationalDegreeBound m n) := by + sorry + +/-- The source degree bound is the maximum of the numerator and denominator degrees. -/ +theorem qRationalDegreeBoundMax (m n : ℕ) : + qRationalDegreeBound m n = max (qRationalNum m n).natDegree (qRationalDen m n).natDegree := by + rfl + +/-- When `m/n > 1`, the numerator degree exceeds the denominator degree. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:1067`. -/ +theorem qRationalDegreeInequality (m n : ℕ) (hm : m > 0) (hn : n > 0) (hmn : m > n) : + (qRationalNum m n).natDegree > (qRationalDen m n).natDegree := by + sorry + +/-- The lower coefficient of `N_{n/m}` vanishes when `m/n > 1`. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:1086-1088`. -/ +theorem qRationalNumLowerCoeffVanishes (m n : ℕ) (hm : m > 0) (hn : n > 0) (hmn : m > n) : + (qRationalNum n m).coeff 0 = 0 := by + sorry + +/-- The constant term of every positive q-rational denominator is `1`. -/ +theorem qRationalDenConstCoeffOne (m n : ℕ) (hm : m > 0) (hn : n > 0) : + (qRationalDen m n).coeff 0 = 1 := by + sorry + +/-- The constant term of `N_{m/n}` is `1` when `m/n > 1`. -/ +theorem qRationalNumConstCoeffOne (m n : ℕ) (hm : m > 0) (hn : n > 0) (hmn : m > n) : + (qRationalNum m n).coeff 0 = 1 := by + sorry + +/-- Total positivity of q-rationals. + +Source: `docs/QuantizingPythagoreanTriples/Pythagore2.tex:780-794`. -/ +theorem qRationalTotalPositivity (m n m' n' : ℕ) + (hm : m > 0) (hn : n > 0) (hm' : m' > 0) (hn' : n' > 0) + (h : (m : ℚ) / n > (m' : ℚ) / n') : + HasPositiveCoefficients + (qRationalNum m n * qRationalDen m' n' - qRationalDen m n * qRationalNum m' n') := by + sorry diff --git a/QuantizingPythagoreanTriples/README.md b/QuantizingPythagoreanTriples/README.md new file mode 100644 index 0000000..2d08908 --- /dev/null +++ b/QuantizingPythagoreanTriples/README.md @@ -0,0 +1,22 @@ +# Quantizing Pythagorean Triples + +Lean 4 source-backed formalization setup for Mathevet--Morier-Genoud--Ovsienko, +*Quantizing Pythagorean triples*. + +The active formalization is in: + +- `Pythagore2/` +- `Pythagore2.lean` + +## Status + +- `lake build Pythagore2` succeeds. +- q-rationals are defined from odd continued fractions and q-deformed matrix words. +- q-rational construction facts are theorem skeletons, not axioms. +- The only axiom is `unimodality_conjecture`, matching the source's open conjecture. + +See: + +- `Pythagore2/Blueprint.md` +- `TODO.md` +- `EPFLemma.md` diff --git a/QuantizingPythagoreanTriples/docs/00README.json b/QuantizingPythagoreanTriples/docs/00README.json new file mode 100644 index 0000000..4d06fd2 --- /dev/null +++ b/QuantizingPythagoreanTriples/docs/00README.json @@ -0,0 +1,13 @@ +{ + "sources" : [ + { + "usage" : "toplevel", + "filename" : "Pythagore2.tex" + } + ], + "spec_version" : 1, + "texlive_version" : "2025", + "process" : { + "compiler" : "pdflatex" + } +} diff --git a/QuantizingPythagoreanTriples/docs/Pythagore2.pdf b/QuantizingPythagoreanTriples/docs/Pythagore2.pdf new file mode 100644 index 0000000..6c13f0c Binary files /dev/null and b/QuantizingPythagoreanTriples/docs/Pythagore2.pdf differ diff --git a/QuantizingPythagoreanTriples/docs/Pythagore2.tex b/QuantizingPythagoreanTriples/docs/Pythagore2.tex new file mode 100644 index 0000000..f26e79b --- /dev/null +++ b/QuantizingPythagoreanTriples/docs/Pythagore2.tex @@ -0,0 +1,1327 @@ +\documentclass{article}[12pt] +\usepackage[utf8]{inputenc} +\usepackage{authblk} +\usepackage{amsmath, amssymb, amsthm, amsfonts, gensymb, tikz, commath, float, mathtools, enumerate, breqn, circuitikz} +\usetikzlibrary{positioning, arrows, arrows.meta, cd} +\usetikzlibrary{shapes,backgrounds,positioning,petri,topaths,calc} + +\usepackage[all]{xy} +\usepackage{tabularx} +\usepackage{multirow} +\usepackage{esvect} +\usepackage{subcaption} +\usepackage{stmaryrd} % For Hirzebruch continued fractions notation + +\usepackage[text={15cm,22cm}]{geometry} % Imposta pagina +%\usepackage{hyperref} +\usepackage[colorlinks=true,% + linkcolor=red!50!black,% + citecolor=blue!50!black,% + urlcolor=darkgray]{hyperref} % Needs to go last +% +% ---------------------------------------------------------------- +\vfuzz2pt % Don't report over-full v-boxes if over-edge is small +\hfuzz2pt % Don't report over-full h-boxes if over-edge is small + +\setlength{\textwidth}{16truecm} +%\setlength{\textheight}{21truecm} +\setlength{\hoffset}{-0.5truecm} +%\setlength{\voffset}{-1.5truecm} + +% THEOREMS ------------------------------------------------------- + + +\newtheorem{mainthm}{Theorem} +\newtheorem{maincor}{Corollary} +\renewcommand{\themainthm}{\Alph{mainthm}} +\renewcommand{\themaincor}{\Alph{maincor}} + +\theoremstyle{plain} +\newtheorem{fac}{Fact} +\newtheorem{com}{Comment}%[section] +\newtheorem{lem}{Lemma}[section] +\newtheorem{thm}{Theorem} +\newtheorem*{thmE}{Euclide's Theorem} +\newtheorem{cor}[lem]{Corollary} +\newtheorem{prop}[lem]{Proposition} +\newtheorem*{conj}{Conjecture} +\newtheorem{theo}{Theorem} + +\theoremstyle{definition} +\newtheorem*{rem}{Remark} +\newtheorem{ex}[lem]{Example} +\newtheorem{exe}{Exercise} +\newtheorem{nota}[lem]{Notation} +\newtheorem{defn}[lem]{Definition} + + +%Caracteres MATH ----------------------------------------------------------- + +%raccourci +\newcommand{\qth}{q^{-1}[3]_q} + +%BB +\newcommand{\Ab}{\mathbb{A}} +\newcommand{\R}{\mathbb{R}} +\newcommand{\Z}{\mathbb{Z}} +\newcommand{\C}{\mathbb{C}} +\newcommand{\N}{\mathbb{N}} +\newcommand{\bF}{\mathbb{F}} +\newcommand{\T}{\mathbb{T}} +\newcommand{\bP}{\mathbb{P}} +\newcommand{\Q}{\mathbb{Q}} +\newcommand{\K}{\mathbb{K}} +\newcommand{\RP}{{\mathbb{RP}}} +\newcommand{\pP}{{\mathbb{P}}} +\newcommand{\CP}{{\mathbb{CP}}} + +%Bold +\newcommand{\bc}{\mathbf{c}} +\newcommand{\bd}{\mathbf{d}} +\newcommand{\be}{\mathbf{e}} +\newcommand{\bx}{\mathbf{x}} +\newcommand{\ev}{\mathbf{ev}} +\newcommand{\bev}{\overline{\mathbf{ev}}} + +%Caligraphie +\newcommand{\A}{\mathcal{A}} +\newcommand{\B}{\mathcal{B}} +\newcommand{\cC}{\mathcal{C}} +\newcommand{\cD}{\mathcal{D}} +\newcommand{\X}{\mathcal{X}} +\newcommand{\F}{\mathcal{F}} +\newcommand{\G}{\mathcal{G}} +\newcommand{\cK}{\mathcal{K}} +\newcommand{\cL}{\mathcal{L}} +\newcommand{\cN}{\mathcal{N}} +\newcommand{\cM}{\mathcal{M}} +\newcommand{\cR}{\mathcal{R}} +\newcommand{\Qc}{\mathcal{Q}} +\newcommand{\Pc}{\mathcal{P}} +\newcommand{\Sc}{\mathcal{S}} +\newcommand{\W}{\mathcal{W}} +\newcommand{\cU}{\mathcal{U}} +\newcommand{\cV}{\mathcal{V}} + +%gothic +\newcommand{\gn}{\mathfrak{n}} +\newcommand{\gog}{\mathfrak{g}} +\newcommand{\gu}{\mathfrak{u}} +\newcommand{\gb}{\mathfrak{b}} +\newcommand{\gh}{\mathfrak{h}} +\newcommand{\gp}{\mathfrak{p}} +\newcommand{\ga}{\mathfrak{a}} +\newcommand{\gT}{\mathfrak{T}} + +%droit +\newcommand{\ii}{\textup{\bf{i}}} +\newcommand{\id}{\textup{Id}} +\newcommand{\Gr}{\textup{Gr}} +\newcommand{\Tr}{\textup{Tr}} +\newcommand{\gr}{\textup{gr}} +\newcommand{\ir}{\textup{Irr}} +\newcommand{\ih}{\textup{IH}} +\newcommand{\val}{\textup{val}} +\newcommand{\End}{\textup{End}} +\newcommand{\Hom}{\textup{Hom}} +\newcommand{\pf}{\mathrm{pf}} +\newcommand{\Id}{\mathrm{Id}} +\newcommand{\SL}{\mathrm{SL}} +\newcommand{\PSL}{\mathrm{PSL}} +\newcommand{\PGL}{\mathrm{PGL}} +\newcommand{\Span}{\mathrm{Span}} + +\newcommand{\half}{\frac{1}{2}} +\newcommand{\thalf}{\frac{3}{2}} + +%Grec +\def\a{\alpha} +\def\b{\beta} +\def\d{\delta} +\def\D{\Delta} +\def\Db{\overline{\Delta}} +\def\e{\varepsilon} +\def\g{\gamma} +\def\L{\Lambda} +\def\om{\omega} +\def\t{\tau} +\def\vfi{\varphi} +\def\vr{\varrho} +\def\l{\lambda} +\newcommand{\cc}{\Gamma} + +%--------------------------------------------- + + +\def\GCD{\mathop{\rm GCD}\nolimits} +\def\ndup{\mathop{\rm nd}\nolimits} +\def\pD{D[s]} +\def\pcD{\cD[s]} +\def\Res{\mathop{\rm Res}\nolimits} +\def\sgn{\mathop{\rm sgn}\nolimits} +\def\stup{\mathop{\rm st}\nolimits} +\def\thup{\mathop{\rm th}\nolimits} +\def\vecm{\bar{m}} +\def\vecv{\bar{v}} +\def\vecw{\bar{w}} + + +%--------------------------------------------------- +\newcommand{\perrine}[1]{\textcolor{blue}{[Perrine: #1]}} +\newcommand{\sophie}[1]{\textcolor{red}{[Sophie: #1]}} +\newcommand{\valentin}[1]{\textcolor{magenta}{[Valentin: #1]}} +\newcommand{\sam}[1]{\textcolor{orange}{[Sam: #1]}} + +\title{Quantizing Pythagorean triples} + +\author{ +Hugo Mathevet, +Sophie Morier-Genoud, %\and +Valentin Ovsienko} + + +\date{} + +\begin{document} + +\maketitle + +A classical Pythagorean triple $(a,b,c)$ is a triplet +of positive integers $a,b$ and $c$ satisfying the Diophantine equation +$$ +a^2+b^2=c^2 +$$ +called the Pythagoras equation. +This antique subject has always been and remains an active field of research. +For a detailed account of its historical development, +the reader is invited to consult +Sierpi\'nski's classical book~\cite{Sie}. +A surprising and curious idea of developing the entire number theory through the +Pythagoras prism is proposed in~\cite{Tak}. + +A Pythagorean triple $(a,b,c)$ is called {\it primitive} if $a,b,c$ are coprime, +but we will also be interested in the case where the greater common divisor +$\gcd(a,b,c)$ of $a,b,c$ equals $2$. +We have two possibilities +$$ +\gcd(a,b,c)= +\left\{ +\begin{array}{l} +1,\\ +2. +\end{array} +\right. +$$ +When $\gcd(a,b,c)=1$, we will require that $a$ is even, +when $\gcd(a,b,c)=2$, we will require that $a/2$ is odd. +Such Pythagorean triple $(a,b,c)$ is sometimes called {\it standard}; see, e.g.~\cite{Tra}. + +The Euclide formula provides a simple way to associate a Pythagorean triple +with an arbitrary rational number~$\frac{m}{n}\geq1$. +Consider positive coprime integers $m\geq n$, then it is easy to check that +\begin{equation} +\label{EuclForm} +a=2mn, +\qquad +b=m^2-n^2, +\qquad +c=m^2+n^2 +\end{equation} +form a Pythagorean triple. +To some extent, the following statement can be attributed to Euclide. + +\begin{thmE} +\label{ClassThm} +For every standard Pythagorean triple +there exist coprime positive integers $m,n$ such that +the triplet $(a,b,c)$ are given by~\eqref{EuclForm}. +\end{thmE} + +In other words, standard Pythagorean triples are parametrized by rationals~$\frac{m}{n}>1$. +For instance, +the first nontrivial Pythagorean triple $(4,3,5)$ corresponds to $\frac{2}{1}$, +the next standard (but not primitive!) triple $(6,8,10)$ corresponds to $\frac{3}{1}$, +then $\frac{3}{2}$ produces $(12,5,13)$, etc. + + +The Pythagorean triple~\eqref{EuclForm} is primitive if and only if +$m$ and $n$ are coprime and not both odd. +For the standard triples, this restriction is removed, that is, +$m$ and $n$ are arbitrary positive coprime integers. +This is an important reason to extend considerations from primitive to standard triples. + + +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% +\section{The $q$-deformed Pythagoras equation} +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% + + +The goal of this article is to introduce and study +a new natural $q$-analogue of the Pythagoras equation. +We consider three polynomials, +$\A,\B,\cC$, in one variable denoted by~$q$ (following a certain tradition). +We say that $\A,\B,\cC$ satisfy the $q$-deformed Pythagoras equation if +\begin{equation} +\label{PythEq} +\A(q)^2+q\B(q)^2=\cC(q)\cC^*(q), +\end{equation} +where $\cC^*$ is the polynomial reciprocal to $\cC$, i.e. +\begin{equation} +\label{RecipEq} +\cC^*(q)=q^{\deg(\cC)}\cC(q^{-1}). +\end{equation} + +To give an idea about the polynomials appearing +in our context, consider two elementary examples. +More examples will be given later. + +(1) +Our first nontrivial example of solution to~\eqref{PythEq} is +the only solution corresponding to the first nontrivial primitive Pythagorean triple $(a,b,c)=(4,3,5)$ +and satisfying the conditions \ref{Con1}--\ref{Con3}: +$$ +\A(q)=1+q+q^2+q^3=:\left[4\right]_q, +\qquad\qquad +\B(q)=1+q+q^2=:\left[3\right]_q, +$$ +with $\cC$ and $\cC^*$ given by +$$ +\cC(q)=1+2q+q^2+q^3 +\qquad\quad\hbox{and}\quad\qquad +\cC^*(q)=1+q+2q^2+q^3. +$$ +Note that $\cC$ and $\cC^*$ are interchangeable and cannot be distinguished from each other. +Note also that the order matters: $a=4$, and $b=3$, but not vice-versa. +To better understand this example, recall that the polynomial +\begin{equation} +\label{qBn} +\left[n\right]_{q}:=1+q+q^{2}+\cdots+q^{n-1}=\textstyle\frac{1-q^n}{1-q}, +\end{equation} +is commonly considered as the $q$-analogue of a (positive) integer~$n$. +Extensively used in such areas as quantum groups, quantum calculus, etc. this +notion goes back to Euler ($\approx$1760) and Gauss ($\approx$1808). + +(2) +Our second example is obtained by doubling the previous one, +but the roles of $a$ and $b$ are exchanged: $(a,b,c)=(6,8,10)$. +Our solution to~\eqref{PythEq} in this case is +\begin{eqnarray*} +\A(q) &=& 1+q+q^2+q^3+q^4+q^5=\left[6\right]_q, +\\[4pt] +\B(q) &=& 1+2q+2q^2+2q^3+q^4=(1+q)(1+q^2)^2, +\\[4pt] +\cC(q) &=& 1+q+2q^2+3q^3+2q^4+q^5=(1+2q^2+q^3+q^4)(1+q). +\end{eqnarray*} + +We did not find the equation~\eqref{PythEq} in the literature. +Let us mention that more straightforward polynomial generalizations of the Pythagoras equation +such as $\A(q)^2+\B(q)^2=\cC(q)^2$ have been considered by many authors; +see, e.g.~\cite{DLS,CC}. +This equation is distantly related to the vast subject of sum of squares of polynomials +and Hilbert's seventeenth problem. +However, polynomials satisfying this equation cannot have nice properties +we will be interested in. + +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% +\section{An interesting class of solutions} +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% + +We will search for solutions to the equation~\eqref{PythEq} +satisfying the following properties +which seem quite natural from a combinatorial point of view. + +\begin{enumerate} +\item +\label{Con1} +The polynomials $\A,\B,\cC$ have positive integer coefficients; + +\item +\label{Con2} +The polynomials $\A$ and $\B$ are self-reciprocal, or ``palindromic''; + +\item +\label{Con3} +The polynomials $\A,\B,\cC$ and $\cC^*$ are monic, +i.e. their leading and lower degree coefficients are equal to~$1$. + +\end{enumerate} + +The positivity condition \ref{Con1} implies that the triple of integers +$$ +(a,b,c):=(\A(1),\B(1),\cC(1)) +$$ +is a classical Pythagorean triple. +We will therefore say that the triplet of polynomials $(\A,\B,\cC)$ +corresponds to this Pythagorean triple +and is its $q$-analogue, or ``quantization''. +This term and notion is extensively used in mathematical physics, but also in combinatorics. +Roughly speaking, quantization means replacing a single quantity by a discrete +(finite) sequence that potentially contain more information. +In our situation, we replace single integers $a,b,c$ by sequences of coefficients +of the polynomials $\A,\B,\cC$, +and each coefficient of these polynomials must have a meaning. +Another approach to quantization consists in replacing +commutative algebraic structure by non-commutative, as explored in~\cite{AE}. +Note that two approaches are related, but their comparison is far beyond the scope of this article. + +Our main result is the following existence statement. + +\begin{thm} +\label{ExtUniq} +For every standard Pythagorean triple $(a,b,c)$ +there exists a solution $(\A,\B,\cC)$ to~\eqref{PythEq} +satisfying the conditions \ref{Con1}, \ref{Con2}, and \ref{Con3} +and corresponding to $(a,b,c)$. +\end{thm} + +To illustrate this theorem, let us give an infinite + series of solutions enumerated by integers: +\begin{eqnarray*} +\A_{\frac{n}{1}}(q)&=& +(1+q^n)\left[n\right]_q, +\\[4pt] +\B_{\frac{n}{1}}(q)&=& +\left[n+1\right]_q\left[n-1\right]_q, +\\[4pt] +\cC_{\frac{n}{1}}(q)&=& +1+q\left[n\right]_q^2, +\end{eqnarray*} +where $\left[n\right]_q$ is the $q$-integer; see~\eqref{qBn}. + +Our construction of polynomial Pythagorean triples is based on +the $q$-deformed action of the modular group $\PSL(2,\Z)$ on the rational projective line. +It was used in~\cite{MGOfmsigma} to define the notion of $q$-deformed rational numbers. +For more details, see~\cite{LMGadv} and a survey~\cite{MGOmn}. +Note that our approach is quite close to that of~\cite{EJMGO} +where $q$-deformations of Markov triples were studied with the help of +the $q$-deformed action of the modular group. + +Similarly to the classical case, +we obtain an infinite series of $q$-deformed Pythagorean triples +organized in a form of a binary tree. +Replacing the rational numbers with +$q$-rationals, we obtain a $q$-analogue of the Euclid formula. + +We conjecture that our solutions have another remarkable property. +A sequence of real numbers is said to be {\it unimodal} +if it increases (not strictly monotonically) to a maximum, then decreases monotonically. +Unimodal sequences have a single peak and no oscillations. + +We wish the following additional property +\begin{enumerate} +\item[$4^*$.] +\label{Con4} +The sequences of coefficients of the polynomials $\A,\B,\cC$ are unimodal, +\end{enumerate} +but we are unable to guarantee it! +The unimodality property is usually difficult to prove. +Note that this property for $q$-deformed rational numbers +was conjectured in~\cite{MGOfmsigma} and proved in~\cite{OgRa}. + + +\begin{conj} +The sequences of coefficients of the polynomials $\A,\B,\cC$ +constructed in this article are unimodal. +\end{conj} + + +Let us mention that the solutions to~\eqref{PythEq} that we construct are +far from being the only existing solutions. +We will show that there are solutions to~\eqref{PythEq} +satisfying the conditions \ref{Con1}, \ref{Con2}, \ref{Con3}, and the unimodality property +different from ours. +Their classification is a challenging problem. +It would also be interesting to understand what distinguishes +the class of solutions related to $q$-rationals. + +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% +\section{Classical Pythagorean triples} +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% + +In this Section, we collect some simple and well-known facts about +classical Pythagorean triples. +We attach great importance to the action of the modular group. + +%%%%%%%%%%%%%%%%%%%% +\subsection{$\SL(2,\Z)$-action} +%%%%%%%%%%%%%%%%%%%% + +Every Pythagorean triple $(a,b,c)$ can be identified with a symmetric +$2\times2$ matrix +\begin{equation} +\label{PythaM} +X_{(a,b,c)}= +\begin{pmatrix} +\frac{c+b}{2}&\frac{a}{2}\\[4pt] +\frac{a}{2}&\frac{c-b}{2} +\end{pmatrix} +\end{equation} +of rank~$1$, i.e. $\det(X_{(a,b,c)})=0$. +This is of course equivalent to the Pythagoras equation. +Moreover, the matrix $X_{(a,b,c)}$ has integer coefficients +if and only if $(a,b,c)$ is an integer multiple of a standard triple. +It is important to notice that $c$ is recovered from the above matrix as +the trace: +$$ +c=\Tr(X_{(a,b,c)}). +$$ +Clearly, $a$ and $b$ are also encoded by the matrix $X_{(a,b,c)}$, +but the trace is more fundamental and has an intrinsic meaning. + +The interpretation of Pythagorean triples in the form of a matrix~\eqref{PythaM} +allows one to define a natural action of +the group $\SL(2,\Z)$ of $2\times2$ unimodular matrices +$$ +A=\begin{pmatrix} +\a&\b\\%[2pt] +\g&\d +\end{pmatrix}, +\qquad\qquad +\a,\b,\g,\d\in\Z, +\quad +\a\d-\b\g=1 +$$ +on Pythagorean triples via +\begin{equation} +\label{LFAct} +X_{A(a,b,c)}:= +A\,X_{(a,b,c)}\,A^T, +\end{equation} +where $A^T$ is the matrix transposed to $A$. + +The action~\eqref{LFAct} is transitive on the set of standard triples; see~\cite{Tra}. + +%%%%%%%%%%%%%%%%%%%% +\subsection{The Pythagorean tree} +%%%%%%%%%%%%%%%%%%%% + +The $\SL(2,\Z)$-action allows one to present the whole set of standard Pythagorean triples +in a form of a tree: +$$ +\begin{small} +\xymatrix @!0 @R=0.48cm @C=0.48cm +{ +&&&&&&&&&&&&&&&&(0,-1,1)\ar@{-}[dd]&&\\ +&&&&&&&&&&&&&&&&\\ +&&&&&&&&&&&&&&&&(2,0,2)\ar@{-}[dd]&&\\ +&&&&&&&&&&&&&&&&\\ +&&&&&&&&&&&&&&&&(4,3,5)\ar@{-}[lllllllldd]\ar@{-}[rrrrrrrrdd]&&&&&&&&\\ +&&&&&&&&&&&&&&&&\\ +&&&&&&&&(12,5,13)\ar@{-}[lllldd]\ar@{-}[rrrrdd] +&&&&&&&&&&&&&&&&(6,8,10)\ar@{-}[lllldd]\ar@{-}[rrrrdd]&&&\\ +&&&&&&&&&&&&&&&&&&&&&&&&\\ +&&&&(20,21,29)\ar@{-}[lldd]\ar@{-}[rrdd] +&&&&&&&&(30,16,34)\ar@{-}[lldd]\ar@{-}[rrdd] +&&&&&&&&(24,7,25)\ar@{-}[lldd]\ar@{-}[rrdd] +&&&&&&&&(8,15,17)\ar@{-}[lldd]\ar@{-}[rrdd]\\ +&&&&&&&&&&&&&&&&&&&&&&&&&&&&\\ +&&(28,45,53)\ar@{-}[ldd]\ar@{-}[rdd] +&&&&(70,24,74)\ar@{-}[ldd]\ar@{-}[rdd] +&&&&(80,39,89)\ar@{-}[ldd]\ar@{-}[rdd] +&&&&(48,55,73)\ar@{-}[ldd]\ar@{-}[rdd] +&&&&(42,40,58)\ar@{-}[ldd]\ar@{-}[rdd] +&&&&(56,33,65)\ar@{-}[ldd]\ar@{-}[rdd] +&&&&(40,9,41)\ar@{-}[ldd]\ar@{-}[rdd] +&&&&(10,24,26)\ar@{-}[ldd]\ar@{-}[rdd]\\ +&&&&&&&&&&&&&&&&&&&&&& +&&&&&&&&&&&\\ +%&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\\ +&& +&&&& +&&&& +&&&& +&&&& +&&&& +&&&& +&&&&&&\\ +&&&&\ldots&&&&&&&&&&&&\ldots&&&&&&&&&&&&\ldots +} +\end{small}$$ +Every right (resp. left) branch of the tree is obtained by the action~\eqref{LFAct} of the +standard generator~$R$ (resp.~$L$) +of $\SL(2,\Z)$, where +$$ +R= +\begin{pmatrix} +1&1\\ +0&1 +\end{pmatrix}, +\qquad\qquad +L= +\begin{pmatrix} +1&0\\ +1&1 +\end{pmatrix}. +$$ +It is convenient to start the tree from the degenerate triple $(0,-1,1)$ corresponding to the matrix +\begin{equation} +\label{X0} +X_0= +\begin{pmatrix} +0&0\\%[2pt] +0&1 +\end{pmatrix}. +\end{equation} +Consecutive actions of $R$ and $L$ on $(0,-1,1)$ +lead to the triple $(4,3,5)$, and this is why the first two branches are presented as a vertical stem. + + +\begin{rem} +Another, perhaps more common, version of the Pythagorean tree that +contains only primitive Pythagorean triples can be obtained using the action +of the congruence subgroup $\Gamma(2)\subset\SL(2,\Z)$. +Our preference however is to keep the whole group $\SL(2,\Z)$, +which results in adding Pythagorean triples with $\gcd(a,b,c)=2$. +\end{rem} + + +%%%%%%%%%%%%%%%%%%%% +\subsection{Euclide's formula in a matrix form} +%%%%%%%%%%%%%%%%%%%% + + +In terms of the symmetric matrices~\eqref{PythaM}, the Euclide formula reads +$$ +X_{(a,b,c)}= +\begin{pmatrix} +m^2&mn\\ +mn&n^2 +\end{pmatrix}= +\begin{pmatrix} +m\\ +n +\end{pmatrix} +\begin{pmatrix}m, &n\end{pmatrix}. +$$ +That is why it is practical to use another notation for $X_{(a,b,c)}$, namely +$X_{\frac{m}{n}}$. +The $\SL(2,\Z)$-action on pairs $(m,n)$ is then simply the linear action on $2$-vectors +$$ +A:\begin{pmatrix} +m\\ +n +\end{pmatrix} +\mapsto +A\begin{pmatrix} +m\\ +n +\end{pmatrix}, +$$ +while the action on rational numbers is given by fractional-linear transformations +\begin{equation} +\label{LFT} +\begin{pmatrix} +\a&\b\\%[2pt] +\g&\d +\end{pmatrix}\left(x\right)= +\frac{\a x+\b}{\g x+\d}. +\end{equation} + +Note that for $x\in\Q$ the result of~\eqref{LFT} can become infinite. +This is why the action~\eqref{LFT} is correctly understood as an action +on the rational projective line $\Q\cup\{\infty\}$, +where $\infty$ is represented by the quotient~$\frac{1}{0}$. +Note also that the center of $\SL(2,\Z)$ acts trivially, therefore +is is more convenient to think of $\PSL(2,\Z)$-action, +where $\PSL(2,\Z)$ is the quotient of $\SL(2,\Z)$ by the center: +$$ +\PSL(2,\Z)=\SL(2,\Z)/\Z_2. +$$ +When thinking of $\PSL(2,\Z)$ instead of $\SL(2,\Z)$, one should +consider all $2\times2$ matrices up to a scalar multiple. +Note that the group $\PSL(2,\Z)$ is usually called the {\it modular group}. + + +%%%%%%%%%%%%%%%%%%%% +\subsection{Relation to continued fractions}\label{CFSec} +%%%%%%%%%%%%%%%%%%%% + +Every rational number~$\frac{m}{n}>1$ can be written as a finite continued fraction +$$ +\frac{m}{n} +\quad=\quad +a_1 + \cfrac{1}{a_2 + + \cfrac{1}{\ddots +\cfrac{1}{a_{k}} } }, + $$ +with integer coefficients~$a_i$, such that $a_i\geq1$ for all $i\geq1$. +The standard notation is +$$ +\frac{n}{m}=[a_1,a_2,\ldots,a_{k}]. +$$ +The above continued fraction expansion is unique +if one chooses an even or odd number of coefficients. +For convenience, we assume that $k$ is odd. + +Written in the matrix, or fractional-linear form, the above continued fraction reads +\begin{equation} +\label{MCF} +\frac{m}{n}= +R^{a_1}L^{a_2}R^{a_3}L^{a_4}\cdots{}R^{a_k} +\left(\frac{0}{1}\right). +\end{equation} +We conclude that the matrix~\eqref{PythaM} of a Pythagorean triple +corresponding to $\frac{n}{m}$ is given by +\begin{equation} +\label{Matmn} +X_{\frac{m}{n}}= +A\,X_0\,A^T, +\end{equation} +where $A=R^{a_1}L^{a_2}R^{a_3}L^{a_4}\cdots{}R^{a_k}$ and $X_0$ is as in~\eqref{X0}. + +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% +\section{A brief account on $q$-rationals}\label{RatSec} +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% + +The notion of $q$-deformed rationals was introduced in~\cite{MGOfmsigma}. +In this section, we briefly remind the definition and some properties +of $q$-rationals that will be useful for what follows. + +%%%%%%%%%%%%%%%%%%%% +\subsection{An intrinsic definition} +%%%%%%%%%%%%%%%%%%%% + +Given a rational number,~$\frac{m}{n}$, its $q$-deformation is a rational function in~$q$ +$$ +\left[\frac{m}{n}\right]_q= +\frac{\cN_{\frac{m}{n}}(q)}{\cD_{\frac{m}{n}}(q)}, +$$ +where the numerator $\cN_{\frac{m}{n}}$ and the denominator $\cD_{\frac{m}{n}}$ +are polynomials in~$q$ that both depend on $m$ and $n$. +Assume that we know the $q$-analogue +of one point, for instance, +$$ +[0]_q:=0. +$$ + +More precisely, the $q$-rationals are characterized by the following two recurrence formulas +\begin{equation} +\label{RecRat} +\left[\frac{m}{n}+1\right]_q= +q\left[\frac{m}{n}\right]_q+1, +\qquad\qquad +\left[-\frac{n}{m}\right]_q= +-\frac{1}{q\left[\frac{m}{n}\right]_q}. +\end{equation} +Polynomials $\cN_{\frac{m}{n}}$ and $\cD_{\frac{m}{n}}$ +possess many interesting properties; see~\cite{MGOmn} and references cited therein. +In particular, they are monic polynomials with positive integer coefficients. +An important property of unimodality was proved in~\cite{OgRa}. + +%%%%%%%%%%%%%%%%%%%% +\subsection{The $q$-deformed $\PSL(2,\Z)$-action} +%%%%%%%%%%%%%%%%%%%% + +The action is determined by two generators of $\PSL(2,\Z)$ represented by the matrices +\begin{equation} +\label{Gens} +R_{q}= +\begin{pmatrix} +q&1\\ +0&1 +\end{pmatrix}, +\qquad\qquad +L_{q}= +\begin{pmatrix} +q&0\\ +q&1 +\end{pmatrix} +\end{equation} +considered up to a scalar multiple by a power of~$q$. +The map $\frac{m}{n}\mapsto\left[\frac{m}{n}\right]_q$ is characterized by the property +that it intertwines the $\PSL(2,\Z)$-action~\eqref{LFT} and the $\PSL(2,\Z)$-action +with the generators $R_q$ and $S_q$ as in~\eqref{Gens}. + + +%%%%%%%%%%%%%%%%%%%% +\subsection{An explicit formula} +%%%%%%%%%%%%%%%%%%%% + +Given a rational number $\frac{m}{n}$ whose continued fraction expansion is +$\frac{m}{n}=[a_1,a_2,\ldots,a_k]$, where $k$ is odd. +A simple way to calculate a $q$-rational is to replace $R$ and $L$ in~\eqref{MCF} by +$R_q$ and $L_q$. +$$ +\left[\frac{m}{n}\right]_q += +R_q^{a_1}L_q^{a_2}R_q^{a_3}L_q^{a_4}\cdots{}R_q^{a_k} +\left(\frac{0}{1}\right). +$$ +This can be viewed as one of several equivalent definitions: + +\begin{ex} +The first interesting examples +$$ +\left[\frac{5}{2}\right]_{q}= +\frac{1+2q+q^{2}+q^{3}}{1+q}, +\qquad\qquad +\left[\frac{5}{3}\right]_{q}= +\frac{1+q+2q^{2}+q^{3}}{1+q+q^{2}} +$$ +illustrates the fact that the numerator (and denominator) of the $q$-rational +$\frac{m}{n}$ depend both on~$m$ and~$n$. +Observe that the polynomials in the numerators +of these $q$-rationals are precisely the polynomials $\cC$ and~$\cC^*$ +from our first example. + +\end{ex} + +%%%%%%%%%%%%%%%%%%%% +\subsection{The total positivity property}\label{TPSec} +%%%%%%%%%%%%%%%%%%%% + +An important property of the $q$-rationals is the fact that the $q$-deformation +``preserves the order'' of rationals +in the following sense (see~\cite{MGOfmsigma}, Theorem~2). +Suppose we have two rationals~$\frac{m}{n}>\frac{m'}{n'}$, +then the polynomial +$$ +\mathcal{P}_{\frac{n}{m},\frac{n'}{m'}}(q)= +\cN_{\frac{m}{n}}(q)\cD_{\frac{m'}{n'}}(q)-\cD_{\frac{m}{n}}(q)\cN_{\frac{m'}{n'}}(q) +$$ +has positive integer coefficients. +This statement is topological in nature, +since every ordered set is endowed with a natural topology. +It was essential for extension of the notion of $q$-rationals to irrationals; +see~\cite{MGOexp}. +This property will be important for us. + +%%%%%%%%%%%%%%%%%%%% +\subsection{The inverse $q$-rational} +%%%%%%%%%%%%%%%%%%%% + +The following property of $q$-rationals +can be deduced from~\eqref{RecRat}; see~\cite{LMGadv}. +It allows one to calculate +$q$-analogs for inverse rationals. +\begin{equation} +\label{InvqRat} +\left[\frac{n}{m}\right]_q= +\frac{1}{\left[\frac{m}{n}\right]_{q^{-1}}}. +\end{equation} +Using this formula it is easy to calculate explicitly the numerator and denominator. + +\begin{cor} +\label{NDProp} +For every $\frac{m}{n}\in\Q$, one has +\begin{equation} +\label{NumDenExp} +\cN_{\frac{n}{m}}(q)=q^d\cD_{\frac{m}{n}}(q^{-1}), +\qquad\qquad +\cD_{\frac{n}{m}}(q)=q^d\cN_{\frac{m}{n}}(q^{-1}), +\end{equation} +where $d=\max(\deg(\cN_{\frac{m}{n}}),\deg(\cD_{\frac{m}{n}}))$. +\end{cor} + +\begin{proof} +This readily follows from~\eqref{InvqRat}. +\end{proof} + + +\begin{rem} +Another formula was obtained in~\cite{Per2}: +$$ +\left[\frac{n}{m}\right]_q= +\frac{\left(q-1\right)\left[\frac{m}{n}\right]_q+1}{q\left[\frac{m}{n}\right]_q+1-q}. +$$ +One of the advantages of this formula is that it is not necessary to invert the parameter~$q$ +and can be useful in many different situations. +\end{rem} + + +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% +\section{A construction of $q$-Pythagorean triples}\label{SecTwo} +%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%% + +In this section, we describe a $q$-analogue for each +standard Pythagorean triple. +We show that our solutions satisfy the conditions~\ref{Con1}--\ref{Con3}, +thus proving Theorem~\ref{ExtUniq}. + + +%%%%%%%%%%%%%%%%%%%% +\subsection{The main definition}\label{DefSec} +%%%%%%%%%%%%%%%%%%%% + +Given a rational number~$\frac{m}{n}>1$ and its continued fraction +expansion $\frac{m}{n}=[a_1,a_2,\ldots,a_k]$, where $k$ is odd, +we define a $q$-analogue of the matrix~\eqref{PythaM} and~\eqref{Matmn} +by the following formula: +\begin{equation} +\label{Xq} +X_{\frac{m}{n}}(q):= +A_q\,X_0\,A_q^T, +\end{equation} +where +$$ +A_q:=R_q^{a_1}L_q^{a_2}R_q^{a_3}L_q^{a_4}\cdots{}R_q^{a_k} +\qquad\hbox{and}\qquad +A_q^T:=L_q^{a_k}R_q^{a_{k-1}}L_q^{a_{k-2}}R_q^{a_4}\cdots{}L_q^{a_1}. +$$ + +\begin{rem} +Note that $A_q^T$ is not exactly the transposition of~$A_q$. +Indeed, the notion of transposition in the $q$-deformed case has the following form +$$ +\begin{pmatrix} +\a(q)&\b(q)\\[4pt] +\g(q)&\d(q) +\end{pmatrix}^T +:=\begin{pmatrix} +\a(q)&q^{-1}\g(q)\\[4pt] +q\b(q)&\d(q) +\end{pmatrix}. +$$ +For details; see~\cite{XY}. +\end{rem} + +%%%%%%%%%%%%%%%%%%%% +\subsection{The trace of the matrix $X_{\frac{m}{n}}(q)$}\label{qEuclSec} +%%%%%%%%%%%%%%%%%%%% + +We have the following statement. + +\begin{prop} +\label{TraceProp} +The trace of the matrix~\eqref{Xq} has the following expression in terms of the +corresponding $q$-rational +\begin{equation} +\label{TraceForm} +\Tr\left(X_{\frac{m}{n}}(q)\right)= +q\cN_{\frac{m}{n}}(q)^2+\cD_{\frac{m}{n}}(q)^2, +\end{equation} +where $\cN_{\frac{m}{n}}(q)$ and $\cD_{\frac{m}{n}}(q)$ are the numerator and denominator +of the $q$-deformedrational~$\left[\frac{m}{n}\right]_q$. +\end{prop} + +\begin{proof} +The matrixces $A_q$ and $A_q^T$ have the following explicit form +$$ +A_q= +\begin{pmatrix} +*&\cN_{\frac{m}{n}}(q)\\[4pt] +*&\cD_{\frac{m}{n}}(q) +\end{pmatrix}, +\qquad\qquad +A_q^T= +\begin{pmatrix} +*&*\\[4pt] +q\cN_{\frac{m}{n}}(q)&\cD_{\frac{m}{n}}(q) +\end{pmatrix}. +$$ +Note that the first column of $A_q$ and the first row $A_q^T$ +are not relevant, but can be calculated from the continued fraction +of~$\frac{m}{n}$; see~\cite{MGOfmsigma}. +It follows from~\eqref{Xq} that +\begin{eqnarray*} +X_{\frac{m}{n}}(q) &=& +\begin{pmatrix} +*&\cN_{\frac{m}{n}}(q)\\[4pt] +*&\cD_{\frac{m}{n}}(q) +\end{pmatrix} +\begin{pmatrix} +0&\;0\\[4pt] +0&\;1 +\end{pmatrix} +\begin{pmatrix} +*&*\\[4pt] +q\cN_{\frac{m}{n}}(q)&\cD_{\frac{m}{n}}(q) +\end{pmatrix}\\[6pt] +&=& +\begin{pmatrix} +q\cN_{\frac{m}{n}}(q)^2&*\\[4pt] +*&\cD_{\frac{m}{n}}(q)^2 +\end{pmatrix}, +\end{eqnarray*} +and hence the result. +\end{proof} + +\begin{defn} +For every rational $\frac{m}{n}$, we thus naturally associate the polynomial +$$ +\cC_{\frac{m}{n}}(q):=q\cN_{\frac{m}{n}}(q)^2+\cD_{\frac{m}{n}}(q)^2. +$$ +\end{defn} + +Our goal is to show that the product of the polynomial $\cC_{\frac{m}{n}}(q)$ +and its reciprocal $\cC^*_{\frac{m}{n}}(q)$ (see~\eqref{RecipEq}) satisfies the +$q$-Pythagoras equation~\eqref{PythEq}. + + +%%%%%%%%%%%%%%%%%%%% +\subsection{Solutions to the $q$-Pythagoras equation}\label{qPitSec} +%%%%%%%%%%%%%%%%%%%% + +We have the following result. + +\begin{thm} +\label{CalcThm} +The polynomials +\begin{eqnarray} +\label{qEucl1} +\A_{\frac{m}{n}}(q)&=& +q\cN_{\frac{m}{n}}(q)\cN_{\frac{n}{m}}(q)+\cD_{\frac{m}{n}}(q)\cD_{\frac{n}{m}}(q), +\\[4pt] +\label{qEucl2} +\B_{\frac{m}{n}}(q)&=& +\cN_{\frac{m}{n}}(q)\cD_{\frac{n}{m}}(q)-\cD_{\frac{m}{n}}(q)\cN_{\frac{n}{m}}(q), +\\[4pt] +\label{qEucl3} +\cC_{\frac{m}{n}}(q)&=& +q\cN_{\frac{m}{n}}(q)^2+\cD_{\frac{m}{n}}(q)^2. +\end{eqnarray} +are solutions to~\eqref{PythEq}. +\end{thm} + +\begin{proof} +From the definition of the reciprocal polynomial, +\begin{eqnarray*} +\cC^*_{\frac{m}{n}}(q) &=& +q^{\deg(\cC)}\cC_{\frac{m}{n}}(q^{-1})\\ +&=& +q^{\deg(\cC)}\left(q^{-1}\cN_{\frac{m}{n}}(q^{-1})^2+\cD_{\frac{m}{n}}(q^{-1})^2\right). +\end{eqnarray*} +The degree of $\cC$ is given by +$$ +\deg(\cC)=2d+1, +$$ +where $d=\max(\deg(\cN_{\frac{m}{n}}),\deg(\cD_{\frac{m}{n}}))$, as in~\eqref{NumDenExp}. +Using~\eqref{NumDenExp}, we thus obtain +$$ +\cC^*_{\frac{m}{n}}(q)= +\cD_{\frac{n}{m}}(q)^2+q\cN_{\frac{n}{m}}(q)^2. +$$ +It follows that +$$ +\cC_{\frac{m}{n}}(q)\cC^*_{\frac{m}{n}}(q)= +\left(q\cN_{\frac{m}{n}}(q)^2+\cD_{\frac{m}{n}}(q)^2\right) +\left(q\cN_{\frac{n}{m}}(q)^2+\cD_{\frac{n}{m}}(q)^2\right). +$$ +Finally, using the classical Brahmagupta-Fibonacci square identity +$$ +(x^2+y^2)(z^2+t^2)=(xz+yt)^2+(xt-yz)^2, +$$ +for $x=q^\half\cN_{\frac{m}{n}}(q), +y=\cD_{\frac{m}{n}}(q), +z=q^\half\cN_{\frac{n}{m}}$, and $t=\cD_{\frac{n}{m}}(q)$, +one obtains +\begin{eqnarray*} +\cC_{\frac{m}{n}}(q)\cC^*_{\frac{m}{n}}(q) &=& +\left(q\cN_{\frac{m}{n}}(q)\cN_{\frac{n}{m}}(q)+\cD_{\frac{m}{n}}(q)\cD_{\frac{n}{m}}(q)\right)^2\\ +&&+q\left(\cN_{\frac{m}{n}}(q)\cD_{\frac{n}{m}}(q)-\cD_{\frac{m}{n}}(q)\cN_{\frac{n}{m}}(q)\right)^2, +\end{eqnarray*} +as desired. +\end{proof} + +\begin{rem} +The expressions \eqref{qEucl1}--\eqref{qEucl3} constitute a $q$-analogue of the Euclide +formula~\eqref{EuclForm}. +\end{rem} + + +%%%%%%%%%%%%%%%%%%%% +\subsection{Properties of the polynomials $\A_{\frac{m}{n}},\B_{\frac{m}{n}}$ and $\cC_{\frac{m}{n}}$}\label{PropSec} +%%%%%%%%%%%%%%%%%%%% + +Let us give some simple properties of the polynomials +$\A_{\frac{m}{n}},\B_{\frac{m}{n}}$ and $\cC_{\frac{m}{n}}$ defined by +\eqref{qEucl1}--\eqref{qEucl3}. + +\begin{prop} +\label{PropProp} +If $\frac{m}{n}\geq1$, then + +(i) +The polynomials $\A_{\frac{m}{n}}$ and $\B_{\frac{m}{n}}$ are self-reciprocal. + +(ii) +All three polynomials $\A_{\frac{m}{n}},\B_{\frac{m}{n}}$ and $\cC_{\frac{m}{n}}$ +are monic and have positive coefficients. + +\end{prop} + +\begin{proof} +Part (i). +By~\eqref{NumDenExp}, another expression for +the polynomials $\A_{\frac{m}{n}}$ and $\B_{\frac{m}{n}}$ is as follows +\begin{eqnarray*} +\A_{\frac{m}{n}}(q) &=& +q^d\left( +q\cN_{\frac{m}{n}}(q)\cD_{\frac{m}{n}}(q^{-1}) ++\cD_{\frac{m}{n}}(q)\cN_{\frac{m}{n}}(q^{-1}) +\right), +\\[6pt] +\B_{\frac{m}{n}}(q)&=& +q^d\left(\cN_{\frac{m}{n}}(q)\cN_{\frac{m}{n}}(q^{-1}) +-\cD_{\frac{m}{n}}(q)\cD_{\frac{m}{n}}(q^{-1})\right), +\end{eqnarray*} +where $d=\deg(\cN_{\frac{m}{n}})>\deg(\cD_{\frac{m}{n}})$. +The above expression for $\B_{\frac{m}{n}}$ is manifestly self-reciprocal. +For $\A_{\frac{m}{n}}$ one has $\deg\left(\A_{\frac{m}{n}}\right)=2d+1$ +and therefore +$$ +\begin{array}{rcl} +\A^*_{\frac{m}{n}}(q) &=& +q^{\deg\left(\A_{\frac{m}{n}}\right)}\A_{\frac{m}{n}}(q^{-1})\\[6pt] +&=& +q^{d}\cN_{\frac{m}{n}}(q^{-1})\cD_{\frac{m}{n}}(q) ++q^{d+1}\cD_{\frac{m}{n}}(q^{-1})\cN_{\frac{m}{n}}(q)\\[6pt] +&=&\A_{\frac{m}{n}}(q). +\end{array} +$$ + + +Part (ii). +For $\frac{m}{n}\geq1$ polynomials +$\cD_{\frac{m}{n}}$ and $\cD_{\frac{n}{m}}$ are monic, and so is $\A_{\frac{m}{n}}$. +The polynomial $\cN_{\frac{m}{n}}$ is also monic, +while the lower coefficient of $\cN_{\frac{n}{m}}$ vanishes. +Hence $\B_{\frac{m}{n}}$ is monic as well. + +The polynomials $\A_{\frac{m}{n}}$ and $\cC_{\frac{m}{n}}$ have positive coefficients since +all numerators and denominators of the positive $q$-rationals have positive coefficients; +see~\cite{MGOfmsigma}. +The fact that $\B_{\frac{m}{n}}$ has positive coefficients is a corollary of +Theorem~2 of~\cite{MGOfmsigma}. +\end{proof} + +In all the examples we explored with numerical experimentation, +the formulas~\eqref{qEucl1}--\eqref{qEucl3} produce unimodal polynomials. +However, we were not able to prove the unimodality in general. + +%%%%%%%%%%%%%%%%%%%% +\subsection{Further examples} +%%%%%%%%%%%%%%%%%%%% + +To conclude this article, here are a few more examples. +We will consistently indicate whether the polynomials are factorable. +A surprise awaits the persistent reader who makes it to the end. + +(1) +Consider the Pythagorean triple $(12,5,13)$ that corresponds to the rational~$\frac{3}{2}$. +The $q$-analogues of this $q$-rational and its inverse are +$$ +\left[\frac{3}{2}\right]_q=\frac{1+q+q^2}{1+q}, +\qquad\qquad +\left[\frac{2}{3}\right]_q=\frac{q+q^2}{1+q+q^2}. +$$ +Applying~\eqref{qEucl1}--\eqref{qEucl3}, we get +\begin{eqnarray*} +\A_{\frac{3}{2}}(q)&=& +(1+q)(1+q^2)(1+q+q^2), +\\[4pt] +\B_{\frac{3}{2}}(q)&=& +1+q+q^2+q^3+q^4=[5]_q, +\\[4pt] +\cC_{\frac{3}{2}}(q)&=& +1+3q+3q^2+3q^3+2q^4+q^5. +\end{eqnarray*} + +(2) +The Pythagorean triple $(56,33,65)$ corresponds to the rational~$\frac{7}{4}$. +In this case, +$$ +\left[\frac{7}{4}\right]_q=\frac{1+q+2q^2+2q^3+q^4}{1+q+q^2+q^3}, +\qquad\qquad +\left[\frac{4}{7}\right]_q=\frac{1+q+2q^2+2q^3+q^4}{1+q+q^2+q^3} +$$ +In this case, applying~\eqref{qEucl1}-\eqref{qEucl3} we have +\begin{eqnarray*} +\A_{\frac{7}{4}}(q)&=& +(1+q)(1+q^2)(1+2q+3q^2+2q^3+3q^4+2q^5+q^6), +\\[4pt] +\B_{\frac{7}{4}}(q)&=& +(1+q+q^2)(1+q+2q^2+3q^3+2q^4+q^5+q^6), +\\[4pt] +\cC_{\frac{7}{4}}(q)&=& +1+3q+5q^2+9q^3+11q^4+12q^5+11q^6+8q^7+4q^8+q^9. +\end{eqnarray*} +It is interesting to notice that $\cC_{\frac{7}{4}}$ +is not factorable and $\A_{\frac{7}{4}}$ is not a multiple of +a polynomial corresponding to $7$. +Note also that all three polynomials, $\A_{\frac{7}{4}},\B_{\frac{7}{4}}$, +and $\cC_{\frac{7}{4}}$, are unimodal. + +(3) +Take the simple example of the Pythagorean triple $(24,7,25)$ +that corresponds to the rational $\frac{4}{3}$. +In this case, we found two different $q$-deformations satisfying all the conditions. +The first $q$-Pythagorean triple is obtained by applying~\eqref{qEucl1}-\eqref{qEucl3}: +\begin{eqnarray*} +\A_{\frac{4}{3}}(q) &=& (1+q)(1+q^2)^2(1+q+q^2), +\\[4pt] +\B_{\frac{4}{3}}(q) &=& 1+q+q^2+q^3+q^4+q^5+q^6=[7]_q, +\\[4pt] +\cC_{\frac{4}{3}}(q) &=& 1+3q+5q^2+5q^3+5q^4+3q^5+2q^6+q^7. +\end{eqnarray*} +But we also have another solution to~\eqref{PythEq}! +It looks completely different from the above one: +\begin{eqnarray*} +\A'_{\frac{4}{3}}(q) &=& (1+q)(1 + 10q + q^2), +\\[4pt] +\B'_{\frac{4}{3}}(q) &=& 1 + 5q + q^2, +\\[4pt] +\cC'_{\frac{4}{3}}(q) &=& 1 + 10q + 13q^2 +q^3. +\end{eqnarray*} + +A complete classification of solutions to~\eqref{PythEq} is a challenging problem +which is out of reach so far. +Can we distinguish our solutions~\eqref{qEucl1}-\eqref{qEucl3} from the other classes? +They might be the ``most quantized'' solutions, those with maximal number of terms. +Given that each term of a $q$-analogue should have a combinatorial meaning, +this would be beneficial. +But this combinatorial meaning remains to be elucidated. + +\bigskip + +\noindent{\bf Acknowledgments}. +We are grateful to Perrine Jouteur for enlightening discussions. + +\bigskip + +\noindent +{\bf Corresponding Author}: Valentin Ovsienko. + +\bigskip + +\noindent +{\bf Funding declaration}: there was no funding for this manuscript. + +%%%%%%%%%%%%%%%%%%%% +\begin{thebibliography}{99} +%%%%%%%%%%%%%%%%%%%% + + \bibitem{AE} +M. Arnold, A. Eydelzon, +{\it On matrix Pythagorean triples}, +Amer. Math. Monthly 126 (2019), 158--160. + + \bibitem{CC} +B. Cha, R. Concei\c{c}ao, +{\it A polynomial analogue of Berggren's theorem on Pythagorean triples}, +Proc. Amer. Math. Soc. 152 (2024), 1925--1937. + + \bibitem{DLS} +H. Davenport, D.J. Lewis, A. Schinzel, +{\it Polynomials of certain special types}, +Acta Arith. 9 (1964), 107--116. + +\bibitem{EJMGO} + S.J. Evans, P. Jouteur, S. Morier-Genoud, V. Ovsienko, + {\it On $q$-deformed Markov numbers. Cohn matrices and perfect matchings with weighted edges}, +arXiv:2507.19080. + + \bibitem{Per2} +P. Jouteur, +{\it Symmetries of the $q$-deformed real projective line}, +arXiv:2503.02122. + +\bibitem{LMGadv} +L. Leclere, S. Morier-Genoud, +{\it {$q$}-deformations in the modular group and of the real quadratic + irrational numbers}, +Adv. Appl. Math. {\bf 130} (2021) Paper No. 102223, 28 pp. + +\bibitem{MGOfmsigma} +S. Morier-Genoud, V. Ovsienko, +{\it {$q$}-deformed rationals and {$q$}-continued fractions}, +Forum Math. Sigma 8 (2020), e13, 55 pp. + +\bibitem{MGOexp} +S. Morier-Genoud, V. Ovsienko, +{\it On $q$-deformed real numbers}, +{\em Exp. Math. 31 (2022), 652--660.} + +\bibitem{MGOmn} +S. Morier-Genoud, V. Ovsienko, +{\it $q$-deformed rationals and irrationals}, +arXiv:2503.23834. + +\bibitem{OgRa} +E.K. Oguz, M. Ravichandran, +{\it Rank polynomials of fence posets are unimodal}, +Discrete Math. {\bf 346} (2023), Paper No. 113218. + +\bibitem{Tak} +R. Takloo-Bighash, +A Pythagorean introduction to number theory. +Right triangles, sums of squares, and arithmetic. +Undergraduate Texts in Mathematics. Springer, Cham, 2018. + +\bibitem{Tra} +A. Trautman, +{\it Pythagorean spinors and Penrose twistors}, +The geometric universe (Oxford, 1996), 411--419, +Oxford Univ. Press, Oxford, 1998. + +\bibitem{XY} +X. Ren, K. Yanagawa, +{\it Transposes in the $q$-deformed modular group and their applications to +$q$-deformed rational numbers}, +arXiv:2502.02974. + +\bibitem{Sie} +W. Sierpi\'nski, +Pythagorean triangles, +The Scripta Mathematica Studies, No. 9, +Yeshiva Univ., New York, 1962. + +\end{thebibliography} + + +\bigskip + +\bigskip + +\noindent +{\sc + +\noindent +{Hugo Mathevet, +Universit\'e de Reims Champagne Ardenne, +Laboratoire de Math\'e\-ma\-tiques, CNRS UMR9008, +Moulin de la Housse - BP 1039, +51687 Reims cedex 2, +France, +}\\ +{Email: hugo.mathevet@univ-reims.fr} + +\medskip + +\noindent +{Sophie Morier-Genoud, +Universit\'e de Reims Champagne Ardenne, +Laboratoire de Math\'e\-ma\-tiques, CNRS UMR9008, +Moulin de la Housse - BP 1039, +51687 Reims cedex 2, +France, +}\\ +{Email: sophie.morier-genoud@univ-reims.fr} + +\medskip + +\noindent +{Valentin Ovsienko, +Centre National de la Recherche Scientifique, +Laboratoire de Math\'e\-ma\-tiques, +Universit\'e de Reims Champagne Ardenne, +Moulin de la Housse - BP 1039, +51687 Reims cedex 2, +France},\\ +{Email: valentin.ovsienko@univ-reims.fr} +} + +\end{document} + + + + diff --git a/QuantizingPythagoreanTriples/lake-manifest.json b/QuantizingPythagoreanTriples/lake-manifest.json new file mode 100644 index 0000000..73c9e0e --- /dev/null +++ b/QuantizingPythagoreanTriples/lake-manifest.json @@ -0,0 +1,106 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/repl", + "type": "git", + "subDir": null, + "scope": "", + "rev": "f0a88bfca1fa6ac75e2a33d1678a3b67c90fb492", + "name": "repl", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.98", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "QuantizingPythagoreanTriples", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/QuantizingPythagoreanTriples/lakefile.toml b/QuantizingPythagoreanTriples/lakefile.toml new file mode 100644 index 0000000..d053938 --- /dev/null +++ b/QuantizingPythagoreanTriples/lakefile.toml @@ -0,0 +1,23 @@ +name = "QuantizingPythagoreanTriples" +version = "0.1.0" +keywords = ["math", "formalization"] +defaultTargets = ["Pythagore2"] + +[leanOptions] +pp.unicode.fun = true +relaxedAutoImplicit = false +weak.linter.mathlibStandardSet = true +maxSynthPendingDepth = 3 + +[[require]] +name = "mathlib" +scope = "leanprover-community" +rev = "v4.30.0-rc2" + +[[lean_lib]] +name = "Pythagore2" + +[[require]] +name = "repl" +git = "https://github.com/leanprover-community/repl" +rev = "v4.30.0-rc2" diff --git a/QuantizingPythagoreanTriples/lean-toolchain b/QuantizingPythagoreanTriples/lean-toolchain new file mode 100644 index 0000000..6c7e31f --- /dev/null +++ b/QuantizingPythagoreanTriples/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.30.0-rc2