Email Gateway (Aug 23 2022 at 08:17): Email Gateway (Aug 23 2022 at 08:17):From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
Dear Isabelle/HOL users,
Is there a library about the properties of this function
int (multiplicity p (fst (quotient_of x)) ) - int (multiplicity p (snd (quotient_of x)) ),
known as p-adic valuation? I know that there is a valuation which is already defined in Isabelle/HOL,
valuation::"[('b, 'm) Ring_scheme, 'b => ant] => bool"
"valuation K v ==
v ∈ extensional (carrier K) ∧
v ∈ carrier K -> Z∞ ∧
v (\<zero>K) = ∞ ∧ (∀x∈((carrier K) - {\<zero>K}). v x ≠ ∞) ∧
(∀x∈(carrier K). ∀y∈(carrier K). v (x ·rK y) = (v x) + (v y)) ∧
(∀x∈(carrier K). 0 ≤ (v x) --> 0 ≤ (v (1rK ±K x))) ∧
(∃x. x ∈ carrier K ∧ (v x) ≠ ∞ ∧ (v x) ≠ 0)"
https://www.isa-afp.org/browser_info/Isabelle2008/HOL/Valuation/Valuation1.html
but this definition is extremely abstract compared with the previous definition.
Kind regards,
José M.
Email Gateway (Aug 23 2022 at 08:18):From: Manuel Eberl <eberlm@in.tum.de>
To my knowledge: No.
However, Jeremy Silvestre has been working on p-adic numbers a bit. I
don't know what he has exactly, but I cc'ed him in case he wants to
chime in.
If you do end up defining it and prove the basic properties, I would
suggest we add this to HOL-Number_Theory.
Manuel
Email Gateway (Aug 23 2022 at 08:21):From: AARON CRIGHTON <crightoa@mcmaster.ca>
I have been working on a rather extensive project involving the p-adics,
based on the HOL-Algebra library. In particular I have defined Qp, Zp,
their respective valuations, many basic results on the valuative topology,
as well as Hensel's Lemma. I have had to also prove many lemmas about
univariate and multivariate polynomials along the way.
My own goal is to prove MacIntyre's quanitifer elimination result for
p-adic fields, and I would estimate that I am about 90% of the way there.
If you are interested in seeing what I've done so far, let me know and I
can share my progress.
I must admit that I have been learning Isabelle "on the fly" over the past
10 months for this project, so my approacj may not be as systematic or
paradigmatic as would be desired.
Aaron
Email Gateway (Aug 23 2022 at 08:22):From: Jeremy Sylvestre <jsylvest@ualberta.ca>
Hi, I have some basic properties for the p-adic absolute value:
abbreviation "pint_exp p a \<equiv> p ^ (multiplicity (of_int p) a)"
definition padic_abs_factorial_prod :: "int \<Rightarrow>
('a::{factorial_semiring,ring_1})\<times>'a \<Rightarrow> int\<times>int"
where "padic_abs_factorial_prod p x = (
if (fst x * snd x = 0) \<or> \<not> prime_elem
((of_int::int\<Rightarrow>'a) p)
then (0,1) else ( pint_exp p (snd x), pint_exp p (fst x) )
)"
setup_lifting Quotient_rat
lift_definition padic_abs :: "int \<Rightarrow> rat \<Rightarrow> rat" is
padic_abs_factorial_prod
using padic_abs_factorial_prod_ratrel by fast
I also have an edited version of Real.thy that constructs the ring of
Cauchy sequences out of a ring equipped with a rat-valued absolute value
function.
Haven't pursued this too much so far, was hoping to hire a summer student
to work on this for me.
Cheers,
Jeremy S.
Email Gateway (Aug 23 2022 at 08:22):From: Manuel Eberl <eberlm@in.tum.de>
That sounds like amazing work. I would be very interested to see where
this goes (and what you have so far). I have some vague long-term
interest in p-adic analysis, p-adic integration etc, but I don't know
very much about it as of yet and I haven't done any work on it either.
Clearly, HOL-Algebra was always the obvious "correct" route to formalise
the p-adics, but I feared that doing so would be much too painful. So it
is good to hear that you actually got somewhere with that approach.
Email Gateway (Aug 23 2022 at 08:22):From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
By the way, the proof of the first statement that André Weil conjectured when he was in prison, was done using p-adic analysis (Dwork). After that, Grothendieck re-proved this result using cohomology and his approach was extended to the proofs of other statements conjectured by Weil.
The consensus is that Grothendieck-Deligne’s approach is better than p-adic analysis in order to prove Weil’s conjectures and related subjects, because cohomology reduces computations. Nevertheless, such a consensus among mathematicians does not take into account the power of automatic reasoning in proof assistants.
It would be impressive, to the degree of getting a Field medal, if someone is capable of finding a new proof of all the Weil’s conjectures using p-adic analysis and not cohomology. The extensive calculations involved in the p-adic approach may be impossible for humans, but not for a computer. Such a research may open a way to prove Riemann’s hypothesis using the automatic reasoning Isabelle/HOL, because Riemann’s hypothesis is a variation of Weil’s conjecture.
Good luck to the adventures (I am not going myself in that direction)
José M.
Last updated: May 01 2024 at 20:18 UTC