Foundation Reflexivity Index Level Index Roundtrip

The roundtrip guarantee

The declaration level_index_roundtrip is a theorem in the framework's machine-checked library of formal theorems. It proves a consistency property between two ways of labeling levels of self-modeling, which the framework calls reflexivity, the depth at which a system models itself. The first labeling, indexToLevel, maps a natural number to a named level of consciousness, such as 0 to None, 1 to Prereflective, 2 to Bodily, and so on up to 7 to Reflective, with any number 8 or above mapping to Transcendent. The second labeling, levelToIndex, maps each named level back to a number, with None to 0, Prereflective to 1, and so on, with Transcendent to 8.

The theorem states that for any natural number n at most 7, converting n to a level with indexToLevel and then back with levelToIndex returns the original n. In plain terms, for the first eight levels, the two naming systems are perfect inverses of each other: the roundtrip journey from number to name and back to number loses nothing. The proof is a direct case analysis on the eight possibilities, and the library's kernel checks it without any special axioms. The result is a small but load-bearing sanity check: the framework's central ladder of consciousness levels is internally consistent at its base.

What the theorem does not claim is just as important. It says nothing about levels above 7. For n = 8, the roundtrip fails, because indexToLevel sends 8 to Transcendent, but levelToIndex sends Transcendent to 8, which is not 8. The theorem also does not assert that any system actually attains these levels, nor that the named levels correspond to any empirical reality. It is a purely formal statement about two functions defined in the library, not a claim about consciousness itself. The framework's own documentation describes the levels as a phenomenological interpretation, with a table mapping index 0 to rocks, 1 to flow states, 2 to animal consciousness, and so on, but that table is a descriptive gloss, not a theorem.

The roundtrip guarantee matters because it anchors the framework's vocabulary. When the library later reasons about reflexivity costs, sustainable levels, or the strength of self-modeling layers, it can rely on the fact that the first eight level names are unambiguous. A reader can now see that the framework's ladder is not a loose metaphor but a precisely defined structure, at least in its formal foundations, and that the formal precision stops exactly where the empirical claims begin.

In Recognition Science, the roundtrip theorem sits inside a broader apparatus. The library defines a reflexivity cost as a function of a level, and proves it is non-negative and increases with level, using the golden ratio as a base. It defines a maximum sustainable level of 7, which matches the theorem's range. It proves an invariance result under what it calls cognitive homeomorphisms, smooth changes of representation that preserve the index. The roundtrip theorem is the hinge that makes these other results legible: without it, the mapping between numbers and levels could drift, and the framework's claims about higher reflexivity would rest on sand. With it, the first eight rungs of the ladder are fixed, and the framework can build upward from a stable base.

/-- Round-trip for levels ≤ 7 -/
theorem level_index_roundtrip (n : ℕ) (hn : n ≤ 7) :
    levelToIndex (indexToLevel n) = n := by
  interval_cases n <;> rfl

/-- Round-trip for levels ≤ 7 -/
theorem level_index_roundtrip (n : ℕ) (hn : n ≤ 7) :
    levelToIndex (indexToLevel n) = n := by
  interval_cases n <;> rfl

What this page does not claim

The theorem does not prove that any system actually attains any of the named consciousness levels. The theorem does not establish that the named levels correspond to any empirical reality. The theorem does not apply to levels above 7, where the roundtrip property fails.

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/Foundation/ReflexivityIndex.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: