nativeReciprocalGeneratorSplit_holds
plain-language theorem explainer
Assembles the reciprocal-generator facts that live entirely on rational ratio orbits: involution, cost symmetry under reciprocal, and the unit as the unique zero-cost fixed point. The golden self-similar scale is explicitly excluded as non-native. Cited by the structural stratification certificate. Proof is a four-field structure pack of already-proved lemmas.
Claim. The reciprocal generator on ratio orbits splits as follows: reciprocal is an involution; the native cost is symmetric under reciprocal; on the positive cone, reciprocal fixes an orbit if and only if its cost is zero; and no positive ratio orbit satisfies the golden fixed-point equation $1 + q^{-1} = q$.
background
In the primitive recognition calculus, ratio orbits carry a native cost built from the character $J_q$ (the discrete $J$-cost on rationals). Reciprocal acts on orbits by $q \mapsto q^{-1}$. Three structural facts about this action are purely $\delta$-native: double reciprocal recovers the orbit, cost is unchanged under reciprocal, and on the positive cone the only self-reciprocal orbit is the unit (equivalently, the only zero-cost orbit).
The fourth clause is negative: no positive rational orbit solves $1 + q^{-1} = q$, the fixed-point equation whose real solution is the golden ratio $\varphi$. That scale is therefore not native to the rational ledger; it must be purchased by completion. The structure packages this split: everything the reciprocal generator says about cost is $\delta$-native; only the fixed point is bought.
Upstream lemmas already establish each field separately: involution by double inversion, cost symmetry via $J_q(q^{-1}) = J_q(q)$, the fixed-point/zero-cost equivalence on the positive cone, and absence of a rational golden scale.
proof idea
Term-mode structure inhabitant. Each field is filled by a named lemma:
involutivefrom double reciprocal ontoRatviainv_inv;cost_symmetricby rewriting both sides through the $J_q$ character and $J_q(q^{-1}) = J_q(q)$;unit_is_cost_zeroby specializing the positive-cone equivalence (reciprocal fixes iff cost vanishes);scale_is_a_purchaseby the nonexistence theorem that no positive rational solves the golden equation, reduced to the corresponding rational statement.
No new algebra is done here; the proof only wires the four prior results into the structure.
why it matters
This is the $\varphi$ split inside the native-cost structural ledger: it isolates which reciprocal-generator claims are already proved on rational orbits and which single claim (the self-similar scale) requires leaving the native carrier. Downstream it is consumed by the structural stratification certificate, which bundles uniqueness, slimness, positivity, and gauge-inhabitation into one certificate object.
In the Recognition forcing chain, $\varphi$ is forced as the self-similar fixed point (T6) of the $J$-cost geometry. The present split makes that forcing precise at the ledger level: three reciprocal facts are free on $\mathbb{Q}$-orbits; the golden fixed point is the purchase that completes the generator. It therefore marks the exact boundary between $\delta$-native structure and the real completion used later for the public spine and trace-closure certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.