structure
definition
Generator
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 529.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
nontrivial -
of -
Chain -
of -
SatisfiesLawsOfLogic -
identity -
is -
of -
Before -
from -
is -
of -
is -
was -
of -
is -
and -
value -
Chain -
Chain -
identity -
comparison
used by
formal source
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
544 have hx : 0 < x ∧ derivedCost C x ≠ 0 := Classical.choose_spec hLaws.non_trivial
545 { value := x
546 pos := hx.1
547 nontrivial := by
548 intro hx_eq_one
549 apply hx.2
550 show derivedCost C x = 0
551 rw [hx_eq_one]
552 show C 1 1 = 0
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