No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
100theorem logic_embeds (L : LogicSystem) :
101 Nonempty (Embeds L.Prop' universalStructure) :=
proof body
Term-mode proof.
102 ⟨{ embed := fun _ => (0 : ℝ), structure_preserved := rfl }⟩
103
104/-- Qualia can be embedded. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (9)
Lean names referenced from this declaration's body.
-
embed
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
embed
in IndisputableMonolith.Foundation.HamiltonianEmergence
decl_use
-
LogicSystem
in IndisputableMonolith.Mathematics.LogicSystemsFromConfigDim
decl_use
-
Qualia
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use
-
Embeds
in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism
decl_use
-
LogicSystem
in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism
decl_use
-
universalStructure
in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism
decl_use