Source-linked AI summary
Existence of an infinite family of substrates satisfying all the postulates of integrated information theory, exclusion included, with arbitrarily large integrated information
A. Mayeux
TL;DR
The paper asks how integrated information can grow with system size and which architectures attain high values. It proves a lower bound for an explicit cycle of XOR-connected binary units, showing that these systems are complexes and that log2 Φ grows as Ω(N^2) for infinitely many sizes.
Problem
How large integrated information can become with system size, and which architectures attain it, remain difficult questions because the nested optimizations require exact control uniformly in size.
Source: §1 · pp. 1–2Method
Results
For N ≥ 8 with 3 ∤ N, A_N is a complex in every state and log2 Φmax(A_N, 1) = Ω(N^2) at the all-ones state.
Source: §3 · p. 6Takeaways & Limitations
This is the first lower bound on Φ for a growing-size family and the first substrate shown to satisfy every IIT 4.0 postulate, exclusion included.
Source: §3 · p. 6
Abstract
from arXiv · showhide
For infinitely many sizes we exhibit a cycle of binary units, each taking the exclusive-or of itself and its two clockwise neighbours, that is a complex in every state, no proper subsystem being more integrated, and whose integrated information grows as two raised to a power quadratic in the number of units.
1 Introduction
The paper asks how integrated information grows with system size and which architectures attain high values. It addresses the missing proof of a growing-size lower bound on substrates that satisfy exclusion, using formal proof to establish its result.
1 Introduction
- The open question is how large integrated information can become with system size and which architectures achieve it, a mathematical question relevant to claims about consciousness.The answer matters because a small versus astronomical range across systems would mean something different.Source: §1 · p. 1
- Prior work established hyper-exponential upper bounds and identified obstacles to simultaneous mechanism saturation, but did not show that any system attains a given magnitude.The constructions and numerical evaluations did not establish that the substrates satisfy exclusion.Source: §1 · pp. 1–2
- Lower bounds are difficult because nested optimizations range over exponentially many choices, interact, and cannot be handled by averaging or convex relaxations without losing the measured feature.The value is non-compositional and can change discontinuously with wiring, requiring exact control of all optimizations uniformly in system size.Source: §1 · p. 2
- Exact evaluation has a horizon of roughly a dozen units and cannot by itself settle growth with size, since distinct asymptotic behaviors may look similar at computable sizes.The authors use PyPhi [7] as an indispensable implementation for evaluating small systems and discovering candidates.Source: §1 · pp. 2–3
- The cycle family yields a lower bound on integrated information growing as two raised to a power quadratic in the number of units, while prevailing over every subsystem.Every contiguous arc of length at least three is an irreducible mechanism, and quadratically many such arcs share any given unit.Source: §1 · p. 3
- Lean formalization checks the paper’s theorems against IIT definitions, enabling symbolic arguments across system sizes and reliable handling of extensive case analyses.The formal development was guided by human mathematicians with AI assistants; the authors’ original doubly-exponential conjecture was false, and formal verification could not detect that expectation error.Source: §1 · p. 3
2 Preliminaries
The preliminaries distinguish the system-level quantity that determines substratehood from the structure-level quantity bounded in the paper. They also fix the formal conventions for states, ties, exclusion, and background units.
2 Preliminaries
- The formalization assumes IIT 4.0 as formulated by Albantakis et al. [1], and proper-subsystem cause information uses marginalization of outside units.The definitions were transcribed into Lean 4 in a separate library, without modifying that library in this paper.Source: §2 · pp. 4–5
- Mechanism information φd is local, system information φs measures resistance to cuts and determines competition between candidates, while Φ sums irreducible mechanisms and their relations.The proof must make the whole system’s φs exceed that of every part while also making Φ large.Source: §2 · p. 4
- Substrates are deterministic systems of N binary units; φd is the minimum of mechanism effect and cause information, and φs depends on partitions and their severed connections.The notation also tracks supports as unit-state pairs, with a unit in opposite states not counted as shared.Source: §2 · pp. 4–5
- When maximizing cause and effect purviews tie, Φ is parameterized by a selector, and the lower bound holds for every selector because each must contain the exhibited distinctions.Source: §2 · p. 5
- A complex strictly exceeds every overlapping candidate in φs; the paper proves the whole universe beats each nonempty proper subsystem, ruling out ties.This is the strongest exclusion comparison for the whole system.Source: §2 · p. 5
3 The substrate and the results
For infinitely many cycle sizes, the paper proves both that the cycle is a complex and that its integrated information grows at a rate exponential in a quadratic function of size. The construction uses a uniform local XOR rule, with the results applying when N ≥8 and 3 ∤N.
3 The substrate and the results
- The cycle has N binary units, each taking the exclusive-or of itself and its two clockwise neighbours.The rule is uniform across units, and each unit reads only three units as the cycle grows.Source: §3 · p. 5
- The transition map is bijective exactly when 3 ∤N, the arithmetic condition used in both main theorems.Bijectivity makes the cycle's past determinate as well as its future and lets the cause-side analysis reduce to the effect side.Source: §3 · p. 6
- For N ≥8 with 3 ∤N, A_N is a complex in every state and background: φ_s(A_N,s) ≥4 while every proper subsystem has φ_s <4.Thus no proper subsystem is more integrated than the whole cycle.Source: §3 · p. 6
- log2 Φmax(A_N,1)=Ω(N²) for N ≥8 with 3 ∤N, a lower bound stated at the all-ones state.The theorem's constants are deliberately crude, and its displayed bound is vacuous for N ≤11.Source: §3 · p. 6
- Together, the theorems give the first proved lower bound on integrated information for a growing family and the first substrate shown to satisfy every IIT 4.0 postulate, exclusion included.The family is uniform, sparse, and flat, rather than densely connected.Source: §3 · p. 6
4 The damage model
The damage model makes system-level integrated information tractable by reducing nested optimizations to a count of damaged units. For the whole cycle, the reduction relies on bijectivity; a related rescaling handles proper subsystems.
4 The damage model
- For a fixed partition, a unit is damaged when a live input it reads lies in the cut set of its own block; dmg(θ) counts damaged units.Inputs outside the candidate subsystem are held at the background and contribute nothing.Source: §4 · p. 7
- For the whole cycle at all-ones, the effect-side calculation gives 2^-dmg(θ): severed live inputs flatten a unit's effect repertoire to 1/2, while undamaged units retain probability 1.Taking the logarithm returns the damage count.Source: §4 · p. 7
- When 3 ∤N, bijectivity gives a single point in the fibre over all-ones, reducing the cause-side calculation to the effect side.This is where the arithmetic condition on N enters the reduction.Source: §4 · p. 7
- For proper subsystems, the corresponding expression is rescaled by 2^-corank(C_S), the conditioned-map fibre size; singularity penalizes a subsystem by at least a factor of two.This penalty helps the crude bound rule out a large class of competing candidates.Source: §4 · p. 7
5 Exclusion
The whole cycle has integrated information at least 4, while every proper subsystem has less than 4. The proof compares partition damage across the whole cycle and uses the cycle’s geometry to bound proper subsystems.
5 Exclusion
- The whole cycle has φ_s ≥ 4, while every proper subsystem has φ_s < 4, establishing strict exclusion.The result holds for every state and background.Source: §5 · pp. 7–9
- A three-arc partition damages at most four units and has a normalizer that strictly beats the floors for partitions damaging one, two, or three units.The three damage cases have separate cut-count bounds; the proof uses one explicit witness rather than assuming the ratio increases with damage.Source: §5 · p. 8
- The whole-cycle lower bound follows because one partition’s damage-to-normalizer ratio is below the least ratio available at damage one, two, or three.Thus no minimizing partition can damage three or fewer units, and the supremum over minimizers gives φ_s ≥ 4.Source: §5 · p. 8
- For a proper subsystem, a shielded partition damages exactly one unit, yielding φ_s < 4 even when the subsystem is not itself an arc.The bound applies to every proper subsystem with at least two units, for every background and state; subsystems of size at most one have φ_s = 0.Source: §5 · pp. 8–9
6 The distinctions of the cycle
At the all-ones state, the cycle’s distinctions are exactly its arcs of length at least three, including the whole cycle. The paper uses arcs’ mechanism-level properties to support the later lower-bound construction.
6 The distinctions of the cycle
- Every arc of length at least three is a distinction at the all-ones state, and its maximally irreducible cause purview contains the arc itself.The positive effect side follows from the nonempty arc of units whose three inputs lie in the mechanism; the cause side requires windows of mechanism units to be contained in the purview.Source: §6 · p. 9
- The distinctions are exactly the arcs of lengths three through N−1 and the whole cycle, totaling N(N−3) + 1.The classification’s general argument uses criteria for positive effect and cause information based on connected components in the window-overlap graph.Source: §6 · p. 9
- The exact classification is not formally developed; it was exhaustively evaluated for N = 8, 10, 11, and 13 and cross-checked independently.The paper says its main theorems do not depend on this proposition; its role is to show that the quadratic growth rate is forced on this cycle.Source: §6 · p. 9
7 The lower bound
The lower-bound argument combines a family of distinctions sharing a stated unit with a uniform floor on their integrated distinction values. Its key input is the cycle’s family of arcs.
7 The lower bound
- Every subset of at least two distinctions sharing a stated unit contributes a relation, so the family’s size and uniform floor determine the lower-bound input.This counting identity is specialized from [2, Eq. 11]; the paper attributes the new work to supplying the certified family of distinctions.Source: §7 · p. 10
- The formalized overlap definition agrees with the union-of-face-purviews definition for relations, the only setting where φ_r is used.The equality is a theorem of the imported library.Source: §7 · p. 10
- Distinct arcs through a fixed unit are distinctions whose supports contain that unit, supplying the family used in the lower-bound argument.The construction indexes arcs by pairs (s, e), with each arc containing unit 0 and having length at least three.Source: §7 · p. 10
- Each distinction in the constructed family has a uniform floor c = (1/2)N/(2N), based on φ_d ≥ (1/2)N and support size at most 2N.The paper notes that both constants are generous; sharper values require an exact purview computation not formalized there.Source: §7 · p. 10
8 Method: direction, assistance, and certification
The authors chose to use a proof assistant as an instrument for discovering results, with human mathematical direction and mechanical assistance. Lean certification checked the development, including claims that computation or intuition had suggested.
8 Method: direction, assistance, and certification
- The human-led decision to formalize IIT from first principles made it possible to pose the question for interactive theorem proving.The formal system was used as an instrument of discovery, not only to certify results obtained elsewhere.Source: §8 · p. 11
- Exact evaluation of small systems supplied conjectures, while language-model assistants carried out file-by-file formal proofs against human-fixed statements and blueprints.The assistants also found positivity criteria and counterexamples to proposed lemmas.Source: §8 · p. 11
- Lean certification caught plausible but false intermediate claims, including the doubly exponential conjecture; damage-truncated enumeration can miss a high-damage minimizer.The authors report that enumerated numbers come from certified or exhaustive runs.Source: §8 · p. 11
9 The formal development
The formal development imports IIT 4.0 definitions from a separate library and proves substrate-specific exclusion and lower-bound results against those definitions. Lean checks both theorems in one import closure without escape hatches.
9 The formal development
- The substrate-specific library imports the definitions library as a pinned dependency, so both theorems use the same Lean constants and are checked in one import closure.The development uses no axioms beyond the three of ambient logic and no escape hatches such as sorry or native_decide.Source: §9 · p. 12
- For N ≥ 8 with 3 ∤ N, the cycle is a complex for every background and every state.Theorem 3.4 states this exclusion result for the full system.Source: §9 · p. 12
- Every arc of length at least three is a distinction when N ≥ 3 and 3 ∤ N.The theorem quantifies over the state and the arc's starting unit.Source: §9 · p. 12
- For N ≥ 8 with 3 ∤ N, Theorem 3.5 gives a lower bound on Φ_max at the all-ones state.The theorem states a bound for the cycle; the state quantification differs from Theorem 3.4.Source: §9 · p. 12