IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.GoalClosure

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/GoalClosure.lean
   3
   4  D4 closure ledger for the factorization plan. The transform now exists in two
   5  theorem-level forms: classical transport of `Nat.primeFactorsList`, and a
   6  native noncomputable δ-choice transform by prime/factorization descent.
   7-/
   8
   9import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PrimeCoordinateTransform
  10
  11namespace IndisputableMonolith
  12namespace Foundation
  13namespace PrimitiveRecognitionCalculus
  14namespace Factorization
  15
  16open DistinctionNat
  17
  18/-- The residual names allowed at the D4 finish line. -/
  19inductive PrimeCoordinateResidualName : Type
  20  | primeCoordinateReadout
  21  | characterSpectrumReadout
  22  | physicalPeriodReadout
  23  | classicalFactorizationTransport
  24deriving DecidableEq, Repr
  25
  26/-- Current residual label retained for historical compatibility. The
  27commitment it names is closed below by the native-choice transform. -/
  28def currentPrimeCoordinateResidual : PrimeCoordinateResidualName :=
  29  .primeCoordinateReadout
  30
  31/-- The original D4 commitment. Supplying this is exactly supplying the
  32δ-prime-coordinate transform, not a weaker benchmark or heuristic. It is now
  33closed by `deltaPrimeCoordinateTransform_classicalTransport`. -/
  34def PrimeCoordinateReadoutCommitment : Prop :=
  35  Nonempty DeltaPrimeCoordinateTransform
  36
  37/-- Provenance of the currently closed transform. -/
  38inductive PrimeCoordinateTransformProvenance : Type
  39  | classicalFactorizationTransport
  40  | nativeDeltaReadout
  41deriving DecidableEq, Repr
  42
  43/-- Current transform provenance: native δ choice by prime/factorization
  44descent. -/
  45def currentPrimeCoordinateTransformProvenance :
  46    PrimeCoordinateTransformProvenance :=
  47  .nativeDeltaReadout
  48
  49theorem current_residual_named :
  50    currentPrimeCoordinateResidual = .primeCoordinateReadout := rfl
  51
  52theorem primeCoordinateReadoutCommitment_exact :
  53    PrimeCoordinateReadoutCommitment ↔ Nonempty DeltaPrimeCoordinateTransform := by
  54  rfl
  55
  56/-- The commitment is closed in the theorem-ledger sense by the native-choice
  57transform. -/
  58theorem primeCoordinateReadoutCommitment_closed :
  59    PrimeCoordinateReadoutCommitment :=
  60  deltaPrimeCoordinateTransform_nativeChoice_exists
  61
  62theorem current_transform_provenance :
  63    currentPrimeCoordinateTransformProvenance =
  64      .nativeDeltaReadout := rfl
  65
  66/-- If the named residual commitment is supplied, factor recovery is immediate.
  67This is the theorem-level content of "solving becomes coordinate readout." -/
  68theorem primeCoordinateReadoutCommitment_recovers_prime_divisor
  69    (h : PrimeCoordinateReadoutCommitment) :
  70    ∀ N : DistinctionNat, N ≠ zero → ¬ unit N →
  71      ∃ p : DistinctionNat, primeOrbit p ∧ divides p N := by
  72  rcases h with ⟨T⟩
  73  exact deltaPrimeCoordinateTransform_recovers_prime_divisor T
  74
  75/-- D4 closure certificate. It records that factor recovery is closed by a
  76native noncomputable δ-choice transform; classical transport remains a separate
  77proved path in `PrimeCoordinateTransformCertificate`. -/
  78structure GoalClosureCertificate : Prop where
  79  residual_named :
  80    currentPrimeCoordinateResidual = .primeCoordinateReadout
  81  transform_provenance :
  82    currentPrimeCoordinateTransformProvenance =
  83      .nativeDeltaReadout
  84  residual_exact :
  85    PrimeCoordinateReadoutCommitment ↔ Nonempty DeltaPrimeCoordinateTransform
  86  residual_closed :
  87    PrimeCoordinateReadoutCommitment
  88  residual_would_recover :
  89    PrimeCoordinateReadoutCommitment →
  90      ∀ N : DistinctionNat, N ≠ zero → ¬ unit N →
  91        ∃ p : DistinctionNat, primeOrbit p ∧ divides p N
  92
  93theorem goal_closure_certificate : GoalClosureCertificate where
  94  residual_named := current_residual_named
  95  transform_provenance := current_transform_provenance
  96  residual_exact := primeCoordinateReadoutCommitment_exact
  97  residual_closed := primeCoordinateReadoutCommitment_closed
  98  residual_would_recover := primeCoordinateReadoutCommitment_recovers_prime_divisor
  99
 100end Factorization
 101end PrimitiveRecognitionCalculus
 102end Foundation
 103end IndisputableMonolith
 104