module module moderate

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostStructuralLedger`

Structural ledger for the primitive recognition calculus: a cross-equivalence is read as equality of two displays, and a native cost jq is attached to real characters on ratio orbits. Supplies the closed form, nonnegativity, and zero-locus of jq used by gauge-orbit constructions. Mostly definitions and elementary algebraic certificates, not a deep existence proof.

claimA cross-equivalence is identified with equality of displays. On a ratio orbit one defines a native cost $j_q$ from a real character, with $j_q(1)=0$, $j_q\ge 0$, $j_q(x)=0\Leftrightarrow x=1$ (on the orbit), a closed form, and the usual sign/negation relations; cost-from-character is identified with $j_q$.

background

In the Primitive Recognition Calculus, recognition data is carried by displays and by real characters on multiplicative ratio orbits. The Recognition Science cost is the unique symmetric defect $J(x)=(x+x^{-1})/2-1$ forced by the composition law (T5); native costs on characters are meant to recover that shape on orbits.

This module sits on the minimality-certificate layer for PRC native cost. It treats a cross-equivalence not as an abstract relation but as equality of the two associated displays (crossDisp / dispCross), so ledger identities become ordinary equalities of displayed quantities.

The central object is jq: the cost pulled from a real character on a ratio orbit (jq_onRatioOrbit, costFromCharacter_jq). Sibling facts record the unit value, vanishing, closed form, nonnegativity, and sign behaviour needed downstream.

proof idea

Definition-and-certificate module rather than a single theorem. Cross-display maps turn equivalence into equality; jq is defined from the character and shown to match cost-from-character. The remaining lemmas are short algebraic checks: value at one, zero locus, closed expression, nonnegativity, and negation/sign rules on the orbit. No heavy analysis; the work is bookkeeping so later gauge-orbit arguments can quote a single native cost.

why it matters in Recognition Science

Gives Cost.GaugeOrbitFromRealCharacter a concrete structural ledger: cross-equivalences as display equalities and a native $j_q$ with the J-cost signature (nonnegative, zero only at the identity on the orbit). That is the bridge from PRC minimality certificates to gauge-orbit constructions in the cost layer, aligning character data with the forced $J$ of the T5 uniqueness step and the Recognition Composition Law. Without this ledger, orbit arguments would re-derive display equality and positivity ad hoc.

scope and limits

Does not prove uniqueness of J globally; only sets up native jq on ratio orbits.
Does not derive T5–T8 forcing; assumes the PRC/cost setting from imports.
Does not construct gauge orbits; only supplies the ledger they import.
Does not claim numerical constants (alpha band, masses); pure structural cost bookkeeping.
Does not replace full minimality certificates; builds on that upstream module.

used by (1)

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

IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimalityCertificate module_import

declarations in this module (104)

theorem crossDisp L69
theorem dispCross L73
def jq L77
theorem jq_onRatioOrbit L79
theorem costFromCharacter_jq L82
theorem jq_one L85
theorem jq_zero L87
theorem jq_closed L89
theorem jq_nonneg L94
theorem jq_lt_zero L98
theorem jq_eq_zero L105
theorem jq_neg L116
theorem jq_inv L121
theorem jq_mono L128
theorem jq_strictMono L143
theorem jq_le_reflect L160
theorem jq_rcl L168
theorem jq_two L176
theorem jq_eq_two_cases L179
def natOrbit L199
theorem natOrbit_toRat L201
def IsPosIntOrbit L205
theorem natOrbit_isPosInt L207
theorem two_isPosInt L210
theorem primeDirection_isPosInt L212
def PRCNativeCostSignReversing L228
def PRCNativeCostMonotone L234
def PRCNativeCostPositive L240
theorem canonicalSelectedNativeCost_jq L245
theorem canonicalSelectedNativeCost_signReversing L249
theorem canonicalSelectedNativeCost_monotone L259
theorem canonicalSelectedNativeCost_positive L267
theorem signReversing_forces_signed_unit L277
structure PRCSignReversingNativeCostHypotheses L291
def PRCSignReversingNativeCostUniquenessTarget L297
theorem PRCSignReversingNativeCostUniquenessTarget_proved L303
theorem canonicalSelectedNativeCost_signReversing_hypotheses L316
theorem signReversing_class_forces_slim L326
theorem absValueGeneratedNativeCost_not_signReversing L339
lemma exists_pow_gt_rat L363
lemma cut_pins_aux L378
theorem cut_pins L414
structure MonoMult L428
theorem pow L436
theorem pos L445
theorem ge_one L461
theorem transfer_le L502
theorem transfer_ge L511
theorem trivial_of_two_eq_one L522
theorem monoMult_gauge L548
theorem natCast_monoMult L569
theorem monotone_multiplicative_pins L580
structure PRCStructuralNativeCostHypotheses L594
def PRCStructuralNativeCostUniquenessTarget L601
theorem structural_character_calibrated_on_positive_integers L609
theorem PRCStructuralNativeCostUniquenessTarget_proved L688
theorem canonicalSelectedNativeCost_structural_hypotheses L744
theorem structural_forces_slim L755
theorem structural_forces_positive L770
structure PRCStructuralNativeCostHypothesesSansAnchor L786
def PRCStructuralSansAnchorUniquenessTarget L793
theorem structural_iff_sansAnchor_and_two_calibrated L800
def powerGeneratedNativeCost L833
theorem powerGeneratedNativeCost_toRat L837
theorem powerGeneratedNativeCost_base L845
theorem powerGeneratedNativeCost_monotone L865
theorem powerGeneratedNativeCost_zero_calibrated L873
theorem powerGeneratedNativeCost_signReversing L884
def oddPowerGeneratedNativeCost L892
theorem oddPowerGeneratedNativeCost_toRat L895
theorem oddPowerGeneratedNativeCost_sansAnchor L899
theorem oddPowerGeneratedNativeCost_anchor_injective L911
def cubeGeneratedNativeCost L927
theorem cubeGeneratedNativeCost_toRat L930
theorem cubeGeneratedNativeCost_sansAnchor L934
theorem oddPowerGeneratedNativeCost_zero L940
theorem cubeGeneratedNativeCost_two_not_canonical L945
def GaugeOrbitIsOddPowerFamily L1065
theorem gauge_orbit_contains_every_odd_power L1072
theorem PRCStructuralSansAnchorUniquenessTarget_refuted L1083

… and 24 more