Replying to
@mwichary@mastodon.online As a VI user, this burned me in Terminal. Terminal applications should be immune to control- shortcuts just as they should be immune to shift- shortcuts.
Remote
Richard Penner
@Arpie4Math@mathstodon.xyz
mastodon 4.7.2SW Engineer, Amateur mathematician (contributed to metamath.org, oeis.org, ...), Legal Tourist (went to Honolulu in 2010 to watch the end of Sancho v. DOE).
256 Followers
1327 Following
50 Posts
Joined December 16, 2022
Location:
California
Metamath Symbolic Proofs:
Integer Sequences:
Replying to
@futurebird@sauropods.win @JamesWidman@mastodon.social This is what language nerds feel when “literally” is used as an intensifier or ironically.
Perl invented “vstrings” so v1.10 could be parsed as a semantic unit unconnected to decimals.
Of course the real offender is the ITU OIDs in, say, ASN.1 — the home base of “dotted strings of numbers.”
For example 2.16.840.1.113883.6.205.13686 is Solenopsis invicta in the NCBI Taxonomy (pending 205’s admission)
Replying to
@nomdeb@mstdn.social @newsguyusa@flipboard.social#Trump’s shift from malicious but disinterested #kakistocracy to incompetent #kleptocracy? I think he calls this #TheWeave.
Boosted by @MaryAustinBooks@mstdn.social
Replying to
@MaryAustinBooks@mstdn.social It’s ok because nowadays we have purse-sized geneengineered camels and needles that you can thread with bridge suspension cables.
Replying to
@SeanCasten@mastodon.social
Similar to my comments on
Beatty v. Trump (25-cv-04480, District Court, D.C.) The lawsuit over the Kennedy Center capture, renaming, and closure. https://www.courtlistener.com/docket/72069932/beatty-v-trump/
https://mathstodon.xyz/@Arpie4Math/116851261741403114
Replying to
From the links in that article, we learn that the figures 500 GL (est. in the 1960's, frequently quoted) / 562 GL (high tide, 1999-2004 survey) are associated with the whole drowned valley/estuary.
I have not found the original 2004 report.
———
Port Jackson, containing Sydney Harbour, is a drowned river valley and is considered a natural harbour. It is 19 km long with an area of 55 km².
One Sydney Harbour (Sydharb), (the amount of water in Sydney Harbour) is approximately 500 gigalitres or 200,000 Olympic size pools.
———
https://media.bom.gov.au/social/blog/39/when-dam-size-matters/
Sydney Harbour holds about 500 GL.
———
A five-year effort by the NSW Maritime Authority to measure the exact dimension of greater Sydney Harbour has revealed the estuary has nearly 80 kilometres more shoreline than anyone thought, 62,000 megalitres more water and is, on average, 1.6metres deeper.
The best estimate of the estuary's volume at high tide had been about 500,000 megalitres, but the authority now knows it is 562,000 megalitres.
Another source of confusion has been the definition of "Sydney Harbour". The estuary does not have one official name; instead, there are five formally defined parts, of which Sydney Harbour is one. All five together are sometimes called greater Sydney Harbour, while the combined parts of Sydney Harbour, North Harbour and Middle Harbour are collectively known as Port Jackson.
"Our definition of the harbour goes around every rock and every little nook and cranny," Mr Buttigieg said.
Replying to
@ami_angelwings@urusai.social
Project Horizons over Fallout: Equestria on the fate of Rainbow Dash and Discord in the event the timeline of My Little Pony: Friendship is Magic got badly derailed early in season two.
#FalloutEquestria
Replying to
@n_dimension@infosec.exchange
Dear Valued Customer,
As always, the doomscrolling is a core feature we provide for free, but dopamine levels are now gated by your subscription status as we make improvements to the service. We will happy to have you give feedback on this change to our world-class support system which, as you recall from last year’s change now features the option to speak to a human at Platinum level and above. (Platinum level became obsolete in May, currently this level of support requires subscription to *any one* of our partner luxury car brands at Freeway on-ramp acceleration + seat warmer level or above.) For best levels of support, please ensure you have your account number and at least 1% of our stock at time of call.
Replying to
@puppygirlhornypost2@transfem.social @asokel@ohai.social Only if geometry is commutative.
Replying to
@Arapalla@aus.social @mcnado@mstdn.social Actually, it is only the neighbours of selfish people to whom I offer good luck. The selfish people, after all, look out for themselves.
Replying to
@enoent@ravenation.club @futzle@old.mermaid.town
https://en.wikipedia.org/wiki/Reply_guy
A plethora of social media sins:
- Annoying strangers
- Rude strangers
- Mansplaining posters
- Strangers intruding into an intended limited reach out to specific individuals
- Post necromancy
It is perhaps from "Stranger" → "guy" and social media's unrestricted reply which turns their replies into an uncomfortable experience as if by being approached by a stranger when trying to have a tête-à-tête or have a productive (so necessarily focused or limited) conversation.
Cantor's claim is that the infinity of the set real numbers, |ℝ|, is larger than the infinity of the set of counting numbers, |ℕ|. If Cantor is wrong, then there must be a function 𝑓:ℕ⟶ℝ such that the set of real numbers, ℝ, is exactly the same as the image of all natural numbers under function 𝑓, 𝑓(ℕ) = { 𝑓(1), 𝑓(2), 𝑓(3), ... }. If Cantor is right, then there is no such function, 𝑓 where 𝑓(ℕ) = ℝ.
Cantor's diagonal argument is, at its heart, a proof that a set of size 2^n is strictly larger than n, is true for all n when n is the size of a set, and this works for infinite sets. If n is 3, we have A = {1, 2, 3}, B={000, 001, 010, 011, 100, 101, 110, 111}, and if 𝑓(1) = 𝑎𝑏𝑐, 𝑓(2) =𝑟𝑠𝑡, 𝑓(3) = 𝑥𝑦𝑧, the symbol D = 𝑎𝑠𝑧 might or might not be in 𝑓(A), but D̅ = 𝑎̅𝑠̅𝑧̅ cannot be. We know 𝑓(1) ≠ D̅ since 𝑎 ≠ 𝑎̅; we know 𝑓(2) ≠ D̅ since 𝑠 ≠ 𝑠̅; we know 𝑓(3) ≠ D̅ since 𝑧 ≠ 𝑧̅, so we know 𝑓(A) failed to include all the elements of B. The diagonal argument is not a procedure or task to be carried out, but logical reasoning about operating 𝑓 on the whole of A at once, even when A is an infinite set, like ℕ.
ℕ and ℝ are already concrete. ℝ^ℕ, the set of all injective functions from ℕ into ℝ, is already concrete. So 𝑓 is an element of ℝ^ℕ and 𝑓(ℕ) ≠ ℝ, because none of the injective functions from ℕ into ℝ is also an surjective function from ℕ onto every element of ℝ. That's pretty much the definition of "larger."
Since D̅ differs from 𝑓(𝑛) at the 𝑛th position, D̅ cannot be an element of 𝑓(ℕ) because there is no 𝑛 such that 𝑓(𝑛) = D̅.
Effectively, Cantor's diagonal argument is the proposition that describes a concrete 𝑔:ℝ^ℕ⟶ℝ such that for all 𝑓 in ℝ^ℕ, 𝑔(𝑓) = D̅, is in ℝ but not in 𝑓(ℕ).
Replying to
I should have been a restaurant critic. My opinions are objectively correct.
Me, misquoting Moxxie from Helluva Boss
Boosted by @MaryAustinBooks@mstdn.social
Replying to
@MaryAustinBooks@mstdn.social Wait? Their chili is made from Wagyu beef, but their burgers are made from Angus, and they have hot dogs but no chili dogs or soups other than chili or sizes of chili other than “cup”? That’s not a dinner!
The cinnamon rolls are house made, but they look decidedly amateurish next to the pie and pastries. More than half the menu is merch. The freaking tuna melt looks like the most labor intensive item.
This is not a dinner. It lives in the restaurant identity space that includes gas station convenience stores, dive bars that lost their liquor license, and street peddlers of merchandise that fell off a truck.
Replying to
@raymaccarthy @m_berberich @davidrevoy Star Trek: The Next Generation added "Heisenberg Compensators" to the standard list of technobabble to lampshade just how broken the described "physics" of transporters were. #WernerHeisenberg is closely associated with the #UncertaintyPrinciple which is a powerful barrier to even describing the state of a body's position and momentum at the same time.
Disturbing thought, what if transporters vaporized people and got some information, and then recreated living beings on the other side with AI slop?
Boosted by @GroupNebula563@mastodon.social
Replying to
@asokel@ohai.social @andromeda42.bsky.social It looks like it was created during a quest for backup coffee, so someone probably looted a corpse from that tragically failed expedition.
Replying to
@frankashwood@flipping.rocks I just realized that I have never seen a Californian banana slug despite being just two hours away from their wetlands.
Replying to
@mcfadden It might leave a bruise on your neck, but it might be just dirt, so don't alarm us by yelling "ouch!"
Replying to
@petealexharris@mastodon.scot California currently has 62 active candidates for governor.
Replying to
@atoponce
Feature flag is here: chrome://flags/#prompt-api-for-gemini-nano
When enabled, it powers demos like this: https://chrome.dev/web-ai-demos/prompt-api-playground/
#AI #GeminiNano
Replying to
Proposition 83, p. 65: If the image of the union of 𝑈 and 𝑊 is a subset of the union of 𝑈 and 𝑊, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the #TransitiveClosure of 𝑅, then 𝐵 is an element of the union of 𝑈 and 𝑊.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V) ; 𝑅 is a set, i.e. an element of the universal class V (not 𝑉).
Hyp. ⊢ (𝜑 → 𝐴 ∈ 𝑈) ; 𝐴 is an element of class 𝑈.
Hyp. ⊢ (𝜑 → 𝐵 ∈ V) ; 𝐵 is a set.
Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)
Hyp. ⊢ (𝜑 → (𝑅 “ (𝑈 ∪ 𝑊)) ⊆ (𝑈 ∪ 𝑊)) ; Relation 𝑅 is hereditary in the union of classes 𝑈 and 𝑊.
Therefore ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∪ 𝑊))
———
Proposition 96, p. 71. If 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 ∈ V)
Hyp. ⊢ (𝜑 → 𝐵 ∈ V)
Hyp. ⊢ (𝜑 → 𝐶 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐶) ; i.e. 𝐶 eventually follows 𝐴
Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵) ; 𝐵 immediately follows 𝐶
Therefore ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)
———
Proposition 87, p. 66: If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 is an element of 𝑈.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 ∈ V)
Hyp. ⊢ (𝜑 → 𝐵 ∈ V
Hyp. ⊢ (𝜑 → 𝐶 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐶)
Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵)
Hyp. ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈)
Hyp. ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)
Therefore ⊢ (𝜑 → 𝐵 ∈ 𝑈)
———
Proposition 91, p. 68. If 𝐵 follows 𝐴 in 𝑅 then 𝐵 follows 𝐴 in the transitive closure of 𝑅.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴𝑅𝐵)
Therefore ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)
———
Proposition 97, p. 71: If 𝐴 contains all elements after those in 𝑈 in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 = ((tc‘𝑅) “ 𝑈))
Therefore ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴)
Boosted by @GroupNebula563@mastodon.social
Replying to
@nyanbinary@infosec.exchange So sorry to hear about the upcoming manslaughter charges, as all surviving parties agree the victim brought it upon themselves. In the meantime, I hear there's a job opening?
Replying to
Proposition 98, p. 71: If 𝐶 follows 𝐴 and 𝐵 follows 𝐶 in the #TransitiveClosure of 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅.
Hyp. ⊢ (𝜑 → 𝐴 ∈ V)
Hyp. ⊢ (𝜑 → 𝐵 ∈ V)
Hyp. ⊢ (𝜑 → 𝐶 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐶)
Hyp. ⊢ (𝜑 → 𝐶(tc‘𝑅)𝐵)
Therefore ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)
———
Proposition 102, p. 72: If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then 𝐵 follows 𝐴 in the transitive closure of 𝑅.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 ∈ V)
Hyp. ⊢ (𝜑 → 𝐵 ∈ V)
Hyp. ⊢ (𝜑 → 𝐶 ∈ V)
Hyp. ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐶 ∨ 𝐴 = 𝐶))
Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵)
Therefore ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)
———
Proposition 106, p. 73: If 𝐵 follows 𝐴 in 𝑅, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in 𝑅.
Hyp. ⊢ (𝜑 → 𝐴𝑅𝐵)
Therefore ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))
———
Proposition 108, p. 74: If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in the transitive closure of 𝑅.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 ∈ V)
Hyp. ⊢ (𝜑 → 𝐵 ∈ V)
Hyp. ⊢ (𝜑 → 𝐶 ∈ V)
Hyp. ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐶 ∨ 𝐴 = 𝐶))
Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵)
Therefore ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐵 ∨ 𝐴 = 𝐵))
———
Proposition 109, p. 74: If 𝐴 contains all elements of 𝑈 and all elements after those in 𝑈 in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((tc‘𝑅) “ 𝑈)))
Therefore ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴)
———
Proposition 114, p. 76: If either 𝑅 relates 𝐴 and 𝐵 or 𝐴 and 𝐵 are the same, then either 𝐴 and 𝐵 are the same, 𝑅 relates 𝐴 and 𝐵, 𝑅 relates 𝐵 and 𝐴.
Hyp. ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))
Therefore ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵𝑅𝐴))
Replying to
@theandreaborden@sunny.garden If you don't notice the gaps between the slats, it looks like a charcuterie board prepared by someone not willing to limit themselves to edible flowers. :) ☠️ Iris? I knew her well, but she was poisonous.
Replying to
@futurebird@sauropods.win @JamesWidman@mastodon.social
And Internal Revenue Manual, § 3.28.3.5.3 is support for the proposition in Trump c. IRS (the fig leaf for the #Jan6 #SlushFund "settlement") that auditing Trump every year is *mandatory* ; the § is the context to know that you are looking at a hierarchical reference, a branch on a "tree", not of life but IRS regulations.
Replying to
@crazyeddie @KMWool @nixCraft It's not an open source project for city planning in Edinburgh?
https://mathstodon.xyz/@hiscursedness@mastodon.art/116268287281637393
Replying to
@cmconseils@mastodon.social Ginny said you were a bit long in the tooth, my lord, but I certainly. don't. see. it. Oh.
Replying to
@LillyHerself@mastodon.social @jspath55@chaos.social But would Trump’s DOJ still have prosecuted #Comey if the shared photo of seashells spelled out “86 *47*” ?
Boosted by @mattsheffield@mastodon.social
Replying to
@HistoPol@mastodon.social @mattsheffield@mastodon.social That is not evidence, but simple conclusory statements. One of the principal failures of LLMs to fill the shoes of AGI is that they learn nothing. Agentic AI tries to patch this by having the LLM maintain a serial file of “memory” but it is just a LLM conversation prefix to prime the pump of autocomplete.
Real AGI doesn’t just answer yes if it is asked if it thinks, it thinks and acts based on its desires. So it needs memory, it needs to color memories as good or bad, a trait we call sentience, and it needs to contemplate what justice and fairness mean ; currently every Agentic AI needs to be supervised as LLMs are trained to be prolix and sound confident at all times, even when wrong. So Agentic “decisions” are just a simulation of a conversation of humans who authored the content of its training data. Agentic AI makes mistakes no reasoning being would because there is no reasoning not present in its training data. Conversations go sideways because LLMs associate Xur with The Last Starfighter because those words came close together in training data, not because they had original opinions about a film it never saw.
Replying to on eigenmagic.net
@elebertus@eigenmagic.net @kajer@infosec.exchange There’s a TLD for my ForTran art?
Replying to
@kde Looking good for 30, maybe she doesn't jog but at least looks open to it. Sadly, the BSD Daemon (originally by Phil Foglio, but reworked a bit since) is finding that potbelly isn't looking so cherubic as the years drag on. (He also seems to have lost all of his hair since the very first illustration.)
Replying to
Proposition 77, p. 62: If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐵 follows 𝐴 in the #TransitiveClosure of 𝑅, then 𝐵 is an element of 𝑈.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V) ; 𝑅 is a set, which we newly require so that transitive closure may be a function. Implied, it has relation content. (tc‘𝑅) is its transitive closure, the smallest relation which contains it and has the transitive property.
Hyp. ⊢ (𝜑 → 𝐴 ∈ V) ; 𝐴 is a set.
Hyp. ⊢ (𝜑 → 𝐵 ∈ V) ; 𝐵 is a set.
Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵) ; 𝐴 is related to 𝐵 by the transitive closure of 𝑅
Hyp. ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈) ; The image of class 𝑈 is contained in 𝑈, which means the relation 𝑅 is hereditary in 𝑈
Hyp. ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈) ; The image of the singleton {𝐴} is contained in 𝑈
Therefore ⊢ (𝜑 → 𝐵 ∈ 𝑈) ; 𝐵 is an element of 𝑈.
———
Proposition 81, p. 63: If the image of 𝑈 is a subset of 𝑈, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of 𝑈.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 ∈ 𝑈) ; 𝐴 is not just a set, but an element of class 𝑈. This trick allows us to eliminate the last hypothesis of Proposition 77.
Hyp. ⊢ (𝜑 → 𝐵 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴(tc‘𝑅)𝐵)
Hyp. ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)
Therefore ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Replying to
@petealexharris@mastodon.scot While I have seen footage of the counting process, this is my first image of a British-style ballot.
https://mathstodon.xyz/@Pamela1960@kolektiva.social/116533433623411927
Replying to
@misty@digipres.club Can you host the Javascript for the mod player? NOONE should load javascript from some random site which may fall under hostile control at any time.
Simple just the music with little thought to UI:
https://atornblad.se/making-the-mod-player-available (part of a longer tutorial for js-mod-player)
Example of use:
import { ModPlayer } from './player.js'; // Load your copy of the player
const player = new ModPlayer(new AudioContext()); // Initialize
await player.load(url); // Load Mod File from network URL
player.play(); // Play it
Replying to
@petealexharris@mastodon.scot Ah, marking a box on a paper ballot. Many of ours are machine-read so punching holes for mechanical counters has been widely replaced by fully filling in a bubble.
I guess making a Christian-themed talisman to ward off vampires and Nazis will need to wait for a different day.
Replying to
Proposition 111, p. 75: If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then either 𝐴 and 𝐵 are the same or 𝐴 follows 𝐵 or 𝐵 and 𝐴 in the #TransitiveClosure of 𝑅.
Hyp. ⊢ (𝜑 → 𝑅 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 ∈ V)
Hyp. ⊢ (𝜑 → 𝐵 ∈ V)
Hyp. ⊢ (𝜑 → 𝐶 ∈ V)
Hyp. ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐶 ∨ 𝐴 = 𝐶))
Hyp. ⊢ (𝜑 → 𝐶𝑅𝐵)
Therefore ⊢ (𝜑 → (𝐴(tc‘𝑅)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝑅)𝐴))
———
Proposition 122, p. 79: If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 is the successor of 𝑋, then 𝐴 and 𝐵 are the same (or 𝐵 follows 𝐴 in the transitive closure of 𝐹).
Hyp. ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋)) ; 𝐴 is the value of 𝐹 (implicitly assumed to be a function) at 𝑋 such that 𝐴 is the unique value that 𝐴 immediately follows 𝑋, 𝑋𝐹𝐴.
Hyp. ⊢ (𝜑 → 𝐵 = (𝐹‘𝑋))
Therefore ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵))
———
Proposition 124, p. 80: If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 follows 𝑋 in the transitive closure of 𝐹, then 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in the transitive closure of 𝐹.
Hyp. ⊢ (𝜑 → 𝐹 ∈ V)
Hyp. ⊢ (𝜑 → 𝑋 ∈ dom 𝐹) ; 𝑋 is in the domain of relation 𝐹
Hyp. ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋))
Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐵)
Hyp. ⊢ (𝜑 → Fun 𝐹) ; relation 𝐹 is a function
Therefore ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵))
———
Proposition 126, p. 81: If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 follows 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹.
Hyp. ⊢ (𝜑 → 𝐹 ∈ V)
Hyp. ⊢ (𝜑 → 𝑋 ∈ dom 𝐹)
Hyp. ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋))
Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐵)
Hyp. ⊢ (𝜑 → Fun 𝐹)
Therefore ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝐹)𝐴))
Replying to
@mc@mathstodon.xyz @JacquesC2@types.pl @maxsnew@types.pl It appears to be a math library, perhaps a Lean library of theorems or the LaTeX source of a manuscript. "Cubical Category" is a term of art which I recognize but cannot define from remembered reading. These guys can't agree on it's definition: https://ncatlab.org/nlab/show/cubical+category
CITATION.cff is a YAML file that indicates how the repository is to be cited when used in an academic context. This reinforced the assumption this is math-related academic matter like a manuscript, Lean theorem library, or perhaps custom software to implement an algorithm which is the topic of a paper.
As Notes is the most stable folder, it might have useful exposition on the original intent.
Replying to
@david@fouroclockfarms.club Actually enough orthophosphate to require a literal ton (assuming 3x excess as per pool practice) of alum to precipitate out which needs time and filtration or it would just make the pool look worse.
Replying to
@david@fouroclockfarms.club Peoples is gefilled mit all kinds of phosphate. Is chocolate phosphate best one?
Replying to
@pzmyers@freethought.online California law prohibits operating a motor vehicle while using a car microscope.
At least, I think it does. The California Legislature website went down while I was researching this claim.
New: The Donald J. Trump Revocable Trust v. Capital One, N.A. (25-cv-21596) District Court, S.D. Florida https://www.courtlistener.com/docket/69853458/the-donald-j-trump-revocable-trust-v-capital-one-na/
2013-2017 DOJ ran "Operation Choke Point" using informal pressure on banks to sever ties ("de-banking") with high-risk-for-fraud businesses like payday lenders, firearm dealers, and pornographic film producers.
2021/01/06 #Trump holds #Jan6 rally
2021/01/20 Trump leaves office
2021/03/08 #CapitalOne, a bank, sent notice that "hundreds of [his] bank accounts" would be closed on 2021/06/07 (some extensions granted) (Doc 1-1, PDF page 13)
2022/02/07 The Biden Administration's effort to similarly target banking access to cryptocurrency and digital assets ramps up. https://blockspace.media/insight/operation-chokepoint-2-0-a-complete-timeline/
2025/03/07 Trump sues in Florida State court claiming he knows this de-banking was for his political acts.
2025/04/07 Removed to Federal Court
2025/06/12 Doc 32 First Amended Complaint
2025/07/11 Doc 37 Motion to Dismiss for Failure to State a Claim
2026/03/23 Doc 54 — FAC dismissed
2026/07/17 Doc 82 Trump's Second Amended Complaint (redacting the reasons Capital One said they closed the accounts) but admitting bank could close account “at any time, for any or no reason and without notice.”
2026/07/31 Doc 91 — Motion to Dismiss SAC for Failure to State a Claim: "We already told you, your accounts were closed because you move money around like a common money launderer."
those documents [attached to SAC] and Plaintiffs’ own allegations make clear that Capital One closed Plaintiffs’ accounts for anti-money laundering (“AML”) reasons.
p. 1
Capital One’s decision to close Plaintiffs’ accounts only became public because of Plaintiffs’ own decision to pursue this litigation.
p. 3
Replying to
@theking@mskey.nekomimi.party It's called a restraining order and the cat girls knew what they were doing when they sought one.
Replying to
Replying to
Notation guide (adapted from Metamath):
• 𝜑, a metavariable standing for any logical formula, abbreviates the conjunction of all hypotheses listed for a given proposition; writing each line as ⊢ (𝜑 → …) puts the theorem in "deduction form," which can be easier to apply in #Metamath.
• ⊢ 𝜑 asserts that 𝜑 is true; the turnstile is descended from #Frege's own Urteilsstrich (judgment stroke).
• 𝐴𝑅𝐵 means the ordered pair ⟨𝐴, 𝐵⟩ is an element of 𝑅, or we could say 𝐵 immediately follows 𝐴
• 𝐵 = (𝑅‘𝐴) means 𝐵 is the unique set such that 𝐴𝑅𝐵 is true (when such a 𝐵 exists) which means 𝑅 is function-like when restricted to operating on the singleton {𝐴}
• (𝑅”𝐴) is the image of 𝐴
• dom 𝑅 is the domain of 𝑅, the class of all sets 𝑥 such that there is a set 𝑦 that would make 𝑥𝑅𝑦 true.
• Fun 𝑅 is true when 𝑅 is function-like for all sets in its domain.
• ◡𝑅 is the converse of 𝑅 so 𝐴◡𝑅𝐵 iff 𝐵𝑅𝐴
• (tc‘𝑅) is the #TransitiveClosure of 𝑅 (Metamath uses (t+‘𝑅) which can be awkward.) Whitehead and Russell use the term ancestral to describe how 𝐴(tc‘𝑅)𝐵 means 𝐴 is some “ancestor” of 𝐵. Alternately, we can say 𝐵 eventually follows 𝐴.
• V is the universal class, every set is a member, and only sets may be members of any class. After Frege’s later work ran into Russell’s Paradox, it was discovered that not every class {𝑥 | 𝜑} makes sense as a set and so we need the hypothesis ⊢ (𝜑 → 𝐴 ∈ V) before we can talk about the function value of 𝐴 or the ordered pair ⟨𝐴, 𝐵⟩ being an element of 𝑅. V is not italic because it is a constant symbol, like tc, dom, and Fun.
Replying to
Proposition 129, p. 83: If 𝐹 is a function and (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹, the successor of 𝐴 is either 𝐵 or it follows 𝐵 or it comes before 𝐵 in the #TransitiveClosure of 𝐹.
Hyp. ⊢ (𝜑 → 𝐹 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 ∈ dom 𝐹)
Hyp. ⊢ (𝜑 → 𝐶 = (𝐹‘𝐴))
Hyp. ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝐹)𝐴))
Hyp. ⊢ (𝜑 → Fun 𝐹)
Therefore ⊢ (𝜑 → (𝐵(tc‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(tc‘𝐹)𝐵))
———
Proposition 131, p. 85: If 𝐹 is a function and 𝐴 contains all elements of 𝑈 and all elements before or after those elements of 𝑈 in the transitive closure of 𝐹, then the image under 𝐹 of 𝐴 is a subclass of 𝐴.
Hyp. ⊢ (𝜑 → 𝐹 ∈ V)
Hyp. ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((◡(tc‘𝐹) “ 𝑈) ∪ ((tc‘𝐹) “ 𝑈))))
Hyp. ⊢ (𝜑 → Fun 𝐹)
Therefore ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐴)
———
Proposition 133, p. 86: If 𝐹 is a function and 𝐴 and 𝐵 both follow 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹 (or both if it loops).
Hyp. ⊢ (𝜑 → 𝐹 ∈ V)
Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐴)
Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐵)
Hyp. ⊢ (𝜑 → Fun 𝐹)
Therefore ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝐹)𝐴))
———
So what's nice about the transitive closure that #Frege felt compelled to invent a new language in which to present mathematical arguments? When 𝑅 is a function, two sets being related by the transitive closure of 𝑅 is much like induction. When 𝑅 is a more general relation, we have a more general form of induction, that is truly #ancestral in the language of #Whitehead and #Russell.