Pith. sign in
module module moderate

IndisputableMonolith.Foundation.UniversalForcing.ReciprocalGenerator

show as:
view Lean formalization →

Module packaging the reciprocal involution ι(x)=x⁻¹ on the positive reals as the dual-recognition symmetry of Recognition Science. It proves involutivity, J-cost symmetry, the link from fixed points to zero cost, and the recip-shift whose unique positive fixed point is φ. Downstream PublicSpine and the dual forcing surface import the certificate that reciprocal action pins unit and scale.

claimOn $\mathbb{R}_{>0}$, the map $\iota(x)=x^{-1}$ is an involution. The J-cost is symmetric under $\iota$, and $\iota(x)=x$ if and only if the cost vanishes. A reciprocal shift has unique positive fixed point $\varphi$, and the reciprocal generator certificate asserts that $\iota$ forces both the cost functional and the scale unit.

background

Recognition Science treats dual recognition as the map sending a positive scale factor to its inverse. The cost functional of the framework is the unique continuous solution of the Recognition Composition Law with $J(1)=0$ and $J(x)=J(x^{-1})$; explicitly $J(x)=(x+x^{-1})/2-1$ (T5). Thus reciprocity is not an optional symmetry: it is built into the cost.

This module sits in Foundation.UniversalForcing and imports Cost together with golden-ratio support lemmas (φ²=φ+1, the fixed-point identity φ=1+1/φ, uniqueness of the positive root of $x^2=x+1$). The local objects are the bare reciprocal recip, a shifted reciprocal used to isolate φ, and a Boolean-style certificate ReciprocalGeneratorCert that packages the generation claims for the public spine.

The theoretical setting is the dual forcing surface: reciprocity generates both the cost landscape and the self-similar scale, before the eight-tick and dimension steps of the full chain.

proof idea

Definition layer first: recip is $x\mapsto x^{-1}$ on positives. Involutivity and the fixed-point criterion are elementary field algebra. J-cost symmetry is the identity $J(x^{-1})=J(x)$ read off the closed form (or the RCL axioms). Zero-cost iff fixed under recip follows because $J(x)=0$ forces $x+x^{-1}=2$, hence $x=1$ on $\mathbb{R}_{>0}$.

The recip-shift is the standard rearrangement whose fixed-point equation is equivalent to $x=1+1/x$; uniqueness of the positive solution is the golden-ratio uniqueness lemma from PhiSupport. The certificate reciprocalGeneratorCert_holds assembles these facts into a single discharged Prop for PublicSpine consumption: reciprocal action pins the unit (cost zero only at 1) and the scale (φ as the self-similar fixed point).

why it matters in Recognition Science

PublicSpine imports this module as part of the dual forcing surface (the public δ-stratified counterpart of UnifiedForcingChain). Without a pinned reciprocal generator, the J-uniqueness step (T5) and the forcing of φ as self-similar fixed point (T6) lack their symmetry substrate.

The certificate is the honest packaging of “reciprocity generates cost and scale” for the Boolean/certificate spine kept for loop compatibility and pedagogy. Downstream δ-only tower material and classical continuum extension sit above this foundation; they do not re-prove involution or φ-uniqueness.

Framework landmarks touched directly: T5 (J from $x+x^{-1}$), T6 (φ fixed by the self-similar reciprocal shift), and the RCL symmetry $J(x)=J(x^{-1})$.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)