IndisputableMonolith.Gravity.Analysis.ClassicalSourceProjection

   1import IndisputableMonolith.Loom.Separation
   2
   3/-!
   4# Classical source projection for order-sensitive gravity
   5
   6Frozen world G0 of
   7`holography/plans/OrderSensitive_Gravity_Proposition_20260802.html`.
   8
   9A classical source projection is a typed reading of a Loom `Config` that is
  10allowed to stand in for the "conventional source" half of the discovery
  11discriminator. Only readings already proved equal on the gauge-separated
  12certificate pair may inhabit the interface at THEOREM grade. Identifying any
  13such reading with continuum stress-energy remains MODEL.
  14
  15## What is proved
  16
  17* Depth-one and abelianised projections equalize `cfgA`/`cfgB` (and
  18  `cfgC`/`cfgD`).
  19* Depth-two separates both pairs, so the classical-equal / recognition-unequal
  20  shape is inhabited.
  21* Additive / occupation-style bag readings (depth one) are blind: decoy D2.
  22
  23## Honesty
  24
  25* THEOREM: the equalities and separations below, by reduction to
  26  `Loom.Certificate.depth_one_is_blind`, `abelianised_is_blind`,
  27  `depth_two_separates` and their cfgC/cfgD siblings.
  28* MODEL: any claim that these projections are physical `T_{μν}`.
  29* Not claimed: a continuum Einstein equation, a seating into Fin 16, or that
  30  the depth-two residue is gravitational.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Gravity
  35namespace Analysis
  36namespace ClassicalSourceProjection
  37
  38open IndisputableMonolith.Loom
  39open IndisputableMonolith.Loom.Certificate
  40
  41/-- A typed classical-source interface on Loom configurations.
  42
  43`source` extracts the classical reading. `Equal` is the equality relation used
  44by the discovery gate (propositional equality on the carrier is the default).
  45`factorsThroughAbelian` records whether the reading ignores depth-two content.
  46Physical stress-energy identification is never a field of this structure. -/
  47structure SourceProjection (Source : Type) where
  48  source : Config → Source
  49  Equal : Source → Source → Prop
  50  factorsThroughAbelian : Bool
  51  nontrivial : ∃ c₁ c₂ : Config, ¬ Equal (source c₁) (source c₂)
  52
  53/-- Depth-one (loop-by-loop / amplitude bag) projection. -/
  54def depthOneSource (c : Config) : List Nat :=
  55  (invariant base c).1
  56
  57/-- Depth-two (commutator / pair-trace) reading. Not a classical source; the
  58recognition residual the campaign asks about. -/
  59def depthTwoReading (c : Config) : List Nat :=
  60  (invariant base c).2
  61
  62/-- Abelianised bag-of-relations projection. -/
  63def abelianSource (c : Config) : List (List Int) :=
  64  abelBag c
  65
  66/-- Depth-one projection as a classical source interface. -/
  67def DepthOneProjection : SourceProjection (List Nat) where
  68  source := depthOneSource
  69  Equal := (· = ·)
  70  factorsThroughAbelian := true
  71  nontrivial := by
  72    refine ⟨cfgA, [], ?_⟩
  73    decide
  74
  75/-- Abelianised projection as a classical source interface. -/
  76def AbelianProjection : SourceProjection (List (List Int)) where
  77  source := abelianSource
  78  Equal := (· = ·)
  79  factorsThroughAbelian := true
  80  nontrivial := by
  81    refine ⟨cfgA, [], ?_⟩
  82    decide
  83
  84/-! ## G0 on the discovery pair -/
  85
  86/-- **G0, depth one.** Classical depth-one sources of `cfgA` and `cfgB` agree. -/
  87theorem depthOne_equal_cfgAB :
  88    DepthOneProjection.Equal (DepthOneProjection.source cfgA)
  89      (DepthOneProjection.source cfgB) :=
  90  depth_one_is_blind
  91
  92/-- **G0, abelian.** Classical abelianised sources of `cfgA` and `cfgB` agree. -/
  93theorem abelian_equal_cfgAB :
  94    AbelianProjection.Equal (AbelianProjection.source cfgA)
  95      (AbelianProjection.source cfgB) :=
  96  abelianised_is_blind
  97
  98/-- Recognition depth-two reading separates the discovery pair. -/
  99theorem depthTwo_separates_cfgAB :
 100    depthTwoReading cfgA ≠ depthTwoReading cfgB :=
 101  depth_two_separates
 102
 103/-- Second discovery pair: depth-one equal. -/
 104theorem depthOne_equal_cfgCD :
 105    DepthOneProjection.Equal (DepthOneProjection.source cfgC)
 106      (DepthOneProjection.source cfgD) :=
 107  depth_one_is_blind2
 108
 109/-- Second discovery pair: abelian equal. -/
 110theorem abelian_equal_cfgCD :
 111    AbelianProjection.Equal (AbelianProjection.source cfgC)
 112      (AbelianProjection.source cfgD) :=
 113  abelianised_is_blind2
 114
 115/-- Second discovery pair: depth-two separates. -/
 116theorem depthTwo_separates_cfgCD :
 117    depthTwoReading cfgC ≠ depthTwoReading cfgD :=
 118  depth_two_separates2
 119
 120/-- **Decoy D2.** Any reading that factors as the depth-one bag is blind on the
 121discovery pair. Instantiated at the depth-one projection itself. -/
 122theorem decoy_depthOne_blind_on_discovery :
 123    depthOneSource cfgA = depthOneSource cfgB :=
 124  depth_one_is_blind
 125
 126/-- **Decoy D2 (abelian).** The unique abelianised bag reading is blind. -/
 127theorem decoy_abelian_blind_on_discovery :
 128    abelianSource cfgA = abelianSource cfgB :=
 129  abelianised_is_blind
 130
 131/-- Composite certificate: classical equal and recognition unequal. -/
 132theorem classicalEqual_recognitionUnequal_cfgAB :
 133    depthOneSource cfgA = depthOneSource cfgB ∧
 134      abelianSource cfgA = abelianSource cfgB ∧
 135      depthTwoReading cfgA ≠ depthTwoReading cfgB :=
 136  ⟨depth_one_is_blind, abelianised_is_blind, depth_two_separates⟩
 137
 138end ClassicalSourceProjection
 139end Analysis
 140end Gravity
 141end IndisputableMonolith
 142