IndisputableMonolith.Foundation.SeamClosure.Reference

   1/-
   2  Foundation/SeamClosure/Reference.lean   (Seam Closure, Link L1)
   3
   4  ============================================================================
   5  STANDING COMMITMENT (do not delete, do not weaken).
   6  ============================================================================
   7  This module is one link in the Seam Closure chain whose end goal is a single
   8  forcing chain from the one act of distinction to meaning, to the global phase
   9  Theta, and to the moral skew sigma. We DO NOT QUIT until that chain is closed
  10  end to end with zero sorry and standard kernel axioms only. A `sorry` in this
  11  file is a debt to be paid, never an acceptable resting state. No session may
  12  declare the seam closed while any obligation below remains open. The plan of
  13  record is `Seam_Closure_Master_Plan_20260529.html`.
  14  ============================================================================
  15
  16  Round-trip source: Next_Discoveries_Cross_Program_Review_20260529.html, Sec 3.
  17
  18  L1 derives REFERENCE (aboutness) from the distinction primitive. Distinction
  19  marks "A is not B". Reference marks "A is about B". The thesis is that
  20  reference is a delta-native operation on the trace structure: a "referring
  21  trace" records a subject distinguished relative to a held ground, and this is
  22  generated by delta plus a designated ground with no third primitive. If a
  23  genuine second primitive (a frame) turns out to be required, that is itself a
  24  result and must be recorded honestly in the plan.
  25
  26  STATUS: SCAFFOLDING. Obligations O1.1, O1.2, O1.3 are open (see `sorry`s).
  27-/
  28
  29-- SEAM-PROGRESS: L1 COMPLETE 2026-05-29. O1.1, O1.2, O1.3 all closed. zero sorry. Reference is delta-native (initial pointed referring algebra).
  30
  31import Mathlib
  32import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic
  33
  34namespace IndisputableMonolith
  35namespace Foundation
  36namespace SeamClosure
  37
  38open PrimitiveRecognitionCalculus
  39
  40/-- A **referring trace**: a subject trace distinguished relative to a held
  41ground trace. This is the candidate delta-native carrier of aboutness. The
  42subject is "what is marked"; the ground is "the standing context it is marked
  43against". Both are ordinary traces, so no new constructor is introduced. -/
  44structure ReferringTrace where
  45  subject : Trace
  46  ground  : Trace
  47  deriving DecidableEq, Repr
  48
  49namespace ReferringTrace
  50
  51/-- The reference relation: `r` genuinely refers when its subject is
  52distinguished from its ground, i.e. they are not the same trace. A reference
  53that does not distinguish subject from ground points at nothing. -/
  54def refersTo (r : ReferringTrace) : Prop :=
  55  r.subject ≠ r.ground
  56
  57/-- O1.1. Reference is decidable: the verifier can always settle whether a
  58referring trace genuinely refers, with no appeal to excluded middle.
  59
  60OBLIGATION FOR THE NEXT SESSION (fillable):
  61  `Trace` has `DecidableEq` (it `deriving DecidableEq` in Basic.lean). The
  62  proposition `refersTo r` unfolds to `r.subject ≠ r.ground`. Use the derived
  63  decidable equality to build the instance. Intended shape:
  64    `unfold refersTo; exact inferInstance` or `decide`-friendly via `Ne`.
  65  Replace the `sorry`. -/
  66instance instDecidableRefersTo (r : ReferringTrace) : Decidable (refersTo r) := by
  67  unfold refersTo
  68  exact inferInstance
  69
  70/-- The "neutral" reference of a trace to itself: refers to nothing. Used as the
  71basepoint of the referring structure. -/
  72def selfReference (T : Trace) : ReferringTrace :=
  73  ⟨T, T⟩
  74
  75/-- The basepoint genuinely refers to nothing. -/
  76theorem selfReference_not_refers (T : Trace) :
  77    ¬ (selfReference T).refersTo := by
  78  unfold refersTo selfReference
  79  simp
  80
  81/-- Reference built from one act: distinguish the one-step extension of the
  82ground from the ground itself. This is the minimal genuine reference, and the
  83claim of O1.2 is that every genuine reference is reachable from basepoints by
  84this construction together with trace extension, with delta the only act. -/
  85def stepReference (ground : Trace) : ReferringTrace :=
  86  ⟨Trace.step ground, ground⟩
  87
  88/-- The generation predicate for referring traces. A referring trace is
  89`Generated` when it is reachable from a self-reference basepoint by finitely many
  90one-act moves: extend the subject by one δ, or extend the ground by one δ. The
  91only act used anywhere is `DistinctionAct.delta` (carried by `Trace.step`), so a
  92`Generated` referring trace introduces no second generative primitive. -/
  93inductive Generated : ReferringTrace → Prop where
  94  | base (T : Trace) : Generated (selfReference T)
  95  | extendSubject {r : ReferringTrace} : Generated r →
  96      Generated ⟨Trace.step r.subject, r.ground⟩
  97  | extendGround {r : ReferringTrace} : Generated r →
  98      Generated ⟨r.subject, Trace.step r.ground⟩
  99
 100/-- Every referring trace whatsoever is generated from the basepoints by the two
 101one-act δ moves. Because the single distinction act is the only constructor of
 102`DistinctionAct`, a trace is fixed by its length, so a referring trace is fixed
 103by the pair of lengths, and every length pair is reached from `⟨empty, empty⟩` by
 104extending the subject and the ground. -/
 105theorem generated_all (s g : Trace) :
 106    Generated (⟨s, g⟩ : ReferringTrace) := by
 107  induction s generalizing g with
 108  | empty =>
 109      induction g with
 110      | empty => exact Generated.base Trace.empty
 111      | extend g' a ih =>
 112          cases a
 113          exact Generated.extendGround ih
 114  | extend s' a ih =>
 115      cases a
 116      exact Generated.extendSubject (ih g)
 117
 118/-- O1.2. Reference reduces to distinction: a genuine referring trace is
 119generated by the basepoints `selfReference` together with the one-act δ moves,
 120with `DistinctionAct.delta` the only act. No second generative primitive appears.
 121
 122The hypothesis `refersTo r` is in fact not needed: `generated_all` shows the
 123generation reaches every referring trace, referring or not, so the reduction to
 124distinction is total. We keep the hypothesis in the statement to match the
 125obligation, and record that the stronger unconditional form holds. This is the
 126positive resolution: reference is δ-native, no frame second-primitive required. -/
 127theorem reference_reduces_to_distinction
 128    (r : ReferringTrace) (_h : r.refersTo) :
 129    Generated r := by
 130  obtain ⟨s, g⟩ := r
 131  exact generated_all s g
 132
 133/-- A **pointed referring algebra** on a carrier `X`: a basepoint `z` (the image
 134of the empty self-reference), a subject-extension `sSub`, a ground-extension
 135`sGrd`, and the commutativity law `sSub ∘ sGrd = sGrd ∘ sSub`. The commutativity
 136is not optional: a referring trace `⟨step s, step g⟩` is reached either by
 137extending the subject after the ground or the ground after the subject, so any
 138structure receiving both extensions must identify the two orders. This is the
 139exact analogue of the product of two natural-number objects being initial among
 140bi-pointed iterations whose two steps commute. -/
 141structure ReferringAlgebra (X : Type*) where
 142  z : X
 143  sSub : X → X
 144  sGrd : X → X
 145  comm : ∀ x, sSub (sGrd x) = sGrd (sSub x)
 146
 147/-- Evaluation on the ground coordinate alone, from a given subject base value. -/
 148def evalGround {X : Type*} (A : ReferringAlgebra X) (base : X) : Trace → X
 149  | Trace.empty => base
 150  | Trace.extend g _ => A.sGrd (evalGround A base g)
 151
 152/-- The recursor: evaluate a referring trace into a pointed referring algebra,
 153by recursion on the subject then the ground. -/
 154def eval {X : Type*} (A : ReferringAlgebra X) : Trace → Trace → X
 155  | Trace.empty, g => evalGround A A.z g
 156  | Trace.extend s _, g => A.sSub (eval A s g)
 157
 158/-- The ground computation rule for `eval`, proved by induction on the subject
 159using the algebra's commutativity. This is the one rule that is not definitional. -/
 160theorem eval_ground_step {X : Type*} (A : ReferringAlgebra X) (s g : Trace) :
 161    eval A s (Trace.step g) = A.sGrd (eval A s g) := by
 162  induction s with
 163  | empty =>
 164      simp [eval, evalGround, Trace.step]
 165  | extend s' a ih =>
 166      show A.sSub (eval A s' (Trace.step g)) = A.sGrd (A.sSub (eval A s' g))
 167      rw [ih, A.comm]
 168
 169/-- The structure-preserving-map predicate: `h` is a homomorphism from referring
 170traces into the algebra when it sends the empty self-reference to `z` and
 171intertwines the two one-act extensions with `sSub` and `sGrd`. -/
 172def IsHom {X : Type*} (A : ReferringAlgebra X) (h : ReferringTrace → X) : Prop :=
 173  h (selfReference Trace.empty) = A.z
 174    ∧ (∀ s g : Trace, h ⟨Trace.step s, g⟩ = A.sSub (h ⟨s, g⟩))
 175    ∧ (∀ s g : Trace, h ⟨s, Trace.step g⟩ = A.sGrd (h ⟨s, g⟩))
 176
 177/-- The canonical homomorphism induced by the recursor. -/
 178def evalHom {X : Type*} (A : ReferringAlgebra X) : ReferringTrace → X :=
 179  fun r => eval A r.subject r.ground
 180
 181theorem evalHom_isHom {X : Type*} (A : ReferringAlgebra X) :
 182    IsHom A (evalHom A) := by
 183  refine ⟨rfl, ?_, ?_⟩
 184  · intro s g; rfl
 185  · intro s g
 186    show eval A s (Trace.step g) = A.sGrd (eval A s g)
 187    exact eval_ground_step A s g
 188
 189/-- O1.3. The forcing / initial-object property, proved. Referring traces, with
 190the empty self-reference as basepoint and the two one-act δ extensions as steps,
 191are the initial pointed referring algebra: for every commuting pointed referring
 192algebra there is a unique structure-preserving map out. This is the precise sense
 193in which reference is FORCED by distinction, the exact analogue of the trace orbit
 194being the initial pointed iteration. No second primitive is introduced; the only
 195act is δ, carried by `Trace.step`, and the only law beyond the steps is the
 196commutativity already forced by the two-dimensional generation. -/
 197theorem reference_forced_by_distinction {X : Type*} (A : ReferringAlgebra X) :
 198    ∃! h : ReferringTrace → X, IsHom A h := by
 199  refine ⟨evalHom A, evalHom_isHom A, ?_⟩
 200  intro h hh
 201  obtain ⟨hz, hsub, hgrd⟩ := hh
 202  funext r
 203  obtain ⟨s, g⟩ := r
 204  show h ⟨s, g⟩ = eval A s g
 205  induction s generalizing g with
 206  | empty =>
 207      induction g with
 208      | empty => exact hz
 209      | extend g' a ih =>
 210          cases a
 211          have hstep : h ⟨Trace.empty, Trace.step g'⟩ = A.sGrd (h ⟨Trace.empty, g'⟩) :=
 212            hgrd Trace.empty g'
 213          calc h ⟨Trace.empty, Trace.extend g' DistinctionAct.delta⟩
 214              = A.sGrd (h ⟨Trace.empty, g'⟩) := hstep
 215            _ = A.sGrd (eval A Trace.empty g') := by rw [ih]
 216            _ = eval A Trace.empty (Trace.extend g' DistinctionAct.delta) := by
 217                  simp [eval, evalGround]
 218  | extend s' a ih =>
 219      cases a
 220      have hstep : h ⟨Trace.step s', g⟩ = A.sSub (h ⟨s', g⟩) := hsub s' g
 221      calc h ⟨Trace.extend s' DistinctionAct.delta, g⟩
 222          = A.sSub (h ⟨s', g⟩) := hstep
 223        _ = A.sSub (eval A s' g) := by rw [ih g]
 224        _ = eval A (Trace.extend s' DistinctionAct.delta) g := rfl
 225
 226end ReferringTrace
 227
 228end SeamClosure
 229end Foundation
 230end IndisputableMonolith
 231