Algebra F2 Power Card Weight Zero Three

Counting the empty vector

Consider all strings of three bits: 000, 001, 010, 100, 011, 101, 110, 111. Exactly one of them, namely 000, contains no 1s. The declaration card_weight_zero_three establishes this trivial-sounding fact as a proved theorem in the framework's machine-checked library of formal theorems. The statement reads: the number of three-bit strings whose Hamming weight (the count of 1s in the string) equals zero is exactly 1.

The proof is short and fully computational. The library first proves a general lemma: for any length D, a string has Hamming weight zero if and only if it is the all-false string. At D = 3, this reduces the set of weight-zero strings to the singleton {000}, whose cardinality is 1 by definition. The theorem is tagged THEOREM, meaning it is verified with no unproved assumptions and no framework-specific axioms; it relies only on the standard logical postulates of the ambient type theory.

The fact sits inside a fuller counting pattern for three-bit strings. The eight strings split by weight as 1 + 3 + 3 + 1: one string of weight 0, three of weight 1, three of weight 2, and one of weight 3. The library proves all four counts, and card_weight_zero_three is the first of them. This decomposition matters because the seven nonzero strings generate exactly seven one-dimensional subgroups under pointwise XOR addition, a structure the framework's aesthetics modules use to count plot families. The count 7 is proved here rather than hardcoded.

What the declaration does not claim is just as precise. It does not assert anything about why three bits are special, nor about any physical or narrative interpretation of the count. It is a pure combinatorial statement about finite strings. The framework's later modules may use this count as an ingredient, but the theorem itself carries no meaning beyond the arithmetic of bit strings. It neither proves the golden ratio, nor fixes three spatial dimensions, nor derives any constant of physics. It is a load-bearing but deliberately narrow result: one small gear in a larger machine.

/-- The unique weight-0 element: the zero vector. -/
theorem card_weight_zero_three :
    (Finset.univ.filter (fun v : F2Power 3 => hammingWeight v = 0)).card = 1 := by
  have hsubset :
      (Finset.univ.filter (fun v : F2Power 3 => hammingWeight v = 0)) = {0} := by
    ext v
    simp [Finset.mem_filter, Finset.mem_univ, Finset.mem_singleton, weight_zero_iff]
  rw [hsubset]
  rfl

theorem weight_zero_iff (v : F2Power D) :
    hammingWeight v = 0 ↔ v = 0 := by
  constructor
  · intro h
    unfold hammingWeight at h
    rw [Finset.card_eq_zero] at h
    funext i
    have hi : i ∉ Finset.univ.filter (fun j => v j = true) := by
      rw [h]; exact Finset.notMem_empty _
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi
    -- hi : ¬ v i = true
    cases hv : v i
    · rfl
    · exact absurd hv hi
  · intro h
    subst h
    exact hammingWeight_zero

/-- The unique weight-0 element: the zero vector. -/
theorem card_weight_zero_three :
    (Finset.univ.filter (fun v : F2Power 3 => hammingWeight v = 0)).card = 1 := by
  have hsubset :
      (Finset.univ.filter (fun v : F2Power 3 => hammingWeight v = 0)) = {0} := by
    ext v
    simp [Finset.mem_filter, Finset.mem_univ, Finset.mem_singleton, weight_zero_iff]
  rw [hsubset]
  rfl

/-- At `D = 3`, the non-zero count is `7`. The seven Booker plot
    families bijection in `Aesthetics.NarrativeGeodesic` chains off
    this corollary. -/
theorem nonzero_card_three :
    (Finset.univ.filter (fun v : F2Power 3 => v ≠ 0)).card = 7 := by
  have h := @nonzero_card 3
  -- h : … = 2 ^ 3 - 1
  have h2 : (2 : ℕ) ^ 3 - 1 = 7 := by norm_num
  rw [h2] at h
  exact h

theorem oneDimSubspace_card (v : F2Power D) (hv : v ≠ 0) :
    (oneDimSubspace v).card = 2 := by
  unfold oneDimSubspace
  simp [Finset.card_insert_of_notMem, Ne.symm hv]

/-- The 1-dimensional subspace is closed under addition. -/
theorem oneDimSubspace_closed (v : F2Power D) (a b : F2Power D)
    (ha : a ∈ oneDimSubspace v) (hb : b ∈ oneDimSubspace v) :
    a + b ∈ oneDimSubspace v := by
  unfold oneDimSubspace at ha hb ⊢
  simp [Finset.mem_insert, Finset.mem_singleton] at ha hb ⊢
  rcases ha with ha | ha <;> rcases hb with hb | hb <;>
    subst_vars <;> simp [add_self]

What this page does not claim

The theorem does not claim any physical or narrative interpretation of the count 1. The theorem does not derive the golden ratio, three spatial dimensions, or any physical constant. The theorem does not assert that three bits are special beyond the arithmetic fact that 2^3 = 8.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Algebra/F2Power.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: