Integrated information theory (IIT 4.0) has known upper bounds on integrated information, but no family of growing systems had been proved to have growing integrated information. No substrate had been proved to satisfy the exclusion postulate.

The paper studies a cycle of N binary units, each computing the XOR of itself and its two clockwise neighbours. A damage model reduces system integrated information under partitions to a count of damaged units, using bijectivity when 3 does not divide N. Partitions are classified by damage budget to show the whole cycle beats every proper subsystem, and arcs of length at least 3 are shown to be distinctions that feed a relation-counting lower bound. All statements except one classification proposition are formalized in Lean 4 against Mathlib and a separate IIT 4.0 library. Language-model assistants wrote the proofs against human-fixed statements.

For infinitely many N, the cycle is a complex in every state, with system integrated information at least 4 against strictly less than 4 for every proper subsystem. Its integrated information satisfies Φ ≥ 2^{⌊N²/8⌋}·2^{-N}/(2N) − 1. The development is kernel-checked with only standard axioms; the arc classification (Proposition 6.2) is verified only numerically.