IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostSelection

   1/-
   2  PrimitiveRecognitionCalculus/PRCNativeCostSelection.lean
   3
   4  Round-trip source:
   5    δ/plans/JCost_Free_Side_Mint_Prereg_20260724.json   (frozen prereg)
   6    plans/Delta_JCost_Free_Side_Rederivation_Session_Prompt_20260724.txt
   7
   8  The free-side mint of the cost-selection keystone (campaign P-delta-jfree).
   9
  10  `PublicSpine.cost_selection_holds` deposits J-uniqueness at
  11  `StrengthTag.traceClosure`: its statement lives on the completed line and
  12  consumes continuity (`law_of_logic_forces_jcost`). This module deposits the
  13  δ-native counterpart on the countable carrier `RatioOrbit`, at
  14  `StrengthTag.deltaOnly`, together with the typed wall naming exactly what
  15  the continuum premise was buying.
  16
  17  WIN-A (`cost_selection_native_holds`): every native cost satisfying the
  18  itemized algebraic premise ledger (reciprocity, normalization invariance,
  19  canonical RCL on nonzero orbits, unit-zero, prime-pair product calibration,
  20  signed-unit calibration, all-prime-axis calibration, zero-orbit trace
  21  calibration) is crossEq-pointwise the canonical `onRatioOrbit` cost. The
  22  package also carries non-vacuity (an explicit witness inhabits the full
  23  hypothesis class) and the frozen decoy exclusions (the constant-zero cost
  24  and the linear cost fail the class).
  25
  26  WIN-B (`continuum_price_residue_wall_tagged`): the residue of the continuum
  27  price, stated as theorems. The proven necessity chain is STAGED: the base
  28  ledger fails (two-adic twist), the pair-strengthened ledger fails
  29  (absolute-value cost), and the prime-signed ledger without zero-orbit
  30  calibration fails (zero-flat cost). Separately, every prime axis is an
  31  independent CHARACTER-orientation freedom. Honesty note (cross-family
  32  review, 2026-07-24): the per-axis freedom is a character-level statement;
  33  at the cost level a single-axis twist is invisible on its own axis (J is
  34  reciprocal) and is caught by the pair-product field, so minimality of the
  35  all-prime calibration family relative to the base+pairs+sign ledger is
  36  OPEN (`PRCSignedStrengthenedNativeCostUniquenessTarget` is undetermined in
  37  the parent module). The wall is tagged `classicalExtension` because its
  38  countermodel characters are classical verifier-side constructions
  39  (panel K2: classical negatives never ride under `deltaOnly`).
  40
  41  Scope: this module only reads `PRCNativeCostUniqueness.lean` and
  42  `PublicSpine.lean`. It never edits `cost_selection_holds` or its tag.
  43-/
  44
  45import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
  46import IndisputableMonolith.Foundation.PublicSpine
  47
  48namespace IndisputableMonolith
  49namespace Foundation
  50namespace PrimitiveRecognitionCalculus
  51namespace PRCJCost
  52
  53/-! ## Non-vacuity witness
  54
  55The raw `onRatioOrbit` cannot inhabit `PRCNativeCostHypotheses` verbatim: the
  56`unit_zero` field demands the literal `RatioOrbit.zero` representative, while
  57`onRatioOrbit RatioOrbit.one` computes to the crossEq-equal but structurally
  58distinct representative `0/2`. The selected witness routes the unit display to
  59the canonical zero representative and is elsewhere the canonical cost. Its
  60verifier display is the J formula everywhere, including at the unit. -/
  61
  62/-- The canonical selected native cost: the J cost with the unit orbit sent to
  63the literal zero representative. This is the non-vacuity witness for the full
  64zero-calibrated prime-signed strengthened hypothesis class. -/
  65def canonicalSelectedNativeCost (q : RatioOrbit) : RatioOrbit :=
  66  if q.toRat = 1 then RatioOrbit.zero else onRatioOrbit q
  67
  68/-- The selected witness displays as the J formula on every orbit; on the
  69unit-display branch both sides are `0`. -/
  70theorem canonicalSelectedNativeCost_toRat (q : RatioOrbit) :
  71    (canonicalSelectedNativeCost q).toRat = (q.toRat + q.toRat⁻¹) / 2 - 1 := by
  72  rw [canonicalSelectedNativeCost]
  73  by_cases h : q.toRat = 1
  74  · rw [if_pos h, RatioOrbit.zero_toRat, h]
  75    norm_num
  76  · rw [if_neg h, onRatioOrbit_toRat]
  77
  78/-- The selected witness is crossEq-pointwise the canonical cost. -/
  79theorem canonicalSelectedNativeCost_crossEq_onRatioOrbit (q : RatioOrbit) :
  80    RatioOrbit.crossEq (canonicalSelectedNativeCost q) (onRatioOrbit q) := by
  81  rw [RatioOrbit.crossEq_iff_toRat_eq, canonicalSelectedNativeCost_toRat,
  82    onRatioOrbit_toRat]
  83
  84/-- The selected witness satisfies the base native-cost hypotheses. -/
  85theorem canonicalSelectedNativeCost_native_hypotheses :
  86    PRCNativeCostHypotheses canonicalSelectedNativeCost where
  87  reciprocal := by
  88    intro q
  89    rw [RatioOrbit.crossEq_iff_toRat_eq, canonicalSelectedNativeCost_toRat,
  90      canonicalSelectedNativeCost_toRat, RatioOrbit.recip_toRat]
  91    by_cases hq : q.toRat = 0
  92    · simp [hq]
  93    · field_simp [hq]
  94      ring
  95  normalized_invariant := by
  96    intro q
  97    rw [RatioOrbit.crossEq_iff_toRat_eq, canonicalSelectedNativeCost_toRat,
  98      canonicalSelectedNativeCost_toRat, DistinctionNat.normalizeRatio_toRat]
  99  canonical_rcl := by
 100    intro x y hx hy
 101    rw [RatioOrbit.crossEq_iff_toRat_eq]
 102    simp only [RatioOrbit.add_toRat, RatioOrbit.mul_toRat,
 103      canonicalSelectedNativeCost_toRat, div_toRat, two_toRat]
 104    have hxy : x.toRat * y.toRat ≠ 0 := mul_ne_zero hx hy
 105    field_simp [hx, hy, hxy]
 106    ring_nf
 107  unit_zero := by
 108    rw [canonicalSelectedNativeCost, if_pos RatioOrbit.one_toRat]
 109  two_calibrated := canonicalSelectedNativeCost_crossEq_onRatioOrbit two
 110
 111/-- The selected witness satisfies the full zero-calibrated prime-signed
 112strengthened hypothesis class: the frozen ledger is non-vacuous. -/
 113theorem canonicalSelectedNativeCost_full_hypotheses :
 114    PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
 115      canonicalSelectedNativeCost where
 116  prime_signed :=
 117    { signed_strengthened :=
 118        { strengthened :=
 119            { native := canonicalSelectedNativeCost_native_hypotheses
 120              prime_pair_product_cost := fun p hp r hr =>
 121                canonicalSelectedNativeCost_crossEq_onRatioOrbit
 122                  (RatioOrbit.mul (primeDirection p hp) (primeDirection r hr)) }
 123          signed_unit :=
 124            canonicalSelectedNativeCost_crossEq_onRatioOrbit negativeOneRatio }
 125      prime_direction_cost := fun p hp =>
 126        canonicalSelectedNativeCost_crossEq_onRatioOrbit (primeDirection p hp) }
 127  zero_calibrated := by
 128    rw [PRCDoubledTraceZeroCalibrated, RatioOrbit.crossEq_iff_toRat_eq]
 129    simp only [nativeCostDoubledTrace, doubledTraceValue, RatioOrbit.mul_toRat,
 130      RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat,
 131      canonicalSelectedNativeCost_toRat, RatioOrbit.zero_toRat]
 132    norm_num
 133
 134/-! ## Frozen decoys
 135
 136Preregistered known-wrong costs (prereg PREREG-jfree-mint-20260724). Both must
 137fail the frozen hypothesis class; the failure point is the two-calibration
 138field, exactly as frozen before proving. These two are smoke tests: they die
 139at the shallowest field. The layer-wise near-miss decoys are the wall's
 140countermodels themselves (two-adic twist, absolute-value cost, zero-flat
 141cost), each of which passes every ledger layer above the one it refutes. -/
 142
 143/-- Decoy 1: the constant-zero cost. -/
 144def constantZeroNativeCost : RatioOrbit → RatioOrbit :=
 145  fun _ => RatioOrbit.zero
 146
 147/-- Decoy 2: the linear cost `q - 1`. -/
 148def linearNativeCost (q : RatioOrbit) : RatioOrbit :=
 149  RatioOrbit.sub q RatioOrbit.one
 150
 151/-- The constant-zero cost already fails the base hypothesis ledger: the
 152canonical cost of the two orbit displays as `1/4`, not `0`. -/
 153theorem constantZeroNativeCost_not_native_hypotheses :
 154    ¬ PRCNativeCostHypotheses constantZeroNativeCost := by
 155  intro h
 156  have h2 := h.two_calibrated
 157  rw [RatioOrbit.crossEq_iff_toRat_eq] at h2
 158  simp only [constantZeroNativeCost, RatioOrbit.zero_toRat, onRatioOrbit_toRat,
 159    two_toRat] at h2
 160  norm_num at h2
 161
 162/-- The linear cost already fails the base hypothesis ledger: `2 - 1 = 1` is
 163not the canonical display `1/4`. -/
 164theorem linearNativeCost_not_native_hypotheses :
 165    ¬ PRCNativeCostHypotheses linearNativeCost := by
 166  intro h
 167  have h2 := h.two_calibrated
 168  rw [RatioOrbit.crossEq_iff_toRat_eq] at h2
 169  simp only [linearNativeCost, RatioOrbit.sub_toRat, RatioOrbit.one_toRat,
 170    onRatioOrbit_toRat, two_toRat] at h2
 171  norm_num at h2
 172
 173/-- Decoy exclusion 1 against the full frozen class. -/
 174theorem constantZeroNativeCost_excluded :
 175    ¬ PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
 176        constantZeroNativeCost :=
 177  fun h =>
 178    constantZeroNativeCost_not_native_hypotheses
 179      h.prime_signed.signed_strengthened.strengthened.native
 180
 181/-- Decoy exclusion 2 against the full frozen class. -/
 182theorem linearNativeCost_excluded :
 183    ¬ PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
 184        linearNativeCost :=
 185  fun h =>
 186    linearNativeCost_not_native_hypotheses
 187      h.prime_signed.signed_strengthened.strengthened.native
 188
 189/-! ## Zero-orbit calibration is necessary (the missing necessity witness)
 190
 191The prime-signed strengthened ledger WITHOUT zero-orbit calibration does not
 192force uniqueness: `zeroFlatNativeCost` (canonical away from zero, flat at the
 193zero orbit) satisfies every field of that ledger, because the canonical RCL
 194only constrains nonzero orbits and every calibration probe is nonzero, yet it
 195disagrees with the canonical cost at the zero orbit. -/
 196
 197/-- The zero-flat countermodel satisfies the prime-signed strengthened ledger
 198(everything except zero-orbit calibration). -/
 199theorem zeroFlatNativeCost_prime_signed_strengthened_hypotheses :
 200    PRCPrimeSignedStrengthenedNativeCostHypotheses zeroFlatNativeCost where
 201  signed_strengthened :=
 202    { strengthened :=
 203        { native := zeroFlatNativeCost_hypotheses
 204          prime_pair_product_cost := by
 205            intro p hp r hr
 206            refine zeroFlatNativeCost_crossEq_onRatioOrbit_of_nonzero ?_
 207            rw [RatioOrbit.mul_toRat]
 208            exact mul_ne_zero (primeDirection_toRat_ne_zero p hp)
 209              (primeDirection_toRat_ne_zero r hr) }
 210      signed_unit := by
 211        refine zeroFlatNativeCost_crossEq_onRatioOrbit_of_nonzero ?_
 212        rw [negativeOneRatio_toRat]
 213        norm_num }
 214  prime_direction_cost := fun p hp =>
 215    zeroFlatNativeCost_crossEq_onRatioOrbit_of_nonzero
 216      (primeDirection_toRat_ne_zero p hp)
 217
 218/-- **Zero-orbit calibration is irreducible.** Without it, the prime-signed
 219strengthened ledger admits the zero-flat countermodel: uniqueness fails at the
 220zero orbit, where the canonical cost displays `-1` and the countermodel
 221displays `0`. -/
 222theorem PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted :
 223    ¬ PRCPrimeSignedStrengthenedNativeCostUniquenessTarget := by
 224  intro h
 225  have hzero :=
 226    h zeroFlatNativeCost zeroFlatNativeCost_prime_signed_strengthened_hypotheses
 227      RatioOrbit.zero
 228  rw [zeroFlatNativeCost_zero, RatioOrbit.crossEq_iff_toRat_eq,
 229    RatioOrbit.zero_toRat, onRatioOrbit_toRat, RatioOrbit.zero_toRat] at hzero
 230  norm_num at hzero
 231
 232/-! ## WIN-A: the native cost-selection deposit -/
 233
 234/-- **The native cost-selection package** (prereg PREREG-jfree-mint-20260724).
 235The δ-native counterpart of `PublicSpine.CostSelectionPackage`:
 236
 237* `j_unique_native`: every native cost satisfying the itemized ledger
 238  (base hypotheses + prime-pair products + signed unit + all prime axes +
 239  zero orbit) is crossEq-pointwise the canonical `onRatioOrbit` cost.
 240* `non_vacuous`: an explicit witness inhabits the full ledger and agrees with
 241  the canonical cost, so the class is neither empty nor drifted.
 242* `zero_cost_excluded` / `linear_cost_excluded`: the frozen known-wrong costs
 243  fail the ledger, so the predicate discriminates.
 244
 245Read this as CONDITIONAL δ-native rigidity: the RCL plus an explicit
 246countable J-valued calibration ledger (prime, pair, sign, zero) determines J
 247on `RatioOrbit`. It removes the completion cost of the continuum deposit; it
 248does not remove the calibration cost, which is the ledger itself. The
 249uniqueness content is real (calibration lives on generators; the RCL must
 250still propagate it to every orbit, and the parent module's refuted
 251propagation targets show that step is not free), but the honest name is
 252rigidity from extensive calibration data, not an economical selector.
 253
 254Every hypothesis in the ledger is an algebraic condition on the countable
 255carrier `RatioOrbit` (countable quantification over prime orbits included):
 256the statement consumes no completed orbit, no trace closure, no continuity.
 257The tag is an audit assertion under the PublicSpine statement-carrier
 258convention, not a kernel-derived semantic grade; the classical proof shell
 259is disclosed by the axiom audit receipts and never upgrades the statement
 260grade. -/
 261structure CostSelectionPackageNative : Prop where
 262  j_unique_native :
 263    PRCZeroCalibratedPrimeSignedStrengthenedNativeCostUniquenessTarget
 264  non_vacuous :
 265    ∃ F : RatioOrbit → RatioOrbit,
 266      PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses F ∧
 267        ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (onRatioOrbit q)
 268  zero_cost_excluded :
 269    ¬ PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
 270        constantZeroNativeCost
 271  linear_cost_excluded :
 272    ¬ PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
 273        linearNativeCost
 274
 275/-- The native cost-selection package holds. -/
 276theorem costSelectionPackageNative_holds : CostSelectionPackageNative where
 277  j_unique_native :=
 278    PRCZeroCalibratedPrimeSignedStrengthenedNativeCostUniquenessTarget_proved
 279  non_vacuous :=
 280    ⟨canonicalSelectedNativeCost, canonicalSelectedNativeCost_full_hypotheses,
 281      canonicalSelectedNativeCost_crossEq_onRatioOrbit⟩
 282  zero_cost_excluded := constantZeroNativeCost_excluded
 283  linear_cost_excluded := linearNativeCost_excluded
 284
 285/-- **WIN-A deposit: cost selection on the free side of the meter.** The
 286selection of J on the δ-native countable carrier, tagged strictly below the
 287continuum deposit (`cost_selection_holds` at `traceClosure`). -/
 288theorem cost_selection_native_holds :
 289    PublicSpine.Tagged StrengthTag.deltaOnly CostSelectionPackageNative where
 290  holds := costSelectionPackageNative_holds
 291
 292/-- The native deposit sits strictly below the continuum deposit on the K1
 293strength ledger. -/
 294theorem native_deposit_strictly_below_continuum_deposit :
 295    StrengthTag.deltaOnly < StrengthTag.traceClosure :=
 296  StrengthTag.deltaOnly_lt_traceClosure
 297
 298/-! ## WIN-B: the continuum price residue, as a typed wall -/
 299
 300/-- **The irreducible residue of the continuum price** (prereg
 301PREREG-jfree-mint-20260724). What `ContinuousOn` plus one-point calibration
 302buys in `law_of_logic_forces_jcost`, the δ-native carrier must purchase as an
 303infinite independent calibration family. Each field is a kernel-checked
 304theorem:
 305
 306* `base_insufficient`: the base ledger admits the two-adic axis twist.
 307* `strengthened_insufficient`: adding prime-pair products still admits the
 308  absolute-value countermodel (the signed unit is invisible).
 309* `prime_signed_insufficient`: adding the signed unit and every prime axis
 310  still admits the zero-flat countermodel (the zero orbit is invisible to the
 311  nonzero RCL).
 312* `every_prime_axis_free`: for every prime orbit there is a ratio character
 313  fixing all other prime axes and inverting that one. This is
 314  character-orientation freedom, exactly as stated; whether a proper
 315  subfamily of the cost-level prime calibrations suffices (given pairs and
 316  sign) remains OPEN, because J's reciprocity hides a single-axis twist on
 317  its own axis.
 318* `zero_spike_still_excluded`: the frozen zero-spike decoy keeps failing the
 319  zero-orbit calibration that repairs it. -/
 320structure ContinuumPriceResidueWall : Prop where
 321  base_insufficient : ¬ PRCNativeCostUniquenessTarget
 322  strengthened_insufficient : ¬ PRCStrengthenedNativeCostUniquenessTarget
 323  prime_signed_insufficient :
 324    ¬ PRCPrimeSignedStrengthenedNativeCostUniquenessTarget
 325  every_prime_axis_free :
 326    ∀ (p : DistinctionNat) (hp : DistinctionNat.primeOrbit p),
 327      ∃ χ : RatioOrbit → RatioOrbit,
 328        PRCRatioCharacter χ ∧
 329          (∀ (r : DistinctionNat) (hr : DistinctionNat.primeOrbit r),
 330            r ≠ p →
 331              RatioOrbit.crossEq (χ (primeDirection r hr))
 332                (primeDirection r hr)) ∧
 333          ¬ RatioOrbit.crossEq (χ (primeDirection p hp)) (primeDirection p hp)
 334  zero_spike_still_excluded :
 335    ¬ PRCDoubledTraceZeroCalibrated zeroSpikeDoubledTrace
 336
 337/-- The continuum price residue wall holds. -/
 338theorem continuumPriceResidueWall_holds : ContinuumPriceResidueWall where
 339  base_insufficient := PRCNativeCostUniquenessTarget_refuted
 340  strengthened_insufficient := PRCStrengthenedNativeCostUniquenessTarget_refuted
 341  prime_signed_insufficient :=
 342    PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted
 343  every_prime_axis_free := prc_every_prime_axis_orientation_free
 344  zero_spike_still_excluded := zeroSpikeDoubledTrace_not_zero_calibrated
 345
 346/-- **WIN-B deposit: the residue wall, honestly tagged.** The countermodel
 347characters are classical verifier-side constructions, so the wall rides at
 348`classicalExtension` (panel K2). -/
 349theorem continuum_price_residue_wall_tagged :
 350    PublicSpine.Tagged StrengthTag.classicalExtension ContinuumPriceResidueWall
 351    where
 352  holds := continuumPriceResidueWall_holds
 353
 354/-! ## The premise ledger (design requirement 1)
 355
 356Every hypothesis that replaces continuity, itemized with the grade it costs on
 357the K1 strength ledger, each with its necessity witness. The highest-cost
 358premise sets the tag of the deposit; every item below is `deltaOnly`, so the
 359deposit is `deltaOnly`. -/
 360
 361/-- The itemized premise ledger for the native cost-selection deposit. -/
 362def nativeCostSelectionPremiseLedger : List StrengthClaim :=
 363  [ { label := "base"
 364      tag := StrengthTag.deltaOnly
 365      statement := "Reciprocity, normalization invariance, canonical RCL on \
 366nonzero orbits, unit-zero, two-calibration (PRCNativeCostHypotheses). \
 367Necessity: PRCNativeCostUniquenessTarget_refuted (two-adic axis twist)." }
 368  , { label := "prime_pair_products"
 369      tag := StrengthTag.deltaOnly
 370      statement := "Calibration on products of two prime directions \
 371(PRCNativeCostPrimePairProductCalibrated). Necessity: the two-adic generated \
 372cost slips through the base ledger exactly on such products." }
 373  , { label := "signed_unit"
 374      tag := StrengthTag.deltaOnly
 375      statement := "Calibration at the signed unit -1 \
 376(PRCNativeCostSignedUnitCalibrated). Necessity: \
 377PRCStrengthenedNativeCostUniquenessTarget_refuted (absolute-value cost)." }
 378  , { label := "all_prime_axes"
 379      tag := StrengthTag.deltaOnly
 380      statement := "Calibration on every native prime direction, a countable \
 381family (PRCNativeCostPrimeDirectionCalibrated). Character-level necessity: \
 382prc_every_prime_axis_orientation_free (every axis is an independent \
 383character-orientation freedom). Cost-level minimality relative to \
 384base+pairs+sign is OPEN (PRCSignedStrengthenedNativeCostUniquenessTarget \
 385undetermined)." }
 386  , { label := "zero_orbit"
 387      tag := StrengthTag.deltaOnly
 388      statement := "Zero-orbit calibration of the doubled trace \
 389(PRCDoubledTraceZeroCalibrated). Necessity: \
 390PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted (zero-flat \
 391countermodel); the nonzero RCL never sees the zero orbit." }
 392  ]
 393
 394/-- The ledger is uniformly at the δ-only floor: the weakest link of the
 395deposit is `deltaOnly`. -/
 396theorem nativeCostSelectionPremiseLedger_all_deltaOnly :
 397    ∀ c ∈ nativeCostSelectionPremiseLedger, c.tag = StrengthTag.deltaOnly := by
 398  intro c hc
 399  simp only [nativeCostSelectionPremiseLedger, List.mem_cons,
 400    List.not_mem_nil, or_false] at hc
 401  rcases hc with h | h | h | h | h <;> subst h <;> rfl
 402
 403/-! ## Axiom audit (headline receipts) -/
 404
 405#print axioms costSelectionPackageNative_holds
 406#print axioms cost_selection_native_holds
 407#print axioms continuumPriceResidueWall_holds
 408#print axioms continuum_price_residue_wall_tagged
 409#print axioms canonicalSelectedNativeCost_full_hypotheses
 410#print axioms PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted
 411
 412end PRCJCost
 413end PrimitiveRecognitionCalculus
 414end Foundation
 415end IndisputableMonolith
 416