def definition def or abbrev

`embed`

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

formal statement (Lean)

 556def embed (γ : Generator) : LogicNat → ℝ
 557  | .identity => 1
 558  | .step n   => γ.value * embed γ n
 559

used by (26)

From the project-wide theorem graph. These declarations reference this one in their body.

DomainInstance in IndisputableMonolith.Algebra.RecognitionCategory decl_use
CoarseGrain in IndisputableMonolith.ClassicalBridge.CoarseGrain decl_use
RiemannSum in IndisputableMonolith.ClassicalBridge.CoarseGrain decl_use
embed_add in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_eq_pow in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_injective in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_le_iff_of_one_lt in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_lt_iff_of_one_lt in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_pos in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_strictMono_of_one_lt in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_succ in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_zero in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
ClosedObservableFramework in IndisputableMonolith.Foundation.ClosedObservableFramework decl_use
diagonalHamiltonian in IndisputableMonolith.Foundation.HamiltonianEmergence decl_use
embed in IndisputableMonolith.Foundation.HamiltonianEmergence decl_use
embed_norm_sq in IndisputableMonolith.Foundation.HamiltonianEmergence decl_use
no_moduli_forces_uniform_ratios in IndisputableMonolith.Foundation.HierarchyRealization decl_use
nonuniform_ratios_yield_moduli in IndisputableMonolith.Foundation.HierarchyRealization decl_use
no_injective_real_to_bool in IndisputableMonolith.Foundation.HierarchyRealizationObstruction decl_use
ZeroParameterComparisonLedger in IndisputableMonolith.Foundation.LedgerCanonicality decl_use
positiveRatioOrbitInterpret_val in IndisputableMonolith.Foundation.LogicRealization decl_use
recognition_dimension_unique in IndisputableMonolith.RecogGeom.Charts decl_use
Embeds in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism decl_use
logic_embeds in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism decl_use
physics_embeds in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism decl_use
qualia_embeds in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism decl_use

depends on (7)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
Generator in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed in IndisputableMonolith.Foundation.HamiltonianEmergence decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use