IndisputableMonolith.Cost.TraceRationalExponent
Number-theoretic support for Cost: no rational square root of five, the golden unit squared has trace three, and rational traces on powers force positive-integer exponents. Real character factorization imports the package. Proofs mix five-adic valuation parity, Z[φ] coordinate expansions, and a six-exponentials-style input bundle.
claimPackage of lemmas: $\sqrt{5}\notin\mathbb{Q}$; $\varphi^2$ has field trace $3$; powers of the golden unit expand with integer coordinates; if a power has rational trace then the exponent is a positive integer (via rationality of coordinates and a six-exponentials trace input).
background
In the Cost layer, real characters and factorization identities are constrained by the arithmetic of the golden unit $\varphi=(1+\sqrt{5})/2$. Its minimal polynomial is $x^2-x-1$; powers live in $\mathbb{Z}[\varphi]$ and admit unique coordinates relative to the basis ${1,\varphi}$. The field trace of $\varphi^2$ is $3$, so rational-trace hypotheses sit on a concrete integer.
The module isolates the elementary Diophantine facts needed before any analytic character identity: five is not a rational square (five-adic valuation is odd), and rationality of a trace propagates to rationality of the coordinate pair of the corresponding power. Those coordinate facts feed an integer-exponent conclusion.
A bundled input shape for six-exponentials-type reasoning appears as a named structure, so downstream factorization can cite a single arithmetic package rather than re-proving valuation and coordinate lemmas in place.
proof idea
The module is a lemma cluster, not a single theorem. no_rational_sqrt_five is a pure valuation argument: $v_5$ of a square is even while $v_5(5)=1$. Trace three for the golden square is a direct expansion of $\varphi^2$. Coordinate lemmas equate powers with their $\mathbb{Z}$-basis coefficients and show that a rational trace forces those coefficients (hence the power) to be rational when the exponent is rational. The integer-exponent theorem assembles those facts with the six-exponentials input bundle to conclude the exponent is a positive integer. No single master proof; each sibling is short and self-contained.
why it matters in Recognition Science
Real character factorization in Cost imports this module. Without ruling out non-integer rational exponents on trace-rational golden powers, character identities could admit spurious rational scalings that break the unique J-cost and $\varphi$-ladder normalization used upstream in the forcing chain (T5–T6). The five-adic lemma closes the quadratic irrationality gap for $\sqrt{5}$; the trace-three and coordinate lemmas pin the arithmetic of $\varphi^n$; the exponent theorem supplies the integrality step factorization needs. Scaffolding elsewhere in Cost can treat integer exponents as discharged once this import is in place.
scope and limits
- Does not prove the six-exponentials theorem; only packages a trace input shape.
- Does not address complex characters or non-real embeddings beyond the golden field.
- Does not derive J-uniqueness or the RCL; those live in the forcing chain.
- Does not claim anything about irrational exponents or transcendental bases outside $\varphi$.
- Does not close full real-character factorization; that is the downstream module.