On 01/22/2024 06:49 PM, Ross Finlayson wrote:
> You know I haven't read your library yet then for for drawing a circle,
> it's generally appreciated that drawing a circle is difficult freehand,
> while, a line, or stroke, can sometimes be drawn in a faster line or straighter,
> or, sometimes the curve can make a round, where, the drawing the curve
> is "The Turtle of the Logo Language", which is like a snake or otherwise
> filling in neighboring regions according to parametrically that the turtle
> points in a direction and draws line of a length.
>
> For drawing a circle I appreciate, that, parametrically for an angle about
> "2 Pi radians", sine and cosine fill in the +-1 quadrants, about some origin
> or co-site or "the pixel in the middle", in pixels and voxels or picture elements
> and volume elements, after ray-tracing in 3D what is drawing.
>
>
> It has to be right from the center, about that there will be some values of
> rotation, that, should or will give, ellipses, while in the course-of-passage
> one rotation, "the circle of the same perimeter does not have this ellipsoid".
>
>
> I.e., for each angle offset, it has an apparent perimeter. There's a circle
> with the same perimeter. The ellipse has only two axes of symmetry,
> X and Y. They cross and that's the center of the ellipse and the two
> nails that define the "tautochrone" what in constant time draws the
> same perimeter, so, it's only an ellipse, if, it results the ratio of the
> half-height and half-width, of the ellipse, must be same, as
>
>
> root c, + b
> and
> root c, + a
>
> of side b in x and a in y and side c the hypotenuse the bisection of
> the obtuse angle of what results the triangle that has same perimeter,
> as a polygon, as the length of the diameter, a line.
>
> Then I forget the formula for perimeter of one quadrant or
> "drawing chord", then to figure it with "secant".
>
> So, this is what I am thinking is that according to some properties
> I heard that defines an ellipse in terms of a circle instead of a conic
> section, of course that besides it's defined in conic sections only
> as "not parabolic, or circular, or, hyperbolic, ...", for making the "cone"
> as the usual projection, in that the cone is open in the direction of
> travel or "vision" in the sense of drawing perspective. (View, image.)
>
>
> I figure that by computing the value of the perimeter of the ellipse
> with
>
> width: 2 (root c + a)
> height: 2 (root c + b)
>
> it indicates the circle with diameter 2b as being an ellipsoid of the circle.
>
>
> Then, there's that, at any point, in the first quadrant (where both coordinates
> are positive), for a point D on the circle, O the center and A the point where OA the line is a,
> there is a triangle with sides OD and AD, two "diameters" of a sort, and OA - that with sides
> a = OA, o = OD, d = AD, that a + o + d = 2(a + b + c).
>
> Then, according to the angle between a and o, is to figure out how to break the
> obtuse triangle that is not isosceles, also to find the points where it's isosceles.
>
> Here by "break" it's that I want to compute, given angle ao, that is basically between
> the x axis and the line from the center to a point on the ellipse, to compute the length
> of o, or rather to solve for the value of o, given b, and a.
>
> Then, ellipse-drawing would be similar your circle drawing approach, over 2 Pi radians.
>
>
> Here it seems like the approach to breaking the triangle OAD, is to break the obtuse
> triangle into a right triangle, and a smaller obtuse triangle with what was left of AD
> the hypotenuse and what was left of OD the middle length, then from the height of
> this triangle, to, break down the resulting leftovers , to compute the length of OD given
> the angle between a and o, and, a, and b.
>
>
> "Seems we're all to read Seminaire de Geometrie Algebrique du Bois Maries
> as for Dieudonne and Groethendieck, but my French is poor and accents
> terrible. "
>
>
>
> "Ellipses don't have a radius, ..., it's two diameters, ...".
>
> "Frame contractions: fields and couples", ....
>
> "Lagrangians: I ate a zinc today"
>
> "Lagrangians: I ate a zinc today, the Lagrangian held up the derivative"
>
> -- "it is not a lemma"
>
>
> Already gave all the answers.
>
>
> Heh, surprise: two surprises.
>
>
> "That a full logic, is built up in so few terms,
> from that an empty logic is not an empty logic."
>
>
> Here "Hartogs is the Pope, not Russell, ..., who is also not the Pope".
>
> "Is Hartogs even Catholic?"
>
> "Russell, is not the Pope."
>
>
>
>
> Hmm. So, the ellipse, is having a parametric definition, in a and b.
> So is the circle, where b = c. This is a triangle, connecting as if two
> nails in a board and a closed loop of string, were drawn about them an ellipse.
>
> It's that the perimeter is same what is confounding.
>
> For as if any about around drawing the loop, it's the same perimeter.
>
>
> I read this fact I think in some Ordinary Differential Equations work, ....
>
> That the perimeter was same - I had already drawn the ellipse, then as
> what I'd wonder how is the Bezier curve, what must be functional, when
> everyone knows Bezier though nice, is not polygonal and geometric at all.
>
> Yet, here only I am weakening when there is to be breaking the triangle,
> breaking off small right triangles, until the triangle is exhausted, to compute
> the length of the distance between the center, and some point on the curve,
> according to the angle, given a and c.
>
> The first is is pretty clear or a's, figuring, that, at for example small angles,
> then it would be a would be large the first, pointing out a good feature that
> in the method, if correspondingly the first triangle is specifically measured
> when also the angle is small, or rather 90 or 270 degrees, small from that,
> otherwise for example at 0 and Pi radians, a's triangle is small, and the recursion
> to compute each next triangle, then starts from that it's _under_ where a's
> triangle intersected the triangle and the ray up from a, the same rather,
> that the triangle under that is right, and, it's base is according to the angle
> of a thus cos a on the unit circle, thetriangle's hypotenuse is up AD, then that
> the next next is what's left above it, in OA OD AD.
>
>
>
>
> Cantor was very enthusiastic that the centrality of uncountability, was fundamental.
>
> He had found several proofs to said effect.
>
> He was a model aggrandizer. I.e. that his other conjectures were contradictory, or
> underdefined when translated to the models of numbers, he dropped them.
>
>
>
>
> Then for something like "Cantor's sets where CH and GCH are strong, are rather mostly
> like sets yet instead in cardinal theory", is about for making cardinals besides a primary
> theory, nudging it alongside the set theory that include "Not CH", "Not GCH", ....
>
> I.e. it's said Cantor's goal mostly was the continuum hypothesis, but there are ordinals.
> The notion of cardinal theory came after Cantor's convincing uncountability theorems.
>
> In cardinal theory sets share a rank or order in cardinals, next rank is up, while
> in ordinal theory sets share a rank or order in ordinals, next rank is next.
>
> I.e. ordinals don't share a rank, but,in "well-founded" set theory, the "simplest"
> ordinals, the initial ordinal has a cardinals, the ordinals happen to share.
>
>
>
> I only have ten or so books on Ordinary Differential Equations, and boundary
> value problems, here the idea is making the triangle into a strip or strips and
> perhaps building squares what fill acute or obtuse from an angle and axis,
> these few different patterns, for a >= 0 and b <= c.
>
> Then it's like "the ellipse is the catenary outside and all around, equilibriating
> pressure, while outside is compression as between discs".
>
> They must already have one or its parts but here I'm still looking at this "2 (a + root c)",
> and "2 (b + root c)". Adding values and roots of other values, must have a graphical
> representation. I.e. "the square with area c its side", and b being the same value,
> makes that where b = root c, about that c = b^2, then that according to addition
> it simplifies to 2 (x + x), then to take advantage of where power terms have additive
> terms like logarithms, in usual replacements and substition what result a solution,
> that "according to the graphical representation its transforms under terms", build
> generally a making for that each these expressions are also parameters themselves,
> i.e. then as to how in terms of a and b, and 2a + b + c, and a + o + d, that about 2 (a + root c)
> and 2(b + root c), that a graphical representation results.
>
> That c = b^2, here is for that where c = 1, the radius, then it's different than "whatever
> is the diameter of the circle of the ellipsoid, c > 1", about whether exists only c = b = 1,
> or, that it's root c < c.
>
>
> "Ellipses don't have a radius, ..., it's two diameters, ...".
>
>
> That's like "there's somebody in the pub, if they drink, they forget".
>
> Then there's "if you came here to drink to forget, please pay in advance".
>
>
> The primes-as-multisets-courtesy-arithmetic is pretty great,
> multiplications are mutiset-unions, resulting the combined contents.
>
>
> About density in primes and the modular, for arithmetic, I'm wondering
> I suppose about density of primes, and density of small and larger primes,
> when what results terms in arithmetic, factor both sides the primes,
> out of the distribution of their roots existing or factors, where, there
> are for factors and "fundamental theorem of algebra", real roots,
> then for "fundamental theorem of arithmetic", ..., is for probabilities
> in primes, then also, guarantees filling, when it's sure so many primes,
> are under some bounds.
>
>
>
>
>
>
> https://mathworld.wolfram.com/InverseCurve.html
>
> Hm, this says the Peaucellier inverser, makes a linkage of lines connected
> at points that is a linkage, which resuils a drawing machine of sorts,
> as to the pantograph arm.
>
> " The lituus is the locus of the point P moving such that the area of a circular sector remains constant."
> -- https://mathworld.wolfram.com/Lituus.html
>
>
> "The locus of the apex of a variable cone containing an ellipse fixed in three-space
> is a hyperbola through the foci of the ellipse. In addition, the locus of the apex of
> a cone containing that hyperbola is the original ellipse.
> Furthermore, the eccentricities of the ellipse and hyperbola are reciprocals. "
> -- https://mathworld.wolfram.com/Hyperbola.html
>
>
> https://mathworld.wolfram.com/ReflectionProperty.html
>
> More facts about ellipses, ....
>
> "In 1882, Staude discovered a "thread" construction for an ellipsoid analogous
> to the taut pencil and string construction of the ellipse (Hilbert and Cohn-Vossen 1999, pp. 19-22).
> This construction makes use of a fixed framework consisting of an ellipse and a hyperbola. "
> -- https://mathworld.wolfram.com/Ellipsoid.html
>
> "The" "parametric equations of an ellipsoid", ..., here notice under inverses are
> their re-parameterizations, i.e. what are various parametric definitions that result
> the same objects according to geometry.
>
>
> A deck of cards has, each card, has fourfold synmmetry, horiztonal, vertical, and either way
> diagonally.
>
> So, if a deck of cards is split in half by one of its axes of symmetry, there results two decks
> of cards, that can be split again, and again, but, not again, into decks of cards with at least
> half the legible pip.
>
> Because the pips are on the corners, they can only be split diagonally once, besides that
> horizontally and certically they can be split once, each, resulting 4 pips those split into two,
> for 8 pips, making four decks of rectangular cards or eight decks of triangular cards.
>
>
>
>
>
> Here it's for that ellipses have two axes of symmetry except the special case spheres, that,
> those split the quadrants to make what rolls up in cones, what results that how much the
> cone is not a right cone, is the same the eccentricity, so parameterized the same way as by
> a which is not the eccentricity,
>
> Also there's for circles at each corner of a triangle and their ellipses with respect to each
> circle's coordinates with respect to each other.
>
>
>
> Here it looks "eccentricity" and "curvature" are defined about same.
>
> https://en.wikipedia.org/wiki/Eccentricity_(mathematics)#Ellipses
> https://en.wikipedia.org/wiki/Confocal_conic_sections
>
>
> https://en.wikipedia.org/wiki/Ellipse#Pins-and-string_method
>
>
> So, here "a" is just the distance from the center to a locus.
>
>
>
> Ellipse is two diameters, ....
>
>
>
> About that OA is longer than OD when x < a, and up to 2a, , is for that OD OA < c^2.
>
> I.e., here the point is to work down, the part before and after, here is that drawing the
> first quadrant of this ellipse, sees that OA is the hypotenuse or "long side", "the long side's
> always the hypotenuse". OA is only the long side up to point at ( a/2, f(a2) ), where f is some
> function that's parameterized in part by a, and later b or c. Then in the rest of the curve OD
> is the long sideas where it reaches (a + 2 (a + root c), 0 ), that f(a + 2(a + root c) ) = 0, or here
> for example about f ( 3a + root c ) = 0.
>
>
> --- "Gray-scale area-averaging"?
>
> Mostly for sure there is that after something is already rasterized, in a quadrant,
> that basically affine transformations are computed, for all right angles, just make
> "8 orientations", ..., about off-by-one.
>
> High screen resolution's afforded a lot of complacency in raster registration,
> and usual enough aliasing and artifacts, ..., of ... aliasing.
>
> https://docs.oracle.com/javase/7/docs/api/java/awt/image/AreaAveragingScaleFilter.html
>
> Have I implemented such before or an area-averaging filter, yes, so, in the generation of
> grayscale thmubnails from page images. I invented and implemented one.
>
>
>
> As they pass each other seeing each other their field of view takes in both origins and destinations.
>
>
>
> That's what you get for getting led along.
>
>
> Here an example is "division by zero". All these people starting with zero and numbers,
> then adding division, leaving out zero instead of no zero, these are clumsy and cumbersome.
>
> Not contradicting each other while still have mutually compatible interpretations of views,
> what result abstractly the value of fairness where it's the only principle, that all the
> definitions are composed into one definition, besides that inference exists.
>
> One of the other here for example "numbers with zero" and "numbers and division",
> entirely are differently varied smaller collections of direct resulting inferences,
> that only one or the other is eventually exhausted in any sense of completion.
>
>
>
> "Infinite" ordinals, ....
>
>
>
> https://www.maa.org/press/maa-reviews/a-history-of-japanese-mathematics
>
> "... and Wada Nei's contributions to the understanding of hypotrochoids".
>
> "Sections of an elliptic wedge, for example, ...".
>
>
>
> How about Tableau?
>
>
>
> Various Goldbach conjectures are undecide-able in extra-Archimedean extensions of integers.
>
> So, the "don't care" bit was "already got a wider world".
>
> There's also models with a triple prime at infinity.
>
> Of course, that's in a number theory, with a prime at infinity. There are others, ....
>
> Anyways though it's great youre boring and under-informed.
>
>
> Saying it's in Windows doesn't mean being used -
> most of that (..., user-space) uses _you_, not the other way around.
>
> Old "ball and chain" as it were.
>
>
>
>
> f = f'
> ...
>
> f' = 0
> f' = c
>
>
> d^2 f = 0
> /dx^2
>
> f = cx
>
>
> I guess that depends whether it's me or your profile. Like a sock-puppet.
>
>
> "Ordinary Integral Equations"
>
> "Scholze and Clausen say they have already found simpler, ‘condensed’ proofs
> of a number of profound geometry facts, and that they can now prove theorems
> that were previously unknown. They have not yet made these public."
>
> "Relies on facts from stable homotopy theory, ...". Adding a univalency axiom is a lot of
> strength, though, there are derivable immediately usual contradictions of the illative
> to the well-founded.
>
> Differential equations:
>
> f' = f
>
> e^x
> f(n/d), d->oo, n-> d
>
>
> "Most special functions are solutions of differential equations, ...".
>
> https://leanprover-community.github.io/mathlib_docs/measure_theory/measurable_space.html
>
> https://leanprover-community.github.io/mathlib_docs/meta/univs.html
> https://leanprover-community.github.io/mathlib_docs/logic/small.html
>
> https://leanprover-community.github.io/mathlib_docs/model_theory/definability.html
>
> Yeah, running out "not definable" helps remind that adding univalency to ordinary
> set theory, makes for that "Russell is not the Pope".
>
> https://leanprover-community.github.io/mathlib_docs/set_theory/zfc/basic.html
>
> Lean "Class": "set Set".
>
> https://leanprover-community.github.io/mathlib_docs/init/data/set.html#set
>
> You see Lean defines Set in terms of membership predicates, but,
> the only relation in ZFC is "elt".
>
> Yeah, it's a usual hypocritical mish-mash, but, I suppose lots of nCatLabs has
> ready reading into anything, it..., "says".
>
> https://leanprover-community.github.io/mathlib_docs/set_theory/zfc/basic.html#Class
>
> "Class: the collection of all classes".
>
> Class-set distinction and the group-noun game,
> makes for writing many simply inconsistent multiplicities in Lean's words,
> but if you ignore the part that disagrees with you then your ignorance will be invincible.
>
> Yes it looks a very usual these days' "the strength of ZFC and two large cardinals".
>
> https://leanprover-community.github.io/mathlib_docs/topology/subset_properties.html
>
>
>
> Big ripoff of nCatLabs?
>

I doubt that any of this fits into your squirrel brain.

For lean prover you have to first do this:

Simple Types
https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus

A formulation of the simple theory of types, Alonzo Church
https://www.semanticscholar.org/paper/28bf123690205ae5bbd9f8c84b1330025e8476e4

I mean how do you want to understand a type notation like α → Prop ?

Ross Finlayson schrieb:
> https://leanprover-community.github.io/mathlib_docs/set_theory/zfc/basic.html#Class