falsehoods programmers believe about time: if you have two weekly recurring meetings which
- both happen at the same time every week
- don't conflict this week
then they will not conflict next week
Remote
jcreed
@jcreed@mastodon.social
mastodon 4.8.0-nightly.2026-10-06theorems, types, tunes, typefaces, terms-of-art, tropes, technicalities. [en/eo, +ε es/zh/fr/pl/jp]
0 Followers
0 Following
40 Posts
Joined January 03, 2017
foundations:
constructive, univalent
You are faced with two shakiras, one of whose hips *always* tells only lies, and the oth
Replying to
@chrisamaphone@hci.social "i ain't reading all that" = propositional truncation modality
Replying to
@leah I knew that europe and the us switch times at different moments in the calendar, but it didn't really sink in to me how much it means that a *meeting itself* (if it is to recur "at the same time") must have a notion of which tz it belongs to.
This feels like something something mumble holonomy around vector bundles or something. "If you are to compare whether two times of day are the same time, you must actually transport one and then compare."
I was going back through some of the Lean Together talks I missed since videos seem to be up now, and trying to figure out the actual math content of Yaël's talk https://www.youtube.com/watch?v=cz9Q4TtveL0 started blowing my mind a bit
Yaël Dillies - Hopf algebras, affine group schemes and all of that (Lean Together 2026)
good times with the online pictionary with friends
Replying to
@chrisamaphone @cbaberle @jonmsterling but it was big and hard and challenging, and, idk, maybe you meant to include that time range in the ish of your "newish" :)
and in any case I'd agree with you that it would be a new *norm* if this sort of scale is what every mathematician feels they have to routinely engage with all the time
Replying to
ok, I managed to make a minimal native android app with 'capacitor', which is apparently the spiritual descendant of 'cordova'. Reminds me how much pain java development always seems to entail. Nonetheless it works and I can get vibration on notifications, even.
Replying to
@mjd@mathstodon.xyz @svat@mathstodon.xyz nice blog post! I tentatively suspect (but haven't proved) that the following picture visually summarizes the same bjection as the one in the post: https://mastodon.social/@jcreed/116155046190192425
Replying to
@alexr@tilde.zone oh wow I hadn't thought of it that way but now that you point it out it feels right
Replying to
@chrisamaphone @cbaberle @jonmsterling although I may have been hoodwinked by breezily written math-outreach writing (not just today, but in the past when I've read about the classification as well)
see the last comment on https://plus.maths.org/enormous-theorem-classification-finite-simple-groups which is a mathematician saying it's not necessarily as impenetrable as claimed
Replying to
Is this even decidable in general? Does this run into "undecidability of spheres"-style problems? I guess it's trivially decidable when restricted to a particular n, because then the question is finite...
Replying to
ah, I think I have a counterexample for "if boundary is tame, then occupancy must be monotone or antitone in each variable"
This shape is not monotone or antitone in x.
Replying to
The thing I'm actually curious about is: Is this topological condition equivalent to to asserting that, for each dimension d, occupancy/colored-in-ness either always increases or decreses monotonically? If not, is there some other purely combinatorial condition that captures it?
Replying to
ah, CSS "container-type: size;" is also a crucial piece of making this work correctly.
oof power still out after 24h
Replying to
@svat@mathstodon.xyz @mjd@mathstodon.xyz @robinhouston@mathstodon.xyz neat! very cool that there are so many angles to look at the same problem from. thanks for collecting them together!
oh oh no big walk is out? this looks so delightful https://www.youtube.com/watch?v=Y-0rj_BcYsI
Replying to
@mark ah there was some video that smelled like an announce trailer but I see it was just drumming up interest. Well, it worked on me :)
Replying to
@svat@mathstodon.xyz @mjd@mathstodon.xyz Here's a js implementation: https://jsbin.com/yilucacavu/1/edit?html,output
Replying to
@mjd@mathstodon.xyz @svat@mathstodon.xyz (it does so by describing a bijection
indecomposable tilings of a 2x2N by 1x1 and 1x2 blocks <->
indecomposable tilings of a 2x2N by tetris pieces; a general tiling is the horizontal composition of some sequence of indecomposable tilings)
Replying to
@mjk@hachyderm.io really cool project! dumb question, and I'm sorry this is maybe over-fixating on the demo and not the underlying library despite your plea to not do exactly that :) but I'm just curious --- do you reckon that what I'm seeing here is merely some near-plane culling/clipping?
Replying to
Is A₀ necessarily contractible? Be careful not to think I'm asking a very similar-sounding but distinct question: I know if the sequence was ordered the other way around, with A₀ = 0, A₁ = ΣA₀, A₂ = ΣA₁, etc. then the colimit of the sequence ("the infinite-dimensional sphere") would be contractible.
Replying to
whoops, this was meant to be a link to https://hci.social/@chrisamaphone/116307319860900149
fun little trivia game, I got
catfishing.net
#643 - 7/10
🐈🐈🐟🐟🐟
🐈🐈🐈🐈🐈
Replying to
If it's possible for A₀ to not be trivial, then I have a hunch it ought to behave kind of like a "negative point"; I think for any function B → C I can naturally construct a map from a colimit of C many copies of A₀ to B many copies of A₀.
Replying to
Possible proof strategy for "if monotone or antitone in each dimension, then boundary is tame": assume wlog that it's monotone in every dimension. Construct the homeomorphism by projecting the boundary onto the hyperplane orthogonal to (1, 1, ... 1)
Replying to
So here's a restatement of the question that I still don't know the answer to:
Let f : 𝔹ⁿ → 𝔹 be a boolean function. Turn this into a subset of ℝⁿ by saying
S = { v ∈ ℝⁿ | f(v₁ ≥ 0, …, vₙ ≥ 0) }
Is there a nice purely combinatorial condition on f that is equivalent to "the boundary ∂S is homeomorphic to ℝⁿ⁻¹"?