I know the lines are generated by projecting geodesics on a hyperboloid to a plane and the boundary of the disk comes from the asymptotic cone around the hyperboloid, but I just don't see why the projections intersect the boundary of the circle at a right angle.
On
Why do lines in the poincare model meet the infinite edge at right angles?
Interesting question
you can look at it from many different points:
Axiomatic
Trough very two points there is one line and one line only, and when the limitation was not in place then trough two points there could be more than one line. (and making the whole model a geometrical farce)
limit line
the boundary is the limit how else than orthogonal can you reach it? or in other words how else would you transform a segment into a line?)
Klein model
The Poincare model is a projection from the Beltrami Klein model https://en.wikipedia.org/wiki/Beltrami%E2%80%93Klein_model and just the projection causes the lines to be orthogonal.
Poincare half plane model (something similar as above for the https://en.wikipedia.org/wiki/Poincar%C3%A9_half-plane_model ) not very convincing, why would lines have to be orthogonal in this model :)
so I would stick to the axiomatic one, but having said all this
In projections from the normal euclidean plane into the unit circle other rules apply (lines become lines or elipses connecting two opposite points on the boundary circle) and for elliptic geometry ( lines are circles or lines connectiing opposite points of the boundary circle)
On
Another point of view (which is the theme of John Stillwell's book "Four pillars of modern geometry"), is a synthetic derivation that starts with the upper half plane equipped with its group of rigid motions: namely, the group generated by the fractional linear action by $PSL_2(\mathbb{R})$ together with reflection across the upper $y$-axis.
From this, build up your knowledge of the geodesics in steps.
First, since the upper $y$-axis is the invariant line of a reflection, it is a geodesic.
Next, using translations $f(z)=z+b$ one sees that all upper half vertical lines are geodesics.
Next, using the inversion $f(z) = -1/z$ one sees that certain semicircles with endpoints on the real axis are geodesics.
Next, again using translations, one sees that all semicircles with endpoints on the real axis are geodesics.
Next, one verifies the set of upper half vertical lines union the set of all semicircles with endpoints on the real axis is invariant under the group of rigid motions (it suffices to check generators, $f(z)=az$, $f(z)=z+b$, $f(z)=-1/z$, and the reflection across the upper $y$-axis).
Next, check that Euclid's first axiom holds: two points determine a line.
Now you should be convinced that you have found exactly the correct set of lines.
I should add as a final point, that the upper half plane and the Poincare disc (which is what you asked about directly) are connected by a Mobius transformation that preserves angles and that preserves the set of Euclidean lines and circles, and so from the form of lines in the upper half plane one derives their form in the Poincare disc.
You need to follow through a sequence of maps. Project the intersection of the hyperboloid $z=\sqrt{x^2+y^2+1}$ with a plane through the origin onto the unit disk at height $z=1$. This gives a general chord of that disk. Move the disk down to the unit disk at height $z=0$. Project the line segment back up to the unit hemisphere (now the segment becomes an arc of a circle orthogonal to the unit circle), then project back to the unit disk by stereographic projection from the south pole (so the arc becomes an arc of a circle which remains orthogonal to the unit circle)!