theorem proved term proof

`internal_consistency_exists`

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

formal statement (Lean)

 162theorem internal_consistency_exists : Nonempty InternalConsistency :=

proof body

Term-mode proof.

 163  ⟨rrf_internally_consistent⟩
 164
 165/-! ## The Compilation as Recognition -/
 166
 167/-- Compilation is a recognition event.
 168
 169When Lean type-checks this file, it is performing a recognition:
 170verifying that the propositions are consistent with the type theory.
 171-/

depends on (9)

Lean names referenced from this declaration's body.

consistent in IndisputableMonolith.Complexity.SAT.Backprop decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
InternalConsistency in IndisputableMonolith.RRF.Foundation.SelfReference decl_use
rrf_internally_consistent in IndisputableMonolith.RRF.Foundation.SelfReference decl_use