module module high

`IndisputableMonolith.Philosophy.ProbabilityMeaningStructure`

The module shows that probability-meaning structures derived from the ledger imply lossy projections for any observer. Researchers examining epistemic interpretations of probability in deterministic theories would cite it. The argument assembles definitions of fibers, projections, and relational probability directly from the unique-minimizer property established in the upstream Determinism module.

claimA probability-meaning structure on the ledger implies lossy projection: for any observer the map from ledger states to observed distinctions loses information.

background

The module sits in the Philosophy domain and imports IndisputableMonolith.Foundation.Determinism. That upstream module (F-007) states: 'Formalizes the resolution of the determinism question' and gives the key step 'Deterministic dynamics: The J-cost function is strictly convex on (0, ∞). For any constrained optimization (ledger update), the minimizer is UNIQUE.'

proof idea

This is a definition module, no proofs. It organizes the implication through the listed sibling declarations that introduce fibers, projections, epistemic status, and the relational character of probability.

why it matters in Recognition Science

The module extends the determinism resolution (F-007) by supplying the probability interpretation that makes apparent randomness epistemic rather than ontological. It supports the broader Recognition Science claim that all physics follows from the J-cost ledger and its unique minimizers.

scope and limits

Does not derive numerical probability values or distributions.
Does not treat quantum measurement beyond ledger projections.
Does not claim the structure is the only possible interpretation of probability.
Does not address consistency across multiple simultaneous observers.

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