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

MeasureTheoryCert

show as:
view Lean formalization →

The MeasureTheoryCert structure records that the inductive type of canonical measures has exactly five inhabitants and that the J-cost function is non-negative on the positive reals. Measure theorists building the RS foundation would cite this certificate when verifying that J-cost behaves as a valid measure. The definition simply assembles the Fintype cardinality fact with the non-negativity lemma imported from the cost module.

claimA structure asserting that the set of canonical measures (Lebesgue, counting, Dirac, Hausdorff, Borel) has cardinality five and that the J-cost function satisfies $J(r) ≥ 0$ for all $r > 0$.

background

In the Recognition Science framework, measure theory is introduced to support probability and integration. The module defines five canonical measures via the inductive type CanonicalMeasure: Lebesgue, counting, Dirac, Hausdorff, and Borel measures, whose count equals the configuration dimension D = 5. The J-cost function is treated as a measurable object, with its non-negativity established by upstream theorems such as jcost_nonneg in PhysicsComplexityStructure and EntropyArrowFromJCost, which prove Jcost x ≥ 0 for x > 0 by case analysis on whether x equals 1 or not.

proof idea

The declaration is a structure definition with no proof body. It packages the cardinality equality Fintype.card CanonicalMeasure = 5, which follows directly from the Fintype deriving instance on the inductive type, together with the non-negativity statement supplied by the referenced jcost_nonneg theorems from cost and entropy modules.

why it matters in Recognition Science

This certificate supplies the measure-theoretic foundation required by the downstream measureTheoryCert definition in the same module. It fills the step that links the five canonical measures to the non-negativity of J-cost, consistent with the RS claim that J-cost serves as a measure-compatible cost function. The construction supports later developments in entropy arrows and tachyon-free conditions, where J ≥ 0 is used to exclude unphysical states.

scope and limits

formal statement (Lean)

  36structure MeasureTheoryCert where
  37  five_measures : Fintype.card CanonicalMeasure = 5
  38  jcost_nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ Jcost r
  39

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.