pith. machine review for the scientific record. sign in
def definition def or abbrev high

embed

show as:
view Lean formalization →

The embed definition recursively maps the inductive LogicNat type into the positive reals by sending the identity constructor to 1 and each step constructor to multiplication by the generator value γ. Researchers deriving arithmetic from the Law of Logic in the Recognition framework cite this to realize the orbit {1, γ, γ², ...} explicitly. The definition proceeds by direct pattern matching on the two constructors of LogicNat with no lemmas or tactics applied.

claimLet γ be a Generator (positive real ≠ 1). The map e_γ : LogicNat → ℝ is defined by e_γ(identity) = 1 and e_γ(step n) = γ ⋅ e_γ(n).

background

LogicNat is the inductive type forced by the Law of Logic, with identity as the zero-cost multiplicative identity and step as one iteration of the generator; its two-constructor structure mirrors the orbit {1, γ, γ², ...} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1. A Generator is the structure with value : ℝ, pos : 0 < value, and nontrivial : value ≠ 1, extracted from the non_trivial field of SatisfiesLawsOfLogic. This definition sits in the ArithmeticFromLogic module, which builds natural-number arithmetic directly from the functional equation of logic after importing LogicAsFunctionalEquation.

proof idea

This is a recursive definition by pattern matching on the constructors of LogicNat. The identity case returns the constant 1. The step case multiplies the generator value by the recursive call on the predecessor. No lemmas from upstream results are invoked.

why it matters in Recognition Science

This definition supplies the concrete orbit realization used by downstream results such as embed_add (multiplicative homomorphism) and embed_eq_pow (identification with powers of γ.value). It feeds into DomainInstance in RecognitionCategory for domain embeddings and into CoarseGrain for Riemann sums. In the Recognition framework it closes the step from the Law of Logic to explicit arithmetic on the positive reals, enabling the phi-ladder and eight-tick octave. It touches the open question of extension to continuous limits in coarse-graining.

scope and limits

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.

depends on (7)

Lean names referenced from this declaration's body.