pith. sign in
theorem

embed_injective

proved
show as:
module
IndisputableMonolith.Foundation.ArithmeticFromLogic
domain
Foundation
line
620 · github
papers citing
470 papers (below)

plain-language theorem explainer

Distinct elements of the inductive natural-number type map to distinct points under the orbit embedding generated by any non-trivial positive real γ. Workers on realizing the Law of Logic in real-number models cite this result to guarantee faithful representation of abstract numbers. The argument reduces equality of embedded values to equality of exponents by taking logarithms and canceling the nonzero factor log γ.

Claim. Let γ be a positive real not equal to one. The map from the inductive natural numbers (built from an identity element and a successor step) to the positive reals, sending the identity to 1 and each successor step to multiplication by γ, is injective.

background

The Generator structure consists of a positive real value distinct from one, extracted from the non-triviality condition in the Law of Logic. The inductive type of natural numbers is the smallest set containing the identity and closed under the step operation, corresponding to the orbit under multiplication by the generator. The embedding function is defined recursively to realize this orbit in the positive reals.

proof idea

The tactic proof assumes two logic naturals map to the same real under the embedding. It rewrites both sides using the power equivalence, takes the real logarithm of both sides, cancels the common nonzero multiplier log of the generator value, casts the resulting equality back to natural numbers, and applies the round-trip property of fromNat and toNat to recover equality of the original elements.

why it matters

This result is invoked by the injectivity theorem for the positive-ratio orbit interpretation in the LogicRealization module. It completes the demonstration that the abstract Peano structure forced by the Law of Logic embeds injectively into the multiplicative group of positive reals. Within the Recognition Science framework, the construction supports the transition from the abstract forcing chain to concrete numerical realizations used in mass and astrophysical derivations.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.