module module moderate

`IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter`

Structural ledger data on the native cost imply the light hypothesis pack needed for real-character factorization. The module builds a sign-gauge native cost from that ledger, records its monotonicity, zero-calibration, and rational-trace properties, and packages it as a real-character candidate. Gauge-orbit classification cites this bridge. The argument is mostly structural unpacking plus elementary sign-gauge identities.

claimFrom the PRC native-cost structural ledger one obtains the light hypothesis pack for real-character factorization. A sign-gauge native cost $C_{\mathrm{sg}}$ is defined on the ledger data; it is monotone, zero-calibrated, sign-reversing in the appropriate sense, has rational trace two in the base case, and is a real-character candidate. In particular the structural data without anchor already satisfy real-character factorization.

background

Recognition Science treats cost as a J-type functional on positive reals (classically $J(x)=(x+x^{-1})/2-1$), subject to the Recognition Composition Law. The Primitive Recognition Calculus supplies a structural ledger for the native cost: a fixed package of algebraic and calibration fields that any admissible cost display must satisfy.

Real-character factorization isolates a lighter hypothesis pack under which a cost factors through a real character (a multiplicative map into ${\pm 1}$ times a positive radial part). That pack is what downstream gauge-orbit work needs, rather than the full ledger.

This module sits between those two layers. It reads the structural ledger, defines a sign-gauge presentation of the native cost (cost displayed after quotienting or fixing a sign gauge), and checks that the ledger fields already imply the factorization hypotheses.

proof idea

The module is not a single theorem; it is a short bridge. One direction constructs the light hypothesis pack from structural ledger fields (realCharacterFactorizationHypotheses_of_structural). Another specializes to the sans-anchor structural data and obtains real-character factorization directly.

In parallel it defines the sign-gauge native cost and its display form, then proves a checklist of elementary properties: conversion to rationals, base case without the factor two, sign-reversal, monotonicity, zero-calibration, sans-anchor reduction, rational trace equal to two, and finally that the object is a real-character candidate. Those lemmas are mostly rewriting and ledger-field projection rather than deep analysis.

why it matters in Recognition Science

Gauge-orbit classification imports this module: once native cost is known to be a real-character candidate under structural hypotheses, orbits under sign (and related) gauges can be named and compared without carrying the full ledger. That is the step that turns raw PRC cost structure into the language used for cost-gauge taxonomy in the Cost domain.

In the broader RS chain, cost uniqueness and the J-functional (T5) sit upstream; here the concern is representational: which gauge-fixed displays still carry the same recognition cost. Closing the ledger-to-factorization bridge removes a hypothesis interface between structural PRC data and orbit classification, so downstream statements can quote a single candidate object rather than an open pack of assumptions.

scope and limits

Does not derive the J-cost functional equation or T5 uniqueness from scratch.
Does not classify full gauge orbits; that lives in GaugeOrbitClassification.
Does not claim every abstract cost display arises from the structural ledger.
Does not fix physical units or evaluate alpha, masses, or rung formulae.
Does not remove all anchors in every theorem; some lemmas retain calibrated base cases.

used by (1)

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

IndisputableMonolith.Cost.GaugeOrbitClassification module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.RealCharacterFactorization module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostStructuralLedger module_import

declarations in this module (41)

theorem realCharacterFactorizationHypotheses_of_structural L30
theorem structural_sansAnchor_realCharacterFactorization L47
def signGaugeCostDisplay L64
def signGaugeNativeCost L68
theorem signGaugeNativeCost_toRat L73
theorem signGaugeNativeCost_base_sans_two L84
theorem signGaugeNativeCost_signReversing L128
theorem signGaugeNativeCost_monotone L140
theorem signGaugeNativeCost_zero_calibrated L152
theorem signGaugeNativeCost_sansAnchor L163
theorem signGaugeNativeCost_rationalTrace_two L171
theorem signGaugeNativeCost_realCharacterCandidate L182
theorem signGaugeNativeCost_characterExponent_zero L191
theorem signGaugeNativeCost_character_not_oddPower L208
theorem signGaugeNativeCost_not_oddPowerGeneratedNativeCost L224
theorem GaugeOrbitIsOddPowerFamily_refuted L243
def GaugeOrbitIsSignOrOddPowerFamily L251
def signedPow L283
theorem signedPow_zero_arg L285
theorem signedPow_one_arg L288
theorem signedPow_mul L291
theorem signedPow_inv L296
theorem signedPow_div L300
theorem signedPow_neg L304
theorem signedPow_ne_zero L309
theorem signedPow_of_one_le L312
theorem signedPow_mono L318
theorem signedPow_even L330
def signedPowerNativeCost L337
theorem signedPowerNativeCost_toRat L341
theorem signedPowerNativeCost_base L349
theorem signedPowerNativeCost_signReversing L369
theorem signedPowerNativeCost_monotone L375
theorem signedPowerNativeCost_zero_calibrated L384
theorem signedPowerNativeCost_sansAnchor L396
theorem signedPowerNativeCost_even_eq_oddPower L404
theorem signedPowerNativeCost_one_two_toRat L410
theorem signedPowerNativeCost_one_not_oddPower L415
theorem signedPowerNativeCost_one_not_signGauge L435
theorem GaugeOrbitIsSignOrOddPowerFamily_refuted L446
def GaugeOrbitIsSignedPowerFamily L461