theorem proved term proof

`cell_eq_iff_kernel`

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

formal statement (Lean)

  64theorem cell_eq_iff_kernel {K : Type*} (I : PrimitiveInterface K) (x y : K) :
  65    cellOf I x = cellOf I y ↔ I.kernel x y := by

proof body

Term-mode proof.

  66  exact Quotient.eq
  67
  68/-! ## Finite-resolution labels and neighborhoods -/
  69
  70/-- The finite event label of a recognition cell. This is well-defined because
  71the quotient identifies exactly configurations with equal observed labels. -/

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
PrimitiveInterface in IndisputableMonolith.Foundation.ObserverFromRecognition decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
cellOf in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use