module module moderate

`IndisputableMonolith.Philosophy.ProbabilityMeaningStructure`

The module shows that any probability-meaning structure in a deterministic universe requires a lossy projection from the full ledger for observers. Researchers in foundations of physics examining how determinism accommodates probabilistic descriptions would cite it. The structure relies on the strict convexity of the J-cost function to establish unique ledger minimizers and derive epistemic probability implications.

claimA probability-meaning structure for an observer implies a lossy projection of the deterministic J-cost ledger.

background

This module operates in the Philosophy domain of Recognition Science and imports the Determinism module. The upstream result states that the J-cost function is strictly convex on (0, ∞), ensuring unique minimizers for any constrained optimization in ledger updates. It introduces notions such as fibers covering the ledger, probability from projection, and distinctions between epistemic and frequentist interpretations of probability.

proof idea

This is a definition module, no proofs. It organizes the argument through a sequence of definitions including Fiber, fibers_cover, and probability_from_projection, followed by statements linking probability meaning to lossy projections and epistemic interpretations.

why it matters in Recognition Science

The module advances the F-007 determinism resolution by formalizing how probability arises in a determined universe through lossy projections. It supports related results on epistemic probability and the vindication of frequentist and Bayesian views. It connects to the broader framework where deterministic dynamics with unique J-minimizers underpin all physical descriptions.

scope and limits

Does not quantify the degree of information loss in the projection.
Does not derive specific probability distributions from the phi-ladder.
Does not address multi-observer consistency beyond basic coverage.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.Determinism module_import

declarations in this module (18)

def probability_meaning_from_ledger L74
theorem probability_meaning_structure L77
theorem probability_meaning_implies_lossy L80
def Fiber L87
theorem fibers_cover L91
theorem probability_from_projection L102
theorem each_fiber_nonempty L108
theorem prob_is_epistemic L129
theorem frequentist_vindicated L149
theorem bayesian_vindicated L165
theorem higher_resolution_finer_distinctions L180
theorem probability_is_relational L198
theorem propensity_vindicated L209
theorem born_rule_structure L226
def obs_probability L236
theorem probability_sums_to_one L241
theorem probability_nonneg L250
theorem ph006_probability_certificate L273