Danijela Simić
email: danijela@matf.bg.ac.rs

Filip Marić

Pierre Boutry
email: pierre.boutry@inria.fr

Danijela Simi¢

Filip Mari¢

Formalization of the Poincaré Disc Model of Hyperbolic Geometry

Keywords:

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

1 Introduction oinré dis is model of hyperoli geometryF ht ft hs een mtheE mtil folklore for more thn IHH yersF roweverD up to the est of our knowlE edgeD fully preiseD forml proofs of this ft re lkingF glssi mthemtis textooks on geometry usully show only proofEskethes tht lk rigor nd often rely on intuition nd oviousness from the drwn digrmsF wore rigE orous exposition of the sujet @eFgFD WD RHA usully formlize uleinEfeltrmi model nd rgue tht it is muh simpler to formlize thn the oinré disD sine hEetweenness reltion oinides with the iuliden etweenness so ll xioms tht express properties of etweenness re proved esilyF sn this pper we present formliztion of the oinré dis model in sselleGryvD introdue its si notions @hEpointsD hElinesD hEongrueneD hE isometriesD hEetweennessA nd prove tht it models rski9s xioms exept for iulid9s xiomF e show tht is stis(es the negtion of iulid9s xiomD ndD moreoverD the existene of limiting prllels xiomF he model is de(ned within the extended omplex plne @CP 1 AD whih hs een desried quite preisely y hwerdfeger TI nd formlized in the previous work of the (rst two uthors RIF yn the other hndD ll proofs out the properties of the model @most notly the proofs tht rski9s xioms re stis(edA re originlD nd re diret in the sense tht they do not rely on ny other modelsF he whole formliztion is ville from the erhive of porml roofs RPD TRF sn this pper we shll present forml de(nitions of ll relevnt onepts nd forml sttements of ll relevnt lemms nd theoremsF e shll lso outline their proofs in mthemtil prose @often mking some simpli(tions nd introduing some minor impreisions in order to mke them more omE prehensileAF e hope tht this exposition of the oinré dis ould e lso interesting even outside the intertive theorem proving ommunityD nd tht this rtile ould (ll in some gps in the lssi litertureF Related work. elthough the ide of nonEiuliden geometry @suh s hyperE oli geometry tht we fous on in this pperA hs ppered even in nE ient qreeeD heri is the (rst mthemtiin to hve onsidered the se where iulid9s prllel postulte would not hold SWF henD in IVQP nd IVRHD folyi V nd vohevsky QT pulished developments out nonEiuliden geometryF tillD more intense study egn hlf entury lterF his ws most 'eted y pplying the mhinery of omplex numers disovered t the end of the IVth enturyF gomplex numers were n importnt tool for exploring properties of ojets in di'erent geometriesF epling the grtesin oordiE nte plne y omplex plne provided simpler formuls to desrie geometri ojetsF efter qussin theory of urved surfes QH nd iemnn9s work on mnifolds SVD the work of folyi nd vohevsky eme signi(nt nd led to feltrmi9s independene proof of the prllel postulte UF ryperoli geometry is studied through mny of its modelsF he onept of projetive dis model ws introdued y ulein while oinré investigted the hlfEplne model proposed y viouville nd feltrmi nd primrily studied the isomeE tries of the hyperoli plne tht preserve orienttionF sn this pperD we fous on the formliztion of the ltterF here re mny formliztions of frgments of di'erent geometries in the intertive theorem proversF he mjor prt of this reserh hs een deE voted to Euclidean geometry with proly the lrgest lirry S eing out rski9s system of geometry THF his development ws initited during xrE oux9s thesis with the formliztion of the (rst eight hpters RTF vterD the lirry got extended to ontin the results from the (rst twelve hpters ISD thus llowing frun nd xroux to mehnize the link from rski9s xE ioms to rilert9s in goqD feeson hs lter written note Q to demonstrte tht the min results to otin rilert9s xioms re ontined in THF henD thnks to the formliztion of ppus9 theorem ITD the third uthorD frun nd xroux ompleted the formliztion of the (rst prt of TH with the rithmetiztion of iuliden geometry IHD thus pving the wy for the use of lgeri utomted dedution methods in syntheti geometryF woreoverD the lirry lso ontins the link from rilert9s xioms to rski9s IR s well s studies out deidility properties IPD prllel postultes IH nd ontinuity xioms QIF yther developments sed on rski9s system of geometry hve een rE ried outF por exmpleD ihterD qrowski nd elm hve ported some of these goq proofs to wizr @fortyEsix lemmsA SUF woreoverD feeson nd os proved PHH lemms of the (rst twelve hpters of TH with the ytter theorem prover TF pinllyD tojnovi¢EÐurevi¢D xroux nd tni£i¢ TS generted utomtilly some redle proofs in rski9s system of geometryF ome formliztion of rilert9s foundtions of geometry hve een proE posed y hehlingerD hufourd nd hrek PQ in the goq proof ssistntD nd y hixonD weikle nd pleuriot RR using sselleGryvF hehlingerD hufourd nd hrek hve studied the formliztion of rilert9s foundtions of geomeE try in the intuitionisti setting of goq PQF hey fous on the (rst two groups of xioms nd prove some etweenness propertiesF weikle nd pleuriot hve done similr study within the sselleGryv proof ssistnt RRF hey went up to twelfth 1 theorem of rilert9s ookF ott hs ontinued the formlizE tion of weikle using sselleGryv nd revised it TPF re hs orreted some sutle errors in the formliztion of qroup sss y weikleF ott ws interE ested in trying to otin redle proofsF vterD he developed system within the ryvEvight proof ssistnt to utomtilly (ll some gps in the inidene proofs TQF woreover ihter hs formlized sustntil numer of results sed on rilert9s xioms nd metri xiom system using ryvEvight STF pinllyD von lto9s onstrutive geometry TU hs een formlized in goq y uhn QSF fesides iuliden geometryD projective geometry hs lso een explored using proof ssistntsF wgudD xroux nd hrek proposed lterntives to the trditionl xiom systems PH for plne nd spe projetive geometry sed on the notion of rnks nd veri(ed using goq tht hesrgues9 property holds in the ltter QWF he mutul interpretility of their systems with the trditionl ones ws then formlly proved y frunD wgud nd hrek in goq IQF hespite not eing rnhes of geometryD two (elds strongly onneted to geE ometry hve een the ojet of signi(nt formliztion e'ortsX nonEstndrd nlysis nd omputtionl geometryF Non-standard analysis is the (eld dedE ited to the nlysis of in(nitesimls through hyperrel numersF pleuriot formlized notions of nonEstndrd nlysis in geometry in sselle to mehE nize the geometri prt of xewton9s Principia PU nd uepler9s lw of iqul eres PT using methods of utomted theorem provingF edditionllyD the disrete model of the ontinuum known s the rrthongEee line hs een formlized in goq y wgudD ghollet nd puhs QV nd in sselle y pleuE riot PVF Computational geometry is the study of dt strutures nd lgoE rithms used for solving geometri prolemsF sn goqD the formliztion of omiE ntoril mps nd hypermps hve een rried out y uitg nd hufourd SS s well s hehlinger nd hufourd PPD nd hufourd PRD respetivelyF hese strutures hve llowed to formlly prove the orretness of severl lgorithms suh s the plne heluny tringultion lgorithmD studied y hufourd nd fertot PS in goqF purthermoreD vrious onvex hull lgorithms hve lso een proved orret y ihrdie nd fertot SR in goqD y weikle nd pleuriot RS in sselleD nd y frunD hufourd nd wgud IU in goqF here re severl formliztions of nonEiuliden geometryF sn his w thesisD wkrios used sselleGryv to show formlly the independene of iuE lid9s xiom RHD y proving tht the ulein!feltrmi model is model of rski9s xioms exept his iuliden xiomF he strting point of this work ws the formliztion of the projetive plne RP 2 D in whih the ulein!feltrmi model is de(nedF oints re represented y their homogeneous oordintesD s quotients of nonEzero vetors in R 3 over the vetor proportionlity reltionF gollinetionsD invertile liner trnsformtion from the projetive plne to itE selfD re represented y equivlene lsses of 3 × 3 invertile rel mtriesF he ollinetions form group nd preserve inideneF ulein!feltrmi model of the hyperoli plne relies on (xing ijetion etween the grtesin plne nd the projetive plne with one line removedD nd nturl ijetion @mpE ping (x, y) to (x, y, 1)A is hosenF he set of points of the hyperoli plne is represented y the open unit dis in R 2 D or y its imge in the projetive plneD ording to the nturl ijetionF fetweenness of the hyperoli plne is lifted from etweenness in the grtesin plneF rski9s etweennessEonly xiomsD lredy veri(ed in the grtesin plneD were esy to lift to equivlent results in the ulein!feltrmi modelF roweverD the de(nition of ongruene depends on ollinetions tht mp the unit dis to itself nd this de(nition proved to e di0ult to work withF he de(nition of distne is sed on rossE rtio in the projetive plne @insted of distne itselfD its hyperoli osine ws usedAF elthough the formliztion followed forsuk nd zmielew9s textE ook PWD some proofs were missingD some were inomplete nd others were di0ult to formlize some originl proofs hd to e inventedF ome proofs re rther involved @most notlyD the proof tht the model stis(es the xiom of segment onstrutionD the (veEsegments xiomD nd the upper PEdimensionl xiomA nd they use the de(nition nd properties of perpendiulrity @hyperE oli ythgor9s theorem nd hyperoli lw of osinesAF ine the min gol ws to show the independene of iulid9s xiomD nd not to investigte hyE peroli geometryD it ws not proved tht limiting prllels postulte holds in the uleinEfeltrmi modelF he formliztion lso does not de(ne irlesD line intersetionD distne @exept its hyperoli osineA nor nglesF fsed on the work of wkriosD rrrison hs shown the independene of iulid9s xiom in ryvEvightD nd goghetto formlized the uleinEfeltrmi model within wizr IVD IWF en exhustive desription of the existing formliztions of geometry is given y xrouxD tni£i¢ nd pleuriot RUF Outline of the paper. he rest of the pper is strutured s followsF sn etion P we introdue si onepts of sselleGryv relevnt for the present formlE iztionD introdue rski9s xioms of geometryD nd summrize min results of the previous work of the (rst two uthors on formliztion of the extended omplex plne geometry RI tht re relevnt for the present formliztionF sn etion Q we de(ne the oinré dis model @its pointsD linesD distneD nd etweennessD nd prove their propertiesAF sn etion R we prove tht oinré model stis(es rski9s xiomsF sn etion S we drw onlusions nd indite possile diretions for further workF 2 Background PFI sselleGryv sselle SPD SQ is generi ssistnt prover tht hs numerous speilizE tions for di'erent logisD ut is most developed for higherEorder logiD ssE elleGryv SHD RWF pormliztion of mthemtil theory onsists of giving de(nitions of new onepts @typesD onstntsD funtionsD etFA nd providing proofs tht justify them @lemmD theoremsD etFAF heories re usully deE sried in the lnguge Isar TV whih is prt of the sselleGryv nd whih llows writing strutured nd redle proofsF st is very well dpted for usul mthemtil nottionF sselleGryv hs n extensive lirry of theories tht is onstntly inresing nd is ville through the erhive of porml roofs 2 F ryv is typed logiD with mny prede(ned types ville in the lirryD suh s bool @foolen vlues true nd flseAD int @integer numersAD rat @rtionl numersAD real @rel numersAD nd complex @omplex numersAF sn this pper we shll use rel nd omplex numersF smginry numer is denoted y iiF gonversion from rel numer to omplex numer is denoted y corD rel nd imginry prt of omplex numer y Re nd ImD the omplex onjugte z of z y cnjD modulus of omplex numer |z| y cmodD nd the omplex rgument of the numer with arg @in the sselleGryv is lwys in the intervl (-π, π]AF e omplex funtion for the sgn determines the omplex numer on single irle tht hs the sme rgument s well s the given nonE zero omplex numer @iFeD sgn z a z/|z|AF puntion cis pplied to α lultes cos α + ii• sin αF he determinnt of mtrix |M | is denoted y mat_detD nd the djoint mtrix @onjugte trnsposeA M * is denoted y mat_adjF e set of elements of type 'a is denoted y 'a setF hi'erene sets re denoted y X -Y D nd the imge of the funtion f over the set X is denoted with f 'XF he produt type is mrked with τ 1 × τ 2 @where τ 1 nd τ 2 re types of setsAF he type of funtions is denoted s τ 1 ⇒ τ 2 F puntions re urried nd funtion pplition within terms is minly written in pre(x form f x @insted of f (x)D whih is loser to the stndrd mthemtil nottionAD s it is often the se with funtionl progrmmingF he terms re λEexpressions with expnded syntxF sn spite of the supE ported type dedution mehnismD it is sometimes neessry expliitly stte the type of the termF o express tht some term t hs τ typeD we write t :: τ F he funtion strtion e written in form λx. f xF erms lso support let-constructionsX let x = t in u whih is equivlent to u in whih ll free oE urrenes re vrile x re repled y tD ifthenelse expressionsX if b then t 1 else t 2 D where type for b must e boolD nd t 1 nd t 2 must e the sme typeD nd case expressionsX case e of c 1 ⇒ e 1 | c 2 ⇒ e 2 | ...| c n ⇒ e n D tht hs the vlue e i if e is equl to some c i F vogil formuls re terms of type bool nd re written in stndrd nottionF upported onnetives re ∧D ∨D ¬D -→D the qunti(ers re ∀ nd ∃D nd the expression ∃! x. P x denotes tht there is extly one x tht meets the predite P F elsoD there re rilert9s de(nite nd inde(nite desription opertors @T HE x. P x denotes the unique vlue x tht stis(es the predite P AF he type_synonym onstrution introdues new nme for lredy existing typeF Subtypes of given type n e lso formed y the typedef onstruE tion @eFgFD the type of m × n nonEdegenerte mtries onsists of ll m × n mtries tht hve nonEzero determinntAF he lifting/transfer pkge QR tht filittes de(ning nd using sutypes is ville within the min ssE elleGryv distriutionF puntions ting on the sutype re de(ned y liftE ing funtion de(nitions given on the widerD rrier type @y using ommnds setup_liftingD lift_definitionAF iFgFD de(ning inverse mtrix would reE quire giving de(nition for every mtrixD nd then lifting it to nonEdegenerte mtries where it is wellEde(nedF enother wy to introdue new typesD often used in mthemtisD re quoE tient typesF por exmpleD positive rtionl numers iFeFD frtions re quotient of pirs of nturl numersD where two pirs re identi(ed if they nel out to the sme irreduile frtionF upport for working with quotient types is lso provided y the liftingGtrnsfer pkgeF o de(ne quotientEtype one must (rst de(ne reltion over the rrier typeD prove tht it is n equivlene reltion nd then use the quotient_type ommndF puntion over quotient types re de(ned y (rst de(ning funtions on the rrier typeD nd then usE ing lift_definition ommnd to utomtilly otin the de(nition of the funtion ting on the quotient type @howeverD it must e proved tht the de(nition does not depend on the hoie of representtivesAF he(nitions re given using the syntx denition x :: τ where "x = . . ."

where x is the onstnt or the funtion of the type τ D tht is de(nedF vemms re given using syntxX lemma name xes vars assumes assms shows concl where name is the nme of the lemmD vars onditions tht pplyD assms ssumptionsD nd concl is the onlusion of the propositionF sf there re no ssumptionsD the keyword shows n e omittedF elsoD we will use the synE tx lemma "

A2 Pseudo-Transitivity AB ≡ CD ∧ AB ≡ EF ⇒ CD ≡ EF A3 Cong Identity AB ≡ CC ⇒ A = B A4 Segment construction ∃E, A B E ∧ BE ≡ CD A5 Five-segment AB ≡ A B ∧ BC ≡ B C ∧ AD ≡ A D ∧ BD ≡ B D ∧ A B C ∧ A B C ∧ A = B ⇒ CD ≡ C D A6 Between Identity A B A ⇒ A = B A7 Inner Pasch A P C ∧ B Q C ⇒ ∃X, P X B ∧ Q X A A8 Lower Dimension ∃ABC, ¬A B C ∧ ¬B C A ∧ ¬C A B A9 Upper Dimension AP ≡ AQ ∧ BP ≡ BQ ∧ CP ≡ CQ ∧ P = Q ⇒ A B C ∨ B C A ∨ C A B A10 Euclid A D T ∧ B D C ∧ A = D ⇒ ∃XY, A B X ∧ A C Y ∧ X T Y A11 Continuity ∀ΞΥ, (∃A, (∀XY, ΞX ∧ Υ Y ⇒ A X Y )) ⇒ ∃B, (∀XY, ΞX ∧ Υ Y ⇒ X B Y )
le IX rski9s xiom system for iuliden geometryF he symmetry xiom for equidistne @eI on FIA together with the trnsitivity xiom for equidistne eP imply tht the equidistne reltion is n equivlene reltion etween pir of pointsF he identity xiom for equidistne eQ ensures tht only degenerte segE ments n e ongruent to degenerte segmentF ine we will de(ne the ongruene y formul of the form f (A, B) = f (C, D) for some funtion f stisfying tht f (x, x) = 0 for every xD these properties will e esy to verifyF

A D B C E A B C D E
pigF IX exiom of segment onstrution eRF he xiom of segment onstrution eR llows to extend segment y given length @pigF I 3 AF rereD properties out wöius trnsformtions will llow to simplify the proof using without loss of generality resoningF [START_REF] Beeson | Proving Hilbert's axioms in Tarski geometry[END_REF] To highlight the fact that all of the axioms except for Euclid's axiom indeed denes a neutral geometry we provide gures both in the Euclidean model and a non-Euclidean model, namely the Poincaré disc model. The gure on the left hand side illustrates the validity of the axiom in Euclidean geometry. The gure on the right hand side either depicts the validity of the statement in the Poincaré disc model or exhibits a counter-example. he (veEsegment xiom eS orresponds to the wellEknown ideEengleEide postulte ut is expressed with the etweenness nd ongruene reltions onlyF he lengths of ABD AD nd BD nd the ft tht A B C (x the ngle ∠CBD @pigF PAF por proving tht this xiom holds in our modelD ruil point will e tht in the oinré dis modelD the segment ongruent to given segment in the model form iuliden irleF he identity xiom for etweenness eT expresses tht the only possiility to hve B etween A nd A is to hve A nd B equlF st lso insinutes tht the reltion of etweenness is nonEstritD unlike rilert9s oneF es feeson suggests in RD this hoie ws proly mde to hve redued numer of xioms y llowing degenerte ses of the sh9s xiomF his property will follow esily from our de(nition of etweennessF pigF QX sh9s xiom eUF he inner form of sh9s xiom eU is the xiom sh introdued in SI to repir the defets of iulidF st intuitively sys tht if line meets one side of tringleD then it must meet one of the other sides of the tringleF here re three forms of this xiomF hnks to qupt9s thesis QPD one knows tht the inner form nd the outer form of this xiom re equivlent nd tht oth of them llow us to prove the wek formF he inner form enunites sh9s xiom without ny se distintionF sndeedD it indites tht the line BP must meet the tringle ACQ on the side AQD s Q is etween B nd C @pigF QAF ogether with iulid9s xiomD this xiom will e the one requiring the iggest e'ort s it requires to prove the intersetion of hElinesF he lower twoEdimensionl xiom eV sserts tht the existene of three nonEolliner pointsF ine our de(nition of etweenness only llows for hE olliner points to e hEetweenD this xiom will e proved to hold in our model mostly through lultionsF pigF SX rski9s prllel postulte eIHF iulid9s xiom eIH @pigF SA is modi(tion of n impliit ssumption mde y vegendre while ttempting to prove tht iulid9s prllel postulte ws onsequene of iulid9s other xiomsF eording to wprlndD wprE lnd nd mith RQD the suggestionD mde y qupt QP nd othersD tht this postulte is due to vorenz QU is doutfulF sn ftD the sttement to whih qupt refers seems to e the one given in PI whih is indeed di'erentF hile there exist mny sttements equivalent to the prllel postulteD this version is prtiulrly interestingD s it hs the dvntges of eing esily expressed only in term of etweennessD nd eing vlid in spes of dimension higher thn twoF roweverD we will see tht version eing expressed with oth etweenness nd ongruene n e esier to work withF he ontinuity xiom eII orresponds to the geometri version of hedekind9s utsF e should remrk tht hereD Ξ nd Υ orrespond to (rstEorder formuE lsF his restrition ws mde with view to otin very importnt metE theoretil property for the theoryX its ompletenessF es it ould e expetedD this restrition wekens the xiom QIF eginD properties out wöuis trnsE formtions will e helpful to simplify this proofF ryperoli geometry is hrterized y the existene of limiting prllelsF e ry Aa is limiting prllel to ry Bb if they lie on distint lines not equl to the line ABD they do not meetD nd every ry in the interior of the ngle BAa meets the ry BbF sn oinré modelD two rys re limiting prllels i' they meet on the soluteF he existene of limiting prllels xioms sttes tht for eh line X 1 X 2 nd eh point A not on tht lineD there exist two rysD not lying on sme lineD tht re limiting prllels to rys on the line

X 1 X 2 F X1 X2 A
pigF TX ixistene of limiting prllels e speify rski9s xioms in two lolesF he (rst one ssumes ll xioms exept for the iulid9s xiom nd the ontinuity xiom nd orresponds to solute geometryD the seond one dds the negtion of iulid9s xiom nd the existene of limiting prllels to orrespond to hyperoli geometry nd the third one then dds the ontinuity xiom to orrespond to elementry hyperoli geometryF locale TarskiAbsolute = xes cong :: "'p ⇒ 'p ⇒ 'p ⇒ 'p ⇒ bool" xes betw :: "'p ⇒ 'p ⇒ 'p ⇒ bool" assumes cong_reflexive: "cong x y y x" assumes cong_transitive: "cong x y z u ∧ cong x y v w -→ cong z u v w" assumes cong_identity: "cong x y z z -→ x = y" assumes segment_construction: "∃ z. betw x y z ∧ cong y z a b" assumes five_segment:

"x = y ∧ betw x y z ∧ betw x' y' z' ∧ cong x y x' y' ∧ cong y z y' z' ∧ cong x u x' u' ∧ cong y u y' u' -→ cong z u z' u'" assumes betw_identity: "betw x y x -→ x = y" assumes Pasch: "betw x u z ∧ betw y v z -→ (∃ a. betw u a y ∧ betw x a v)" assumes lower_dimension:

"∃ a. ∃ b. ∃ c. ¬ betw a b c ∧ ¬ betw b c a ∧ ¬ betw c a b"
assumes upper_dimension: PFQ pormliztion of the extended omplex plne heep onnetions etween omplex numers nd geometry hd een well known nd refully studied enturies goF pundmentl ojets tht re inE vestigted re the omplex plne @usully extended y single in(nite pointAD its ojets @pointsD lines nd irlesAD nd groups of trnsformtions tht t on them @eFgFD inversions nd wöius trnsformtionsAF sn the previous work of the (rst two uthors RID the geometry of the extended omplex plne C is formlized s omplex projetive line CP 1 @y using homogeneous oordintesAF st is shown tht it is equivlent to the omE plex plne C extended y n dditionl element @treted s the in(nite pointAD nd to the iemnn sphere @y mens of the stereogrphi projetion RVD TIAF sn the present formliztion we hve updted this previous work nd simpliE (ed mny de(nitions y using liftingGtrnsfer pkge QR for oth sutypes nd quotient typesF 2.3.1 Extended complex plane he extended complex plane C is identi(ed with omplex projetive line " the oneEdimensionl projetive spe over the omplex (eldD sometimes denoted y CP 1 F ih point of CP 1 is represented y a pair of complex homogeneous coordinates @not oth equl to zeroAF wo pirs of homogeneous oordintes represent the sme point in C i' they re proportionl y nonE zero omplex ftorF pormliztion of this is done in severl stgesF pirstD the type synonym for pirs of omplex numers is introduedX type_synonym cvec2 = "complex × complex" xextD equivlene of two pirs of omplex numers is de(ned @they re equivlent i' they re proportionlD where multiplition of the omplex vetor y omplex slr is done omponentwiseAF denition eq_cvec2 :: "cvec2 ⇒ cvec2 ⇒ bool" where

"cong x u x v ∧ cong y u y v ∧ cong z u z v ∧ u = v -→ betw x
"eq_cvec2 z 1 z 2 ⇐⇒ (∃ k::complex. k = 0 ∧ z 2 = k * z 1 )"
st is rther strightforwrd to prove tht this is n equivlene reltionF xextD the type of nonEzero omplex vetors is de(ned s sutype @these represent homogeneous oordintes of points in CP 1 AX typedef hc = "{v::cvec2. v = (0, 0)}" he equivlene of pirs of omplex numers is esily lifted to this sutypeX setup_lifting type_definition_hc lift_denition eq_hc :: "hc ⇒ hc ⇒ bool" is eq_cvec2 st is esily proved tht this is lso n equivlene reltionF pinllyD the elements of the extended omplex plne re de(ned s equivE lene lsses of the eq_hc reltion nd the extended omplex plne is de(ned y the following quotient typeX quotient_type cp1 = hc / eq_hc he innity point is de(ned y lifting the homogeneous oordintes (1, 0)X denition inf_cvec2 :: "cvec2" ("∞v") where "inf_cvec2 = (1, 0)" lift_denition inf_hc :: "hc" ("∞ hc ") is inf_cvec2 lift_denition inf :: "cp1" ("∞ h ") is inf_hc ih lifting to quotient type requires to prove tht the de(nition does not depend on the hoie of representtiveF hese proofs re sometimes tediousD ut usully strightforwrdD so we will not disuss themF yther distinguished elements of the extended omplex plne @0D 1 nd iA re de(ned in the sme mnnerF he conversion between the ordinary complex numbers and points in the extended complex plane is lso de(ned4 F denition of_complex_cvec2 :: "complex ⇒ cvec2"

where "of_complex_cvec2 z = (z, 1)" lift_denition of_complex :: "complex ⇒ cp1" is . . . erithmeti opertions on ordinry omplex numers @dditionD sutrE tionD multiplitionD nd divisionA re extended to the extended omplex plne nd re de(ned over homogeneous oordintesF por exmpleD addition is deE (ned in the following wyF denition add_cvec2 :: "cvec2 ⇒ cvec2 ⇒ cvec2" where

"add_cvec2 z w = (let (z 1 , z 2 ) = z; (w 1 , w 2 ) = w in if z 2 = 0 ∨ w 2 = 0 then (z 1 *w 2 + w 1 *z 2 , z 2 *w 2 ) else (1, 0))" lift_denition add :: "cp1 ⇒ cp1 ⇒ cp1" is . . . Ratio of omplex numers zD v nd w is de(ned s z-v z-w nd the cross- ratio of omplex numers zD uD vD nd w s (z-u)(v-w) (z-w)(v-u)
F his is extended to homogeneous oordintes nd points in the extended omplex plneF

denition cross_ratio_cvec2 :: "cvec2 ⇒ cvec2 ⇒ cvec2 ⇒ cvec2 ⇒ cvec2" where "cross_ratio_cvec2 z u v w = (let (z 1 , z 2 ) = z; (u 1 , u 2 ) = u; (v 1 , v 2 ) = v; (w 1 , w 2 ) = w; n 1 = z 1 *u 2 -u 1 *z 2 ; n 2 = v 1 *w 2 -w 1 *v 2 ; d 1 = z 1 *w 2 -w 1 *z 2 ; d2 = v 1 *u 2 -u 1 *v 2 in if n 1 * n 2 = 0 ∨ d 1 * d 2 = 0 then (n 1 * n 2 , d 1 * d 2 ) else (1, 1))" lift_denition cross_ratio :: "cp1 ⇒ cp1 ⇒ cp1 ⇒ cp1 ⇒ cp1" is . . .
foth opertions re very importnt in the extended omplex plne @rossErtio is hrterizing invrint of wöius trnsformtions " the fundmentl lss of trnsformtions of CD nd it is possile to de(ne lines using rtio sine rtio is rel i' the three points re on the sme line nd irles using rossErtio of points sine the rossErtio is rel i' the four points re on the sme irle or lineAF e re going to use rossErtio in our formliztion of the oinré dis model nd in de(nition of its entrl onepts @distne nd etweennessAF 2.3.2 Möbius transformations sn our formliztion Möbius transformations re introdued lgerillyD s liner trnsformtions of homogeneous oordintesF ih trnsformtion is represented y regulr @nonEsingulrD nonEdegenerteA 2 × 2 mtrixF roporE tionl mtries @y nonEzeroD omplex slrA represent the sme trnsforE mtionF egin we need to use severl stges of de(nitionsF pirst we introdue the sutype of nonEdegenerte omplex 2 × 2 mtries @represented y qudruples of omplex numersAF typedef cmat2 = "complex × complex × complex × complex" typedef mmat2 = "{M ::cmat2. mat_det M = 0}" xext we sy tht two omplex mtries re equivlent i' they re proE portionl y nonEzero omplex slrD nd then lift this to the sutype of nonEdegenerte mtriesF denition eq_cmat2 :: "cmat2 ⇒ cmat2 ⇒ bool" where

"eq_cmat2 A B ←→ (∃ k::complex. k = 0 ∧ B = k * A)" lift_denition eq_mmat2 :: "mmat2 ⇒ mmat2 ⇒ bool" is . . . pinlyD wo ¤
ius trnsformtions re introdued y quotient type over this reltionF quotient_type moebius = mmat2 / eq_mmat2 wöius trnsformtions form group under omposition @neutrl element orresponds to the identity mtrixD inverse element to inverse mtrixD nd omposition orresponds to mtrix multiplitionAF his group is lled the projective general linear group nd denoted y P GL(2, C)F wöius trnsformtions t on the points of the extended omplex plneF e mtrix M trnsforms homogeneous oordintes z to homogeneous oordintes M • zF hereforeD we (rst de(ne tions of mtries to vetors of homogeneous oordintes @y mtrixEvetor multiplitionA nd then lift tht to quotient typesF denition mobius_pt_cmat2_cvec2 :: "cmat2 ⇒ cvec2 ⇒ cvec2" where

"mobius_pt_cmat2_cvec2 M z = M * z" lift_denition mobius_pt :: "mobius ⇒ cp1 ⇒ cp1" is . . .
zeroD rermitin mtrix A B C D @ mtrix is rermitin if H * = HAF
yur formliztion gin proeeds in three stgesF pirstD the type of rerE mitinD nonEzero mtries is introdued @s sutype of ll omplex 2 × 2 mtriesAF denition hermitian :: "cmat2 ⇒ bool" where "hermitian A ←→ mat_adj A = A" typedef hmat2 = "{H :: cmat2. hermitian H ∧ H = mat_zero}" wtries proportionl y rel nonEzero slr re onsidered equivlentF denition real_eq_cmat2 :: "cmat2 ⇒ cmat2 ⇒ bool" where

"real_eq_cmat2 A B ⇐⇒ (∃ k::real. k = 0 ∧ B = cor k * A)" lift_denition real_eq_hmat2 :: "hmat2 ⇒ hmat2 ⇒ bool" is . . .
st is esily shown tht this is n equivlene reltionD nd irlines re de(ned y quotient onstrution s its equivlene lssesF quotient_type circline = hmat2 / real_eq_hmat2 emong ll irlines most prominent ones re the unit circleD x-axisD nd y-axisF por exmpleD denition unit_circle_cmat2 :: cmat2 where "unit_circle_cmat2 = (1, 0, 0, -1)" lift_denition unit_circle :: circline is . . . denition x_axis_cmat2 :: cmat2 where "x_axis_cmat2 = (0, ii, -ii, 0)" lift_denition x_axis :: circline is . . . ih irline de(nes the set of points on the circline @these re the points whose homogeneous oordintes stisfy the reltion z * Hz = 0AF denition on_circline_cmat2_cvec2 :: "cmat2 ⇒ cvec2 ⇒ bool" where "on_circline_cmat2_cvec2 H z ←→ (vec_cnj z) * H * z = 0" lift_denition on_circline :: "circline ⇒ cp1 ⇒ bool" is . . . denition circline_set :: "circline ⇒ cp1 set" where

"circline_set H = { z. on_circline H z }"
he sign of the determinnt of representtive rermitin mtrix deterE mines the circline typeF el irlines hve the type -1 nd ontin in(nitely mny pointsD point irlines hve the type 0 nd ontin single point nd imginry irlines hve the type 1 nd do not ontin ny pointsF e hve lso de(ned oriented irlinesF hey re lso de(ned y rermitin mtriesD ut they stisfy weker equivlene reltion @they re equivlent i' they re proportionl y positive rel slrAF denition pos_eq_cmat2 :: "cmat2 ⇒ cmat2 ⇒ bool" where

"pos_eq_cmat2 A B ⇐⇒ (∃ k::real. k > 0 ∧ B = cor k * A)" lift_denition pos_eq_hmat2 :: "hmat2 ⇒ hmat2 ⇒ bool" is pos_eq_cmat2 quotient_type ocircline = hmat2 / pos_eq_hmat2
he most importnt oriented irlines re the positively oriented unit circleD positively oriented x-axis nd positively oriented y-axisF por exmpleD lift_denition ounit_circle :: "ocircline" is unit_circle_hmat2 ih oriented irline divides the extended omplex plne to three sets of pointsX its interiorD its exterior nd points on the irlineF snterior of n oriented irline is its disc nd is de(ned in the following wyF denition in_ocircline_cmat2_cvec2 :: "cmat2 ⇒ cvec2 ⇒ bool" where

"in_ocircline_cmat_cvec H z ←→ Re ((vec_cnj z) * H * z) < 0" lift_denition in_ocircline :: "ocircline ⇒ cp1 ⇒ bool" is . . . denition disc :: "circline ⇒ cp1 set" where "disc H = { z. in_ocircline H z }"
e shll uild the oinré model within the unit disF denition unit_disc :: "cp1 set" where "unit_disc = disc ounit_circle" engle etween two irlines nd oriented ngle etween oriented irlines is de(ned lgerillyD in terms of determinnts of irline mtries @for the detils we refer the reder to the previous work of the (rst two uthors RID or hwerdtfeger TIAF 2.3.4 Möbius action on circlines wöius trnsformtions lso act on circlines nd oriented irlines @using mE trix congruence opertionAF denition congruence where "congruence M H ≡ mat_adj M * H * M " denition moebius_cl_cmat2_cmat2 :: "cmat2 ⇒ cmat2 ⇒ cmat2" where "moebius_cl_cmat2_cmat2 M H = congruence (mat_inv M ) H" lift_denition moebius_cl :: "moebius ⇒ circline ⇒ circline" is . . . he following lemm onnets wöius trnsformtion of points nd of irlines @nd sillyD shows tht wöius trnsformtions mp irlines to irlinesAF

lemma "mobius_pt M `circline_set H = circline_set (mobius_cl M H)"
wöius trnsformtions re conformal nd preserve ngle etween irE linesF e re speilly interested in trnsformtions tht mp the unit irle to itselfF fy the fundmentl theorem of projetive geometry only suh trnsE formtions tht mp irlines to irlines re either wöius trnsformtions or ompositions of wöius trnsformtions nd the conjugation @its tion on the irlines is de(ned in the following wyAF fun conjugate_cl_cmat2 :: "cmat2 ⇒ cmat2" where where

"unit_circle_fix_cmat2 M ←→ (∃ k::complex. k = 0 ∧ congruence M (1, 0, 0, -1) = k * (1, 0, 0, -1))" lift_denition unit_circle_fix :: "moebius ⇒ bool" is . . . lemma "unit_circle_fix M ←→ moebius_cl M unit_circle = unit_circle"
hese trnsformtions form groupF sts importnt sugroup onsists of soElled Blaschke factorsF he reiprotion n e onsidered speil se of flshke ftor @the in(nity is mpped to zeroD nd the unit irle is preE servedAF ih unitEirle preserving wöius trnsformtion is omposition of flshke ftor @ trnsformtion tht rings some point tht is not on the unit irle to zeroAD nd rotation round the originF denition blaschke_cmat2 :: "complex ⇒ cmat2" where "blaschke_cmat a = (if cmod a = 1 then (1, -a, -cnj a, 1) else eye)" lift_denition blaschke :: "complex ⇒ moebius" is . . . denition rotation_cmat2 :: "real ⇒ cmat2" where "rotation_cmat2 φ = (cis φ, 0, 0, 1)" lift_denition rotation :: "real ⇒ ⇒ moebius" is . . . rnsformtions tht preserve the orienttion of the unit irle mp the unit dis onto itselfD while trnsformtions tht hnge the orienttion of the unit dis exhnge the unit dis nd the re outside the unit irleF gentrl trnsformtions of the oinré dis model will e the ones tht map the unit disc onto itselfF eginD they n e reognized from their mtries @the hve the form s eforeD ut dditionlly it must hod tht |a| 2 > |b| 2 AF lift_denition unit_disc_fix :: "moebius ⇒ bool" is . . . lemma assumes "unit_disc_fix M" shows "moebius_pt M `unit_disc = unit_disc" hese trnsformtions lso form group nd eh of them n e deomE posed to rottion round the origin nd flshke ftors tht mps point within the unit dis to zeroF lemma assumes "unit_disc_fix M" shows "∃ k φ. cmod a < 1 ∧ M = moebius_rotation φ + blaschke a" sn the formliztion of extended omplex plne mny other importnt onE epts were formlly veri(ed @the hordl metri relevnt for ellipti geomeE tryD iuliden similrities relevnt for iuliden geometryD onnetions to the iemnn sphereD onnetions etween wöious trnsformtions nd iemnn sphere rottionsD irlines onnetion with irles nd linesD reltions etween wöius trnsformtions nd the orienttionA ut we re not going to explin those detils here nd refer the reder to the previous work of the (rst two uthors RIF PFR log resoning hen reson out geometry lgerilly in terms of oordintesD often the hoie of pproprite oordinte system mkes the resoning muh more menleF e extensively used without loss of generality @wlogA tehniqueD desried y tohn rrrison QQF log resoning ws extensively used in our formliztion of the extended omplex plne RIF por exmpleD if property is preserved under wöius trnsformtionsD then insted of showing tht the property holds for ny three di'erent pointsD one n show tht the property holds only for points 0 h D 1 h D nd ∞ h @looking from nother perspetiveD the oordinte system on the omplex projetive line n e hosen so tht ny tree di'erent points hve oordintes 0 h D 1 h D nd ∞ h AF his resoning is formlized y the following lemmF lemma xes M::moebius assumes "P 0 h 1 h ∞ h " and "z1 = z2" and "z2 = z3" and "z1 = z3" assumes " M a b c. P a b c =⇒

P (moebius_pt M a) (moebius_pt M b) (moebius_pt M c)"
shows "P z1 z2 z3" yne this rule pplied s (rst step in proof of some sttement out three di'erent pointsD it redues it to two simpler sugols @proving the stteE ment for speil points 0 h D 1 h D nd ∞ h nd proving tht the property is preE served under wöius trnsformtionsAF eutomted ttis n e developed to prove preservne under wöius trnsformtionsD ut we did not do tht in our formliztionF reservne of derived properties is usully proved quite esily y the sselleGryv simpli(erD using the set of lemms tht prove preservne for elementry properties @likeD for exmpleD inideneAF log resoning will e one of the entrl tehniques tht we will use in the formliztion of the oinré disD nd we will formulte nd use mny di'erent wlog lemms tht simplify our proofs @we n freely sy tht without wlog resoning our proof would not hve een possileAF ome of them will e shown in the pperD while others re ville in the forml proof douments TRF 3 Formalization of the Poincaré disc QFI hEpoints nd hElines fsi ojets in the oinre model of the hyperoli plne re h-points nd h-linesF rEpoints re points of the extended omplex plne tht lie within the unit disF typedef h_point = "{z::cp1. z ∈ unit_disc}" rElines re irlines tht re represented y rermitin mtries of the form

H = A B B A , for A ∈ RD nd B ∈ CD nd |B| 2 > A 2 D
where the irline eqution is the usul oneX z * Hz = 0F hereforeD eh hEline is determined y rel prmeter AD nd omplex prmeter BF denition mk_h_line_cmat2 :: "real ⇒ complex ⇒ cmat2" where

"mk_h_line_cmat2 A B = (cor A, B, cnj B, cor A)"
uh mtrix is lwys rermitin nd is nonEzero if one of A or B is nonE zeroF e introdue the predite tht heks if given omplex mtrix is mtrix of hElineD nd then y mens of the lifting pkge lift it to the type of nonEzero rermitin mtriesD nd then to irlines @tht re equivlene lsses of suh mtriesAF eginD lifting requires us to prove tht the predite does not depend on the hoie of representtiveD ut tht is quite trivil to dishrgeF denition is_h_line_cmat2 :: "cmat2 ⇒ bool" where

"is_h_line_cmat2 H ←→ (let (A, B, C, D) = H in hermitian (A, B, C, D) ∧ A = D ∧ (cmod B) 2 > (cmod A) 2 )"
lift_denition is_h_line :: "circline ⇒ bool" is . . . e de(ne sutype of irlines tht ontins only hElinesD nd then lift irline opertions to this typeF por exmpleD hEinidene is de(ned y lifting the on_circline predite @tht heks if point in CP 1 lies on the given irlineAF typedef h_line = "{ H. is_h_line H }" lift_denition h_incident :: "h_line ⇒ h_point ⇒ bool" is on_circline wost lemms in the further text will e presented in their unlifted form iFeFD ll our results shll e proved for irlines nd points in CP 1 nd their types @circline nd cp1A nd shll ontin expliit gurds @. . . ∈ unit_disc nd is_h_line . . .A in their ssumptions nd onlusionsF fy mens of the liftingGtrnsfer pkge their lifting to the h_point nd h_line type eomes lmost immediteF he fundmentl hrteriztion of hElines is tht irline is n hEline i' it is rel @negtiveEdeterminntA irlineD perpendiulr to the unit irE le @where perpendiulrity of irlines is de(ned y mens of ngle etween themAF lemma shows "is_h_line H ←→ circline_type H = -1 ∧ perpendicular H unit_circle" his is n esy onsequene of our purely lgeri de(nition of the ngle etween irlines nd the irline type @oth re de(ned y mens of deterE minnts of irline representtive mtriesAF his hrteriztion enles us to swith from lgeri to geometri proofs nd use the pproh tht gives simpler proofsF he following results re simple onsequenes of the previous hrterizE tionF he xExis is n hElineD while the unit irle is notF ih hEline ontins t lest two di'erent points within the unit dis @it ontins in(nitely mnyD ut showing tht it ontins two ws su0ient for our formliztionD nd this ws surprisingly di0ult to show formllyAF ivery hEline ontins the inverse @wrtF the unit irleA of eh of its points @note tht t most one of them elongs to the unit disAD nd is invrint under unit irle inversionF ine there is unique irline ontining every three di'erent pointsD there is no more thn one hEline tht ontins two di'erent hEpoints @existene is shown lterD onstrutivelyAF e formlly show this only for points within the unit disD ut this ould e relxed @to ny two di'erent points exept the pir of points zero nd in(nityAF sf hEline ontins zeroD thn it lso ontins in(nity @the inverse point of zeroA nd is y de(nition the iuliden lineF ytherwise it must e n iuliden irleF H-isometries re onjugtionD wöius trnsformtions tht mp the unit dis onto itselfD nd their ompositionsF por ll onepts tht we introdue in the modelD we show tht they re preserved y hEisometriesF e show tht hElines re preserved y hEisometries @iFeFD tht hEisometries mp hElines to hElinesAF pirst we show tht ll unit irle preserving wöius trnsforms mp hElines to hElinesF lemma assumes "unit_circle_fix M " shows "is_h_line (moebius_cl M H) ←→ is_h_line H" his is shown s n esy onsequene of the hrteriztion of hElines s rel irlines perpendiulr to the unit irleD the ft tht wöius trnsE formtions preserve the irline type nd re onforml @preserve ngles ndD thereforeD perpendiulrityAD nd tht unit dis preserving trnsforms mp unit irle onto itselfF xext we show tht onjugtion lso preserves hElinesF lemma "is_h_line (conjugate_cl H) ←→ is_h_line H" nlike for the wöius trnsformsD where we used geometri proofD this is esily shown nlytillyD y diret lultionsF e set of points is h-collinear if there exists n hEline ontining ll of themF denition h_collinear :: "cp1 set ⇒ bool" where "h_collinear S ←→ (∃ p. is_h_line p ∧ S ⊆ circline_set p)"

rEollinerity is preserved y hEisometries @sine hElines re preservedAF

Construction of an h-line through the two given points. o show the existene of n hEline through ny two given hEpoints we hve formlized the nlyti onstrutionF por ny two di'erent points u nd v in the unit disD the hEline is given y n hEline mtrix with

A = i • (uv -vu)D nd B = i • (v(|u| 2 + 1) - u(|v| 2 + 1))F sf A = 0 @mening tht 0D u nd v re not ollinerAD it is n iuliden irle with enter in -B A D iFeF in u(|v| 2 + 1) -v(|u| 2 + 1) uv -vu .
sf A = 0 @mening tht 0D u nd v re olliner iFeFD tht there exists rel numer k suh tht v = k • uAD it is n iuliden line with norml vetor BF sf u = vD thn A = B = 0D whih is not vlid irlineF xote tht this onstrution n e used lso if u nd v re points outside the unit disF he onstrution fils when u nd v re mutully inverse s this would lso yield A = B = 0 @interestinglyD the stndrd ruler nd ompss onstrution lso fils in tht seAF sf {u, v} = {0, ∞}D then there is no unique hEline through the two pointsD lthough they re di'erentD ut in other ses of mutully inverse points the previous onstrution n e pplied on 0 nd u yielding vlid irlineF e formlized the previous onstrution in homogeneous oordintesD simE plifying ses when A = 0D nd then lift it to extended omplex plne nd irlines @y showing tht the onstrution lwys yields nonEzeroD rermiE tin mtrixD nd then y showing tht it does not depend on the hoie of representtive vetors of homogeneous oordintesAF denition h_line_cvec2_cmat2 :: "cvec2 ⇒ cvec2 ⇒ cmat2" where

"h_line_cvec2_cmat2 u v = (let (u 1 , u 2 ) = u; (v 1 , v 2 ) = v; nom = v 1 *cnj v 2 *(u 1 *cnj u 1 +u 2 *cnj u 2 ) - u 1 *cnj u 2 *(v 1 *cnj v 1 +v 2 *cnj v 2 ); den = u 1 *cnj u 2 *cnj v 1 *v 2 -v 1 *cnj v 2 *cnj u 1 *u 2 in if den = 0 then mk_h_line_cmat2 (Re(i*den)) (i*nom) else if u 1 *cnj u 2 = 0 then mk_h_line_cmat2 0 (i*u 1 *cnj u 2 ) else if v 1 *cnj v 2 = 0 then mk_h_line_cmat2 0 (i*v 1 *cnj v 2 ) else mk_h_line_cmat2 0 i)"
xote tht the lst rnh is tken only if u = v = 0 or {u, v} = {0, ∞} nd returns the xExis @this hoie is quite ritrry nd is not used in the rest of our formliztionD s we shll lwys ssume tht u = vD nd tht oth points re within the unit disAF elso note tht we onstrut unoriented irlines @lthough we hve developed support for irline orienttion onsidering only unoriented hElines su0es for oinre dis formliztionAF e (rst show tht our onstrution is vlid iFeFD tht it lwys yields hElines tht ontin two strting pointsF lemma assumes "u = v" shows "on_circline (h_line u v) u" "on_circline (h_line u v) v" shows "is_h_line (h_line u v)" he (rst lim is esily shown y diret lultionD ut the seond one requires very umersome lultion for showing tht the irline is rel @iFeD tht it hs negtive determinnt sine |B| 2 > |A| 2 AF roweverD we voided tht y lling upon the lemm tht shows tht there re t lest two points on this irline nd y our previous results this is possile only if it is rel irline @imginry irlines hve positive determinnt nd the empty set of pointsD nd irlines with the determinnt zero degenerte into single pointAF ell properties of hElines propgte to hElines onstruted from two points @eFgFD the hEline through u nd v ontins lso the inverses of u nd vAF he expliit line onstrution enles us to prove tht there is unique hEline through ny given two hEpoints @uniqueness prt ws lredy shown erlierAF lemma assumes

"u = v" "u ∈ unit_disc" "v ∈ unit_disc" shows "∃! l. is_h_line l ∧ u ∈ circline_set l ∧ v ∈ circline_set l"
his theorem gives us mny simpleD ut very useful orollriesF por exmE pleD if u = vD then hEline uv is the sme s the hEline vuF ih hEline is the hEline onstruted out of its two ritrry di'erent pointsF sf n hEline ontins two di'erent points on xExisGyExis then it is the xExisGyExisF he hEline onstrution is preserved y hEisometries iFeFD y unit dis preE serving wöius trnsformtions nd y onjugtionF lemma assumes "unit_disc_fix M " "u ∈ unit_disc" "v ∈ unit_disc" "u

= v" shows "h_line (moebius_pt M u) (moebius_pt M v) = moebius_cl M (h_line u v)" lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "u = v" shows "h_line (conjugate u) (conjugate v) = conjugate_cl (h_line u v)"
foth lemms re onsequenes of the hEline uniquenessF por exmpleD sine hEline uv ontins oth u nd vD its imge y ny wöius trnsformtion ontins imges of u nd v @sine wöius trnsformtion preserve inideneAF hose imges re di'erent @sine wöius trnsformtions re ijetionsAD nd sine we re deling with disEpreserving wöiusD oth re in the unit disF herefore the imge of the hEline uv must oinide y the @uniqueA hEline tht ontins imges of u nd vF QFP hEdistne snformllyD the h-distance etween the two hEpoints is de(ned s the solute vlue of the logrithm of the ross rtio etween those two points nd the two ideal points iFeFD the two points where the hEline onneting those two points intersets the unit disF pormliztion of this onept goes in severl stepsF pirst we needed to show tht eh hEline intersets the unit irle in extly two di'erent pointsF elthough this might e done in other wysD we deided to show the existene onstrutivelyD iFeFD to lulte the oordintes of idel points expliitlyD s it turns out tht the expressions re not too ulkyF xmelyD if the hEline is determined y A nd BD the two intersetion points re

B |B| 2 -A ± i • |B| 2 -A 2 .
yf ourseD we formlize this in homogeneous oordintesD nd lift it to irlines nd points in CP 1 @y showing the independene of representtive rermitin mtriesAF denition calc_ideal_point1_cvec2 :: "complex ⇒ complex ⇒ cvec2" where

"calc_ideal_point1_cvec2 A B = (let discr = Re ((cmod B) 2 -(Re A) 2 ) in (B*(-A -i*sqrt(discr)), (cmod B) 2 ))"
denition calc_ideal_point2_cvec2 :: "complex ⇒ complex ⇒ cvec2" where

(let discr = Re ((cmod B) 2 -(Re A) 2 ) in (B*(-A + i*sqrt(discr)), (cmod B) 2 ))"
denition calc_ideal_points_cmat2_cvec2 :: "cmat2 ⇒ cvec2 set" where

"calc_ideal_points_cmat2_cvec2 H = (if is_h_line_cmat2 H then let (A, B, C, D) = H in {calc_ideal_point1_cvec2 A B, calc_ideal_point2_cvec2 A B } else {(-1, 1), (1, 1)})"
xote tht lthough we re interested only in (nding idel points of hElinesD due to the totlity of ll sselleGryv funtionsD our de(nition needed to over ll irlines @when the irline is not hElineD we quite ritrrily return the points EI nd ID s we shll lwys gurd ginst suh ses using the is_h_line ssumptionAF elso note tht s we re deling with unoriented irlines nd s the order of the two intersetion points depends on irline orienttionD we n only return set of two pointsD nd not list @otherwiseD we ould not prove independene of the irline representtive mtrixAF fy using lengthyD ut quite strightforwrd lultions we show tht for every hEline its two idel points re di'erent nd re on the intersetion of tht line nd the unit irleF lemma assumes "is_h_line H"

shows "∀ z ∈ calc_ideal_points H. z ∈ circline_set H ∩ unit_circle_set" "card (calc_ideal_points H) = 2"
es the intersetion of ny two di'erent irlines n hve t most two points @s irlines re uniquely determined y their three di'erent pointsAD it follows tht calc_ideal_points returns extly the set of ll intersetion points of the given hEline with the unit irle @tht set is denoted y ideal_pointsAF denition ideal_points :: "circline ⇒ cp1 set" where "ideal_points H = circline_set H ∩ unit_circle_set" lemma assumes "is_h_line H" shows "ideal_points H = calc_ideal_points H" pinllyD we n hide our lultions nd express results neessry for furE ther de(nitions in terms of ideal_pointsF lemma assumes "is_h_line H" obtains i 1 i 2 where "i

1 = i 2 " "ideal_points H = {i 1 , i 2 }" shows "∀ z ∈ ideal_points H. z ∈ circline_set H ∩ unit_circle_set" lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "u = v" assumes "ideal_points (h_line u v) = {i 1 , i 2 }" shows "i 1 = i 2 " "u = i 1 " "u = i 2 " "v = i 1 " "v = i 2 "
es we shll very often employ wlog tehniqueD nd mp hElines to the xExis it is importnt to know its idel pointsF e very simple diret lultion shows tht those re -1 nd 1F rEisometries preserve idel points of hElinesF lemma assumes "unit_circle_fix M " "is_h_line H" shows "ideal_points (moebius_cl M H) = (moebius_pt M ) `(ideal_points H)"

shows "ideal_points (conjugate_cl H) = conjugate `(ideal_points H)"

his is esy to proveF por exmpleD sine wöius trnsformtions tht preserve the unit irle lso preserve inideneD imges of originl idel points elong oth to the imge of hEline nd to the unit irleD nd re therefore idel points of the imge of hElineF es wöius trnsformtions re ijetionsD they re di'erentD nd the theorem follows s there n e t most two idel pointsF rving formlized idel pointsD we n formlize hEdistne in spirit of the informl de(nition relying on the rossErtioF he informl de(nition does not expliitly stte the mutul order of the idel points in the ross rtioD nd ssumes tht the rossErtio is lwys rel5 nd positive @so its rel logrithm is well de(nedAF his is ll orret @when the idel points re swppedD the rossE rtio eomes reiprotedD logrithm eomes negtedD nd the solute vlue neutrlizes the hngeAD ut it needs to e formlly provedF pirst note tht the se of u = v needs to e hndled seprtelyD sine there is no unique hE line through themF he de(nition of hEdistne relies on the rilert9s de(nite hoie opertor @THE in sselleGryvA nd hEdistne is de(ned s the numer suh tht for every hoie of idel points tht numer is equl to the solute vlue of the logrithm of the desried ross rtioF yf ourseD it must e shown tht suh numer existsF abbreviation Re_cross_ratio where "Re_cross_ratio z u v w ≡ Re (to_complex (cross_ratio z u v w))" denition calc_h_dist :: "cp1 ⇒ cp1 ⇒ cp1 ⇒ cp1 ⇒ real" where "calc_h_dist u i 1 v i 2 = abs (ln (Re_cross_ratio u i 1 v i 2 ))" denition h_dist_pred :: "cp1 ⇒ cp1 ⇒ real ⇒ bool" where

"h_dist_pred u v d -→ (u = v ∧ d = 0) ∨ (u = v ∧ (∀ i 1 i 2 . ideal_points (h_line u v) = {i 1 , i 2 } -→ d = calc_h_dist u i 1 v i 2 ))"
denition h_dist :: "cp1 ⇒ cp1 ⇒ real" where

"h_dist u v = (THE d. h_dist_pred u v d)"
pirst we shown tht the desried rossErtio is lwys (niteD positive rel numerF lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "u

= v" shows "∀ i 1 i 2 . ideal_points (h_line u v) = {i 1 , i 2 } -→ cross_ratio u i 1 v i 2 = ∞ h ∧ is_real (to_complex (cross_ratio u i 1 v i 2 )) Re_cross_ratio u i 1 v i 2 > 0"
his is the (rst exmple where we employ the wlog tehnique nd otin very simple proofF sing without loss of generlity we n ssume tht u = 0 nd v is point on the positive prt of the xExisD within the unit dis so 0 < v < 1F e use the following wlog lemmF lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "u = v" assumes " M u v. unit_disc_fix M ; u ∈ unit_disc; v ∈ unit_disc; u = v;

P (moebius_pt M u) (moebius_pt M v) =⇒ P u v"
assumes " x. is_real x; 0 < Re x; Re x < 1 =⇒ P 0 h (of_complex x)"

shows "P u v"

hen u = 0 nd v is positive relD then the ross rtio is either (1+v)/(1v) or (1 -v)/(1 + v)D depending on the order of idel pointsD nd in oth ses it is (niteD rel nd positiveF st remins to show tht the property tht is eing proved is preserved y unit dis preserving wöius trnsformtionsD ut it is esy sine suh trnsformtions preserve hElines nd idel points nd ll wöius trnsformtions preserve rossErtiosF xext we n show tht for every di'erent points from the unit dis there is extly one numer tht stis(es the hEdistne prediteF lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" shows "∃! d. h_dist_pred u v d" sf the points re the smeD then tht numer is zeroD nd if they re di'erE entD then there exist some pir of idel points i 1 nd i 2 nd the sought numer is calc_h_dist u i 1 v i 2 F fy the previous lemm tht numer is well de(ned nd it is not hrd to show tht it remins unhnged when the idel points re swppedF pinlly we n eliminte the need for unfolding the omplited hEdistne de(nition y the following lemmsF lemma assumes "u ∈ unit_disc" shows "h_dist u u = 0" lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "u

= v" "ideal_points (h_line u v) = {i 1 , i 2 }" shows "h_dist u v = calc_h_dist u i 1 v i 2 "
snsted of the hEdistne itselfD very frequently its hyperoli osine is nlyzed @it is de(ned y cosh x = (e x + e -x )/2AF st n e expressed s the verge of the following two rossErtios @shown esily y diret lultions sed on the de(nitions of the rossErtio nd hyperoli osineAF abbreviation "cosh_h_dist u v ≡ cosh (h_dist u v)"

lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "u = v" "ideal_points (h_line u v) = {i 1 , i 2 }" shows "cosh_h_dist u v = ((Re_cross_ratio u i 1 v i 2 ) + (Re_cross_ratio v i 1 u i 2 )) / 2"
ine hEdistne is de(ned y mens of rossErtioD it is esy to show tht it is preserved y hEisometries iFeFD y wöius trnsformtions tht preserve the unit dis nd y onjugtion @we hve lredy proved tht hElinesD idel points nd ross rtio re preserved y these trnsformsD so the onlusion follows quite esilyAF lemma assumes "unit_disc_fix M " "u ∈ unit_disc" "v ∈ unit_disc" shows "h_dist (moebius_pt

M u) (moebius_pt M v) = h_dist u v" lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" shows "h_dist (conjugate u) (conjugate M v) = h_dist u v"
sn some ses the hEdistne n esily e lulted diretlyF por exmpleD hEdistne etween ny two points x 1 nd x 2 on the segment of the xExis within the unit dis n e lulted s

ln (1 + x 1 )(1 -x 2 ) (1 -x 1 )(1 + x 2 ) .
his further simpli(es if one of the two points is zeroF sf one of the two points is zeroD the hEdistne n e lulted y ln 1 -|x| 1 + |x| , whih is esily shown y employing the wlog tehnique nd ssuming tht the other point is on the positive prt of the xExis @sillyD y rotting the whole on(gurtionAF e use the following wlog lemmF lemma assumes "u ∈ unit_disc" "u = 0 h " assumes " φ u. u ∈ unit_disc; u = 0 h ; P (moebius_pt (moebius_rotation φ) u) =⇒ P u" assumes " x. is_real x; 0 < Re x; Re x < 1 =⇒ P (of_complex x)"

shows "P u"

Explicit h-distance formula. elthough we found some expliit formuls for hEdistne lultionsD they overed only some speil ses @when the two hEpoints line on hEline tht is n iuliden lineAF xext we show tht the following formul expresses hEdistne etween ny two hEpoints @note tht the idel points do not (gure nymoreAF

d(u, v) = arccosh 1 + 2 • |u -v| 2 (1 -|u| 2 ) • (1 -|v| 2 )
snverse osine is de(ned y arccosh x = ln (x + √ x 2 -1) for x ≥ 1D nd for suh x it is the inverse funtion of the hyperoli osineF xote tht if u nd v re in the unit disD then the denomintor is lwys stritly greter thn zeroD so the rgument of arccosh is within its dominF denition h_dist_formula' :: "complex ⇒ complex ⇒ real" where

"h_dist_formula' u v = 1 + 2 * ((cmod (u-v)) 2 / ((1-(cmod u) 2 ) * (1-(cmod v) 2 )))"
denition h_dist_formula :: "complex ⇒ complex ⇒ real" where "h_dist_formula u v = acosh (h_dist_formula' u v)" he equivlene etween the two hEdistne representtions is given y the following theoremF lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" shows "h_dist u v = h_dist_formula (to_complex u) (to_complex v)" e prove it y employing the wlog pproh nd ssume tht u = 0 nd tht v is rel numer suh tht 0 < v < 1 @the se u = v is dishrged trivE illyAF sn tht se we lredy know tht the leftEhnd side is equl to ln 1-v 1+v nd need to prove tht this is lso the se with the right hnd sideF ine v is relD rightEhnd side is arccosh 1 + 2v 2 1-v 2 F efter unfolding the inverse hyperoli osine de(nition nd simplifying the expression @using the ssumpE tion tht v is within the unit dis so |v| < 1A we get tht the rightEhnd side is equl to ln 1+v 1-v D sine v is rel nd positiveF ht vlue is etween H nd ID so its logrithm is negtive nd its solute vlue is equl to its oppositeF hereforeD the leftEhnd side is equl the logrithm of its reiprolD nd tht is equl the vlue of the the rightEhnd side @sine v is relAF st still needs to e justi(ed tht the wlog ssumption ould hve een used iFeFD tht the sttement of the lemm is preserved y wöius trnsformtions tht preserve the unit disF he hEdistne is de(ned y mens of the rossE rtio nd is lerly preservedD ut we lso need to show tht the hEdistne formul is lso preservedF o do tht we use nother wlog theorem nd show tht the hEdistne formul is preserved y flshke trnsforms nd y roE ttions @this su0es sine every unit dis preserving wöius trnsform is omposition of suh two trnsformsAF e use the following wlog lemmF lemma assumes "unit_disc_fix M " assumes " k. cmod k < 1 =⇒ P (blaschke k)" assumes " φ. P (moebius_rotation φ)"

assumes " M 1 M 2 . unit_disc_fix M 1 ; P M 1 ; unit_disc_fix M 2 ; P M 2 =⇒ P (M 1 + M 2 )"
shows "P M " ottions preserve omplex modulusD so they lerly preserve the hEdistne formulF howing tht flshke ftors preserve hEdistne formul is done y diret lultionsF e (x n ritrry omplex numer k suh tht cmod k < 1D nd nlyze blaschke k trnsformF he hEdistnes etween the originl points nd etween the trnsformed points re given y the following formulsF

arccosh 1 + 2 • |u -v| 2 (1 -|u| 2 )(1 -|v| 2 ) arccosh     1 + 2 • u-k 1-ku -v-k 1-kv 2 1 -u-k 1-ku 2 • 1 -v-k 1-kv 2     hese two re equl sine it holds thtX u-k 1-ku -v-k 1-kv 2 1 -u-k 1-ku 2 • 1 -v-k 1-kv 2 = |u-v| 2 |1-kk| 2 |1-ku| 2 |1-kv| 2 |1-kk|(1-|u| 2 ) |1-ku| 2 • |1-kk|(1-|v| 2 ) |1-kv| 2 = |u -v| 2 (1 -|u| 2 ) • (1 -|v| 2 )
.

xote tht forml justi(tion of the previous equlities is not trivilF por exmpleD showing tht

1 - u -k 1 -ku 2 = 1 - u -k 1 -ku 2
whih is one of the intermedite steps in the previous derivtion requires knowE ing tht flshke trnsform preserves the unit disD so the sutrted vlue is lwys less thn 1F he hEdistne expliit formul enles us to prove some properties of hE distne muh esier thn y using its rossErtio de(nitionF por exmpleD it is trivil to prove tht the distne is nonEnegtiveD tht it is zero only if the two points re equl nd tht it is symmetriF ogether with the following tringle inequlity these properties prove tht hEdistne is metriF lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc" shows "h_dist u v + h_dist v w ≥ h_dist u w" e hve proved tringle inequlity lso y using the hEdistne formulD nd y employing the wlog priniple @it n e esily justi(ed sine the hE distne is preserved y unit dis preserving wöius trnsformtionsA nd ssuming tht v = 0F st holds tht h_dist u w is equl to

arccosh (1 -|u| 2 )(1 -|w| 2 ) + 2|u -w| 2 (1 -|u| 2 )(1 -|w| 2 )
he sum h_dist u 0 + h_dist 0 w is equl to

arccosh 1 + 2|u| 2 (1 -|u| 2 ) + arccosh 1 + 2|w| 2 (1 -|w| 2 )
hen the ddition formul arccosh x + arccosh y arccosh xy + (x 2 -1)(y 2 -1) is pplied nd the otined expression is simpli(edD the previous formul is trnsformed to

arccosh (1 + |u| 2 )(1 + |w| 2 ) + 4|u||w| (1 -|u| 2 )(1 -|w| 2 )
ine arccosh is monotone inresing funtionD it su0es to show tht

(1 -|u| 2 )(1 -|w| 2 ) + 2|u -w| 2 ≤ (1 + |u| 2 )(1 + |w| 2 ) + 4|u||w|, iFeFD tht |u -w| 2 ≤ (|u| + |w|) 2
whih holds y tringle inequlity |u -w| ≤ |u| + |w| for rel numersF ixistene of n hEisometry @unit dis preserving wöius trnsform eventuE lly omposed y onjugtionA etween two pirs of points shows tht they re equidistntF he onverse lso holds iFeFD the group of wöius trnsforms tht preserve the unit dis is rih enough to mp every pir of points to nother pir of points with the sme hEdistneF

lemma assumes "{u, v, u , v } ∈ unit_disc" assumes "h_dist u v = h_dist u v " shows "∃ M . unit_disc_fix M ∧ moebius_pt M u = u ∧ moebius_pt M v = v "
e (rst prove lemm showing tht for eh rel numer d there is extly one point on the positive xExis suh tht hEdistne etween H nd tht point is d @this is done either y showing tht the restrition of the distne funtion to positive xExis tht is ln 1+x 1-x is ijetion etween positive xExis nd R + or y using the existene nd uniqueness of rossErtioAF sf u = v D the theorem holds trivillyF ytherwiseD wlog we ssume tht u = 0 nd tht v is on the positive xExisF hen we (nd unit dis preserving wöius tht mps u to H nd v to the positive xExis @it exists y our previous results nd is omposition of flshke trnsform nd rottionAF fy the previous uniqueness lemmD the imge of v must e equl to v F QFQ hEirles sn every geometry irles onsist of points tht re t the sme distne from the enterF denition h_circle :: "cp1 ⇒ real ⇒ cp1 set" where

"h_circle u r = {z. z ∈ unit_disc ∧ h_dist u z = r}"
xote tht y our de(nition of distne there ould theoretilly exist some points out of the dis tht hve distne r from the enter uD ut our de(nition of hEirle expliitly exluded themF he entrl result is tht hEirles re represented y iuliden irles in the oinré modelF en hEirle entered t u with the rdius r is represented y n iuliden irle entered t

u e = u (1 -|u| 2 ) cosh r-1 2 + 1 nd rdius r e = (1 -|u| 2 ) cosh r-1 2 • cosh r+1 2 (1 -|u| 2 ) cosh r-1 2 + 1 = (1 -|u| 2 ) sinh r (1 -|u| 2 )(cosh r -1) + 2
his is formlized y the following de(nitionF denition h_circle_euclidean :: "cp1 ⇒ real ⇒ (complex × real)" where

"h_circle_euclidean u r = (let R = (cosh r -1) / 2; u = to_complex u; cu = 1 -(cmod u ) 2 ; k = cu * R + 1 in (u / k, cu * sqrt(R * (R + 1)) / k))"
pirst we show tht previous formuls desrie n iuliden irle tht lwys hs positive rdius nd is lwys fully ompletely situted within the unit disF lemma assumes "r > 0" "z ∈ unit_disc" "(ze, re) = h_circle_euclidean z r" shows "cmod ze < 1" "re > 0" "∀ x ∈ circle ze re. of_complex x ∈ unit_disc" vet us demonstrte thisF vet R = cosh r-1 2 nd U = 1 -|u| 2 F sf r > 0 then cosh r > 1 nd R > 0F ine u is in the unit dis it holds tht U > 0D so the denomintor U R + 1 is stritly greter thn oneD nd the enter of the irle otined y dividing the hEenter y this denomintor must e in the unit disF ine r > 0 it holds tht sinh r > 0D so the nomintor U sinh r nd the iuliden rdius re lso stritly positiveF st remins to show tht every point in the irle is within the unit disF sf z is n ritrry point on the irleD then y tringle inequlity it holds tht |z| ≤ |u e | + r e F e shll show tht the right hnd side is lwys stritly less thn 1F fy the inequlity of geometri nd rithmeti men it holds tht R(R + 1) < R+(R+1)

2 D iFeFD tht R(R + 1) -R < 1/2F ine u is within the unit disD it holds tht 1 + |u| < 2D so (1 + |u|)( R(R + 1) -R) < 1F hereforeD U ( R(R + 1) -R) < 1 -|u| nd |u| + U R(R + 1) < 1 + RU F ine 1 + RU > 1 nd |z e | = |u|/(1 + RU ) nd r e = (U R(R + 1))/(1 + RU ) it holds tht |u e | + r e < 1F
he onnetion etween the points on the hEirle nd its orresponding iuliden irle is given y the following lemmF lemma assumes "u ∈ unit_disc" "r > 0" "let (ue, re) = h_circle_euclidean u r in h_circle u r = of_complex `(circle ue re) "

vet z e n ritrry pointF fy the hEdistne formulD it elongs to the hE irle i'

|z| < 1 nd 1 + 2|z-u| 2 (1-|z| 2 )(1-|u| 2 ) = rF vet R = cosh r-1 2 nd U = 1 -|u| 2 F he following equivlenes holdF |z| < 1 ∧ 1 + 2|z -u| 2 (1 -|z| 2 )(1 -|u| 2 ) = r ←→ |z| < 1 ∧ |z -u| 2 = R • (1 -|z| 2 ) • U ←→ |z| < 1 ∧ (z -u)(z -u) + R • U • zz = RU ←→ |z| < 1 ∧ zz - zu 1 + RU - zu 1 + RU + uu 1 + RU = RU 1 + RU ←→ |z| < 1 ∧ z - u 1 + RU 2 - |u| 2 (1 + RU ) 2 + |u| 2 1 + RU = RU 1 + RU ←→ |z| < 1 ∧ z - u 1 + RU 2 = U 2 • R(R + 1) (1 + RU ) 2 |z| < 1 ∧ |z -z e | 2 = r 2 e
fy the previous lemm the whole irle is within the unit dis so |z -z e | = r 2 e implies tht |z| < 1D nd the equivlene is provedF he results out irles tht were just proved give us very simple proof of the following theorem out hEisometriesD tht hppens to e ruil step in proving tht the oinré dis stis(es some of the rski xioms @eFgFD the (veEsegment xiomAF por every pir of tringles suh tht its three pirs of sides re pirwise equl there is n hEisometry @ unit dis preserving wöius trnsformD eventully omposed with onjugtionA tht mps one tringle onto the otherF lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc" and "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc" and "h_dist u v = h_dist u v " "h_dist v w = h_dist v w " "h_dist u w = h_dist u w "

shows

"∃ M . unit_disc_fix_fun M ∧ M u = u ∧ M v = v ∧ M w = w "
sf ny two points of the (rst tringles re the smeD then the proof is trivil @nd redues to previously proved lemms out ongruent segmentsAF ytherwiseD wlog we n ssume tht u = 0 nd tht v is on the positive xE xisF vet M e wöius trnsform tht preserves the unit dis nd mps u to u nd v to v @it exists sine the hEdistne etween u nd v is equl to the hEdistne etween u nd v AF hen w must e n intersetion of the hEirle entered in u with rdius equl to hEdistne d uw from u to w nd the hEirle entered in v with rdius equl to hEdistne d vw from to wF elsoD sine wöius trnsforms preserve distnesD the imge of M (w) must lso e n intersetion of those two hE irlesF xowD oth these hEirles re iuliden irlesD with enters on the xExis nd positive rdiiF es the irles interset nd nnot e the sme @sine v is not 0AD their iuliden enters nnot e in the sme pointF hereforeD y simple nlysis of their iuliden equtions it holds tht they interset in two points tht re mutully onjugteF o M (w) is either equl to w or is its onjugteF hepending on this we either just use M or ompose it with onjugtion @tht (xes oth u nd vD sine they re on the xExisA nd otin the desired trnsformtionF QFR hEetween here re severl equivlent wys to de(ne hEetweenness of three pointsF sn oinré model hElines n e iuliden irles nd there is no notion of etweenness of three points on irle @sine two points divide irles into two di'erent rD nd the third point is etween the two on one of those two rsAF roweverD when two points re (xedD y mens of ross rtio we n deide if some other two given points re on the sme or on di'erent of the two rs determined y the (xed pointsF xmelyD if they re on sme r the ross rtio is positiveD nd otherwise it is negtive @for simpliity we ssume tht ll points re di'erentAF ine four points re on the sme irlineD their rossErtio must e relF elso note tht the inverse point of v is not in the unit dis nd therefore is lwys di'erent from the other three pointsF his nlysis n e used to de(ne hEetweennessF xmelyD if two outer points re (xedD the inner point is not etween them i' it is on the sme r s the r of the hEline tht goes out of the unit disF e know tht the inverse of tht point is not in the unit disD so the point v is etween u nd w if the rossErtio etween the pirs u nd w nd v nd inverse of v is rel nd negtiveF ine rski onsiders nonEstrit etweennessD we extend the de(nition y two speil ses @there must e speil ses sine when u = v = wD the rossErtio is not well de(nedAF denition h_betw :: "cp1 ⇒ cp1 ⇒ cp1 ⇒ bool" where

"h_betw u v w ←→ u = v ∨ v = w ∨ (let cr = cross_ratio u v w (inversion v) in is_real (to_complex cr) ∧ Re (to_complex cr) < 0)"
ome si properties of the hEetweeness follow diretly from this de(niE tionF por exmpleD for three points uD v nd w within the unit dis h_betw u u v nd h_betw u v v follow diretly from the two speil sesD while h_betw u v u implies u = vD sine otherwise the rossErtio would e ID nd not negE tiveF fy exhnging points u nd w rossErtio is reiprotedD so it sign does not hngeD so h_betw u v w i' h_betw w v uF ell these simple lemms re esy to prove y properties of the rossErtioF roweverD ttention must e put on dishrging ssumptions tht no three points re equlD so rossErtio is wellEde(nedF xote tht some of these lemms might hve simpler proofs with some other hrteriztions of etweennessF ine wöius trnsforms tht preserve unit dis rossErtio nd inverse pointsD they preserve etweenessF he sme hold for onjugtion ndD thereforeD for ll hEisometriesF lemma assumes "unit_disc_fix M " "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc" shows

"h_betw (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) ←→ h_betw u v w" "h_betw (conjugate M u) (conjugate M v) (conjugate M w) ←→ h_betw u v w"
sf the three points lie on n hEline tht is iuliden line @eFgFD if one of the points is zeroAD hEetweenness n e hrterized in the following wy @muh simpler thn the de(nitionAF

lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "u = 0 h " "v = 0 h " shows "h_betw u 0 h v ←→ (∃ k < 0. to_complex u = k * to_complex v)" "h_betw 0 h u v ←→ (let u = to_complex u; v = to_complex v in arg u = arg v ∧ cmod u ≤ cmod v )"
foth these hrteriztions re proved y wlog ssumption tht one of the two points is on the positive prt of the xExis nd proving the etweenness hrteriztion for three rel numers @for exmple 0 is etween x nd y i'

x • y ≤ 0D nd x is etween 0 nd y if 0 ≤ x ≤ y or y ≤ x ≤ 0AF st is esily
shown tht rottions preserve ll relevnt expressionsD so the wlog ssumption is justi(edF hree points n e in n hEetween reltion only when they re hEolliner " sine the ross rtio is relD they ll must lie on single irlineF xmelyD hE line through u nd v lso ontins u v nd inversion vD so y the uniqueness of irline through three di'erent pointsD tht irline is n hEline nd the points re ollinerF he onverse is lso vlid in some senseD sine for three hEolliner points t lest one of the three possile hEetweeness reltions must holdF lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc" shows "h_collinear {u, v, w} ←→ h_betw u v w ∨ h_betw u w v ∨ h_betw v u w" efter dishrging degenerte sesD the lemm is proved y ssuming tht u = 0 nd tht v is positive rel numerD nd y using the properties of the etweenness reltion etween points on iuliden lines @iFeFD for the xExisAF enother possile de(nition of the hEetweenness reltion is given in terms of hEdistnes etween pirs of pointsF e prove it s hrteriztion equivE lent to our rossErtio sed de(nition @this ould hve een tken s the hEetweenness de(nitionAF lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc" shows "h_betw u v w ←→ h_dist u v + h_dist v w = h_dist u w" efter eliminting degenerte sesD we prove the theorem y wlog sE sumption tht v = 0 tht w is point on the positive prt of xExisF fy previous results we know tht h_betw u v w holds only if u is rel negtive numerF e need to show the sme for the sum of distnesF e show tht h_dist u 0 + h_dist 0 w = h_dist u w i' u is rel nd negE tiveF fy the sme lultions s in the proof of tringle inequlity for hE distne we show tht previous is equivlent to |u -

w| 2 = (|u| + |w|) 2 F ine Im w = 0D this is equivlent to (Re u -Re w) 2 + (Im u) 2 = (Re u) 2 + (Im u) 2 + 2 ((Re u) 2 + (Im u) 2 )(Re w) 2 + (Re w) 2 D iFeFD to | Re w| (Re u) 2 + (Im u) 2 + Re u • Re w = 0F rene (Re u) 2 + (Im u) 2 = | Re u| nd therefore Im u = 0 nd u is lso relF lugging Im u = 0 into the previous equlity yields tht | Re w| • | Re u| + Re w • Re u = 0F ine | Re w| • | Re u| is positiveD Re w • Re u must e negtiveF
xote tht some properties of hEetweenness re very esily proved y using the previous hrteriztionF QFS sntersetion of hElines with the xes sh9s xiom proves existene of the intersetion of two irlines @nd its positionAF he wlog tehnique enles us to simplify lultions y ssuming tht one of the two irlines is the xExisF sn some other ses @eFgFD when onsidering perpendiulrityA we shll lso onsider intersetions with the yE xisF herefore in this setion we shll introdue some tehniques for resoning out suh intersetionsF pirst we de(ne the ondition tht n hEline intersets the xExisF ine the eqution of xExis is z = zD the intersetion point z of n hEline determined y A nd B nd the xExis is rel nd it must stisfy Az 2 + (B + B)z

+ A = 0D iFeFD Az 2 + 2 • Re B • z + A = 0F sf A = 0D
then the intersetion exists nd is equl to 0F ytherwise the intersetion exists i' the disriminnt is nonEnegtiveF sf it is equl to zeroD then Re B = A or Re B = -AD so z = 1 or -1 nd none of the intersetion points is within the unit disF sf it is stritly positiveD then there re two di'erent intersetion pointsF fy iet9s formul it holds tht their produt is A/A = 1F hereforeD one of the two intersetion points must e within the unit disF his inspires the following de(nitionF denition intersects_x_axis_cmat2 :: "cmat2 ⇒ bool" where

"intersects_x_axis_cmat2 H = (let (A, B, C, D) = H in A = 0 ∨ (Re B) 2 > (Re A) 2 )"
lift_denition intersects_x_axis :: "circline ⇒ bool" is . . . he following lemmD whose proof is sed on the previous nlysisD justiE (es suh de(nitionF lemma assumes "is_h_line H" shows "(∃ x ∈ unit_disc. x ∈ circline_set H ∩ circline_set x_axis) ←→ intersects_x_axis H" ixistene of n intersetion with the yExis is hrterized quite similrlyF denition intersects_y_axis_cmat2 :: "cmat2 ⇒ bool" where

"intersects_y_axis_cmat2 H = (let (A, B, D) = H in A = 0 ∨ (Im B) 2 > (Re A) 2 )" lift_denition intersects_y_axis :: "circline ⇒ bool" is . . . lemma assumes "is_h_line H" shows "(∃ y ∈ unit_disc. y ∈ circline_set H ∩ circline_set y_axis) ←→ intersects_y_axis H"
elthough this n e proved diretlyD it is proved more esily y rotting the on(gurtion WH degrees in the negtive diretionF he intersetion point within the unit dis n e lulted y the folE lowing formulF

x = -Re B A + sgn (Re B) • (Re B) 2 -A 2 A denition calc_x_axis_intersection_cmat2_cvec2 :: "cmat2 ⇒ cvec2"
where

"calc_x_axis_intersection_cmat2_cvec2 H = (let (A, B, C, D) = H in if A = 0 then (0, 1) else (-Re(B) + sgn (Re B) * sqrt((Re B) 2 -(Re A) 2 ), A))"
lift_denition calc_x_axis_intersection :: "circline ⇒ cp1" is . . . st is hrterized y the following lemmF lemma assumes "is_h_line H" "intersects_x_axis H"

shows "calc_x_axis_intersection H ∈ unit_disc"

"calc_x_axis_intersection H ∈ circline_set H ∩ circline_set x_axis" he only interesting prt of the proof is tht the intersetion point is in the unit disF sf Re A = A = 0D tht is trivilF ytherwise Re B = 0 nd it holds tht (Re B) 2 -A 2 < |B| = sgn (Re B) • Re BF wultiplying this y 2 • (Re B) 2 -A 2 D rerrnging the terms nd using the ft tht sgn (Re B) 2 = 1 gives

-Re B + sgn (Re B) • (Re B) 2 -A 2 A 2 < 1.
e shll lso e interested if the intersetion point is on the positive prt of the xExisGyExisF denition intersects_x_axis_positive_cmat2 :: "cmat2 ⇒ bool" where

"intersects_x_axis_positive_cmat2 H = (let (A, B, C, D) = H in Re A = 0 ∧ Re B / Re A < -1)"
lift_denition intersects_x_axis_positive :: "circline ⇒ bool" is . . . denition intersects_y_axis_positive_cmat2 :: "cmat2 ⇒ bool" where

"intersects_x_axis_positive_cmat2 H = (let (A, B, C, D) = H in Re A = 0 ∧ Im B / Re A < -1)"
lift_denition intersects_y_axis_positive :: "circline ⇒ bool" is . . . ghrteriztion is given y the following lemm @nlogous one is proved for the yExisAF lemma assumes "is_h_line H" "H = x_axis" shows "intersects_x_axis_positive H ←→

(∃ x. x ∈ unit_disc ∧ x ∈ circline_set H ∩ positive_x_axis)"
he intersetion point isD of ourseD gin given y calc_x_axis_intersectionF sf Re A = A = 0 nd (Re B) 2 > A 2 @so tht the squre root is wellEde(ned nd there is n intersetion in the disAD it holds tht

sgn (Re B) • Re(B) 2 -A 2 A < sgn (Re B) • | Re B| A = Re B A = -Re B A .
herefore the sign of x depends only on the sign of

-Re B A F ine (Re B) 2 > A 2 D if -Re B A
is positive then it is greter thn ID nd if it is negtiveD then it is less thn IF herefore -Re B A > 1 is the ondition equivlent to tht x is positiveF pinllyD the position of the intersetion depends on the vlue of -Re B A F he smller tht numerD the lrger the xEoordinte of the intersetionF e introdue the funtion tht ompres two irlines nd tells if the xExis inE tersetion of the (rst one is more towrds the edge of the unit dis thn the xExis intersetion of the other oneF denition x_axis_intersection_outward_cmat2 :: "cmat2 ⇒ cmat2 ⇒ bool" where ) 2 -1 @esily shown y se nlysis on the sign of Re BAF he lemm follows from the monotoniity of the rel funtion x -√ x 2 -1 on the intervl (1, +∞)F he next lemm out the hEetweenness will e one of the ruil steps in our proof of the sh9s xiom in the oinré modelF e wnt to hrE terize the hEetweenness of the intersetion point of two hElines wrtF the points determining those hElinesF yur wlog tehnique will enle us to onsider only intersetions of hElines with the xExisF he following lemm sys tht the inE tersetion point of the hEline determined y points u nd v nd the xExis is etween u nd vD then u nd v re in the opposite hlfEplnes @one must e in the upperD nd the other one in the lower hlfEplneAF lemma assumes "u ∈ unit_disc" "v ∈ unit_disc" "z ∈ unit_disc" "u = v" assumes "u / ∈ circline_set x_axis" "v / ∈ circline_set x_axis"

"x_axis_intersection_outward_cmat2 H 1 H 2 = (let (A 1 , B 1 , C 1 , D 1 ) = H 1 ; (A 2 , B 2 , C 2 , D 2 ) = H 2 in -Re B 1 /Re A 1 ≤ -Re B 2 /
assumes "z ∈ circline_set (h_line u v) ∩ circline_set x_axis" shows "h_betw u z v ←→ arg (to_complex u) * arg (to_complex v) < 0"

he entrl ide of the proof is to ssume wlog tht the intersetion point z is zeroF hen uD v nd 0 re hEolliner nd olliner @s their hEline ontins 0 it must e lineAF e rell tht point 0 is hEetween u nd v i' there is negtive rel numer k suh tht u = k • vF sf there is suh kD then arg u = arg (-v)D nd sine u nd v re not on the xExisD arg u nd arg v hve the opposite signF por the other diretionD sine uD v nd 0 re ollinerD u nd v n e represented y u = r u • e iφ nd v = r v • e iφ D for some rel numers r u = 0D r v = 0 nd φF fut then if arg u • arg v < 0D it must hold tht r u • r v < 0 nd tht ru rv < 0F ine u = ru rv vD we hve found negtive numer k suh tht u = k • vD so the hEetweenness holdsF he wlog ssumption must e justi(edF he key rgument is tht there is flshke trnsform tht mps z to 0D ut of speil kindD sine z is on the xExis @in the unit disAF e use the following wlog lemmF lemma assumes "u ∈ unit_disc" "is_real (to_complex u)" assumes " a u. u ∈ unit_disc; is_real a; cmod a < 1;

P (moebius_pt (blaschke a) u) =⇒ P u"

assumes "P 0 h " shows "P u" flshke trnsforms determined y rel prmeter a preserve the xExis @they mp a to 0D 1/a to ∞ nd 0 to -1/a = -1/aD so three di'erent points on the xExis sty on the xExisD so it must e (xedAF elsoD suh flshke trnsforms preserve the sign of the imginry prtF lemma assumes "is_real a" "cmod a < 1" "z = ∞ h " "z = inversion (of_complex a)" shows "sgn (Im (to_complex (moebius_pt (blaschke a) z))) = sgn (Im (to_complex z))" sndeedD imge of point z is z-a 1-az D nd sine a = aD its imginry prt is

(1-a 2 )(Im z) |1-az| 2
D nd its sign is the sme s the sign of Im zF por points not on the xExis the sign of the imginry prt mthes the sign of the rgumentD so suh flshke trnsforms preserve the sign of the rgument of nonEzero pointsF flshke trnsforms re wöius trnsforms tht preserve the unit disD so they preserve the hEetweennessF ine ll the elements of the hEetweenness hrteriztion tht we prove re preserved @unit disD xExisD hEetweennessD nd hElinesAD the wElog ssumption is justi(edF 4 Proving the Tarski's axioms rski9s xioms re given in lole tht is interpreted y speifying the type of pointsD ongruene nd etweenness reltion over tht typeF e shll use the h_point type de(ned efore nd need to de(ne those reltionsF rEongruene etween pirs of points n e de(ned in terms of hEdistne funtionF denition h_cong :: "cp1 ⇒ cp1 ⇒ cp1 ⇒ cp1 ⇒ bool" where

"h_cong u v u v ←→ h_dist u v = h_dist u v "
iquivlentlyD ongruene ould e de(ned y requiring n hEisometry tht mps the (rst pir onto the seond oneF rEongruene n then e lifted to the h-point type @we denote it y ≡ h AF lift_denition ≡ h :: "h_point ⇒ h_point ⇒ h_point ⇒ h_point ⇒ bool" is h_cong imilrlyD hEetweenness n lso esily e lifted to the hEpoint type @nd we denote it y B h AF lift_denition B h :: "h_point ⇒ h_point ⇒ h_point ⇒ bool" is h_betw sn tht wy we otin elements tht interpret the rski xioms lole nd need to prove xiomsF ih xiom formulted over the h_point type is proved y trnsfering it to the cp1 type nd proving it in its unlifted formF hereforeD in this setion we shll show unlifted vrints of xiomsF Congruence axioms. por exmpleD the xiom lemma xes u v :: h_point shows "u v ≡ h v u" is proved y trnsfering it to its unlifted ounterprt lemma xes u v :: cp1 assumes "{u, v} ⊆ unit_disc" shows "h_cong u v v u" his lemm is esily proved y our erlier results on hEdistneF he sme hold for the following two hEongruene xiomsF lemma assumes

"{u, v, u 1 , v 1 , u 2 , v 2 } ⊆ unit_disc" assumes "h_cong u v u 1 v 1 " "h_cong u v u 2 v 2 " shows "h_cong u 1 v 1 u 2 v 2 "
lemma assumes "{u, v, w} ⊆ unit_disc" assumes "h_cong u v w w" shows "u = v" Segment construction axiom. lemma assumes "{u, v, a, b} ⊆ unit_disc" shows "∃ w. w ∈ unit_disc ∧ h_between u v w ∧ h_cong v w = h_dist a b" sf u = vD wlog we n ssume tht u = v = 0F hen there exists point w on the xExis suh tht its hEdistne from 0 is equl to the given hEdistne from a to bF sf u = vD wlog we n ssume tht v = 0 nd tht u is point on the positive xExis @within the unit disAF hen there exists point w on the negtive prt of xExis @within the unit disA suh tht its hEdistne from 0 is equl to the given hEdistne from a to bF log ssumptions re esily justi(ed y the ft tht wöius trnsformE tions tht preserve the unit dis preserve hEetweenness nd hEdistneF Five segment axiom. lemma assumes "{x, y, z, u} ⊆ unit_disc" "{x , y , z , u } ⊆ unit_disc" "x = y" "h_betw x y z" "h_betw x y z " and "h_cong x y x y " "h_cong x u x u " "h_cong y u y u " "h_cong y z y z "

shows "h_cong z u z u " prom our previous results we know tht there is n hEisometry M mpping xD yD nd u to x D y D nd u D respetivelyF e show tht it mps z to z D y using the ft tht there is n unique point on ry tht is on given hEdistne from the ry originF e onsider the ry x y F fy ssumption it ontins z F elsoD sine hEisometries preserve etweeness it must ontin M z @sine its preEimge xy y ssumption ontins zAF elso we know tht the hEdistne etween x nd z is the sme s the hEdistne etween x nd M z @s it is the sme s the hEdistne etween z nd z nd sine hEisometries preserve hEdistneAF herefore M mps z to z nd the theorem holds s hEisometries preserve distneF Identity of betweenness. sdentity of etweenness hs lredy een provedF lemma assumes "{u, v} ⊆ unit_disc" assumes "h_betw u v u" shows "u = v" Pasch's axiom. sh9s xiom is the most di0ult lemm to prove for the oinré modelF he following lemm expresses its nonEdegenerte seF lemma assumes "{x, y, z, u, v} ⊆ unit_disc" assumes "distinct [x, y, z, u, v]" "¬ h_collinear x, y, z" assumes "h_betw x u z" "h_betw y v z" shows "∃ a. a ∈ unit_disc ∧ h_betw u a y ∧ h_betw x a v" pigF UX sh9s xiom ! wlog position he entrl ide of the proof isD of ourseD to use the wlog pprohF rowE everD the hoie of points must e suh tht the intersetion point tht we lim to exist lies on the xExisF yne suh hoie leding to the proof is to ssume tht x = 0 nd tht v is positive rel numerF ine u is hEetween 0 nd zD y our previously proved hrteriztions of hEetweenness we know tht arg u = arg z nd tht |u| ≤ |z|F ine yD zD u nd v re di'erent from x = 0D we n swith to polr oordintes nd ssume tht u = |u|e iφ D z = |z|e iφ nd y = |y|e iθ F oint v is etween y nd z nd is on the positive xExis nd within the unit disF ine neither y nor z n e on the xExis @otherwise xD y nd z would e ollinerAD y our erlier hrteriztion of the hEetweenness of the xExis intersetion we know tht y nd z must e in di'erent hlfEplnes nd tht their rguments θ nd φ must hve opposite signsF e wnt to show tht the hEline yu lso intersets the xExisD y knowing tht the hEline yz interE sets the xExisF e hve seen tht the existene of tht intersetion depends of whether it holds tht (Re B) 2 > A 2 D where A nd B re mtrix oe0ients tht determine the hElineF unowing the polr forms for y nd uD nd mtrix onstrution for hElinesD fter simple lultions we show tht oe0ients A yu nd B yu for the hEline yu n e expressed y

A yu = 2|y||u| sin (φ -θ), B yu = i • (|u|e iφ (1 + |y| 2 ) -|y|e iθ (1 + |u| 2 )). herefore Re B yu = |y|(1 + |u| 2 ) sin θ -|u|(1 + |y| 2 ) sin φ, nd Re B yu A yu = sin θ 2 sin (φ -θ) • 1 |u| + |u| - sin φ 2 sin (φ -θ) • 1 |y| + |y| .
xote tht sin (φ -θ) nnot e zero s x = 0D y nd z re not ollinerF elsoD neither sin φ nor sin θ n e zeroD sine y nd z re not on the xExisF ery similr formuls hold for the hEline yz @otined y repling ll ourrenes of u y zAF e show tht Re B yu

A yu ≤ Re B yz A yz < -1.
he ltter inequlity holds s we know tht the hEline yz intersets the xExis in positive point vF efter sustituting the derived formuls nd neling ommon termsD provE ing the (rst inequlity redues to proving tht sin θ sin (φ -θ)

1 |u| + |u| ≤ sin θ sin (φ -θ) 1 |z| + |z| .
ine the rel funtion 1

x + x is deresing on the intervl (0, 1)D nd sine |u| ≤ |z|D this holds i' sin θ sin (φ-θ) is negtiveF e show tht this is the seF sf φ > 0D then it holds tht sin φ > 0D θ < 0D nd sin θ < 0F hen it holds tht Re B yz = |y|(1

+ |z| 2 ) sin θ -|z|(1 + |y| 2 ) sin φ < 0F ine it holds tht Re Byz Ayz < -1D it must e tht A yz > 0F ine A yz = 2|y||z| sin (φ -θ)D it must hold tht sin (φ -θ) > 0D nd sin θ
sin (φ-θ) is negtiveF he se φ < 0 is proved nlogously @then it holds tht sin θ > 0D ut sin (φ -θ) < 0AAF hereforeD we know tht the line yu lso intersets the xExis in positive point nd we know tht tht point is more inwrd the enter of the dis then the point vF hereforeD tht point is etween 0 nd vF pinllyD we know tht the point is lso etween y nd uD s their rguments φ nd θ hve opposite signs @in those proves we rely on our previously derived hrteriztions of hEetweennessAF hegenerte ses need to e proved seprtelyF sf some of the points xD yD zD u or v oinideD or if xD y nd z re hEollinerD the sought point a lso oinides with some of themD nd the xiom is esily proved due to the nonEstritness of etweennessF Lower dimension axiom.

lemma lower_dimension_axiom: shows "∃ a ∈ unit_disc. ∃ b ∈ unit_disc. ∃ c ∈ unit_disc. ¬ h_betw a b c ∧ ¬ h_betw b c a ∧ ¬ h_betw c a b"
vower dimension is proved very esily y showing tht 0D 1/2D nd i/2 re not hEolliner @sine lultions show tht i/2 does not lie on the xExis whih the hEline etween 0 nd 1/2A nd so none of the hEetweenness n hold @s hEetweenness implies hEollinerityAF Upper dimension axiom. lemma assumes "{x, y, z, u, v} ⊆ unit_disc" "u = v" assumes "h_cong x u x v" "h_cong y u y v" "h_cong z u z v" shows "h_betw x y z ∨ h_betw y z x ∨ h_betw z x y"

x u y z v pigF VX pper dimension xiom ! wlog position his xiom is esily proved y using wlog resoning nd our previous results on hEirlesF sf ny two of the points xD yD nd z re the smeD the sttement trivilly holdsF ytherwiseD wlog we n ssume tht x = 0 nd tht y is point on the positive xExisF ine u = vD hEdistne etween u nd xD hEdistne etween u nd yD nd hEdistne etween u nd z re stritly positive @hE distne is lwys nonEnegtive nd if it would e zeroD thn it would hold tht u = v = x or u = v = yD or u = v = zAF hereforeD we n onstrut hE irles entered t x nd y nd u nd v would e their two intersetion pointsF fy our erlier results we know tht they re iuliden irles ndD sine u = vD tht u nd v re mutully onjugteF he point z is n intersetion of two hE irles entered t u nd vD with the sme rdiusF e know those two hEirles re iuliden irles nd y using the formul for the iuliden enter we n esily show tht their iuliden enters re lso mutully onjugteF hen y simple resoning out omplex numers @in iuliden geometryA we n show tht z must e relD ndD thereforeD hEolliner with x = 0 nd y @tht is on xExisAF rEollinerity then implies one of the three hEetweennessF Negated Euclidean axiom. yn the other hndD hEdistne etween b nd c is equl to arccosh (25/9)F he hEetweenness then follows y the formul 2 arccosh x = arccosh 2x 2 -1D tht holds for x ≥ 1F st remins to show tht forll x nd yD if t is hEetween x nd yD then it does not interset either the positive segment of the x xis within the unit disD or the positive segment of the y xis within the unit disF e onsider n ritrry hEline through t = 1/2 + i/2F sf it is given y prmeters A nd BD then y the irline eqution it must hold tht 3A + 2 Re B + 2 Im B = 0F sf it intersets the positive segment of the xExis within the unit disD it must hold tht A = 0 nd tht Re B/ Re A < -1F fut then it holds tht Im B/A = -Re B/A -3/2 > 1 -3/2 = -1/2F herefore it nnot hold tht Im B/A < -1D wht must hold if the hEline intersets the positive segment of the yExis within the unit disF here re mny equivlent sttements for iulid9s prllel postulteF he equivlene etween QR postultes ws previously formlized in goq IIF ghoosing di'erent version of the postulte n help reduing the omplexity nd size of the proof tht this version does not hold in our modelF husD it would e interesting to otin these equivlene proofs within sselleGryv 6 D sineD fter refully nlyzing the QR postultesD the following one expressing tht for ny three nonEolliner points aD b nd c there exists point equidisE tnt from themD llowed us to otin proof whih ws muh simpler nd two times shorterX lemma

"∃ a b c. a ∈ unit_disc ∧ b ∈ unit_disc ∧ c ∈ unit_disc ∧ ¬ (h_collinear {a, b, c}) ∧ ¬ (∃ x. x ∈ unit_disc ∧ h_cong a x b x ∧ h_cong a x c x)"
e showed tht the sttement holds for points a = i/2D b = -i/2 nd c = 1/5F he (rst prt ws to prove tht points aD b nd c re not hEollinerF his ws esily hieved sine a nd b determine unique lineD the yExisD nd c does not lie on itF he next prt ws to prove tht perpendiulr isetors of segments ab nd ac do not meet @nd thus there does not exist point equidistnt from aD b nd cAF he perpendiulr isetor of segment ab is determined y hEdistne eqution h_dist a x = h_dist b xF oints a nd b re onveniently hosenD so tht the perpendiulr isetor of segment ab is the xExisD thus gretly simplifying the lultionF henD with some smll lultionD we proved tht no point on the xExis stis(es the hEdistne eqution determining tht point elongs to perpendiulr isetor of segment acX h_dist a x = h_dist c xF Existence of limiting parallels. e wnt to show tht for eh point a nd eh line x 1 x 2 not ontining a there exist two di'erent points a 1 nd a 2 so tht rys aa 1 nd aa 2 do not meet the line x 1 x 2 D nd tht for eh point a in ngle a 1 aa 2 the line aa meets the line x 1 x 2 F o prove tht this xiom holds in the [START_REF] Beeson | Finding Proofs in Tarskian Geometry[END_REF] There already exists tools that translate proofs from one proof assistant to another [1]. oinre disD we pply wlog priniple twieF pirstD wlog we n ssume tht a = 0 @this n e hieved y flshke trnsformAF xext we denote y i 1 nd i 2 the two di'erent idel points of the line x 1 x 2 F e show tht a 1 = i 1 /2 nd a 2 = i 2 /2 stisfy the xiom onlusionF ine i 1 = i 2 D it holds tht a 1 = a 2 F sn the extended omplex plneD the ry 0a 1 @it is n iuliden ryA meets the line x 1 x 2 @it is prt of n iuliden irleA in the point i 1 F he point i 1 is not within the unit disF here nnot exist their nother intersetion point within the unit disF sf there would e suh point xD then oth x 1 x 2 nd 0a 1 would ontin xD i 1 nd the inverse of x @wrtF the unit irleAD sine oth x 1 x 2 nd 0a 1 re hElinesF hese three points re di'erent @sine x is withinD i 1 is on nd the inverse of x is outside the unit disAD so x 1 x 2 nd 0a 1 would e the sme irlineD tht is impossile sine a = 0 is not on the line x 1 x 2 F hereforeD x 1 x 2 nd 0a 1 do not meet within the unit disF he proof tht x 1 x 2 nd 0a 2 do not meet within the unit dis is nlogousF pigF WX ixistene of limiting prllels ! wlog position xext we prove tht for eh point a in the ngle a 1 aa 2 the ry 0a meets the line x 1 x 2 F ine a is in the ngle a 1 aa 2 there exists x suh tht it is hE etween a 1 nd a 2 nd on the ry 0a F e gin employ the wlog priniple nd ssume tht x is on the positive prt of the xExis @this n e hieved rotting the whole on(gurtion round the originAF herefore x is positive rel numerF vine a 1 a 2 is not equl to xExis @otherwiseD sineD a 1 = i 1 /2 nd a 2 = i 2 /2D i 1 nd i 2 would hve to e equl to -1 nd 1D nd 0 would lie on x 1 x 2 D whih is flseAF herefore it intersets the positive prt of xExisF he line

A i = i • (i 1 i 2 -i 2 i 1 ) nd B i = i • (i 2 (|i 1 | 2 + 1) -i 1 (|i 2 | 2 + 1
)) e the oe0ients of the hEline i 1 i 2 iFeFD the hEline x 1 x 2 F he oe0ients A a nd A i re relF ine a 1 a 2 intersets the positive prt of the xExisD we know tht A a = 0 nd Re B a / Re A a < -1F ine a 1 = i 1 /2 nd a 2 = i 2 /2 y diret lultions it n e shown tht

Re B i Re A i = Im i 1 -Im i 2 Im i 2 • Re i 1 -Im i 1 • Re i 2 = 4 5
Re B a Re A a soD sine Re B a / Re A a is negtiveD so is Re B i / Re A i F ine 0 is not on the line x 1 x 2 D it is not n iuliden line nd A i = 0F ine x 1 x 2 intersets the xExisD it must hold tht (Re B i / Re A i ) 2 > 1F herefore Re B i / Re A i < -1D nd the line x 1 x 2 intersets the positive prt of xExis @iFeFD the ry 0x whih is the ry aa AF Continuity axiom. rski9s ontinuity xiom is essentilly the hedekind ut onstrutionF sntuitivelyD if ll points of set of points re on one side of ll points of the other set of pointsD then there is point etween the two setsF he originl rski9s xioms re de(ned within the frmework of pirst yrder vogi nd sets re not expliitly reognized in rski9s formliztionF snsted of speking out sets of pointsD rski uses (rst order predites φ nd ψF rowE everD while it would e possile to express the restrition of predites f nd g to pyv predites within the righer yrder vogi frmework of sselleGryv s in QID we hose to void itF hereforeD from strit viewpointD our forE mliztion of rski9s xioms within sselleGryv gives di'erent geometry then rski9s originl xiomti systemF lemma continuity_axiom: assumes "∃ a ∈ unit_disc. ∀ x ∈ unit_disc. ∀ y ∈ unit_disc. tillD it turns out tht it is possile to show tht oinré model lso stisE (es the stronger vrint of the xiom @without pyv restritions on predites φ nd ψAF sf one of the sets is emptyD the sttement trivilly holdsF sf the sets hve point in ommonD tht point is the point soughtF sn other sesD the proof is otined using wlog resoningF wöius trnsformtions tht preserve the unit dis re pplied so tht ll pointsD tht stis(es oth preditesD lie on the positive prt of xExis @nd inside unit disAF roving this requires using nonEtrivil properties of relsD iFeFD their ompletenessF gompleteness of rels in sselleGryv is formlized in the following theorem @the supremumD iFeFD the lest upper ound propertyA 7 X lemma assumes "x ∈ X" "∃ M . ∀ x ∈ X. x ≤ M " shows "x ≤ Sup X" he supremum property of rels n e used sine ll points re on the xExis nd hene their imginry prt is equl zeroF reneD ll points n e oserved s relsF henD the sttement redues to proving tht the (rst set of points @stisfying the (rst prediteA hs supremum nd tht this supremum is the point soughtF he (rst nd the seond sets of points do not hve ommon point @one of the speil ses in the eginning of proofAD so the seond set of points serves s upper ound for the (rst set of pointsF utting everything togetherD we ould prove tht the oinré dis model form model of elementry geometryX interpretation TarskiAbsolute ≡ h B h interpretation TarskiHyperbolic ≡ h B h interpretation ElementaryTarskiHyperbolic ≡ h B h 5 Conclusions and further work e hve formlly de(ned the oinré dis model within the projetive omE plex line CP 1 D nd mehnilly heked tht it stis(es rski9s xioms exept for iulid9s xiomF gontrry to the populr elief tht it is muh hrder to do thn for the uleinEfeltrmi model RHD our experiene shows tht there re oth dvntges nd disdvntges for oth modelsF he(nitelyD the hrdest thing in the oinré model ws to show tht it stis(es sh9s xiomD sine it requires introduing the etweenness on irlines @while the ulein model inE herits the etweenness on the iuliden line segmentsAF roweverD most other xioms re veri(ed more esily thn for the ulein modelD due to the ft tht irles in the oinré model re iuliden irlesD leding to very esy proof of existene of unique hEisometry etween two ongruent tringlesF he negted iuliden xiom ws esier to prove in one of its equivlent forE multionsD showing the usefulness of hving severl equivlent formultions of xioms IIF wny proofs hve een done y lgeri lultionsF implest lemms were proved utomtillyD y employing resoning out (elds @ville in the field_simps olletion of lemmsAF sn severl lemms the tti algebra @sed on qröner sis methodA ws very useful nd helped in reduing size of some proofsF he entrl tehniqueD without whih the formliztion would not hve een possileD ws without loss of generality reasoning QQF e hve proved IR di'erent wlog lemms nd used them undntlyF fsing the model in the extended omplex plne @insted of the rel plneA nd using the wellE developed mhinery of omplex vetors nd mtries @wonderfully desried y hwerdfeger TI nd formlized in the previous work of the (rst two uthors RIA ws lso very importnt deisionD leding to nier nd more elegnt formliztion @for exmpleD we never needed to distinguish etween the line nd irle segments within the oinré disD tht is uiquitous in expositions sed on lssiD iuliden nd grtesin geometryAF he formliztion of the oinré dis model n go eyond showing tht it stis(es the xiomsF por exmpleD sed on our foundtionD hyperoli trigonometry n e developed @we hve lredy esily proved the ythgoren theorem nd the hyperoli lw of osinesAD nd qussEfolyiEvohevsky formul @onneting the ngle of prllelism with the distneA n e provedF e pln to extend our work to other models of hyperoli geometryF elE though proving tht one model stis(es the xioms simpli(es tht proof for the other model @s one n pply trnsformtions from one model to the other oneAD de(ning other models nd their si ojets requires some nonEtrivil e'ortF elthough the exposition in the present pper ws driven y our sselleGryv formliztionD we hope tht it n e useful to wider udiene interested in forml geometryF

  xiom eWF he upper twoEdimensionl xiom eW mens tht ll the points re oplE nrF ine AD B nd C re equidistnt to P nd QD whih re di'erentD they elong to the hyperplne onsisting of ll the points equidistnt to P nd QF feuse the upper twoEdimensionl xiom spei(es tht AD B nd C re ollinerD this hyperplne is of dimension one nd it (xes the dimension of the spe to twoF st forids the existene of the point C @pigF RAF es for the (veEsegment xiomD the ft tht the segment ongruent to given segment in the model form iuliden irle will prove to e very importntF

  y z ∨ betw y z x ∨ betw z x y" begin denition on_line where -point p is on line ab "on_line p a b ←→ betw p a b ∨ betw a p b ∨ betw a b p" denition on_ray where -point p is on ray ab "on_ray p a b ←→ betw a p b ∨ betw a b p" denition in_angle where -point p is inside angle abc "in_angle p a b c ←→ b = a ∧ b = c ∧ p = b ∧ (∃ x. betw a x c ∧ x = a ∧ x = c ∧ on_ray p b x)" denition ray_meets_line where -ray ra-rb meets the line la-lb "ray_meets_line ra rb la lb ←→ (∃ x. on_ray x ra rb ∧ on_line x la lb)" end locale TarskiHyperbolic = TarskiAbsolute + assumes euclid_negation: "∃ a b c d t. betw a d t ∧ betw b d c ∧ a = d ∧ (∀ x y. betw a b x ∧ betw a c y -→ ¬ betw x t y)" assumes limiting_parallels: "¬ on_line a x1 x2 =⇒ (∃ a1 a2. ¬ on_line a a1 a2 ∧ ¬ ray_meets_line a a1 x1 x2 ∧ ¬ ray_meets_line a a2 x1 x2 ∧ (∀ a'. in_angle a' a1 a a2 -→ ray_meets_line a a' x1 x2))" locale ElementaryTarskiHyperbolic = TarskiHyperbolic + assumes continuity: "(∃ a. ∀ x. ∀ y. φ x ∧ ψ y -→ betw a x y) -→ (∃ b. ∀ x. ∀ y. φ x ∧ ψ y -→ betw x b y)"

  sn the (nite omplex plneD wöius trnsformtions re iliner iFeFD trnsE formtion de(ned y the mtrix a b c d mps the omplex numer z to az+b cz+d F 2.3.3 Circlines he si ojet in the extended omplex plne is generalized circleD or circline for shortF e signi(nt property of the extended omplex plne is tht irline represents oth line nd irles in uniform wy using the eqution Azz + Bz + Cz + D = 0D where C = B nd A nd D re relF his eqution represents line when A = 0 @eFgF when in(nite point elongs to the irlineA or irleD otherwiseF sn our lgeri formliztion this eqution eomes z * Hz = 0D where z is vetor of homogeneous oordintesD nd H is nonE

  "conjugate_cl_cmat2 (A, B, C, D) = (cnj A, cnj B, cnj C, cnj D)" lift_denition conjugate_cl :: "circline ⇒ circline" is . . . Möbius transformations that map the unit circle onto itself n e reogE nized y their mtriesF hese mtries re either of the form k • a b b a or k • -a -b b a D ut lso hve the following hrteriztionF denition unit_circle_fix_cmat2 :: "cmat2 ⇒ bool"

  lemma "∃ a b c d t. {a, b, c, d, t} ⊆ unit_disc ∧ h_betw a d t ∧ h_betw b d c ∧ a = d ∧ (∀ x y. x ∈ unit_disc ∧ y ∈ unit_disc ∧ h_betw a b x ∧ h_betw a c y -→ ¬ h_betw x t y)" e show tht the sttement holds for points a = 0D b = 1/2D c = i/2D d = (5 -√ 17)/4 + i • (5 -√ 17)/4D nd t = 1/2 + i/2F rEetweenness of a = 0D dD nd t is esily shown y showing tht d nd t hve the sme rgument @sine they re proportionl y positive rel ftorA nd |d| < |t|F rEetweenness of bD dD nd c is shown y showing tht the hEdistne etween b nd c is equl to the sum of hEdistnes etween b nd d nd d nd cF ine these two re the smeD this redues to showing tht the hEdistne etween b nd c is twie the hEdistne etween b nd dF hese re lulted y the hEdistne expliit formulD derived erlierF fy this formulD fter rief lultions we determine tht the hEdistne etween b nd d is equl to arccosh ( √ 17/3)F

x 1 x 2

 2 intersets xExisF xmelyD sine x is etween a 1 nd a 2 D nd it is on the xExisD it holds tht Im a 1 • Im a 2 < 0F ineD Im i 1 • Im i 2 = 4 • Im a 1 • Im a 2 < 0D x 1 x 2 doesinterset the xExisF e need to show tht it intersets its positive prtF vetA a = i • (a 1 a 2 -a 2 a 1 ) nd B a = i • (a 2 (|a 1 | 2 + 1) -a 1 (|a 2 | 2 + 1))e the oe0ients of the hEline a 1 a 2 D nd let

  φ x ∧ ψ y -→ h_betw a x y" shows "∃ b ∈ unit_disc. ∀ x ∈ unit_disc. ∀ y ∈ unit_disc.

  φ x ∧ ψ y -→ h_betw x b y"

  x 1 , . . . x k . asm 1 ; ...; asm n =⇒ concl" where asm 1 D F F F D asm n re ssumptionsD concl is onlusionD nd x 1 D F F F D x k re universlly qunti(ed vrilesF snsted of lemmaD keyword theorem n e used @s there re no forml di'erenes etween lemms nd theoremsAF exiom systems in sselleGryv re usully spei(ed s locales PF e lole is nmed ontext of onstnts @funtionsA f 1 D F F F D f n nd ssumptions P 1 D F F F D P m out them tht is introdued roughly like locale loc = xes f 1 , . . ., fn assumes P 1 , . . ., Pm.

voles n e hierrhil nd lole n extend n existing lole y dding new ssumptionsD s in locale loc a loc 1 C assumes F F F F sn the ontext of loleD de(nitions n e mde nd theorems n e provedF voles n e interpreted y onrete instnes of f 1 D F F F D f n D nd then it must e shown tht these stisfy ssumptions P 1 D F F F D P m F heorems proved strtly within lole re utomtilly trnsferred to ll their interprettionsF PFP rski9s xioms sn IWSW elfred rski gve set of xioms for sustntil frgment of iuE liden geometry tht is formulle in (rstEorder logi with equlityD requiring no setEtheoryF rski9s xiom system is sed on single primitive type depitE ing points nd two preditesD nmely ongruene nd etweennessF AB ≡ CD sttes tht the segments AB nd CD hve the sme lengthF A B C mens tht AD B nd C re olliner nd B is etween A nd C @nd B my e equl to A or CAF por n explntion of the xioms nd their history see TTF le I lists the xioms for iuliden geometryF A1 Symmetry AB ≡ BA

  Re A 2 )" lift_denition x_axis_intersection_outward :: "circline ⇒ circline ⇒ bool" is . . .

	he hrteriztion of this funtion is given y the following lemmF
	lemma assumes "is_h_line H 1 " "is_h_line H 2 " assumes "intersects_x_axis_positive H 1 " "intersects_x_axis_positive H 2 " assumes "x_axis_intersection_outward H 1 H 2 " shows "Re (to_complex (calc_x_axis_intersection H 1 )) ≥
	Re (to_complex (calc_x_axis_intersection H 2 ))"
	por Re B A	< -1 the position of the xExis intersetion point within the dis
	is given y -Re B A	-( -Re B A

We use the numbering of theorems as of the tenth edition.

http://afp.sourceforge.net/

From this example it can be seen that the lifting must be done in two stages (one for the subtype and the other for the quotient type). However, to simplify the presentation, in the rest of the paper we shall show only the initial and the nal denition.

Note that such claim is slightly imprecise. In a strictly typed setting the value of the cross ratio is a number in the extended complex plane CP 1 . If dierent from ∞ h , then it can be converted to an ordinary complex number and we claim that its imaginary part is equal to 0. Formally we claim that is_real (to_complex (cross_ratio u i 1 v i 2 )), where is_real x ≡ Im x = 0. For simplicity, we shall sometimes make such simplications.

there is no development about real closed elds in Isabelle/HOL. This is the reason that motivated us to avoid the restriction of predicates f and g to FOL predicates.

This work is partially supported by the Serbian Ministry of Education and Science grant 174021