Algebra F2 Power One Dim Subspace Card

Counting one-dimensional subspaces

The elementary abelian 2-group of rank D, written F2Power D, is the set of all binary strings of length D, combined by adding bits without carrying: 1 plus 1 gives 0. This is the same addition rule used in computer memory and error-correcting codes. The group has exactly 2^D elements, one for each possible string, a fact the framework's library proves directly by counting the functions from a D-element set to the two-element set {0, 1}.

A one-dimensional subspace in this setting is the smallest nonempty collection closed under the group operation. For any nonzero vector v, the set {0, v} is such a subspace: adding v to itself gives 0, so the set never leaves itself. The declaration oneDimSubspace_card proves that this set has exactly two elements whenever v is not the zero vector. The companion theorem oneDimSubspace_closed shows the set is genuinely closed under addition, so the name is earned.

The count matters at dimension three. There are 2^3 minus 1, or 7, nonzero vectors, and each generates its own two-element subspace. The framework's library proves the count of nonzero vectors is 2^D minus 1 for any D, and specializes to 7 at D equals 3. It also decomposes the seven nonzero vectors by how many bits they set to true: one vector with weight 3, three with weight 2, three with weight 1. These counts, 1, 3, 3, 1, mirror the binomial coefficients of the third row of Pascal's triangle.

In Recognition Science, this algebraic fact supports a claim about narrative structure: the seven nonzero vectors at dimension three correspond to seven basic plot families. The framework's library proves the count here, so downstream modules can rely on a theorem rather than a hardcoded number. The declaration itself, however, only establishes the cardinality and closure of these subspaces. It does not assert anything about stories, aesthetics, or the meaning of the vectors in any narrative context.

What the theorem does not claim is equally precise. It does not claim that every two-element subset is a subspace; only those of the form {0, v} with v nonzero qualify. It does not claim the subspaces are distinct for different vectors, though in fact they are, since each nonzero vector appears in exactly one such subspace. And it makes no statement about dimensions other than the counting formula, which holds for all D but is only computed explicitly at D equals 3.

/-- `F2Power D` has `2 ^ D` elements. -/
theorem card_eq : Fintype.card (F2Power D) = 2 ^ D := by
  unfold F2Power
  simp [Fintype.card_bool, Fintype.card_fin]

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]

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

/-- 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 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 axis123_weight : hammingWeight axis123 = 3 := by
  unfold hammingWeight axis123
  decide

What this page does not claim

The declaration does not assert any narrative or aesthetic meaning for the vectors. It does not claim that every two-element subset of F2Power D is a subspace. It makes no claim about the distinctness of subspaces for different nonzero vectors, though that follows from the counting.

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: