faithful
plain-language theorem explainer
Two log-characters that agree on every natural number agree on every prime weight: the primes are independent coordinates of the character. Anyone recovering a weight function from its values on ℕ cites this injectivity on the prime axes. The argument is a one-line rewrite through the prime evaluation identity.
Claim. Let $a,b:\mathbb{N}\to\mathbb{R}$. Write $\chi_a(n)$ for the additive extension of the weights $a$ through prime factorization (and likewise $\chi_b$). If $\chi_a(n)=\chi_b(n)$ for every $n\in\mathbb{N}$, then for every prime $p$ one has $a(p)=b(p)$.
background
In the primitive recognition calculus a weight function $a:\mathbb{N}\to\mathbb{R}$ is extended to a log-character by summing over prime factorization: $\chi_a(n)=\sum_p k_p,a(p)$ whenever $n=\prod p^{k_p}$. The value $a(p)$ is the log-weight assigned to the prime axis $p$.
The sibling identity logChar_prime records that this extension is a true section on primes: for prime $p$, $\chi_a(p)=a(p)$. The present module studies when two such characters are the same object, and when their weights align with a reference scale (power-law / axis-coherence statements later in the file).
The local setting is purely arithmetic: no continuum cost $J$, no $\varphi$-ladder, and no physical units enter the statement. The only prior fact needed is the prime evaluation identity above.
proof idea
Specialize the global agreement hypothesis at the prime $p$ to obtain $\chi_a(p)=\chi_b(p)$. Rewrite both sides by the prime evaluation lemma (logChar_prime), which replaces $\chi_a(p)$ by $a(p)$ and $\chi_b(p)$ by $b(p)$. The resulting equality is $a(p)=b(p)$. Term-mode, two rewrites, no induction.
why it matters
This is the independence-of-axes lemma for log-characters: agreement of characters on $\mathbb{N}$ recovers every prime weight, so the primes really are free coordinates. Downstream it is used heavily in the $\mathbb{R}_\delta$ stack (value_ofRat, value_surjective, the calibration interface, and the discrete-vs-one-act unit theorems) and in finite-certificate transfer, where faithfulness of discrete data must be separated from continuum normalization. It also appears in the physics-logic realization skeleton as part of the arithmetic carrier. In the broader Recognition chain it underwrites the claim that discrete prime axes do not secretly force a continuum unit (cf. the calibration pair "discrete does not force the unit" / "one-act forces the unit"), keeping the T5 $J$-uniqueness step cleanly continuum-side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.