A Generator is any positive real number other than 1 that serves as the multiplicative base for embedding LogicNat into the positive reals. Researchers deriving arithmetic from the laws of logic cite this structure to parameterize the orbit under repeated multiplication. The definition extracts the nontrivial witness directly from SatisfiesLawsOfLogic and rules out the unit via the identity event.
claimA generator is a real number $g$ such that $g > 0$ and $g ≠ 1$.
background
The ArithmeticFromLogic module constructs natural-number arithmetic by embedding the inductive type LogicNat into the positive reals. The Generator structure supplies the fixed base for this embedding. Upstream, SatisfiesLawsOfLogic is the structure requiring a comparison operator to obey identity, non-contradiction, excluded middle, scale invariance, and route independence; its non_trivial field supplies the witness that becomes the generator value. The identity event from ObserverForcing is the J-cost minimum at state 1, which excludes the trivial case.
proof idea
The structure is introduced directly as a definition with three fields: the real value, its positivity proof, and the inequality to 1. No tactics or lemmas are applied; the nontrivial field is populated from the corresponding hypothesis in SatisfiesLawsOfLogic.
why it matters in Recognition Science
Generator supplies the parameter for every embedding theorem in the module, including embed, embed_add, embed_eq_pow, and embed_injective. It completes the structural passage from SatisfiesLawsOfLogic to concrete arithmetic in the positive reals. Within Recognition Science this realizes the step from the Law of Logic to the phi-ladder and natural-number arithmetic, feeding the mass formula and the eight-tick octave.
scope and limits
Does not fix any specific numerical value for the generator.
Does not prove existence of a generator beyond the non_trivial field of SatisfiesLawsOfLogic.
Does not incorporate the J-cost function or defectDist explicitly.
Does not extend to complex bases or higher-dimensional embeddings.
formal statement (Lean)
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`. -/
used by (14)
From the project-wide theorem graph. These declarations reference this one in their body.