IndisputableMonolith.Holography.EightTickSubperiodExclusion

   1import Mathlib
   2import IndisputableMonolith.Holography.PixelLocal
   3
   4/-!
   5# EightTickSubperiodExclusion: no proper divisor of 8 realizes the admissible census
   6
   7LEG-B of the Bekenstein-Hawking coefficient program (panel directive 2026-07-02,
   8`plans/RS_Bekenstein_Quarter_Master_Plan_20260701.html`) needs the DISCRETE half of
   9the deficit-free-period argument: the Euclidean period of the analytically continued
  10recognition cycle is the FULL 8-tick turn (hence one full `2π`), not a proper
  11sub-multiple (a conical deficit). The continuum half is the KMS window lemma
  12(`legb_kms_window_unique`, loop-owned). This module supplies the discrete half as a
  13kernel-`decide` enumeration on the forced substrate.
  14
  15## The statement
  16
  17Work on the boundary plaquette configurations `FaceCfg = Fin 16` of
  18`Holography.PixelLocal` (one recognition bit per vertex of a cube face). A
  19recognition walk advances by single-bit flips (one vertex posting per tick, the
  20Gray-code discipline of the 8-tick cube traversal, `Patterns.period_exactly_8`).
  21A walk of length `d` is *closed* when it returns to its starting configuration,
  22and *census-complete* when it visits at least one representative of each of the
  23four admissible ledger-closed sectors of `PixelLocal.admissibleSectors_eq`
  24(the `D₄`-orbits `{0}`, `{3,6,12,9}`, `{5,10}`, `{15}`).
  25
  26**THEOREM (axiom-clean, by `decide`).** For every proper divisor `d ∈ {1, 2, 4}`
  27of 8, NO closed length-`d` flip walk is census-complete; and a closed length-8
  28flip walk that is census-complete EXISTS (witness: flips `[0,1,2,3,0,2,1,3]` from
  29`0000`, visiting `0 → 1 → 3 → 7 → 15 → 14 → 10 → 8 → 0`, which meets all four
  30orbits at `0, 3, 10, 15`).
  31
  32The obstruction for `d ∈ {1,2}` is cardinality (a closed 1- or 2-walk visits at
  33most 2 distinct configurations, but 4 orbits must be met); for `d = 4` it is
  34parity (bit-flip steps alternate the parity of the popcount, so a closed 4-walk
  35visits at most 2 distinct even-parity configurations, again short of the 4 orbits;
  36the full enumeration over all 16 × 4⁴ = 4096 walks is what `decide` checks).
  37
  38## What this proves for LEG-B, and what it does not (honest scope)
  39
  40THEOREM: the minimal closed recognition walk that exhibits the complete admissible
  41sector census on the forced D=3 substrate has length exactly 8. A `d`-shift-invariant
  42counting with `d | 8`, `d < 8` cannot see all four sectors, so identifying ticks
  43modulo a proper divisor of 8 (the discrete analog of a conical deficit `2π/n`)
  44destroys the admissible census. Combined with `legb_eight_tick_circle_period`
  45(one full 8-tick cycle = one full `2π` turn of the continued clock), this forces
  46the census-preserving Euclidean period to be the FULL `2π/κ`, discretely.
  47
  48OPEN (not proved here): that the physical Euclidean continuation must PRESERVE the
  49census (the finite-J-cost / regularity condition at the horizon fixed point). That
  50is the B2 physics core, still owned by the derive captain. This module removes the
  51"which sub-period?" freedom once census preservation is granted; it does not grant it.
  52-/
  53
  54namespace IndisputableMonolith
  55namespace Holography
  56namespace EightTickSubperiodExclusion
  57
  58open PixelLocal
  59
  60/-- One recognition tick on a boundary plaquette: flip the bit of vertex `i`
  61(one vertex posting per tick, the Gray-code step of the 8-tick traversal). -/
  62def flip (c : FaceCfg) (i : Fin 4) : FaceCfg :=
  63  ⟨(c.val ^^^ (1 <<< i.val)) % 16, Nat.mod_lt _ (by decide)⟩
  64
  65/-- The endpoint of a flip walk from `s` through the tick sequence `fs`. -/
  66def walkEnd : FaceCfg → List (Fin 4) → FaceCfg
  67  | s, [] => s
  68  | s, i :: fs => walkEnd (flip s i) fs
  69
  70/-- Every configuration a flip walk visits (including the start). -/
  71def walkVisits : FaceCfg → List (Fin 4) → List FaceCfg
  72  | s, [] => [s]
  73  | s, i :: fs => s :: walkVisits (flip s i) fs
  74
  75/-- The walk meets the given `D₄`-orbit (listed by its member values). -/
  76def hits (s : FaceCfg) (fs : List (Fin 4)) (orbit : List Nat) : Bool :=
  77  (walkVisits s fs).any fun c => orbit.contains c.val
  78
  79/-- Census completeness: the walk meets all four admissible ledger-closed sectors
  80of `PixelLocal.admissibleSectors_eq` (as full `D₄`-orbits: the empty loop `{0}`,
  81the adjacent-edge loops `{3,6,12,9}`, the diagonal loops `{5,10}`, and the full
  82loop `{15}`). -/
  83def censusComplete (s : FaceCfg) (fs : List (Fin 4)) : Bool :=
  84  hits s fs [0] && hits s fs [3, 6, 12, 9] && hits s fs [5, 10] && hits s fs [15]
  85
  86/-- **d = 1 excluded**: no closed 1-tick walk is census-complete (cardinality:
  87it visits at most 2 configurations; 4 orbits are required). -/
  88theorem no_subperiod_one :
  89    ∀ (s : FaceCfg) (fs : Fin 1 → Fin 4),
  90      walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false := by
  91  decide
  92
  93/-- **d = 2 excluded**: no closed 2-tick walk is census-complete (cardinality). -/
  94theorem no_subperiod_two :
  95    ∀ (s : FaceCfg) (fs : Fin 2 → Fin 4),
  96      walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false := by
  97  decide
  98
  99set_option maxRecDepth 4096 in
 100set_option maxHeartbeats 1600000 in
 101/-- **d = 4 excluded**: no closed 4-tick walk is census-complete. The mechanism is
 102parity: single-bit flips alternate popcount parity, so a closed 4-walk sees at most
 1032 distinct even-parity configurations, short of the 4 required orbits. The proof is
 104the full kernel enumeration of all 16 × 4⁴ = 4096 walks. -/
 105theorem no_subperiod_four :
 106    ∀ (s : FaceCfg) (fs : Fin 4 → Fin 4),
 107      walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false := by
 108  decide
 109
 110/-- **d = 8 realizes the census**: a closed 8-tick flip walk exhibiting all four
 111admissible sectors exists. Witness: from `0000`, flip vertices `0,1,2,3,0,2,1,3`,
 112visiting `0 → 1 → 3 → 7 → 15 → 14 → 10 → 8 → 0` (orbits met at `0, 3, 15, 10`). -/
 113theorem eight_tick_census_witness :
 114    ∃ (s : FaceCfg) (fs : Fin 8 → Fin 4),
 115      walkEnd s (List.ofFn fs) = s ∧ censusComplete s (List.ofFn fs) = true := by
 116  exact ⟨0, ![0, 1, 2, 3, 0, 2, 1, 3], by decide, by decide⟩
 117
 118/-- **The subperiod-exclusion capstone**: among the divisors of 8, the census-complete
 119closed walk lengths begin exactly at 8. Every proper divisor fails; 8 succeeds. This
 120is the discrete deficit-free-period statement: identifying the recognition cycle
 121modulo a proper divisor of 8 (the discrete conical deficit `2π/n`) destroys the
 122admissible sector census, so the census-preserving period is the full 8-tick turn. -/
 123theorem minimal_census_period_eight :
 124    (∀ (s : FaceCfg) (fs : Fin 1 → Fin 4),
 125        walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false) ∧
 126    (∀ (s : FaceCfg) (fs : Fin 2 → Fin 4),
 127        walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false) ∧
 128    (∀ (s : FaceCfg) (fs : Fin 4 → Fin 4),
 129        walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false) ∧
 130    (∃ (s : FaceCfg) (fs : Fin 8 → Fin 4),
 131        walkEnd s (List.ofFn fs) = s ∧ censusComplete s (List.ofFn fs) = true) :=
 132  ⟨no_subperiod_one, no_subperiod_two, no_subperiod_four, eight_tick_census_witness⟩
 133
 134end EightTickSubperiodExclusion
 135end Holography
 136end IndisputableMonolith
 137