Foundation Primitive Recognition Calculus Prcnative Cost Structural Ledger Struc

/-- **Round 5 terminal.** The structural ledger forces the canonical cost. -/
theorem PRCStructuralNativeCostUniquenessTarget_proved :
    PRCStructuralNativeCostUniquenessTarget := by
  intro F hF q
  obtain ⟨χ, hχ, hFχ⟩ :=
    PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved F hF.native
      hF.zero_calibrated
  have hcal := structural_character_calibrated_on_positive_integers hF hχ hFχ
  have hresp : PRCCharacterRespectsCrossEq χ :=
    PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical hχ
      PRCNormalizeRatioCanonicalTarget_proved
  have hchi : ∀ a b : RatioOrbit, a.toRat = b.toRat →
      (χ a).toRat = (χ b).toRat := by
    intro a b hab
    exact crossDisp
      (hresp a b (dispCross hab))
  -- every positive integer orbit is calibrated
  have hposcal : ∀ (a : RatioOrbit), IsPosIntOrbit a →
      RatioOrbit.crossEq (costFromCharacter χ a) (onRatioOrbit a) := by
    rintro a ⟨n, hn, han⟩
    have hdisp : a.toRat = (natOrbit n).toRat := by rw [natOrbit_toRat, han]
    rw [RatioOrbit.crossEq_iff_toRat_eq, costFromCharacter_jq, jq_onRatioOrbit,
      han]
    have hn' := hcal n hn
    rw [← hchi a (natOrbit n) hdisp] at hn'
    exact hn'
  have hprime : PRCCharacterPrimeDirectionCalibrated χ := fun p hp =>
    hposcal _ (primeDirection_isPosInt hp)
  have hpair : PRCCharacterPrimePairProductCostConsistent χ := by
    intro p hp r hr
    refine hposcal _ ⟨p.toNat * r.toNat, ?_, ?_⟩
    · obtain ⟨a, ha, _⟩ := primeDirection_isPosInt hp
      obtain ⟨b, hb, _⟩ := primeDirection_isPosInt hr
      have hpn : 1 ≤ p.toNat := by
        have h := primeDirection_toRat_ne_zero p hp
        rw [primeDirection_toRat] at h
        exact Nat.one_le_iff_ne_zero.mpr (by exact_mod_cast h)
      have hrn : 1 ≤ r.toNat := by
        have h := primeDirection_toRat_ne_zero r hr
        rw [primeDirection_toRat] at h
        exact Nat.one_le_iff_ne_zero.mpr (by exact_mod_cast h)
      exact Nat.one_le_iff_ne_zero.mpr (Nat.mul_ne_zero (by omega) (by omega))
    · rw [RatioOrbit.mul_toRat, primeDirection_toRat, primeDirection_toRat]
      push_cast
      ring
  have hsignCost :
      RatioOrbit.crossEq (costFromCharacter χ negativeOneRatio)
        (onRatioOrbit negativeOneRatio) :=
    RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm (hFχ negativeOneRatio))
      (signReversing_forces_signed_unit hF.native.unit_zero hF.sign_reversing)
  have hsign : PRCCharacterSignedUnitCalibrated χ :=
    costFromCharacter_negativeOne_forces_signed_unit hχ hsignCost
  exact RatioOrbit.crossEq_trans (hFχ q)
    (PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved χ
      ⟨⟨hχ, hprime, hpair⟩, hsign⟩ q)

/-- **The continuum gauge orbit is uncountable.** Distinct positive exponents
give distinct costs (`costLambda_injective`) and the positive reals are
uncountable, so what `calibrationAxiom` collapses on the line is not a discrete
list of impostors. Stated here rather than left as a remark, because the size of
the collapsed family is the quantitative half of the comparison with the
carrier. -/
theorem continuum_scale_family_uncountable :
    ¬ continuumScaleFamily.Countable := by
  intro hc
  haveI : Countable continuumScaleFamily := hc.to_subtype
  have hinj : Function.Injective
      (fun l : Set.Ioi (0 : ℝ) =>
        (⟨costLambda (l : ℝ), ⟨(l : ℝ), Set.mem_Ioi.mp l.2, rfl⟩⟩ :
          continuumScaleFamily)) := by
    rintro ⟨l, hl⟩ ⟨m, hm⟩ h
    have hfun : costLambda l = costLambda m := congrArg Subtype.val h
    exact Subtype.ext (costLambda_injective (Set.mem_Ioi.mp hl) (Set.mem_Ioi.mp hm)
      (fun x => congrFun hfun x))
  haveI : Countable (Set.Ioi (0 : ℝ)) := hinj.countable
  have hexp : Function.Injective
      (fun x : ℝ => (⟨Real.exp x, Set.mem_Ioi.mpr (Real.exp_pos x)⟩ :
        Set.Ioi (0 : ℝ))) := by
    intro a b h
    exact Real.exp_injective (congrArg Subtype.val h)
  exact real_not_countable hexp.countable

theorem jq_two : jq 2 = 1 / 4 := by norm_num [jq]

/-- **The golden scale has no δ-native solution.** Elementary and choice-free:
clearing denominators gives `a² = b(a+b)` in lowest terms, so the denominator
divides `a²` and is therefore `1`, and no integer solves `a² = a + 1`. -/
theorem no_rat_golden_scale {t : ℚ} (ht : 0 < t) : 1 + t⁻¹ ≠ t := by
  intro h
  have ht0 : t ≠ 0 := ne_of_gt ht
  have hsq : t * t = t + 1 := by
    field_simp at h
    linarith [h]
  have hdpos : (0:ℚ) < (t.den : ℚ) := by exact_mod_cast t.pos
  have hnd : (t.num : ℚ) = t * (t.den : ℚ) :=
    (div_eq_iff (ne_of_gt hdpos)).mp (Rat.num_div_den t)
  have hkey : (t.num : ℚ) * (t.num : ℚ)
      = (t.num : ℚ) * (t.den : ℚ) + (t.den : ℚ) * (t.den : ℚ) := by
    rw [hnd]
    linear_combination ((t.den : ℚ) * (t.den : ℚ)) * hsq
  have hZ : t.num * t.num = t.num * (t.den : ℤ) + (t.den : ℤ) * (t.den : ℤ) := by
    exact_mod_cast hkey
  have hdvd : (t.den : ℤ) ∣ t.num * t.num := ⟨t.num + (t.den : ℤ), by
    rw [hZ]; ring⟩
  have hdvdN : t.den ∣ t.num.natAbs * t.num.natAbs := by
    have hstep := Int.natAbs_dvd_natAbs.mpr hdvd
    simpa [Int.natAbs_mul] using hstep
  have hcop : Nat.Coprime t.den (t.num.natAbs * t.num.natAbs) :=
    Nat.Coprime.mul_right t.reduced.symm t.reduced.symm
  have hd1 : t.den = 1 := by
    have hg : Nat.gcd t.den (t.num.natAbs * t.num.natAbs) = t.den :=
      Nat.gcd_eq_left hdvdN
    rw [Nat.Coprime] at hcop
    rw [hcop] at hg
    exact hg.symm
  rw [hd1] at hZ
  push_cast at hZ
  have hpos : 0 < t.num := Rat.num_pos.mpr ht
  have hb : t.num ≤ 2 := by nlinarith [hZ, sq_nonneg (t.num - 1)]
  have hcase : t.num = 1 ∨ t.num = 2 := by omega
  rcases hcase with hc | hc <;> rw [hc] at hZ <;> norm_num at hZ