Algebra F2 Power Hamming Weight Le

The weight bound

In combinatorics, the Hamming weight of a binary string is the number of positions where the bit is 1. For a string of length D, that count obviously cannot exceed D. The declaration hammingWeight_le is a machine-checked proof of exactly this bound: for any vector v in the space F2Power D, the weight of v is at most D.

The object F2Power D is the set of all binary strings of length D, with addition defined by XOR (exclusive or) on each position. This makes it an abelian group, meaning addition is commutative and associative, there is a zero element (the all-false string), and every element is its own inverse because XOR with itself gives zero. The library proves the basic facts: the whole space has 2^D elements, the zero string has weight 0, and the nonzero strings number 2^D - 1.

The weight bound is proved by a simple subset argument. The set of positions where v is true is a subset of all D positions, so its cardinality is at most D. The proof is a direct calculation in the framework's machine-checked library of formal theorems, with no axioms beyond the standard logical ones. It is a small lemma, but it anchors the later claim that in three dimensions the 1+3+3+1 weight decomposition holds: exactly one string has weight 0, three have weight 1, three have weight 2, and one has weight 3.

In Recognition Science, this weight bound is not a physical law. It is a combinatorial fact about the elementary abelian 2-group, used as a building block for counting arguments. The framework models certain narrative structures as nonzero elements of F2Power 3, and the bound ensures that the weight of such an element never exceeds 3. It does not by itself force any physical constant, nor does it derive the number 7; that count comes from a separate theorem about nonzero elements.

What the declaration does not claim is broader than what it proves. It does not assert that the weight bound is unique to this group, nor that it has any physical meaning on its own. It does not say that the Hamming weight is a measure of anything in the physical world. It is a lemma about finite sets, proved once and reused, and its value lies in being a reliable step in a longer chain of formal reasoning.

theorem hammingWeight_le (v : F2Power D) : hammingWeight v ≤ D := by
  unfold hammingWeight
  calc (Finset.univ.filter (fun i => v i = true)).card
      ≤ Finset.univ.card := Finset.card_filter_le _ _
    _ = D := by simp [Finset.card_univ, Fintype.card_fin]

theorem hammingWeight_le (v : F2Power D) : hammingWeight v ≤ D := by
  unfold hammingWeight
  calc (Finset.univ.filter (fun i => v i = true)).card
      ≤ Finset.univ.card := Finset.card_filter_le _ _
    _ = D := by simp [Finset.card_univ, Fintype.card_fin]

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

What this page does not claim

The weight bound does not by itself force any physical constant. The declaration does not derive the number 7; that count comes from a separate theorem. The Hamming weight bound has no direct physical interpretation on its own.

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: