IndisputableMonolith.Holography.EdgeSectorBridge

   1import Mathlib.Data.Fin.VecNotation
   2import Mathlib.Data.Fintype.Pi
   3import Mathlib.Data.Finset.Card
   4import Mathlib.Data.Finset.Image
   5import IndisputableMonolith.Holography.PixelLocal
   6
   7/-!
   8# EdgeSectorBridge: sectors are a deterministic, lossy quotient of edge bits
   9
  10Panel verdict (`state/panel/sector_event_bridge_20260701_012004.json`, 2026-07-01, judge
  11Opus 4.8 over 5 directors + one debate round) on whether `SectorAreaQuantization` ("one
  12entropy quantum per area quantum per sector") is a real physical principle or secretly
  13derivable from the kernel: **neither.** It killed the sector-based reading of `4H`
  14outright (a 4-outcome label and a per-event entropy are not commensurable objects; see
  15`AccessCapacity.lean`'s own honesty discipline), and relocated the live candidate one
  16layer down, from the *sector* (a `D₄`-orbit label) to the *edge* (`PixelLocal.vbit`,
  17one of the 4 raw boundary bits before any quotient is taken).
  18
  19The panel named two cheap, decisive `decide`-checks to settle real content before any
  20measure-theoretic work on the harder "edge = independent T9 event" identification:
  21
  221. **Is a sector a deterministic function of the edge bits, with no independent
  23   information of its own?** If yes, `H + log 4` (entropy-per-event PLUS an independent
  24   `log 4` for "which sector") double-counts: the sector adds no information beyond
  25   what the edges already carry. Settled here: `sectorOf` is a computable, total
  26   function of the raw edge bits, and it hits every one of the 4 admissible sectors
  27   (`sectorOf_surjective_on_closed`), while the closed-edge substrate itself carries
  28   `log 8 = 3 log 2` and the sector carries only `log 4 = 2 log 2` — strictly less. The
  29   sector is a **lossy quotient** of the edges, never a free-standing degree of freedom.
  302. **Does the ledger-closure (parity) constraint leave exactly 3 free bits out of the
  31   raw 4, not 4?** This is the fact the live `4H` vs `3H` fork hinges on (a lone,
  32   undebated director found that if pixel area should track *realized* post-closure
  33   information rather than *raw pre-closure capacity*, the count is 3, not 4, and the
  34   headline coefficient is off by 4/3). Settled here: `closed_free_bits` proves the
  35   closed-configuration count is exactly `2³ = 8`, i.e. the parity constraint removes
  36   exactly one of the 4 raw bits' degrees of freedom.
  37
  38## Honest scope (do not overclaim)
  39
  40This module proves the two adjudicating COMBINATORIAL facts. It does **not** decide
  41whether the physically correct pixel-area formula is `4H` (pre-closure edge capacity)
  42or `3H` (post-closure realized information) — that is a physical question (which
  43substrate does `a_pix` actually attach to?) that these `decide`s only sharpen, they do
  44not resolve. It also does **not** prove "one edge = one independent T9 recognition
  45event": that identification is still an unformalized physical assertion, per the
  46judge's honesty check. What is now closed for good: `H + log 4` (additive, sector-only)
  47is dead, confirmed by direct construction rather than by informal argument alone.
  48
  49**Follow-on (2026-06-30/07-01):** a separate panel (`closure_fork_3h_vs_4h`) argued the
  50`3` here is the right count only for an ISOLATED, independently-closed pixel, and is the
  51wrong object for an ENTANGLING SURFACE. `EdgeCutTrace` proves that severing a single
  52GLOBAL closure constraint across a two-pixel cut restores the full `4` — but only on the
  53UNSHARED-edge model this file (and `PixelLocal`) already uses. `SharedEdgeCollapse` shows
  54that identical construction on a SHARED-vertex lattice (the physically natural picture for
  55adjacent horizon pixels) falls well short of `4` under either closure convention. The `3`
  56proved here therefore survives as the correct isolated/local count; whether `3`, `4`, or
  57something between `1` and `2.5` is the physically forced quantity for a horizon depends on
  58which of those two lattice models is correct, not resolved by this module.
  59-/
  60
  61namespace IndisputableMonolith
  62namespace Holography
  63namespace EdgeSectorBridge
  64
  65open PixelLocal
  66
  67/-- The ledger-closed boundary configurations: the 4 raw edge bits satisfying the
  68parity (ledger-closure) constraint, **before** any `D₄` quotient is taken. This is the
  69pre-closure edge substrate that the live `4H`/`3H` fork is about. -/
  70def closedConfigs : Finset FaceCfg := Finset.univ.filter (fun c => closed c = true)
  71
  72/-- **THEOREM (axiom-clean, by `decide`).** Exactly `8 = 2³` ledger-closed edge
  73configurations out of the 16 raw configurations: the parity constraint removes exactly
  74one of the 4 raw edge-bits' degrees of freedom. -/
  75theorem closed_configs_card : closedConfigs.card = 8 := by decide
  76
  77/-- **Restated as "3 free bits."** Ledger closure on 4 raw edge-bits leaves exactly 3
  78independent bits, not 4. This is the fact the `4H` vs `3H` live bet hinges on: if pixel
  79area tracks *realized* (post-closure) information, the count is 3; if it tracks *raw*
  80(pre-closure) capacity, the count is 4. -/
  81theorem closed_free_bits : closedConfigs.card = 2 ^ 3 := closed_configs_card
  82
  83/-- **The sector-of-edges map.** Every face configuration is sent to the numerically
  84least element of its `D₄`-orbit (its canonical sector representative, matching
  85`isSectorRep`'s own criterion). This is a **total, deterministic, computable function
  86of the raw edge bits alone** — sector identity is never an independently specified
  87label; it is read off the edges. -/
  88def sectorOf (c : FaceCfg) : FaceCfg :=
  89  (faceStabilizer.map (fun σ => actBy σ c)).foldr min c
  90
  91/-- **THEOREM (well-definedness, by `decide`).** `sectorOf` sends every ledger-closed
  92edge configuration into `admissibleSectors`: the canonical orbit representative of a
  93closed configuration is itself closed and is a sector representative. Closure is
  94`D₄`-invariant (permuting which vertex holds which bit does not change the XOR of the
  954 bits), verified here by exhaustive finite check rather than assumed. -/
  96theorem sectorOf_mem_admissibleSectors :
  97    ∀ c : FaceCfg, closed c = true → sectorOf c ∈ admissibleSectors := by decide
  98
  99/-- **THEOREM (surjectivity, by `decide`). Sectors carry no information beyond the
 100edge bits.** Every one of the 4 admissible sectors is hit by `sectorOf` from some
 101ledger-closed edge configuration. Combined with `sectorOf_mem_admissibleSectors`, this
 102proves `admissibleSectors` is exactly the image of `closedConfigs` under a
 103deterministic quotient map — a sector is a *projection* of the edges, never an
 104independent quantity added on top of them. -/
 105theorem sectorOf_surjective_on_closed :
 106    admissibleSectors ⊆ closedConfigs.image sectorOf := by decide
 107
 108/-- **The double-count kill (by `decide`).** The closed-edge substrate carries `log 8`
 109of information; the sector quotient carries only `log 4`, exactly half. Since sector
 110identity is entirely recoverable from (a strict compression of) the edge bits, adding
 111an independent `log 4` term on top of a per-edge entropy `H` double-counts information
 112the edges already contain. This is the precise combinatorial content behind killing
 113`H + log 4` as a candidate area law: `admissibleSectors` is a 2-to-1 lossy quotient of
 114`closedConfigs`, not a free-standing degree of freedom. -/
 115theorem sector_is_lossy_quotient_of_closed :
 116    admissibleSectors.card * 2 = closedConfigs.card := by decide
 117
 118/-- **The edge-sector-bridge certificate.** Bundles the two panel-adjudicating facts:
 119the ledger-closure constraint leaves exactly 3 free edge-bits (not 4), and the sector
 120label is a well-defined, surjective, exactly-2-to-1 lossy quotient of the closed edge
 121configurations. This is what settles "is `SectorAreaQuantization` a real physical
 122principle or a conflation" in the negative: the sector adds no independent information
 123beyond the edges, so `H + log 4` (treating the sector as a free-standing degree of
 124freedom) double-counts, and the live candidates move to the edge substrate itself
 125(`4H`, pre-closure capacity) or its closure-reduced form (`3H`, post-closure realized
 126information) — neither of which this certificate decides. -/
 127structure EdgeSectorBridgeCert : Prop where
 128  free_bits_three : closedConfigs.card = 2 ^ 3
 129  sector_well_defined : ∀ c : FaceCfg, closed c = true → sectorOf c ∈ admissibleSectors
 130  sector_surjective : admissibleSectors ⊆ closedConfigs.image sectorOf
 131  sector_lossy_two_to_one : admissibleSectors.card * 2 = closedConfigs.card
 132
 133theorem edgeSectorBridgeCert : EdgeSectorBridgeCert where
 134  free_bits_three := closed_free_bits
 135  sector_well_defined := sectorOf_mem_admissibleSectors
 136  sector_surjective := sectorOf_surjective_on_closed
 137  sector_lossy_two_to_one := sector_is_lossy_quotient_of_closed
 138
 139end EdgeSectorBridge
 140end Holography
 141end IndisputableMonolith
 142