IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCExpLogField
Defines the exp/log field closure generated by π and φ inside the reals: rationals come free as the prime field, and field plus exp/log operations then reach every Recognition Science constant. Downstream cost-on-field and certificate modules import this countable carrier. The construction is an explicit countable directed union of finite generator sets under one-step field and exp/log closure.
claimLet $\mathrm{gens}=\{\pi,\varphi\}$. Let $S$ be the ascending chain obtained by iterating field operations and $\exp/\log$ (on positives) from $\mathrm{gens}$, and let $T=\bigcup S$. Then $T$ is a countable subfield of $\mathbb{R}$ containing every RS constant built from those seeds, and $x\in T$ iff $x$ appears at some finite stage of $S$.
background
Primitive Recognition Calculus needs a concrete real carrier on which the J-cost and related RS constants live, without assuming the full continuum as a primitive. The prior module supplies the minimal field layer; this module adjoins the transcendental and algebraic seeds that actually appear in the RS constant list.
The generators are $\pi$ and $\varphi$ (the golden ratio forced as the self-similar fixed point in the forcing chain). Rationals are free once any subfield is present. From those seeds one closes under field operations and under $\exp$ and $\log$ on the positive ray, producing a directed system $S$ whose union $T$ is the working constant field.
Sibling definitions record finiteness of the generator set, the one-step operator, monotonicity and directedness of $S$, countability of $S$ and of $T$, and the membership criterion relating $T$ to the stages of $S$.
proof idea
Definition-and-construction module rather than a single deep theorem. It packages a finite generator set, a one-step closure operator under field and exp/log moves, the induced monotone directed chain $S$, and the union $T$ with coe and membership lemmas. Countability of $S$ and $T$ follows from finite generators plus countable iteration of finitary operations. No heavy analytic uniqueness argument lives here; the work is bookkeeping of the inductive closure.
why it matters in Recognition Science
Gives the countable real carrier on which later PRC layers evaluate cost and certify constants. Imported by the cost-on-field module and by the shrunk-certificate module, so every downstream claim that RS constants sit in a countable exp/log field routes through this construction.
In the broader framework this is the algebraic home for $\varphi$ (T6 fixed point), for factors such as $\varphi^{\pm5}$ in the native $c,\hbar,G$ normalizations, and for any constant assembled by field and exp/log combinations from $\pi$ and $\varphi$. It keeps the foundation constructive and countable before cost identities are imposed.
scope and limits
- Does not prove uniqueness of J or force φ; those live in the T5–T6 forcing chain.
- Does not define the J-cost or mass ladder; only the carrier field for constants.
- Does not claim T equals all of R or contains non-RS transcendentals beyond the closure.
- Does not discharge analytic identities among constants; only membership in the closure.
- Does not address completeness, topology, or measure on T beyond countability.
used by (2)
depends on (1)
declarations in this module (20)
-
def
gens -
theorem
gens_finite -
def
Sstep -
def
S -
theorem
S_mono -
theorem
S_monotone -
theorem
S_directed -
theorem
S_countable -
def
T -
theorem
mem_T_iff -
theorem
T_coe -
theorem
T_countable -
theorem
T_exp_closed -
theorem
T_log_closed -
theorem
pi_mem_T -
theorem
phi_mem_T -
theorem
e_mem_T -
theorem
alphaInv_mem_T -
theorem
T_proper -
theorem
rs_operations_below_continuum