Foundation Universal Forcing Self Reference Meta Cost Symm

The symmetry of comparison

In mathematics, a comparison between two objects often has a direction. Asking whether one set is a subset of another is not the same as asking it in reverse. But some comparisons are symmetric: if you measure the distance between two points, you get the same answer whether you start from the first or the second. The declaration metaCost_symm establishes that a particular kind of comparison, defined inside the Recognition Science framework, has this symmetric property.

The objects being compared are called LogicRealizations. A LogicRealization is a formal structure that interprets the basic rules of logic and arithmetic. The framework's Universal Forcing Meta-Theorem states that any two such realizations produce the same forced arithmetic, meaning the core mathematical content is invariant across different logical setups. The declaration in question defines a meta-cost, a number assigned to a pair of realizations: zero if they are propositionally equal, one otherwise. This is a discrete record, a ledger, of how different two realizations are.

The theorem metaCost_symm proves that this meta-cost is symmetric. Formally, it states that for any two realizations R and S, the cost of comparing R to S equals the cost of comparing S to R. The proof is short: if R equals S, both costs are zero; if not, both are one. This is not a deep computational result but a structural one. It confirms that the framework's way of measuring difference between logical structures does not depend on the order of comparison, a property that mirrors the symmetry of ordinary equality.

In Recognition Science, this symmetry is one of three definitional conditions, alongside identity (comparing something to itself costs zero) and totality (every pair has a defined cost). Together, these conditions show that the act of comparing realizations is itself a Law-of-Logic-shaped structure, meaning the framework is reflexively closed. The meta-theorem that proves all realizations share the same forced arithmetic fits the same shape as the structures it compares. This is the reflexive-closure content of the framework: the system that studies logical structures can be studied by its own methods.

The declaration does not claim more than symmetry. It does not assert that the meta-cost detects all meaningful differences between realizations; it only distinguishes propositional equality from inequality. It does not prove that the framework can prove its own consistency in the Gödelian sense, which would require a different formal apparatus. And it does not supply a full LogicRealization instance for the meta-level, with all orbit and step coherence axioms, which remains a separate design programme. What it does establish is a clean, machine-checked fact: the comparison operation is order-independent, a small but necessary piece of the framework's self-consistency.

/-- **(L2) Non-Contradiction** for the meta-cost: the comparison is
symmetric in its arguments. -/
theorem metaCost_symm (R S : MetaCarrier) : metaCost R S = metaCost S R := by
  unfold metaCost
  by_cases h : R = S
  · subst h; rfl
  · have hSR : ¬ S = R := fun h' => h h'.symm
    simp [h, hSR]

/-- The **meta-cost** between two realizations. By Classical decidability,
this is `0` if the realizations are propositionally equal and `1`
otherwise. The choice is structural: the cost detects definitional
distinctness, not orbit non-isomorphism (which by the meta-theorem is
always trivial). -/
noncomputable def metaCost (R S : MetaCarrier) : ℕ :=
  if R = S then 0 else 1

/-- **The framework is reflexively closed.**

The Universal Forcing Meta-Theorem itself instantiates the Law-of-Logic
structural shape: the meta-cost satisfies the three definitional
Aristotelian conditions, and the meta-theorem itself supplies the
forced-arithmetic-invariance condition. The framework that proves
"every Law-of-Logic realization has the same forced arithmetic" is
itself a Law-of-Logic-shaped structure on the type of realizations.

The forced-arithmetic-invariance condition is wrapped in `Nonempty`
because the equivalence is `Type 1`-valued, while the conjunction here
is propositional. The Nonempty wrapper is harmless: the equivalence
exists for every pair, so its `Nonempty` is trivially inhabited. -/
theorem framework_is_reflexively_closed :
    -- Identity, non-contradiction, totality of meta-cost are automatic:
    (∀ R : MetaCarrier, metaCost R R = 0) ∧
    (∀ R S : MetaCarrier, metaCost R S = metaCost S R) ∧
    (∀ R S : MetaCarrier, ∃ c : ℕ, metaCost R S = c) ∧
    -- The meta-theorem supplies the comparison law:
    (∀ R S : MetaCarrier, Nonempty (R.Orbit ≃ S.Orbit)) := by
  refine ⟨metaCost_self, metaCost_symm, metaCost_total, ?_⟩
  intro R S
  exact ⟨metaForcedArithmeticInvariance R S⟩

What this page does not claim

The meta-cost detects all meaningful differences between realizations, only propositional equality versus inequality. The framework proves its own consistency in the Gödelian metalogical sense. A full LogicRealization instance with all orbit and step coherence axioms exists for the meta-level.

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/UniversalForcingSelfReference.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: