IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Strength

   1/-
   2  PrimitiveRecognitionCalculus/Strength.lean
   3
   4  Round-trip source:
   5    PRC_Kernel_Spec_20260526.html
   6
   7  Spec anchor:
   8    K1. Strength Ledger
   9
  10  This module records the proof-strength tags used by the Primitive
  11  Recognition Calculus kernel. The tags are not mathematical assumptions.
  12  They are audit labels attached to later definitions and theorems.
  13-/
  14
  15import Mathlib
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace PrimitiveRecognitionCalculus
  20
  21/-- K1. The strength tag attached to a PRC claim. -/
  22inductive StrengthTag where
  23  /-- Forced by distinction and finite repetition alone. -/
  24  | deltaOnly
  25  /-- Uses the completed orbit or completed stable trace families. -/
  26  | traceClosure
  27  /-- Uses selection of witnesses from stable families. -/
  28  | choice
  29  /-- Uses controlled subtrace-class or power-class formation. -/
  30  | powerComprehension
  31  /-- Uses excluded middle or full classical reasoning as an extension. -/
  32  | classicalExtension
  33  deriving DecidableEq, Repr
  34
  35/-- A small audit record tying a claim label to its strength tag. -/
  36structure StrengthClaim where
  37  label : String
  38  tag : StrengthTag
  39  statement : String
  40  deriving Repr
  41
  42/-- K1. Commitment rank: how much a claim assumes beyond distinction itself.
  43`deltaOnly` is the floor (forced by distinction and finite repetition alone);
  44each later tag adds a strictly stronger commitment. The ranks make the
  45"Strength Ledger" an actual ordered ledger, not a flat set of labels. -/
  46def StrengthTag.rank : StrengthTag → ℕ
  47  | deltaOnly => 0
  48  | traceClosure => 1
  49  | choice => 2
  50  | powerComprehension => 3
  51  | classicalExtension => 4
  52
  53/-- A claim at tag `a` is no stronger than one at tag `b` when its commitment
  54rank does not exceed `b`'s. -/
  55def StrengthTag.le (a b : StrengthTag) : Prop := a.rank ≤ b.rank
  56
  57/-- Strict commitment order on strength tags. -/
  58def StrengthTag.lt (a b : StrengthTag) : Prop := a.rank < b.rank
  59
  60instance : LE StrengthTag := ⟨StrengthTag.le⟩
  61instance : LT StrengthTag := ⟨StrengthTag.lt⟩
  62
  63instance (a b : StrengthTag) : Decidable (a ≤ b) :=
  64  decidable_of_iff (a.rank ≤ b.rank) Iff.rfl
  65
  66instance (a b : StrengthTag) : Decidable (a < b) :=
  67  decidable_of_iff (a.rank < b.rank) Iff.rfl
  68
  69/-- The commitment rank is injective: distinct tags carry distinct ranks, so
  70the ledger order is a genuine (anti-symmetric) order, not a preorder collapse. -/
  71theorem StrengthTag.rank_injective : Function.Injective StrengthTag.rank := by
  72  intro a b h
  73  cases a <;> cases b <;> simp_all [StrengthTag.rank]
  74
  75/-- K1 ledger order, exact: the five strength tags form the strict commitment
  76chain `deltaOnly < traceClosure < choice < powerComprehension <
  77classicalExtension`. This is the ordering the "Strength Ledger" anchor names. -/
  78theorem StrengthTag.strict_chain :
  79    StrengthTag.deltaOnly < StrengthTag.traceClosure ∧
  80    StrengthTag.traceClosure < StrengthTag.choice ∧
  81    StrengthTag.choice < StrengthTag.powerComprehension ∧
  82    StrengthTag.powerComprehension < StrengthTag.classicalExtension := by
  83  refine ⟨?_, ?_, ?_, ?_⟩ <;> decide
  84
  85/-- The completion stratum (`traceClosure`) is a strictly stronger commitment
  86than the δ-only floor. This is the exact, type-level statement of the program's
  87central honesty claim: moving from the δ-native carrier to the continuous
  88completion is a real strengthening, not a free step. -/
  89theorem StrengthTag.deltaOnly_lt_traceClosure :
  90    StrengthTag.deltaOnly < StrengthTag.traceClosure := by
  91  decide
  92
  93/-- K1 audit sanity: the δ-only tag is not the trace-closure tag. -/
  94theorem deltaOnly_ne_traceClosure :
  95    StrengthTag.deltaOnly ≠ StrengthTag.traceClosure := by
  96  decide
  97
  98/-- K1 audit sanity: choice is not a δ-only claim. -/
  99theorem choice_ne_deltaOnly :
 100    StrengthTag.choice ≠ StrengthTag.deltaOnly := by
 101  decide
 102
 103end PrimitiveRecognitionCalculus
 104end Foundation
 105end IndisputableMonolith
 106