theorem proved term proof

`chartCompatible_symm`

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

formal statement (Lean)

 116theorem chartCompatible_symm (φ₁ φ₂ : RecognitionChart L r n)
 117    (hcompat : ChartCompatible L r φ₁ φ₂) :
 118    ChartCompatible L r φ₂ φ₁ := by

proof body

Term-mode proof.

 119  intro c h₂ h₁
 120  exact (hcompat c h₁ h₂).symm
 121
 122/-! ## Recognition Atlas -/
 123
 124/-- A recognition atlas is a family of compatible charts that cover the space -/

depends on (18)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
compatible in IndisputableMonolith.Complexity.SAT.Backprop 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
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
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
ChartCompatible in IndisputableMonolith.RecogGeom.Charts decl_use
RecognitionChart in IndisputableMonolith.RecogGeom.Charts decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use