theorem proved decidable or rfl

`switchWinningSet_card`

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

formal statement (Lean)

 130theorem switchWinningSet_card : switchWinningSet.card = 6 := by

proof body

Decided by rfl or decide.

 131  decide
 132
 133/-! ## §4. Probabilities under the uniform measure -/
 134
 135/-- The probability of a stay-win under the uniform measure on
 136`Fin 3 × Fin 3`. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

montyHallCert in IndisputableMonolith.Decision.MontyHall decl_use
monty_hall_one_statement in IndisputableMonolith.Decision.MontyHall decl_use
p_switch_eq in IndisputableMonolith.Decision.MontyHall decl_use

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
switchWinningSet in IndisputableMonolith.Decision.MontyHall decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
probability in IndisputableMonolith.Foundation.QuantumLedger decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
uniform in IndisputableMonolith.Information.ShannonEntropy decl_use
probability in IndisputableMonolith.QFT.SMatrixUnitarity decl_use
probability in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use