Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability

show as:
view Lean formalization →

Defines discrete probability on finite distinction events over the nonempty space Fin(N+1). Events are subsets, counted by cardinality, with probability normalized by the ambient size N+1. Downstream amplitude and native-analysis modules import this layer for comparison and objecthood arguments. The content is definitional plus elementary finitary measure lemmas.

claimOn the nonempty finite space $\mathrm{Fin}(N+1)$, a distinction event $E$ is a subset; its count is $\#E$ and its probability is $\mathrm{prob}(E)=\#E/(N+1)$. The module records $\mathrm{prob}(\emptyset)=0$, $\mathrm{prob}(\mathrm{univ})=1$, nonnegativity, $0\le\mathrm{prob}(E)\le 1$, and monotonicity of count under inclusion.

background

Recognition Science treats primitive recognition as comparison on a finite discrete carrier. Here the carrier is the nonempty finite type $\mathrm{Fin}(N+1)$, so every configuration space has cardinality $N+1\ge 1$. A distinction event is simply a subset of that carrier: the set of outcomes that count as a successful distinction under a fixed comparison rule.

The module equips those events with the uniform counting measure. Count is finset cardinality; probability is count divided by $N+1$. This is the discrete, RS-native stand-in for a probability space before amplitudes or continuous limits appear. No J-cost or $\varphi$-ladder structure is imposed yet; the layer is purely combinatorial.

Sibling names indicate the standard elementary package: empty and universe events, equality of count with card, nonnegativity and unit upper bound for probability, and monotonicity of count under inclusion.

proof idea

This is a definition module with elementary finitary lemmas, not a deep proof development. Events and the maps count, eventFinset, and prob are introduced by definition. The listed facts (empty/universe counts and probabilities, nonnegativity, $\mathrm{prob}\le 1$, count monotonicity) follow from Mathlib finset cardinality and the normalization by $N+1$, typically in one-line rewrites or simp/linarith style arguments.

why it matters in Recognition Science

DeltaProbability is the measure-theoretic substrate for the Primitive Recognition Calculus. Five sibling modules import it: DeltaAmplitude (amplitudes over the same events), DeltaNativeAnalysis and DeltaNativeStrongClosure (analytic and closure properties of native delta comparisons), ObjecthoodRegistry (which configurations count as objects), and ValidComparisonExamples (concrete comparison instances).

In the broader RS stack this sits below the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$). It does not yet force those landmarks; it only supplies the finite probability language in which later recognition and comparison statements are stated. Without a clean event/prob layer, amplitude and objecthood arguments would re-derive counting measure ad hoc.

scope and limits

used by (5)

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

declarations in this module (18)