Foundation Reflexivity Index Reflexivity Invariant

The invariance theorem

The reflexivity index, a non-negative integer, is meant to capture how deeply a system models itself. The framework's library proves it is a topological invariant: it does not change under a smooth change of representation. The theorem is called reflexivity_invariant. It says that if you have two descriptions of a system, and a bijection between them that preserves the level and strength of self-modeling at every level, then the computed index is the same for both. The bijection is a homeomorphism, a continuous, invertible map with a continuous inverse; here it is called a cognitive homeomorphism.

The invariant is built from a profile, a list of strengths at each level of self-modeling. The index counts how many levels have strength at least a threshold, which is a parameter of the configuration. The theorem itself is conditional: it holds when the two profiles have the same maximum level and the same strengths at each level, under the bijection. It does not say that any two systems with the same index are equivalent, nor that the index is invariant under arbitrary maps that do not preserve the profile. The proof is a direct calculation: the index is a function of the profile alone, so if the profile is preserved, the index is preserved.

The library also proves bounds on the index. It is always between zero and the maximum level plus one. A zero profile, one with no strength at any level, has index zero. The cost of reflexivity, defined as phi to the level minus one, grows exponentially with level, and the library proves it is always non-negative. The maximum sustainable level is set to seven, and the attentional budget is phi to the minus fifth power. These are definitions, not theorems.

In Recognition Science, this invariant is a candidate measure of consciousness. The framework's library assigns levels: zero for rocks, one for flow states, three for human baseline, and so on. Those assignments are a model, a definitional choice, not a proved fact about the world. The invariance theorem is proved; the mapping from the index to conscious experience is not.

/-- **Theorem**: Reflexivity index is invariant under cognitive homeomorphisms.

    This is the key topological property: the "degree of I-ness" doesn't
    depend on the particular representation of the cognitive state. -/
theorem reflexivity_invariant
    {α β : Type*} (_h : CognitiveHomeomorphism α β)
    (profile_α : ReflexivityProfile) (profile_β : ReflexivityProfile)
    (config : ReflexivityConfig)
    (h_same_levels : profile_α.max_level = profile_β.max_level)
    (h_strength_preserved : ∀ i : Fin (profile_α.max_level + 1),
      profile_α.strengths i = profile_β.strengths (i.cast (by rw [h_same_levels]))) :
    integerReflexivityIndex config profile_α = integerReflexivityIndex config profile_β := by
  obtain ⟨n, s_α, v_α⟩ := profile_α
  obtain ⟨m, s_β, v_β⟩ := profile_β
  simp only at h_same_levels
  subst h_same_levels
  have cast_id : ∀ (h : n + 1 = n + 1) (i : Fin (n + 1)), Fin.cast h i = i :=
    fun _ i => Fin.ext rfl
  have key : ∀ (i : Fin (n + 1)), s_α i = s_β i := by
    intro i
    have h := h_strength_preserved i
    rw [cast_id] at h
    exact h
  simp only [integerReflexivityIndex, countSignificantLevels]
  congr 1
  apply Finset.filter_congr
  intro i _
  rw [key i]

/-- Maximum possible index equals max_level + 1 -/
theorem max_index_bound (config : ReflexivityConfig) (profile : ReflexivityProfile) :
    integerReflexivityIndex config profile ≤ profile.max_level + 1 := by
  unfold integerReflexivityIndex countSignificantLevels
  calc Finset.card (Finset.filter _ Finset.univ)
      ≤ Finset.card (Finset.univ : Finset (Fin (profile.max_level + 1))) := Finset.card_filter_le _ _
    _ = profile.max_level + 1 := Finset.card_fin _

/-- Zero profile has zero index -/
theorem zero_profile_zero_index (config : ReflexivityConfig) :
    integerReflexivityIndex config
      ⟨0, fun _ => 0, fun _ => ⟨le_refl _, by norm_num⟩⟩ = 0 := by
  simp only [integerReflexivityIndex, countSignificantLevels]
  apply Finset.card_eq_zero.mpr
  simp only [Finset.filter_eq_empty_iff, Finset.mem_univ, true_implies]
  intro i
  simp only [ge_iff_le, not_le]
  exact config.threshold_valid.1

/-- The cost of level k grows exponentially with k -/
theorem reflexivityCost_exponential (config : ReflexivityConfig) (k₁ k₂ : ℕ) (hk : k₁ < k₂) :
    reflexivityCost config k₁ < reflexivityCost config k₂ := by
  unfold reflexivityCost
  have h : config.φ ^ k₁ < config.φ ^ k₂ := pow_lt_pow_right₀ config.φ_gt_one hk
  linarith

What this page does not claim

The reflexivity index is not proved to be a measure of consciousness; the level assignments are a model. The theorem does not show that any two systems with the same index are equivalent. The invariance holds only under maps that preserve the profile, not under arbitrary bijections.

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: