theorem proved term proof

`nonCollapse_monotone_automatic`

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

formal statement (Lean)

 125theorem nonCollapse_monotone_automatic (sys : DirectedRefinement C) :
 126    ∀ i c₁ c₂,
 127      ¬Indistinguishable (sys.recognizer i) c₁ c₂ →
 128      ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂ :=

proof body

Term-mode proof.

 129  monotone_separation_of_refinement sys
 130
 131/-- The convergence condition implies: the intersection of all
 132equivalence relations is the identity (diagonal). -/

depends on (18)

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived 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
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use
DirectedRefinement in IndisputableMonolith.RecogGeom.EffectiveManifold decl_use
monotone_separation_of_refinement in IndisputableMonolith.RecogGeom.EffectiveManifold decl_use
Indistinguishable in IndisputableMonolith.RecogGeom.Indistinguishable decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use