prob_is_epistemic
plain-language theorem explainer
Probability appears random to finite-resolution observers because their projections collapse distinct deterministic states, even though a unique positive real minimizes the defect function. A foundationally-minded physicist or philosopher of physics would cite this to ground the Born rule in J-cost fiber weights rather than postulate it. The proof is a direct term pairing of the uniqueness witness at unity with the explicit lossy-projection theorem.
Claim. There exists a unique positive real number $x$ such that the defect vanishes at $x$, and for every observer with finite positive resolution the projection map from reals to the observer's finite state set is not injective.
background
The module resolves probability interpretations by separating deterministic reality from epistemic appearance under finite resolution. The defect function, taken from the Law of Existence, vanishes uniquely at the J-minimizer (unity in native units). An Observer is a structure with positive finite resolution, and project maps each real to one of the distinguishable states; upstream projection_lossy states that any such map sends distinct inputs to the same output.
proof idea
The term proof constructs a pair. The left component witnesses unique existence: 1 satisfies defect(1)=0 by defect_at_one, and any other positive zero is ruled out by applying defect_zero_iff_one. The right component is the projection_lossy theorem, which directly supplies the required existential witness for lossiness.
why it matters
This anchors the epistemic reading of probability inside the deterministic core of Recognition Science (unique J-minimizer from the T0-T8 forcing chain). It supports the sibling vindications of frequentist and Bayesian interpretations by exhibiting apparent randomness as a projection artifact. The module uses it to derive the Born rule from the J-cost landscape structure without introducing ontological indeterminism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.