San Francisco bay area passes regional measure to fund transit and at least one transit agency here puts "thank you voters" on the front of their busses.

Suppose that you are given the following problem: Given a collection of points in a square grid in a plane, and a specified start and end point, can you find a path in the grid that goes through every point exactly once, and without vising any other points? Here's an example; can you go from 𝑠 to 𝑡, moving along the grid, visiting each blue grid point once, but never touching any of the other grid intersections?

1/10

#math #compsci #quantum

@dantheclamman ... is this you?

Today it was was a beautiful day again. Even though I cycle everyday to commute to work, I decided to cycle, but in the opposite way in the canal, for enjoyment of the beautiful day. It was so nice.

(Just in order to say something positive.)

@soaproot This is a special case of the adjunction between rigs (+, ×, 0, 1) to rings (+, ×, -, 0, 1). You could formalize the fact that any rig R gives a ring R* such that R embeds into R* universally. I believe this is how Unimath library formalizes reals.

Constructive taboos.

I think this terminology was coined by Peter Aczel.

Here is a list of typical constructive taboos.

* Excluded middle (EM). For every proposition P, either P holds or ¬ P holds.

* Weak excluded middle. For every proposition P, either ¬ P holds or ¬¬ P holds.

* De Morgan Law (DM). For all propositions P and Q, we have that ¬ (P and Q) ⇔ (¬ P or ¬ Q).

* Limited Principle of Omniscience (LPO). For every infinite binary sequence α, either there is n with αₙ ＝ 1, or else αₙ ＝ 0 for all n.

* Weak Limited Principle of Omniscience (WLPO). For every infinite binary sequence α, either αₙ = 1 for all n, or not.

* Lesser limited Principle of Omniscience (LLPO). For every infinite binary sequence with at most one 1, either the even terms are all 0, or the odd terms are all 0.

* The world's simplest axiom of choice (WSAC). Every family, all of whose elements are doubletons and which has at most one element, has a choice function.

1/

This is a 🧵 about the Dedekind cut construction of real numbers in #constructiveMathematics , particularly two technical details. The first has to do with defining additive inverse and multiplication, when we can't use excluded middle for things like "is a real number positive or not?". The second is about one sided versus two sided cuts.

1/8

I've posted about this a few times but let me try to do so more clearly. How do we, in #constructiveMathematics , show that a set is countably infinite (that is, there is a bijection between our set and the set of natural numbers)? There's a theorem for this which is elegant and also handles some of the trickier cases such as showing that the set of rational numbers is countably infinite. 1/5

My life as a math nerd:

Me: did you know that any natural number equal to one mod 4 can be written as the sum of two squares?

Them: what about nine?

Me (not in front of reference material): <stammers>

Me (12 hours later): OK, any PRIME equal to one mod 4. For example, 13 = 2^2 + 3^2, 17 = 1^2 + 4^2, 29 = 2^2 + 5^2, etc.

Them: 👍

I'm planning to make a habit of boosting some old mathematics threads (by myself or others), in response to a recent request that we use this network to, uh, talk about math rather than just uh, whether the field is getting ruined or whatever.

I might use use quote posts to explain this is an older thread or any other context, but quote posts aren't available for things that were posted before Mastodon added quoting, if the author turned off quotability, etc.

We work constructively in HoTT/UF.

Let ℕ∞ be the type of conatural numbers, which extends ℕ with a point at infinity.

The type ℕ∞ has decidable equality iff WLPO holds.

However, for every n : ℕ and x : ℕ∞, it is decidable whether n ＝ x. We say that the finite elements of ℕ∞ are "isolated".

An intuition for a general element of ℕ∞ is as the behaviour of a stopwatch that either ticks finitely many times and then stops, or else ticks forever if nobody bothers to stop it.

With this intuition, define x ＝ₘ y, for x y : ℕ∞, to mean that we can't distinguish x and y after only m ticks. I am sure you can make this formal if you want to.

I will abuse language and regard any n : ℕ as an element of ℕ∞ by ticking n times and then stopping.

Let f : ℕ∞ → ℕ be any function.

There are (at least) six senses in which f can be considered to be continuous.

(1) ∃ m ꞉ ℕ , (Π n : ℕ , f (max m n) ＝ f ∞).

