IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.CharacterRigidityForcing
Characters on the positive rationals that are calibrated at a single orbit point (typically 2) are forced to act as the identity character on the whole ratio orbit, and therefore yield a rigid cost equal to the native J-cost. Continuum workers cite this when lifting discrete PRC uniqueness to the completion. The argument is algebraic: multiplicative character laws plus cross-equivalence at one generator pin the trace on squares and products.
claimA multiplicative character $\chi$ on the positive rationals is calibrated at $q$ when $\chi(q)$ is cross-equivalent to $q$ (identity action on the orbit direction of $q$). Calibration at $2$, together with the character laws for $1$, products, and reciprocals, forces $\chi$ to be the identity on the ratio orbit; the associated cost and doubled-trace functionals are then rigidly equal to the native recognition cost $J$.
background
Primitive Recognition Calculus (PRC) works with multiplicative characters on positive rationals and a native cost built from the unique $J$ solving the Recognition Composition Law. Cross-equivalence identifies two positive quantities when they determine the same orbit direction for cost comparison; it is the discrete stand-in for equality of scale factors before continuum completion.
This module sits after native cost uniqueness and before forcing $J$ on the completion. The central definition is calibration at a point $q$: $\chi(q)$ is cross-equivalent to $q$ itself, so $\chi$ acts as the identity character along that orbit ray. The PRC cost hypotheses supply calibration only at $2$; everything else must be deduced.
Supporting lemmas record how characters behave under multiplication, reciprocal, and the unit, and how calibration propagates to products, reciprocals, and squares. Ratio-orbit cross-equivalence then turns single-point calibration into global identity on the orbit.
proof idea
Definition layer first: CharacterCalibratedAt packages the single-point cross-equivalence datum. Multiplicative bookkeeping lemmas (character_one_toRat, character_mul_toRat, character_recip_toRat) and their calibrated counterparts close the character under the group operations while preserving calibration.
The rigidity core is onRatioOrbit_crossEq plus character_trace_rigid: once calibrated at a generator (two), the character agrees with the identity on the full ratio orbit in the cross-equivalence sense, so the trace functional is forced. costFromCharacter_rigid and doubledTrace_character_rigid transport that identity into equality of the induced cost (and doubled trace) with the native $J$-cost. No analytic estimates; pure multiplicative algebra and orbit bookkeeping.
why it matters in Recognition Science
Native PRC uniqueness alone does not yet pin the continuum cost. This module supplies the missing rigidity bridge: a character calibrated only at two is forced to the identity orbit character, so any cost reconstructed from it must be $J$. Downstream, ForcedJOnCompletion imports the module to carry that discrete rigidity onto the completion and force the continuum cost functional.
In the broader Recognition chain this is the continuum-facing half of T5-style $J$-uniqueness: the same $J(x)=(x+x^{-1})/2-1$ that solves the Recognition Composition Law is recovered as the only cost compatible with a calibrated character. Without character rigidity, completion could admit exotic costs; with it, the forcing path stays unique.
scope and limits
- Does not construct or classify characters beyond the calibrated multiplicative case on positive rationals.
- Does not prove continuum completeness or topological extension; that is left to ForcedJOnCompletion.
- Does not replace native cost uniqueness; it assumes the PRC native $J$ and transports rigidity from calibration.
- Does not address non-multiplicative maps or calibration at points other than the orbit generated from two.
- Does not derive physical constants, mass ladders, or dimensional forcing (T6–T8).
used by (1)
depends on (1)
declarations in this module (14)
-
def
CharacterCalibratedAt -
theorem
character_mul_toRat -
theorem
character_one_toRat -
theorem
character_recip_toRat -
theorem
calibrated_one -
theorem
calibrated_mul -
theorem
calibrated_recip -
theorem
calibrated_square -
theorem
onRatioOrbit_crossEq -
theorem
character_trace_rigid -
theorem
costFromCharacter_rigid -
theorem
doubledTrace_character_rigid -
theorem
prime_calibration_forces_identity_on_direction -
def
target_OnePointCalibrationForcesGlobalIdentity