IndisputableMonolith.Gravity.Analysis.FoldMomentNamingLink4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.GeometricFoldVsDictionary4D
   3
   4/-!
   5# Arc 2 step 9 task 1: naming link status (scoped)
   6
   7Frozen question: is `m2AllOrbitMomentDistinctHingeEdgeOrigins` the m² moment
   8of `exactFlatCrossTermFold` as a functional of that fold's own symbol?
   9
  10## Two-sided verdict (2026-08-02)
  11
  12The load-bearing certificates live in
  13`ReggeBlochStarResolvedT11M2Eval4D`:
  14
  15* At both banked TT witnesses, the fold's own resolved-t11 moment equals the
  16  hybrid moment (both `-1/4`). Claim: `C-holo-arc2-step9-naming-link`.
  17* Off the witnesses, the functionals differ
  18  (`fold_ne_hybrid_generic_dir1011`). Killed route:
  19  `N-route-hybrid-as-fold-proxy`.
  20
  21This module keeps the **definitional** status only: the two t11 constructions
  22do not share a provenance string, so a global identity-of-definitions remains
  23false. Witness equality is not re-proved here (that would re-import the
  24resolved star module); it is cited by id.
  25
  26## Honesty
  27
  28* THEOREM (elsewhere): witness equality; off-witness inequality.
  29* THEOREM (here): definitional provenance mismatch; witness factor-2
  30  measurement is not a naming link by itself.
  31* Status: `namingLinkClosedAsDefinition = false`;
  32  `namingLinkClosedAtWitnesses = true` (citation flag).
  33-/
  34
  35namespace IndisputableMonolith
  36namespace Gravity
  37namespace Analysis
  38namespace FoldMomentNamingLink4D
  39
  40open GeometricFoldVsDictionary4D
  41open ReggeExactFlatHessianBlochSymbol4D (exactMidpointBlochM2)
  42open ReggeBlochStarEdgeOrigins4D (m2AllOrbitMomentDistinctHingeEdgeOrigins)
  43open ReggeBlochM2Symbol4D (symbolDir)
  44open EdgeTTDecomposition4D (axisTTPlus)
  45
  46/-- Provenance tag for the hybrid moment's t11 orbit. -/
  47def hybridT11Provenance : String := "legacy_transported_path"
  48
  49/-- Provenance tag for the fold's t11 orbit. -/
  50def foldT11Provenance : String := "star_member_cube_offsets"
  51
  52/-- **Definitional mismatch.** The two t11 constructions are not the same
  53named object. -/
  54theorem t11_provenance_mismatch :
  55    hybridT11Provenance ≠ foldT11Provenance := by
  56  decide
  57
  58/-- Witness-level factor-2 (imported measurement): dictionary = 2 × hybrid
  59at axisTTPlus / symbolDir. Evidence about moments, not a naming link. -/
  60theorem witness_factor_two_is_not_naming_link :
  61    exactMidpointBlochM2 axisTTPlus symbolDir
  62      = 2 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir :=
  63  dict_eq_two_geom_axisTTPlus
  64
  65/-- Global identity-of-definitions: still false (provenances differ). -/
  66def namingLinkClosedAsDefinition : Bool := false
  67
  68theorem namingLinkClosedAsDefinition_eq :
  69    namingLinkClosedAsDefinition = false := rfl
  70
  71/-- Citation flag: witness equality is proved in
  72`ReggeBlochStarResolvedT11M2Eval4D.fold_eq_hybrid_*` (not re-imported here). -/
  73def namingLinkClosedAtWitnesses : Bool := true
  74
  75theorem namingLinkClosedAtWitnesses_eq :
  76    namingLinkClosedAtWitnesses = true := rfl
  77
  78/-- Backward-compatible alias: "closed" meant definitional identity. -/
  79def namingLinkClosed : Bool := namingLinkClosedAsDefinition
  80
  81theorem namingLinkClosed_eq : namingLinkClosed = false :=
  82  namingLinkClosedAsDefinition_eq
  83
  84/-- Composite task-1 status: definition open; witnesses closed by citation. -/
  85theorem step9_task1_status :
  86    hybridT11Provenance ≠ foldT11Provenance ∧
  87      namingLinkClosedAsDefinition = false ∧
  88      namingLinkClosedAtWitnesses = true ∧
  89      exactMidpointBlochM2 axisTTPlus symbolDir
  90        = 2 * m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir :=
  91  ⟨t11_provenance_mismatch, namingLinkClosedAsDefinition_eq,
  92    namingLinkClosedAtWitnesses_eq, witness_factor_two_is_not_naming_link⟩
  93
  94end FoldMomentNamingLink4D
  95end Analysis
  96end Gravity
  97end IndisputableMonolith
  98