(1') Σ m ꞉ ℕ , (Π n : ℕ , f (max m n) ＝ f ∞).

(2) Π x : ℕ∞ , ∃ m ꞉ ℕ , (Π y : ℕ∞ , x ＝ₘ y → f x ＝ f y).

(2') Π x : ℕ∞ , Σ m ꞉ ℕ , (Π y : ℕ∞ , x ＝ₘ y → f x ＝ f y).

(3) ∃ m ꞉ ℕ , (Π x y : ℕ∞ , x ＝ₘ y → f x ＝ f y).

(3') Σ m ꞉ ℕ , (Π x y : ℕ∞ , x ＝ₘ y → f x ＝ f y).

Perhaps surprisingly, they are all logically equivalent, constructively, without the need for Brouwerian intuitionistic axioms.

(1) continuity property at ∞.

(1') continuity data at ∞.

(2) continuity property at all points

(2') continuity data at all points.

(3) uniform continuity property at all points.

(3') uniform continuity data all points.

If you want to see formal definitions, statements and proofs, here they are:
https://www.cs.bham.ac.uk/~mhe/TypeTopology/TypeTopology.DecidabilityOfNonContinuity.html

1/

I hear laments that Mathstodon has more chatter on the death of math than on math these days. So here's a funny math factoid I recently learnt from https://jasonzeshengchen.github.io/blog/2023/three-proofs-of-incomp-Turing-degrees/ . You can prove that there exist incomparable Turing degrees in three lines as follows:

The Turing reducibility order between oracles is arithmetic, hence Borel, hence has the Baire property. As each oracle has countably many predecessors, this relation is meager by Kuratowski–Ulam, and its inverse relation is likewise meager, so it can't be total by the Baire category theorem.

(The argument also works with measure instead of Baire category.)

Of course, the usual proof is more or less a specialization of this, but I found it enlightening to see it written that way.

(And yes, in spite of nominally doing research that involves computability theory, I'm still not familiar with certain things probably considered basic by computability theorists, like the computability-theoretic version of forcing, but I'm catching up.)

I’m working through beginner scheme theory and the affine real line is weird. There’s all the usual points, and sure, the generic point is smeared all over, but then we have a ton of extra closed points too. I’m imagining it as the closed upper half plane, but that doesn’t seem quite right

@soaproot I believe your definition of finitely supported function is correct when the domain is a discrete set. When I is not necessarily discrete and A is a pointed set (a set with a zero element), I would propose to define a finitely supported function from I to A to be an element of the colimit of all sets Map(J, A), taken over all maps J -> I where J is a finite set.

When I is discrete, one can restrict to subsets J of I and one recovers your description. Note that if I is not discrete, there is no natural map from my proposed colimit to the set Map(I, A), so "finitely supported function" is no longer a special case of "function", but something different.

This thread is related:
https://mathoverflow.net/questions/302516/constructively-is-the-unit-of-the-free-abelian-group-monad-on-sets-injective

References:
* https://ncatlab.org/nlab/show/support+of+a+function
* https://us.metamath.org/ileuni/df-fsuppfi.html
* https://github.com/metamath/set.mm/issues/5539 including the comments and linked pull requests
10/10

Perhaps this way of treating finitely supported functions constructively is in the literature (or perhaps it is the kind of technical detail which no one thinks to publish), I'm not too sure. But I hope it was interesting for you to read about my work on polynomials and finite support. 9/10

We will even be a bit bolder and define a "finitely supported function", constructively, as a function which has a finite subset of the domain such that all values outside that subset map to zero. Given decidable equality on both domain and codomain, this is equivalent to the definition of a finitely supported function as a function whose support is finite. 8/10

With these definitions we will be able to show that adding two polynomials yields a polynomial, that multiplying two polynomials yields a polynomial (here we are glad we defined all coefficients rather than just up to some fixed exponent, as the degree of the product is larger than the degree of the polynomials we multiplied), and all the other ring properties hold. 7/10

How do we say that such a multivariate power series is a polynomial (that is, has finitely many terms)? Classically, same as before, the support of the power series is finite. Constructively, we will say there is a finite set of tuples such that any tuple outside that set has a zero coefficient. 6/10

We now wish to extend our definition to multivariate polynomials (polynomials with a finite number of variables). To define a term we need one exponent for each variable (you can call this a tuple, a word, or a function from the set of variables to natural numbers including zero, for this post I'll say tuple). A power series is then a function from tuples to coefficients. 5/10