Algebra F2 Power Nonzero Card Three

The count of seven

Consider a string of three binary digits, each either 0 or 1. There are 2 × 2 × 2 = 8 such strings, from 000 to 111. Exactly one of them, 000, is all zeros. The other seven each contain at least one 1. That is the entire content of the declaration nonzero_card_three: it proves, in a machine-checked library of formal theorems, that the count of nonzero three-bit strings is 7.

The statement lives in a slightly more general setting. The library defines F2Power D as the set of D-bit strings, with addition given by bitwise XOR, so that adding a string to itself always gives the zero string. A theorem called nonzero_card proves that for any D, the number of nonzero strings is 2^D − 1. Plugging in D = 3 gives 2^3 − 1 = 7, which is exactly what nonzero_card_three records. The proof is immediate from the general result, and the library also breaks the seven down by how many 1s they contain: one string with three 1s, three with two 1s, and three with one 1.

The seven nonzero strings have a further structure that the library exploits. Each nonzero string v generates the two-element set {0, v}, which is closed under XOR because v + v = 0. These are the one-dimensional subspaces of the three-bit space, and there are exactly seven of them, one for each nonzero string. This count is what connects the algebra to later work in the framework: a companion paper asserts that seven basic plot families come from (Z/2)^3 \ {0}, and the library upgrades that assertion to a proved theorem.

In Recognition Science, this theorem is a small but load-bearing piece of the forcing chain. The framework derives three spatial dimensions from its recognition-cost axioms, and the count 7 = 2^3 − 1 appears when the framework models discrete structure on that space. The theorem itself, however, is pure combinatorics: it says nothing about physics, recognition, or cost. It only counts nonzero elements in a three-bit system.

What the declaration does not claim is just as important. It does not assert that three dimensions exist, that the number seven has aesthetic meaning, or that any particular plot family is the right one. It merely establishes a counting fact, rigorously, so that downstream arguments can rely on it without re-deriving it.

/-- 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

/-- The number of non-zero vectors in `F2Power D` is `2 ^ D - 1`. -/
theorem nonzero_card :
    (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card = 2 ^ D - 1 := by
  have h : (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card =
           Fintype.card (F2Power D) - 1 := by
    rw [show (Finset.univ.filter (fun v : F2Power D => v ≠ 0)) =
            Finset.univ.erase 0 from ?_, Finset.card_erase_of_mem (Finset.mem_univ _)]
    · rfl
    · ext v
      simp [Finset.mem_filter, Finset.mem_erase, Finset.mem_univ]
  rw [h, card_eq]

/-- 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 assert that three spatial dimensions exist. The theorem does not assign aesthetic or narrative meaning to the number seven. The theorem does not claim any particular plot family is the correct one.

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: