`embed`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticFromLogic
domain: Foundation
line: 556 · github
papers citing: 6 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 556.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 553      exact hLaws.identity 1 one_pos }
 554
 555/-- The orbit embedding: `LogicNat` into the positive reals. -/
 556def embed (γ : Generator) : LogicNat → ℝ
 557  | .identity => 1
 558  | .step n   => γ.value * embed γ n
 559
 560@[simp] theorem embed_zero (γ : Generator) : embed γ LogicNat.zero = 1 := rfl
 561
 562@[simp] theorem embed_succ (γ : Generator) (n : LogicNat) :
 563    embed γ (LogicNat.succ n) = γ.value * embed γ n := rfl
 564
 565/-- The embedding lands in the strictly positive reals. -/
 566theorem embed_pos (γ : Generator) (n : LogicNat) : 0 < embed γ n := by
 567  induction n with
 568  | identity => exact one_pos
 569  | step n ih =>
 570    show 0 < γ.value * embed γ n
 571    exact mul_pos γ.pos ih
 572
 573/-- **Multiplicative homomorphism**: addition in `LogicNat` corresponds
 574to multiplication of orbit elements. This is the structural fact that
 575`LogicNat` *is* the orbit, parameterized by iteration count. -/
 576theorem embed_add (γ : Generator) (a b : LogicNat) :
 577    embed γ (a + b) = embed γ a * embed γ b := by
 578  induction b with
 579  | identity =>
 580    show embed γ (a + LogicNat.zero) = embed γ a * embed γ LogicNat.zero
 581    rw [LogicNat.add_zero, embed_zero, mul_one]
 582  | step b ih =>
 583    show embed γ (a + LogicNat.succ b) = embed γ a * embed γ (LogicNat.succ b)
 584    rw [LogicNat.add_succ, embed_succ, embed_succ, ih]
 585    ring
 586

papers checked against this theorem (showing 6 of 6)

Heartbeat mechanism lets LLM agents learn their own thinking schedule
echoes · 2604.14178

"state evolution s_{t+1} = F(s_t, d_t; Theta); macro/micro state machine; LogicNat-like orbit of activities"
Recursive simulator captures ring-down in fast cavity crossings
echoes · 2605.13599

"recursive formulation of the intracavity electric field as a sum over round trips... sampling frequency... internally adjusted... consistent with the cavity round-trip structure"
Decoupled streams model timing mismatches in agent actions
echoes · 2605.11484

"We define an Engagement Process (EP) over a discrete sequence of ticks T={0,1,2,…}. … actions and observations as decoupled event streams … Yt and At need not be paired."
Discrete linear systems as time group representations
echoes · 2604.08940

"a linear system naturally gives rise to the map ρ: Z → GL(R^n), t ↦ A^t ... equivalent to giving V the structure of a left k[G]-module ... when G = Z/TZ, k[G] ≅ k[x]/(x^T − 1)"
CDF charts turn averaging linear and recover Kolmogorov means
echoes · 2605.02104

"E_G(X) := G⁻¹(E[G(X)]) ... transporting the distribution to probability space, performing linear averaging there, and pulling back to value space."
Multidimensional cost geometry
echoes · 2604.06957

"Affine geodesics on M_t are straight lines in log-coordinates, globally defined; on M_x they are restricted by xᵢ > 0."