Beyond Wood and Water

Tweetrology: a proof, a tweet, and the moment one tested the other. Nietzsche would have posted this as a thread. We are not Nietzsche. We have a proof assistant.

“Supposing truth is a woman — what then?”

— Friedrich Nietzsche, Beyond Good and Evil, Preface (1886)

Asking truth to declare a preferred pronoun while diminishing half the species is neither good nor beyond evil, and explains much about the man’s personal life. Tweetrology holds itself to higher standards.

In metrology — the International Vocabulary of which defines the words I’m about to use — every measurement requires exactly three irreducible components: measurand (μ), procedure (P), result (m). Remove any one and measurement collapses. No two are derivable from each other, however alike they appear. I proved this. The verification stack, for a claim about two likes on a tweet, is as follows:

Three tools that agree on a single cardinality.

structure MeasurementSystem where
  hasMeasurand : Bool
  hasProcedure : Bool
  hasResult    : Bool

def isMeasurement (s : MeasurementSystem) : Bool :=
  s.hasMeasurand && s.hasProcedure && s.hasResult

theorem exactly_three :
    (isMeasurement triad = true) ∧
    (isMeasurement noMeasurand = false) ∧
    (isMeasurement noProcedure = false) ∧
    (isMeasurement noResult = false) := by
  exact ⟨triad_is_measurement, no_measurand_not_measurement,
         no_procedure_not_measurement, no_result_not_measurement⟩

#print axioms exactly_three  -- Lean.ofReduceBool

Then I noticed something.

On X, I pointed out that @hrishioa and @hdarshane have nearly indistinguishable accounts. Hrishi — previously CTO of Greywing, YC W21, now building systems of lasting value at Southbridge, chop wood carry water — responded: which is which? Hiranmay — nineteen, deep learning and large language models, previously a research intern at a lab approximating Solomonoff induction. The observable could not distinguish itself from the other observable. I declared myself the comparand.

Then I looked at the likes on my tweet about minimal cardinality. Two. One from @hrishioa. One from @hdarshane. The quorum was already there — the comparand’s claim and both observables’ acknowledgment — and I realized the proof I’d already completed was staring at its own empirical test.

The three removals: