Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability

show as:
view Lean formalization →

Defines finite distinction events on the nonempty discrete space Fin(N+1), together with their counting measure and normalized probability. Supplies the elementary measure-theoretic substrate for the primitive recognition calculus: empty and universal events, nonnegativity and unit bounds, and monotonicity of counts. Downstream amplitude and native-analysis modules import this layer as the discrete probability base.

claimOn the nonempty finite space $\mathrm{Fin}(N+1)$, an event $E$ is a finite subset of outcomes. Write $\mathrm{count}(E)=|E|$ and $\mathrm{prob}(E)=|E|/(N+1)$. Then $\mathrm{count}(\emptyset)=0$, $\mathrm{count}(\mathrm{univ})=N+1$, $\mathrm{prob}(\emptyset)=0$, $\mathrm{prob}(\mathrm{univ})=1$, $0\le\mathrm{prob}(E)\le 1$, and $A\subseteq B$ implies $\mathrm{count}(A)\le\mathrm{count}(B)$.

background

Primitive recognition calculus needs a discrete probability layer before amplitudes or comparison rules. The ambient space is the nonempty finite type $\mathrm{Fin}(N+1)$: $N+1$ distinguishable outcomes, one of which is always present so the normalizing constant never vanishes.

An Event is a finite distinction set on that space. The module introduces the counting functional $\mathrm{count}$ (cardinality of the event Finset) and the normalized probability $\mathrm{prob}=\mathrm{count}/(N+1)$. Standard boundary facts are recorded: empty and universal events, nonnegativity, the unit upper bound, and monotonicity of counts under inclusion.

Only Mathlib is imported. No Recognition-specific cost $J$, $\phi$-ladder, or forcing-chain material appears here; the module is pure finite discrete measure theory sized for later RS use.

proof idea

Definition-and-lemma module, not a single theorem. Event, count, eventFinset, and prob are introduced as defs/abbrevs on Finsets over Fin(N+1). The named lemmas (count_empty, count_univ, count_eq_card, prob_empty, prob_univ, prob_nonneg, prob_le_one, count_mono) are short cardinality and division arguments from Mathlib Finset and Fin API. No deep tactic scripts; each fact is a direct rewrite or inequality from the definitions.

why it matters in Recognition Science

This is the discrete probability base of PrimitiveRecognitionCalculus. Five sibling modules import it: DeltaAmplitude (amplitudes over the same events), DeltaNativeAnalysis and DeltaNativeStrongClosure (analytic and closure properties of the native delta layer), ObjecthoodRegistry (registry of recognized objects), and ValidComparisonExamples (worked comparison instances). Without normalized event probabilities on Fin(N+1), later amplitude and objecthood constructions have no measure to normalize against. The module sits upstream of any claim that a distinction event carries a well-defined probability in the recognition calculus.

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)