pith. machine review for the scientific record. sign in
structure definition def or abbrev high

for

show as:
view Lean formalization →

The meta-realization certificate equips the type of LogicRealization instances with a meta-cost that is zero on identical pairs, symmetric, and total, while recording that the universal forcing meta-theorem supplies forced arithmetic invariance. Framework developers working on reflexive closure cite this definition to show the meta-theorem fits the Law-of-Logic structural shape. It is a direct structure definition that lists the carrier type, type equality, cost totality, identity, and symmetry fields with no proof obligations.

claimA meta-realization certificate consists of a carrier type $C : Type_1$ with $C = LogicRealization_{0,0}$, a total meta-cost function assigning a natural number to each pair of carriers, and axioms asserting that the meta-cost vanishes on identical pairs and is symmetric.

background

The module shows that the universal forcing meta-theorem itself satisfies the Law-of-Logic structural shape. The meta-carrier is the type of all LogicRealization instances at levels 0,0, which resides in Type 1. The meta-cost returns zero when two realizations are propositionally equal and a positive integer otherwise. The three Aristotelian conditions on this cost are identity, non-contradiction (symmetry), and totality. The forced-arithmetic-invariance condition is supplied directly by the meta-theorem from the parent UniversalForcing module. This follows the universe convention already fixed in the NaturalNumberObject submodule.

proof idea

The declaration is a direct structure definition. It specifies the carrier type at universe level 1, asserts equality to the logic realization type, records totality of the meta-cost by construction, and includes the identity and symmetry properties of the meta-cost as explicit fields. No tactics or lemmas are applied; the structure simply bundles the required properties.

why it matters in Recognition Science

This definition closes the reflexive loop by showing that the universal forcing meta-theorem itself forms a Law-of-Logic-shaped operation, with the three definitional conditions automatic and the meta-theorem supplying forced arithmetic invariance. It feeds downstream results including energy conservation certificates, geodesic equations, ablation predicates, and acoustics derivations. The module states that the framework is reflexively closed. It touches the open question of lifting full orbit and step coherence axioms to the meta level.

scope and limits

formal statement (Lean)

  38structure for the meta-realization (the orbit/step coherence axioms
  39require additional design choices that are not part of the
  40self-reference content). Instead, we give a `MetaRealizationCert`
  41recording all the structural properties that *would* be required of
  42such an instance, and prove that the meta-theorem already supplies
  43each one.
  44
  45## What this earns
  46
  47The framework is reflexively closed: the meta-theorem is itself a
  48Law-of-Logic-shaped operation comparing realizations, with the three
  49definitional Aristotelian conditions automatic and the meta-theorem's
  50canonical equivalence supplying the forced-arithmetic invariance for
  51free.
  52-/
  53
  54namespace IndisputableMonolith
  55namespace Foundation
  56namespace UniversalForcingSelfReference
  57
  58open Classical
  59open UniversalForcing
  60
  61/-! ## The Meta-Carrier and Meta-Cost -/
  62
  63/-- The **meta-carrier**: the type of `LogicRealization.{0,0}` instances.
  64This sits in `Type 1` because `LogicRealization.{0,0}` is itself in
  65`Type 1`. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (30)

Lean names referenced from this declaration's body.