theorem proved term proof

`probability_is_relational`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 198theorem probability_is_relational :
 199    -- The number of probability bins equals the observer's resolution
 200    ∀ (obs : Observer),
 201    Fintype.card (Fin obs.resolution) = obs.resolution := by

proof body

Term-mode proof.

 202  intro obs
 203  simp
 204
 205/-- **Theorem (Propensity Vindicated)**:
 206    There IS something objective about probability: the J-cost landscape
 207    determines the projection fiber structure. The "propensity" of outcome v
 208    is the J-cost-weighted measure of fiber(v). This is objective. -/

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
Observer in IndisputableMonolith.Foundation.Determinism decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
Observer in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
probability in IndisputableMonolith.Foundation.QuantumLedger decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
probability in IndisputableMonolith.QFT.SMatrixUnitarity decl_use
probability in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use