Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Constructible numbers - initial idea #4578

Open
wants to merge 14 commits into
base: develop
Choose a base branch
from
+702 −132
Open

Constructible numbers - initial idea #4578

Changes from 5 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
17f31c3
Constructible numbers - initial idea
tirix Jan 16, 2025
10cf396
Update constr.mm
tirix Jan 17, 2025
7ac6a8d
Update constr.mm
tirix Jan 17, 2025
12f03dc
Update constr.mm
tirix Jan 17, 2025
30a91c9
Update constr.mm
tirix Jan 17, 2025
de56b25
Update constr.mm
tirix Jan 18, 2025
fb17c8c
Fix domain of polynomial
tirix Jan 19, 2025
3bb9073
Indentation
tirix Jan 19, 2025
88f6c66
Merge branch 'constr' of https://github.com/tirix/set.mm into constr
tirix Jan 19, 2025
78fccb9
Minimal polynomials
tirix Jan 26, 2025
118f52b
Merge branch 'develop' into constr
tirix Jan 26, 2025
4b8831c
Fix definitional soundness check.
tirix Jan 26, 2025
6f85644
As per @savask remark
tirix Jan 26, 2025
82795f7
As per @avekens comments
tirix Jan 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
139 changes: 139 additions & 0 deletions constr.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,139 @@
$[ set.mm $]

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
Constructible numbers
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
This section defines the set of constructible points as complex numbers which
can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking
intersections of circles and lines.

We initially define two sets:
<UL>
<LI>geometrically, by recursively adding the intersection points : this is
` Constr ` .</LI>
<LI>algebraically, by using field extensions : this is ` ConstrAlg ` . </LI>
</UL>

We then proceed by showing that those two sets are equal.

This construction is useful for proving the impossibility of doubling the
cube ( ~ imp2cube ), and of angle trisection ( ~ imp3ang )
$)


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Degree of a field extension
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
$)

${
fldextdgirred.b $e |- B = ( Base ` F ) $.
fldextdgirred.0 $e |- .0. = ( 0g ` F ) $.
fldextdgirred.d $e |- D = ( deg1 ` F ) $.
fldextdgirred.o $e |- O = ( eval1 ` F ) $.
tirix marked this conversation as resolved.
Show resolved Hide resolved
fldextdgirred.m $e |- M = ( Poly1 ` F ) $.
fldextdgirred.k $e |- K = ( F |`s E ) $.
fldextdgirred.l $e |- L = ( F |`s ( F fldGen ( E u. { Z } ) ) ) $.
fldextdgirred.f $e |- ( ph -> F e. Field ) $.
fldextdgirred.e $e |- ( ph -> E e. ( SubDRing ` F ) ) $.
fldextdgirred.p $e |- ( ph -> P e. ( Base ` M ) ) $.
tirix marked this conversation as resolved.
Show resolved Hide resolved
fldextdgirred.1 $e |- ( ph -> P e. ( Irred ` M ) ) $.
fldextdgirred.z $e |- ( ph -> Z e. ( B \ E ) ) $.
fldextdgirred.2 $e |- ( ph -> ( ( O ` P ) ` Z ) = .0. ) $.
$( If ` Z ` is the root of an irreducible polynomial ` P ` over a field
` K ` , then the degree of the field extension ` [ K [ Z ] : K ] ` is
the degree of the polynomial ` P ` . $)
fldextdgirred $p |- ( ph -> ( L [:] K ) = ( D ` P ) ) $= ? $.
$}


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Quadratic field extensions
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
$)

$c /FldExt2 $.

$( Extend class notation with the quadratic field extension relation. $)
cfldext2 $a class /FldExt2 $.

${
$d e f $.
$( Define the quadratic field extension relation. Quadratic field
extensions are field extensions of degree 2. $)
df-fldext2 $a |- /FldExt2 = { <. e , f >. | ( e /FldExt f /\ ( e [:] f ) = 2 ) } $.
$}


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Chain
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
$)

$c Chain $.

$( Extend class notation with the (finite) chain builder function. $)
cchn $a class Chain $.

${
$d r c n $.
$( Define the (finite) chain builder function. A chain is defined to be a
sequence of objects, whereas each object is in a given relation with the
next one. $)
df-chn $a |- Chain = ( r e. _V |-> { c e. Word dom r |
A. n e. ( dom c \ { 0 } ) ( c ` ( n - 1 ) ) r ( c ` n ) } ) $.
$}


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Constructible points
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
$)

$c Constr $.

$( Extend class notation with the set of geometrically constructible points. $)
cconstr $a class Constr $.

$( Define the set of geometrically constructible points, by recursively adding
the line-line, line-circle and circle-circle intersections constructions
using points in a previous iteration. $)
df-constr $a |- Constr = ( rec ( ( s e. _V |-> { x e. CC |
( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ -. ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) = 0 )
\/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) )
\/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s E. t e. RR ( -. a = d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) )
} ) , { 0 , 1 } ) " _om ) $.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very long and complicated! Would it be helpful to have separate definitions for "set of intersections of two lines", "set of intersections of a line and a circle" and "set of intersections of two circles"?

Copy link
Contributor Author

@tirix tirix Jan 18, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We try to limit the number of definitions - do you think it would be wise to add them? I don't know about any other use.

BTW, do you think we could reuse any of the theorems of the ~ inlinecirc02p family?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We try to limit the number of definitions - do you think it would be wise to add them? I don't know about any other use.

OK, maybe we can provide theorems instead which show the three kinds of construction explicitly.

BTW, do you think we could reuse any of the theorems of the ~ inlinecirc02p family?

Maybe, but the definitions are too different at the moment. Maybe we need a mapping of the different representations first.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK, maybe we can provide theorems instead which show the three kinds of construction explicitly.

I have suggested some theorems in this post which decompose the definition into three subgoals. We don't have the algebraic definition of constructible numbers with towers yet, so they can't be used as is, but maybe we could restate those only in terms of fields. For example, for a line, given by two points, and a circle, given by three points, if these points lie in some subfield of C, then the intersection also lies in quadratic extension of that subfield.

I think we unfortunately can't use inlinecirc02p since we need to keep track of the subfield we are working in.


${
constrtow2.b $e |- B = ( Base ` F ) $.
constrtow2.q $e |- Q = ( CCfld |`s QQ ) $.
constrtow2.a $e |- ( ph -> A e. Constr ) $.
constrtow2.f $e |- ( ph -> F e. Field ) $.
constrtow2.1 $e |- ( ph -> A e. B ) $.
$( If an algebraically constructible point ` A ` is in a field ` F ` , then
there is a tower of quadratic field extensions from ` QQ ` to ` F ` . $)
constrtow2 $p |- ( ph -> E. t e. ( Chain ` `' /FldExt2 ) ( ( t ` 0 ) = Q
/\ ( lastS ` t ) = F ) ) $= ? $.
$}


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Impossible constructions
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
$)

$( Impossibility of doubling the cube. This is expressed by stating that the
cubic root of 2, which is the side length of a cube of volume ` 2 ` , is
not constructible. $)
imp2cube $p |- -. ( 2 ^c ( 1 / 3 ) ) e. Constr $= ? $.

$( Impossibility of trisecting angles. This is expressed by stating that the
cosine of an angle of ` ( _pi / 9 ) ` which would be the third of the
constructible angle ` ( _pi / 3 ) ` , is not constructible. $)
imp3ang $p |- -. ( cos ` ( _pi / 9 ) ) e. Constr $= ? $.
Loading