theorem proved term proof

`isRecognitionConnected_resolutionCell`

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

formal statement (Lean)

  62theorem isRecognitionConnected_resolutionCell (r : Recognizer C E) (c : C) :
  63    IsRecognitionConnected r (ResolutionCell r c) := by

proof body

Term-mode proof.

  64  intro c₁ c₂ h₁ h₂
  65  simp only [ResolutionCell, Set.mem_setOf_eq] at h₁ h₂
  66  exact Indistinguishable.trans r h₁ (Indistinguishable.symm' r h₂)
  67
  68/-- A subset of a recognition-connected set is recognition-connected -/

used by (1)

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

connectivity_status in IndisputableMonolith.RecogGeom.Connectivity decl_use

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
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
IsRecognitionConnected in IndisputableMonolith.RecogGeom.Connectivity decl_use
Indistinguishable in IndisputableMonolith.RecogGeom.Indistinguishable decl_use
ResolutionCell in IndisputableMonolith.RecogGeom.Indistinguishable decl_use