Algebra F2 Power

The binary vector space

An elementary abelian 2-group of rank D is the set of all binary strings of length D, with addition defined as bitwise XOR: flip a bit where the two strings differ, leave it where they agree. The zero string is all false. Every string is its own inverse, because XORing a string with itself gives the zero string. This structure is a vector space over the two-element field, and its size is exactly 2 to the power D.

In 1854 George Boole published the laws of thought, which formalized the algebra of true and false values. The modern treatment of these structures came with Emmy Noether's 1920s work on abstract algebra, which unified such examples under the concept of a group. For D equal to 3, the space has 8 strings total: one of weight 0, three of weight 1, three of weight 2, and one of weight 3, where the weight of a string is the number of true bits it contains.

In Recognition Science, the framework models a discrete ledger of recognition events as a binary vector space. The module F2Power D defines this space formally and proves its counting theorems in a machine-checked library of formal theorems. It proves that there are 2 to the power D strings total, and that exactly 2 to the power D minus 1 of them are nonzero. At D equal to 3, this gives 7 nonzero strings, which the framework identifies with the seven basic plot families in Booker's taxonomy of narratives.

The framework also proves that each nonzero string generates a one-dimensional subgroup containing just that string and zero. Since XORing a string with itself gives zero, these subgroups are closed under addition. At D equal to 3, there are exactly 7 such subgroups, one for each nonzero string. This structural fact is what lets downstream modules treat the seven plot families as a proved theorem rather than a hardcoded definition.

The practical consequence is that the count 7 is not an assumption but a derived result. Any system that models three independent binary choices, such as three axes of narrative tension, will have exactly 7 nonempty combinations. This is the same reason there are 7 days in a week if you count the empty day, or 7 nonzero vectors in three-dimensional space over the two-element field.

/-- The elementary abelian 2-group of rank `D`, modeled as
    `Fin D → Bool` with pointwise XOR. -/
def F2Power (D : ℕ) : Type := Fin D → Bool

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

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

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

This module does not prove that Booker's seven plot families are the only possible narrative structures. The identification of plot families with nonzero vectors is a framework modeling choice, not a theorem about literature. The module does not derive the golden ratio or other Recognition Science constants.

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: