theorem proved term proof

`eventCount_pos`

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

formal statement (Lean)

 122theorem eventCount_pos (c : C) (U : Set C) (hU : U ∈ L.N c)
 123    (hfin : (r.R '' U).Finite) :
 124    0 < eventCount r U hfin := by

proof body

Term-mode proof.

 125  unfold eventCount
 126  have hc : c ∈ U := L.mem_of_mem_N c U hU
 127  have hne : (r.R '' U).Nonempty := ⟨r.R c, ⟨c, hc, rfl⟩⟩
 128  exact Finset.card_pos.mpr ((Set.Finite.toFinset_nonempty hfin).mpr hne)
 129
 130/-! ## Resolution Bound -/
 131
 132/-- Given a finite set of events, count them -/

depends on (14)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
eventCount in IndisputableMonolith.Decision.SleepingBeauty decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Resolution in IndisputableMonolith.Mathematics.BirchTateStructure decl_use
Resolution in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
Resolution in IndisputableMonolith.Quantum.Firewall decl_use
eventCount in IndisputableMonolith.RecogGeom.FiniteResolution decl_use
L in IndisputableMonolith.Recognition decl_use
U in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use