Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

show as:
view Lean formalization →

Native PRC cost uniqueness via ratio characters: a cost on ratio orbits factors through a d'Alembert character, matched to doubled traces under cross-equivalence. Cited by anyone forcing J-uniqueness (T5) or selecting the native cost before continuum completion. The module defines character-to-cost maps, doubled-trace hypothesis bundles, and matching lemmas that stay quotient-native.

claimDevelops a ratio character $C$ for a PRC cost so that the cost is recovered by the d'Alembert factorization $J(x)=\frac{C(x)+C(x^{-1})}{2}-1$ up to cross-equivalence on ratio orbits, together with doubled-trace identities and hypothesis transfers that identify the native cost with this factorization.

background

Primitive Recognition Calculus places costs on ratio orbits, not bare reals. Equality is therefore cross-equivalence (quotient-native), not definitional identity. The classical cost $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$ solves the Recognition Composition Law in d'Alembert form; T5 asserts its uniqueness under regularity.

Upstream modules supply the PRC kernel, the J-cost interface, monotone d'Alembert structure, and trace closure. A ratio character is a multiplicative map on orbits whose symmetric combination yields a cost candidate. Doubled traces package the pair of character values needed for that factorization, still at the orbit level.

The local setting is discrete/quotient uniqueness before continuum completion: identify which native cost is forced by character and trace data, without yet passing to $\mathbb{R}_{>0}$.

proof idea

Definition layer first: ratio character, cost-from-character (including a rational specialization), doubled-trace value, and the native-cost doubled-trace packaging. Congruence lemmas keep doubled traces well-defined under orbit equivalence.

Hypothesis bundles collect d'Alembert and native-cost assumptions in doubled-trace form; transfer lemmas push ordinary native-cost hypotheses into that shape. Matching theorems then show that, under those hypotheses (or under cost cross-equivalence), the character-derived doubled trace agrees with the cost. Structure is definitional scaffolding plus hypothesis transfer and matching, not a single deep existence proof.

why it matters in Recognition Science

Feeds native cost selection, continuum character-rigidity forcing, forced $J$ on completion, real character factorization, and the universal foundation module. This is the discrete uniqueness step that T5 J-uniqueness and the forcing chain need before continuum rigidity: without quotient-native character/trace matching, one cannot identify the PRC cost with $\cosh(\log x)-1$.

Downstream continuum modules import this package to rigidify characters on the completion; cost factorization and universal foundation reuse the same native-cost bridge. It closes the native-cost side of PRC foundation prior to measure/cardinality arguments on the continuum.

scope and limits

used by (5)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (1168)

… and 1088 more