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)
80structure FaithfulArithmeticInterpretation (R : LogicRealization) : Prop where
81 injective : Function.Injective R.interpret
82 zero_step_noncollapse : ∀ n : R.Orbit, R.interpret R.orbitZero ≠ R.interpret (R.orbitStep n)
83
84/-- Fold over `LogicNat` into the positive-ratio carrier for the selected
85non-trivial generator. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (6)
Lean names referenced from this declaration's body.
-
carrier
in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice
decl_use
-
carrier
in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity
decl_use
-
LogicNat
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
LogicRealization
in IndisputableMonolith.Foundation.LogicRealization
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
interpret
in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization
decl_use