`back`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticFromLogic
domain: Foundation
line: 513 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 513.

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

 510/-! ## 6. Embedding into ℝ₊ via a Generator
 511
 512Section 5 recovers the abstract Peano structure. Section 6 ties that
 513structure back to the comparison operator that started the chain. The
 514embedding `LogicNat → ℝ₊` sends `n` to `γⁿ` for any non-trivial
 515generator `γ` of the multiplicative group of positive reals. This is
 516the structural witness that the abstract Peano structure of
 517`LogicNat` is the orbit structure of any non-trivial element under
 518multiplication.
 519
 520The full chain (existence of γ from `non_trivial`, injectivity of the
 521embedding from the J-cost positivity off-identity, generator-free
 522characterization of the embedding's image) is left for Level 2. The
 523content of this section is the embedding map and its multiplicative
 524homomorphism property. -/
 525
 526/-- A non-trivial generator: any positive real other than the
 527identity. The Law of Logic guarantees existence via the
 528`non_trivial` field of `SatisfiesLawsOfLogic`. -/
 529structure Generator where
 530  value      : ℝ
 531  pos        : 0 < value
 532  nontrivial : value ≠ 1
 533
 534/-- **Chain closure**: a comparison operator satisfying the Law of Logic
 535yields an explicit non-trivial generator. The construction extracts the
 536witness from `non_trivial` and uses `identity` to rule out `value = 1`.
 537
 538This is the structural completion of the chain. Before this lemma,
 539`Generator` was a free structure; now it is *literally* derived from
 540`SatisfiesLawsOfLogic`. -/
 541noncomputable def generatorOfLawsOfLogic
 542    {C : ComparisonOperator} (hLaws : SatisfiesLawsOfLogic C) : Generator :=
 543  let x := Classical.choose hLaws.non_trivial

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.