module module moderate

`IndisputableMonolith.Cost.RealCharacterFactorization`

Module on real-character factorization of the recognition cost: the doubled-trace (d'Alembert) form of the composition law follows from the RCL alone, without the anchor at two. It builds positive-integer orbits, native-cost monotonicity and sign-reversal, and the real-ratio character that recovers the cost. Downstream gauge-orbit work imports it. Argument is algebraic reduction from RCL plus orbit bookkeeping.

claimFrom the Recognition Composition Law alone, the doubled-trace identity for $J$ holds without using the normalization $J(2)=1/2$. The module constructs the positive-integer orbit of a real ratio character, proves native-cost monotonicity and sign-reversal, and recovers the cost functional from that real character.

background

Recognition cost is the unique continuous solution $J$ of the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, with the classical closed form $J(x)=(x+x^{-1})/2-1$ forced at T5. The doubled-trace (d'Alembert) rewrite packages the same identity in a form convenient for character factorization on $\mathbb{R}_{>0}$.

This module sits in the Cost domain. It imports real-trace root structure, rational exponents on the trace, and PRC native-cost uniqueness. The module doc states the key economy: the doubled-trace form needs only the RCL; the anchor at two is not used. Sibling material introduces positive-integer orbits, the map from natural orbits to rationals, base-sans-two and sans-anchor hypothesis bundles, and the real-ratio character that rebuilds the cost.

proof idea

Not a single theorem: a short development. Doubled-trace d'Alembert identities are derived three ways (from RCL, from native cost, and under sans-anchor hypotheses), each by algebraic rearrangement of the composition law. Orbit infrastructure (IsPosIntOrbit, natOrbit, conversion to rationals) supports discrete sampling of the character. Native-cost sign-reversal and monotonicity are recorded as lemmas. The real-ratio character and costFromRealCharacter close the factorization, recovering $J$ from the character data without invoking the two-anchor.

why it matters in Recognition Science

Feeds Cost.GaugeOrbitFromRealCharacter, which builds gauge orbits from the real character constructed here. In the forcing chain this is post-T5 bookkeeping: once $J$ is unique, one still needs a clean factorization that does not smuggle the normalization $J(2)=1/2$ into every identity. Isolating RCL-only doubled-trace facts keeps later gauge and orbit arguments honest about which hypotheses they consume. Touches the RCL landmark directly; no new claim about $\phi$, eight-tick, or $D=3$.

scope and limits

Does not prove J-uniqueness; that is upstream T5 / PRC native-cost uniqueness.
Does not force the anchor J(2)=1/2; the module explicitly avoids it.
Does not construct gauge orbits; that is the downstream GaugeOrbitFromRealCharacter module.
Does not address mass ladder, alpha band, or spacetime dimension claims.
Does not supply a numerical solver or floating-point character evaluation.

used by (1)

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

IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.RealTraceRoot module_import
IndisputableMonolith.Cost.TraceRationalExponent module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness module_import

declarations in this module (73)

theorem doubledTrace_dAlembert_of_rcl L35
theorem doubledTrace_dAlembert_of_native L57
def IsPosIntOrbit L69
def natOrbit L72
theorem natOrbit_toRat L74
def PRCNativeCostSignReversing L77
def PRCNativeCostMonotone L81
structure BaseSansTwo L86
structure SansAnchorHypotheses L104
theorem doubledTrace_dAlembert_of_sansAnchor L110
structure PRCRealRatioCharacter L122
def costFromRealCharacter L135
def exponentOfCharacter L138
def SansAnchorRealCharacterFactorizationTarget L144
abbrev SansAnchorRealCharacterFactorizationInput L154
def traceDisplay L160
theorem traceDisplay_one L164
theorem traceDisplay_recip L172
theorem traceDisplay_dAlembert L181
theorem traceDisplay_posInt_ge_two L192
theorem traceDisplay_two_ge_two L210
theorem traceDisplay_eq_of_crossEq L215
def rationalTrace L231
theorem rationalTrace_eq_traceDisplay L235
theorem rationalTrace_one L242
theorem rationalTrace_recip L253
theorem rationalTrace_dAlembert L266
theorem rationalTrace_neg L299
theorem rationalTrace_nat_ge_two L311
def linearExtraction L322
theorem linearExtraction_unit L326
theorem linearExtraction_multiplicative L338
theorem linearExtraction_recip_sum L416
def anchorRoot L454
def nontrivialCharacterValue L458
theorem anchorRoot_ge_one L462
theorem anchorRoot_add_inv L468
theorem anchorRoot_gt_one L474
theorem anchorRoot_ne_zero L486
theorem anchorRoot_sq_sub_one_ne_zero L491
theorem nontrivialCharacterValue_one L498
theorem nontrivialCharacterValue_mul L505
theorem nontrivialCharacterValue_recip_sum L515
theorem rationalTrace_nat_mono L527
theorem rationalTrace_two_pow_eq_two L550
theorem rationalTrace_nat_eq_two_of_two_eq_two L573
theorem rationalTrace_pos_eq_two_of_two_eq_two L593
def rationalSignCharacter L630
theorem rationalSignCharacter_one L633
theorem rationalSignCharacter_mul L636
theorem rationalSignCharacter_recip L661
theorem rationalSignCharacter_nonzero L670
theorem rationalSignCharacter_of_pos L676
def realCharacterCandidate L682
theorem nontrivialCharacterValue_nonzero L691
theorem nontrivialCharacterValue_recip L702
theorem nontrivialCharacterValue_trace L712
theorem nontrivialCharacterValue_two L723
theorem nontrivialCharacterValue_pow L746
theorem nontrivialCharacterValue_pos_on_nat L761
theorem exists_pow_trace_decrease L778
theorem nontrivialCharacterValue_nat_trace_mono L819
theorem nontrivialCharacterValue_principal_on_nat L836
theorem realCharacterCandidate_unit L868
theorem realCharacterCandidate_mul L877
theorem realCharacterCandidate_recip L890
theorem realCharacterCandidate_nonzero L903
theorem realCharacterCandidate_principal_on_pos_int L913
theorem realCharacterCandidate_is_character L925
theorem realCharacterCandidate_trace_of_pos L934
theorem realCharacterCandidate_cost_agrees L950
theorem realCharacterCandidate_small_traces_rational L962
theorem SansAnchorRealCharacterFactorizationTarget_proved L976