Foundation Universal Forcing Strict Realization To Lightweight

The strict bridge

In the Recognition Science framework, recognition (a discrete record of events) is governed by a cost that is forced, not chosen. The framework's machine-checked library of formal theorems proves that any cost function meeting five plain conditions must equal a specific form, and from that form a chain of results forces arithmetic, the golden ratio, and three spatial dimensions. The declaration toLightweight is a bridge inside that library: it converts one kind of formal description into another, and the conversion is what makes the forcing chain honest.

The earlier LogicRealization interface already proved the lightweight Universal Forcing theorem, but it allowed a realization to carry an internal orbit as a field. That is an escape hatch: the description could supply its own counting device, which would weaken the claim that arithmetic is forced. The strict interface StrictLogicRealization removes that escape hatch. A strict realization supplies only native comparison, composition, identity, invariance, and non-triviality data. The free orbit used by Universal Forcing is then derived uniformly as LogicNat, a fixed iteration object. The declaration toLightweight takes a strict realization and converts it to the existing lightweight interface, with all orbit fields derived from LogicNat rather than supplied by the caller. This means the counting structure is not an input; it is a consequence of the native law data.

What toLightweight establishes, in plain terms, is that the strict description is at least as strong as the earlier one. Every strict realization yields a lightweight realization, and the arithmetic extracted from that derived realization is canonically equivalent to LogicNat. The declaration arith_equiv_logicNat states this equivalence, and universal_forcing then shows that any two strict realizations have Peano carriers that are equivalent. The theorem peano_surface confirms that the derived arithmetic inherits the Peano surface, the usual structure of natural numbers with zero and successor. The net effect is that the framework's claim to force arithmetic does not depend on a realization choosing its own orbit; the orbit is forced too.

What toLightweight does not claim is just as important. It does not claim that arithmetic is forced in the physical world; that is a separate step involving the bridge from recognition to physical linking, which remains open. It does not claim that the strict interface is the only way to describe logic, nor that LogicNat is the only possible free orbit. It establishes a formal equivalence between two interfaces inside the library, nothing more. The declaration is a piece of mathematical infrastructure, not a physical law. Its value is that it closes a loophole: the forcing chain no longer relies on a realization supplying its own counting device, which would have made the forcing circular.

/-- Convert a strict realization to the existing lightweight interface.
The orbit fields are all derived from `LogicNat`, not supplied by the caller. -/
def toLightweight (R : StrictLogicRealization) : LogicRealization where
  Carrier := R.Carrier
  Cost := R.Cost
  zeroCost := R.zeroCost
  compare := R.compare
  zero := R.one
  step := fun x => R.compose R.generator x
  Orbit := FreeOrbit R
  orbitZero := LogicNat.zero
  orbitStep := LogicNat.succ
  interpret := interpret R
  interpret_zero := rfl
  interpret_step := by intro n; rfl
  orbit_no_confusion := by
    intro n h
    exact LogicNat.zero_ne_succ n h
  orbit_step_injective := LogicNat.succ_injective
  orbit_induction := by
    intro P h0 hs n
    exact LogicNat.induction (motive := P) h0 hs n
  orbitEquivLogicNat := Equiv.refl LogicNat
  orbitEquiv_zero := rfl
  orbitEquiv_step := by intro n; rfl
  identity := R.identity_law
  nonContradiction := R.non_contradiction_law
  excludedMiddle := R.excluded_middle_law
  composition := R.composition_law
  actionInvariant := R.invariance_law
  nontrivial := ⟨R.generator, R.nontrivial_law⟩

/-- Every strict realization has forced arithmetic canonically equivalent to
`LogicNat`. -/
def arith_equiv_logicNat (R : StrictLogicRealization) :
    (arith R).peano.carrier ≃ LogicNat :=
  (toLightweight R).orbitEquivLogicNat

/-- Universal forcing for strict realizations. -/
noncomputable def universal_forcing (R S : StrictLogicRealization) :
    (arith R).peano.carrier ≃ (arith S).peano.carrier :=
  ArithmeticOf.equivOfInitial (arith R) (arith S)

What this page does not claim

The declaration does not claim that arithmetic is forced in the physical world, only inside the formal library. The declaration does not claim that LogicNat is the only possible free orbit, only that it is the one derived uniformly. The declaration does not claim that the strict interface is the only way to describe logic.

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/UniversalForcing/StrictRealization.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: