Skip to content

Instantly share code, notes, and snippets.

@icecream17

icecream17/metamath-todo.md

Last active June 3, 2024 20:33
Show Gist options
  • Save icecream17/c85a1288ccebd09e21c7609943a9a8d6 to your computer and use it in GitHub Desktop.
Save icecream17/c85a1288ccebd09e21c7609943a9a8d6 to your computer and use it in GitHub Desktop.
Download ZIP
metamath todo
Raw
metamath-todo.md

Metamath todo

Axioms

  • change df-pnf and df-mnf to use rru
  • Remove ax-icn ax-addcl ax-mulcl ax-i2m1 ax-cnre in 00id by
    • 0cnALT3
    • 00idlem: real hypotheses version of adddir where addcl is circumvented through addrcl and resscn
    • mulcom and ax-1rid in step 18 instead of mulid2i (maybe introduce remulid1i and remulid2i)
  • addition and multiplication with only digits one through nine; see comment at metamath/set.mm#2947
  • swap subs in https://us.metamath.org/mpeuni/opelopabsbALT.html
  • alephon can save ax-inf2 because if infinity is denied in aleph0, then alephnull is the empty set which is also in On

Ideas

  • Note that i 0 = 0 (bc E. r r = i s) and A r = A r + A 0 = A 0 + A r Shorten addid1: A (1 + 0) = A + 0 = A
  • Shorten evlslem3 with psrbagev2
  • Shorten selvval2lem4 with mplasclf and frnd
  • Use nneo to shorten oexpreposd
  • Hypotheses: A e. RR and ( 0 + 0 ) =/= 0:
    • Use fimaxre (not fimaxre2, uses 0re) to prove nnnfi
      • 1 = ( 1 + 1 ) -> NN = { 1 }
      • 1 < ( 1 + 1 ) -> -. NN e. Fin
      • ( 1 + 1 ) < 1 -> -. NN e. Fin
  • Generalize zrtdvds antecedent to A e. CC /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. ZZ (though this lengthens rtprmirr...)
  • Automatic disjoint variable cleanup
  • Automatic shortening using "theorem interchangable forms" (i.e. the varying levels of deduction, closedness, or inference) and "reordering" (i.e. placing wff-theorems like adantr, bicomi, etc. before or after theorems like albii, sbbii, rexbidv, etc. and seeing if shortening is possible)
  • The very specific case of cases a la ((a or b) iff (b or a), (a or b) iff (b or a), anbi12i, bicom) --> ((b or a) iff (a or b), (b or a) iff (a or b), anbi12i)

Additions

  • something with a wff that can be spd
    • A. x ( x = y -> [ x / z ] ph ) <-> [ y / z ] ph $d x z $.
    A. x ( x = y -> A. z ( z = x -> ph ) ) -> A. z ( z = y -> ph )
                                       -> [ y / z ] ph          $d y z
x = y -> [ x / z ] ph <-> [ y / z ] ph
[ y / z ] ph -> x = y -> [ x / x ] ph
  • sbidw
    • x = w -> ( ph <-> ps )
    • then: [ x / x ] ph <-> ph $d x ps $. sbievws
  • prove https://mathcircle.berkeley.edu/sites/default/files/BMC3/bamc.pdf "A is algebraic iff 1,A,A^2,etc lie in a finite dimensional vector space over QQ. So say A satisfies a polynomial of degree N, and B satisfies a polynomial of degree M (over QQ). Then all of the products A^i x. B^j lie in the vector space formed by A^k x. B^l for k<M, l<N. So A^1 B^1 = A x. B is algebraic" Basically this means that multiplying two polynomials results in another polynomial whose zero is algebraic. Somehow this correlates with multiplying the two zeroes of the factor polynomials together
  • sb2iv (would save/shorten equsb1v, sbiev, sbtv)
  • ( A + A ) =/= A --> -. ( x. " ( { A } X. NN ) ) e. Fin
  • ph -> A e. RR , A =/= 0 , B e. RR => ph -> E. x e. RR ( x x. ( B x. A ) ) = B ax-1rid ax-1cn ax-rrecex ax-mulass ax-mulcom

Comments / typos

FLT

I want to be... the first to prove... Fermat's Last Theorem (in a proof setting).

See https://docs.google.com/document/d/19dXkojJJt6gq9rYLo6zbz7HpHpD9iMJJkY0LEpGqPs0/edit?usp=sharing for a proof outline. Conceptually, that means Ribet's theorem and the Modularity theorem (or a weaker version) needs to be proved.

An idea of how to start is to define what a modular form is. (Edit: I'm actually starting with projective planes --> elliptic curves)

The logic

A fermat triple (a, b, c) (and n) is a hypothetical solution to a^n + b^n = c^n

  1. Yves Hellegouarch: Associating fermat triples with elliptic curves of the form y^2 = x(x - a^n)(x + b^n)
  2. Ribet: These curves are non-modular by Ribet's theorem
  3. Wiles: These curves are modular by the modularity theorem (or a weaker version that's easier to prove for the special case)

Thus the curves don't exist, thus solutions don't exist!

Current status on FLT

Elliptic curves are projective, so I'm working on theorems about projective spaces.

Right now, I'm trying to find the most basic stepping stones possible. Many results about projective spaces seem like they need tons of definitions.

Even the many introductory ones, since they rely on the existence of division.

Current todo:

  • Revise variables to be consistent with naming conventions: V e. LVec --> W e. LVec etc ?
  • Work through https://math.ucr.edu/~res/progeom/pg-all.pdf to establish the linear algebra foundation up until projective spaces
    • Page 2 (pdf 12)
    • Define curves in "affine space" (this connects multivariable polynomials and free-left modules/vector spaces together)
    • Show that the separate concepts of lines correspond; spans and the solutions to some degree 1 polynomial

Practical definitions

We already defined projective spaces. In our definition, a point p elof ( N Proj_n K ) is an equivalence class of n-dimensional tuples.

We define f(p) = f(...homogeneous coordinates of p), where ... is like javascript spread, and homogeneous (or projective) coordinates are simply any element of p.

For example, << 1, 2, 3 >> ~~ lambda << 1, 2, 3 >>. Let p = the set of all lambda << 1, 2, 3 >>. Then f(p) = f(1, 2, 3) = f(3, 6, 9) = f(4, 8, 12) = etc.

Equality of such multiples is only guaranteed for homogeneous polynomials.

So first lets show an isomorphism between say df-psr or df-mpl and df-frlm

Explanation of definitions

A polynomial in metamath is represented by a function ( ( variables --> exponents ) --> coefficients ) where variables are arbitrary sets, exponents are NN0, and coefficients are in some ring (ringvals).

Meanwhile an evaluation of a polynomial ( I evalSub R S P ) is represented by a function ( ( variables --> ringvals ) --> ringvals ), i.e. it maps assignments of variables to values (assigns), to the value of the polynomial.

The first thing I want to prove is that when you multiply the range of an assign for a homogeneous polynomial by some ringval A, the value of the polynomial is multiplied by A ^ thedegreeofthepolynomial

  ${
    mhpevlsmul.q $e |- Q = ( ( I evalSub S ) ` R ) $.
    mhpevlsmul.b $e |- B = ( Base ` S ) $.
    mhpevlsmul.x $e |- .x. = ( .r ` S ) $.
    mhpevlsmul.g $e |- G = ( mulGrp ` S ) $.
    mhpevlsmul.e $e |- .^ = ( .g ` G ) $.
    mhpevlsmul.h $e |- H = ( I mHomP U ) $.
    mhpevlsmul.u $e |- U = ( S |`s R ) $.
    mhpevlsmul.y $e |- Y = ( ( ringLMod ` S ) ^s I ) $.
    mhpevlsmul.t $e |- .xb = ( .s ` Y ) $.
    mhpevlsmul.i $e |- ( ph -> I e. V ) $.
    mhpevlsmul.s $e |- ( ph -> S e. CRing ) $.
    mhpevlsmul.r $e |- ( ph -> R e. ( SubRing ` S ) ) $.
    mhpevlsmul.n $e |- ( ph -> N e. NN0 ) $.
    mhpevlsmul.f $e |- ( ph -> F e. ( H ` N ) ) $.
    mhpevlsmul.m $e |- ( ph -> M e. B ) $.
    mhpevlsmul.z $e |- ( ph -> Z : I --> B ) $.
    $( Let ` Z ` be an assignment of variables to values ( ` I --> B ` ) .
       In a homogeneous polynomial, multiplying all these assignments by ` M `
       will result in the evaluation being multiplied by ` M ^ N ` . $)
    mhpevlsmul $p |- ( ph -> ( ( Q ` F ) ` ( M .xb Z ) ) = 
                               ( ( N .^ M ) .x. ( ( Q ` F ) ` Z ) ) ) $=
      ? $.
  $}

More resources

https://www.cis.upenn.edu/~jean/gma-v2-chap5.pdf

Proof of FLT for regular primes

https://kconrad.math.uconn.edu/blurbs/gradnumthy/fltreg.pdf

https://wstein.org/129-05/final_papers/Emily_Riehl.pdf

https://www.youtube.com/watch?v=X6DTIsfyD34

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment