In our retirement we enjoy studying topics in various fields and informally publishing (in online forums or our own document and code repositories) what we have learned (which may take the form of a formal question on occasion).

I ran across a question at the Electrical Engineering community at Stack Exchange, How do I find input capacitance of a CMOS gate?, asking how to use the SPICE circuit emulator software to find the input capacitance and output resistance of a 2-input NAND gate. I researched the subject thoroughly, working on the topic for several months, and in December 2021 completed a formal 118-page paper on the subject, which you can read in your pdf viewer, Measuring dynamic input capacitance of CMOS logic gates, by G. Dalton Bentley. I also posted a brief answer at the Stack Exchange site (visit the link to the question) based on my formal paper.

While investigating the function of the claustrum in early 2021, I was annoyed to find my neuroscience textbook using an odd form to convert the noun "rival" into an adjective ("people and animals report switches in *rivalrous* percepts"). After putting aside the neuroscience to study the relevant linguistics, I wrote a brief paper (view in your pdf viewer), On the morphology and etymology of an English word, taking the reader through means of evaluating word usage patterns over the years with a computer and the Internet, as well as what is known about the evolution of word structure. I also posted a version of the article at the English Language forum at Stack Exchange, What suffix rule applies to making rival into rivalrous?

A few questions had been floating around my mind in 2019 as I finished several years learning quantum mechanics well enough to investigate the behavior of solar neutrinos. In 1976 S. Nussinov had proposed that the length of a solar neutrino packet could be bounded by the beta-plus interval available for its emission in the solar plasma. I found that the packet length was more likely constrained by the lifetime permitted the virtual W-boson in the weak interation process. If the length was constrained solely by plasma collisions the packet length would be on the order of 50 m, which seems unreasonable in light of coherence data available for terrestrially generated neutrinos from nuclear fission. You can read my paper on the subject in your pdf viewer: Bounds on Solar Neutrino Packet Lengths).

After reading my paper in early 2020, a prominent physicist did tell me (in private correspondence) that he agreed with my proposal that "the mass scale of the W boson sets the time scale for the weak interaction that produces a neutrino."

Isabelle is an interactive proof assistant using the Isar proof language, which combines English, logic and programming to read like a formal proof in mathematics. We illustrate its usage in a detailed tutorial with many screen shots, showing how we go about proving that it is impossible to find a rational number whose square is precisely the number 2. You may recognize this problem as one that upset the Pythagoreans considerably a few thousand years ago. You can read my paper in your pdf viewer: Isabelle Proof Assistant Tutorial.

There are historical as well as physical reasons why the smaller neutrino squared mass splitting and the mixing angle between the two smaller mass states are associated with the solar
electron neutrino flux and often offered as the solely relevant parameters in simplified two-neutrino models concerned with the observed flavor change of the solar flux. In 2020 I wrote a paper on the subject, including derivation of the complete three-neutrino oscillation equations, which you can read in your pdf viewer: Solar neutrinos: association with mass states 1 and 2.

As you may have gathered from some of the entries above, I am active on the Stack Exchange question and answer forums in multiple disciplines:

I also publish computer code and articles at my GitHub account Bentley at GitHub