Physical position census

Proved

mme_position_card_eq

by Tamas Fulop · Sep 18, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

matrix-multiplicationmore-asymmetryregional-entropy

Physical positions are one pair per parent occurrence.

The type $Position(n)$ consists of triples $(r,t,h)$ with $r$ a region, $t$ an occurrence, and $h$ a half, so its cardinality is twice the total occurrences $2\sum_r n_r$ .

Formalization Note Direct cardinality computation; used to pin the $N=2$ skeleton.

Preamble

import Definitions.Def_mme_recursive_yz_physical_words
open scoped BigOperators
set_option autoImplicit false

Formal statement

theorem mme_position_card_eq : forall (R : Nat) (n : Fin R → Nat), Fintype.card (MME.RecursiveYZ.Position n) = 2 * ∑ r, n r := by sorry

Source

Cardinality of MME.RecursiveYZ.Position; skeleton lemma for the N=2 regional analysis.

View graph