Huzzah, I fixed my interface issues.
Although I can do the following stuff before I solved the infrastructure so setting this up is easier.
```
λΠ> Positive.decEq Z (S Z)
Left MoreRight
λΠ> Positive.decEqN Z (S Z)
Right MoreRight
λΠ> Positive.decEq (S Z) (S Z)
Right (Succ Zero)
λΠ> Positive.decEqN (S Z) (S Z)
Left (Succ Zero)
```
$50 raised so far this week, the goal is $1000 for putting a proper dent in those debts and fees and still having some food money.
$2000 more would sort out a lot more of the debts and some batteries we need.
$7500 more would pay off the car which would be amazing but I know that's unlikely.
An unknown amount may be needed to inspect and repair the Vulpibus's engine. It's got some kind of coolant related issue. It also needs the brake lines to be checked and resealed.
The occasional paid up night at the local campground also helps take off the pressure from our unofficial hosts at a truckstop.
The kind of money needed to properly sort us out is still cheaper than putting us through the alternatives. Not that the US government presently strikes me as comprehending that.
But this is all the more reason to get our shit together so we can have options for GTFOing.
#LGBTQIA2S #repairs #debt #helpneeded #money #donation #latestagecapitalism #endstagecapitalism #endoligarchy #constructive #action
🌇 If you've ever watched my stuff before, you know I LOVE Cities Skylines📽️
Latest CS2 video just went live, thought I'd plug the playlist, so you can catch up from the start, if you want to!
I don't talk, so it's just the gameplay; the whole gameplay. JSYK!
#citiesskylines #gaming #nocommentary #longplay #simulation #cs2 #citiesskylines2 #game #daily #fyp #strategygame #architecture #sandbox #simcity #constructive #gameplay #planning #weaponizedautism
Have the #RacistHomophobes at #SSG complied with #EULaw, yet? | #StillNope™️
"#BeingRight is #SuperAwesome™️"
#LateStageLotRO also has a #Following...
#DontForget to #HashtagAllTheSmurfs...
#IT's also #StillNotYule... #FictionalChristmas
#Maybe; #JustMaybe... #OneDay, the #RacistHomophobes at #SSG will #DoSomething... #Constructive about #AllTheFraud; but, #IDoubtIT
#WeStandWithPSiReN | #LotROStillDown #DeadGame
🧙🐉🤖🐺🤖🐉🧙 | 💀🦹🀄🦄🀄🦹💀
#Quote: "<<Sings-Like-Jim-Broadbent...>> "Because the #KlanKlanKlan...!"'
You know I am not going to go to a massive negativille. So many have. I have to be mostly constructive and positive. This is what gets me through the day.
Bite Your Tongue: When to #StayQuiet in Your #Relationship
It’s not always #constructive to talk about your relationship. Here's why.
#Editors, this Nov. 26 presentation via #EditorsToronto about giving #authors #constructive #feedback looks good: https://www.tickettailor.com/events/editorstoronto/1471459 . It’s open to members & nonmembers.
@MartinEscardo and I have been working on injective #types in #constructive #univalent mathematics.
Last week I gave an informal talk in our group's seminar and I wrote a brief blog post with several pointers in case you'd like to know more: https://fplunchnott.wordpress.com/2024/10/25/injective-types/
#VicePresident #KamalaHarris' #CodeSwitching Is #American As #ApplePie
Code switching is a common practice within the black community.
Some conservatives have claimed that this #linguisticshift was #evidence of #inauthenticity, essentially #questioning Harris’ #blackness. Their #confusion highlights the need for more #constructive #conversations on #race and #communication.
https://www.levelman.com/kamala-harris-code-switching-american-apple-pie/
C++ Concepts. Good in concept.
OK, OK. It's a good start. Late start, but a good start.
"No one so thoroughly appreciates the value of constructive criticism as the one who's giving it." — Hal Chadwick — — — #HalChadwick #quote #quotes #constructive #criticism #value #valuable #offer #giving #advice
Grim news out of Georgia with Fani Willis confirming the #destructive fact that she's personally and sexually involved with a man she added to the team of prosecutors investigating election interference. Ms. Willis had an enormous responsibility to do her job as perfectly as possible so as to bring this case to trial. Instead the case ballooned to involved nearly 20 people, leading to delays and, importantly, enormous legal fees all around.
She should step down from the case if not her position. Then a determination can be made as to whether the cases can be salvaged (probably not).
#constructive-destructive
David French in the NYTimes had a excellent article on the worst thing the MAGA movement.
Here's my comment: "Donald #Rump preaching a bullying, pro-life, greed-is-good, white power message seems to make him a very appealing figure to evangelicals struggling under the enormous tension of Christ's suffering and commandments and their own baser instincts, material aspirations and competitive status seeking. One things for sure: he's way easier to follow than the original Messiah."
https://www.nytimes.com/2024/01/12/opinion/donald-trump-culture-decline.html
#constructive-destructive
If the #Rump team prevails in its argument that the 14th Amendment only bars insurrectionists from taking office (rather than running for office &/or being elected) then it would be up to the current Justice Department to rule him ineligible to take office, should he win in 2024. Of course #Rump could appeal the decision but the Constitutional remedy is not in the courts but rather a vote by at least 2/3 of both houses to remove the bar.
#constructive-destructive
It would be great for humanity, species and the planet IF this were true but very unfortunately what you're more likely to see is the enslavement of billions women who will be forced to bear more children.
Just look at the debate about abortion rights in the U.S. today, esp. Texas. This is forced pregnancy on a massive scale (or gender rape, if you will). And they're just getting started.
#constructive-destructive
#Roe #abortion #women
RE: https://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/ @andrejbauer
If you can classically prove that a computable number is irrational, there is a constructive proof of the same fact! The same thing applies to proofs that a number is transcendental.
To be more specific, if you prove it in PA, it can also be proven in HA, if you can prove it in ZFC, it can also be proven in IZF, etc... (Probably works with classical #HoTT to HoTT, but that seems a pain to prove.)
Proof: Let p be a program that computes a real number r. (To be specific, for every rational ε>0, p(ε) is rational number such that |p(ε) - r| ≤ ε.) Assume there is a classical proof of "the real number computed by p is irrational". Then there is also a classical proof that "For all rational numbers q, there exists a rational number ε>0 such that |p(ε) - q| > ε". By the Friedman translation, there is a constructive proof of the same sentence (see https://mathoverflow.net/questions/460815/#comment1195059_460815). From there, we can create a constructive proof of "the real number computed by p is apart from every rational number". A similar argument works for proving a number transcendental.
∎
To start your #constructive news fix for the week: A government initiative returns millions of acres of land to Indigenous tribes, an incredible year of solar power installations, promising developments in approving dementia medicines in the UK & more!👇
https://squirrel-news.net/news/three-million-acres-returned-to-tribal-nations-us-sets-solar-installation-record-new-alzheimers-drugs/
Highly recommended:
Columnist David French points out 3 commonalities between #Rump and Christian Fundamentalist culture: "certainty, ferocity and solidarity." He added Muslim fundamentalism and he could have added some ultra-Orthodox Jewish sects + the Salem witch trials.
#constructive-destructive
We can generalize the "use n propositions to split into 2^n lemmas" even further. We can split on infinitely many propositions at once!
Let I be a set with an element representing each proposition (i.e. it's an index set) and T⊆I represent the set of true propositions. Generally, I will be simple (such as the set of natural numbers) but we don't know how to nor do we need to calculate T (since they are unknown propositions).
Let's say you want to use the trick to prove A⇒B.
Here's what you need to prove:
> Let S denote an arbitrary subset of I.
> Assume A and that S⊆T (i.e. that S is a set of true propositions).
> Prove that ((exists x. x∈T\S) or B).
This represents our "2^n lemmas", if we count each S as a separate lemma!
The intuition is that we start with S=∅, and use the lemma to keep adding true propositions to it everytime we hit the first case. Eventually we either hit the second case of the lemma result, or we eventually build up to S=T (and then we must hit the second case).
Proof of A⇒B using the lemma
The actual proof is much simpler though and doesn't use any kind of recursion. Just let S=T in the lemma! (We could've actually done that to start with, but the intuition works better if we think of S as being any subset of I.) We have A and that S⊆T, so we can use the lemma. There are two cases:
- exists x. x∈T\S: Since, T\S=T\T=∅, we have a contradiction. By the principle of explosion, conclude B.
- B: We conclude B.
Therefore B.
∎
#constructive #math tip
Often in a proof using classical math, you might take a related proposition X and split into cases "X" and "not X". Some examples in number theory: <https://en.wikipedia.org/wiki/Riemann_hypothesis#Excluded_middle>.
We can't do this in constrictive math, but there is a trick that is equivalent (and more elegant)!
X is any kind of proposition, such as:
- a conjecture, like the Riemann hypothesis
- a statement with free variables, like "n > k" or "G is finite" or any instance of "x has property P"
- a statement independent of your axioms, like the continuum hypothesis or the axiom K
In many cases you might be able to prove excluded middle (EM) for your specific X, but here's an alternative that works for any X.
**The trick**
If you are trying to prove A⇒B, prove the following two lemmas first:
- A⇒(X or B)
- (A and X)⇒B
Classically this is equivalent to splitting on "X or not X" (the first lemma is the "not X" case since "A⇒(X or B)" is equivalent to "(A and not X)⇒B" if EM holds for X), but it's still a theorem constructively that those two lemmas imply A⇒B!
Proof
Assume A. By the first lemma we conclude X or B. There are two cases:
- X: By the second lemma conclude B.
- B: We conclude B.
Therefore B.
∎
If you are just trying to prove C, then use the above trick on "1=1⇒C". If you are trying to refute C, use the above trick on "C⇒0=1". For proof by induction, A can include the induction hypothesis.
Moreover, if you have n propositions of interest, you can split into 2^n lemmas. Adding more propositions never hurts since you can ignore any unneeded propositions when proving any of the lemmas! Many of the lemmas may be trivial or redundant if you already know some relationships between the propositions.
