Sector
plain-language theorem explainer
Names the three algebraic columns of the RS quantum-gravity discriminator matrix: leading-log BH entropy coefficient, echo-damping amplitude ratio, and rung-phase coefficient. Anyone citing Track 6.D cells or rival-prediction tables depends on this enumeration. It is a plain inductive type with decidable equality; no proof content.
Claim. There is a finite type of discriminator sectors with exactly three inhabitants: the leading-log sector (black-hole entropy leading-log coefficient), the echo-damping sector (quarantined $\varphi$-rung amplitude ratio), and the rung-phase sector (quarantined $\varphi$-rung phase coefficient). Equality of sectors is decidable.
background
Track 6.D of the quantum-gravity master plan requires a $4\times N$ discriminator matrix: four rival programs (LQG, string, CDT, Bohmian) against $N$ observationally accessible algebraic sectors. Each cell is a numerical band that separates Recognition Science from that rival.
This inductive type fixes $N=3$. The leading-log sector is the physical BH-entropy coefficient (Session 90 QNM / holographic channel). Echo damping and rung phase are $\varphi$-rung algebra held in quarantine until a full echo mechanism is derived; they still supply positive-existence discriminators against rivals that predict no signal.
The sibling inductive Rival enumerates the four alternative QG programs. Together the two types index the matrix whose cells are theorem-grade inequalities (margins such as $>1/4$, $>5/4$, or mere positivity).
proof idea
No proof: a three-constructor inductive type deriving DecidableEq. The constructors are pure labels; mathematical content lives in the prediction maps and cell theorems that pattern-match on them.
why it matters
Closes the structural half of Track 6.D: without a named sector type the $4\times 3$ matrix cannot be stated. Downstream cell theorems (cell_LQG_LeadingLog, cell_String_EchoDamping, etc.) and rival-prediction functions index on these constructors. Combined with Session 93 DiscriminatorCert, the module meets the binding success criterion of three or more theorem-grade $\varphi$-derived discriminators with named channels.
The quarantine note on EchoDamping and RungPhase is deliberate: leading-log is fully physical; the other two remain rung algebra pending the missing echo mechanism, yet still discriminate CDT and Bohmian by positive existence. The type is also reused outside gravity (Born-rule sector measure, SM Lagrangian sector cost), so the name is framework-wide rather than gravity-local.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.