IndisputableMonolith.Gravity.QuantumChannel.BMVFalsifierBand

   1import Mathlib
   2import IndisputableMonolith.Gravity.QuantumChannel.BMVPositive
   3import IndisputableMonolith.Gravity.QuantumChannel.NoClassicalMediator
   4import IndisputableMonolith.Gravity.QuantumChannel.SubstrateLocalAccess
   5
   6/-!
   7# BMV Falsifier Band: the certified entanglement witness and the falsifier floor
   8
   9## Panel framing (binding)
  10
  11BMV entanglement is predicted by ANY quantum mediator, so this package is
  12permanently EXCLUDED from the pillar-3 discriminator slot. It cannot
  13distinguish RS from GR+QFT or from any other quantum-mediator model that
  14produces the same four branch phases (see
  15`same_branch_phases_same_BMV_witness` below, which records exactly why).
  16
  17Instead, this package is the FALSIFIER FLOOR. What a clean null
  18formally refutes is stated exactly here, with no inflation:
  19
  20* THEOREM (this file): under the package {Newtonian weak-field phase
  21  model (`BMVPositive.weakFieldPhase`, a MODEL input) + the named
  22  geometry (MODEL inputs of Section 1)}, the joint state is non-product
  23  (nonzero amplitude-matrix determinant), with the invariant certified
  24  in `[1/2, 7/10]`, bounded away from `0 mod 2 pi`. A measured product
  25  state at this geometry therefore contradicts THAT PACKAGE:
  26  `clean_null_refutes_rs` (model-point form) and
  27  `bmv_band_entanglement` (band-robust form).
  28* MODEL/OPEN (not formalized here or upstream): the premise that the
  29  RS gravitational channel produces the Newtonian weak-field phases at
  30  this geometry with this magnitude. The Track 2.C/2.D forcing theorems
  31  cited in `rs_amplitude_channel_unique` force the CHANNEL to be
  32  amplitude-linear under their named structural premises; they say
  33  nothing formal about the MAGNITUDE of the branch phases. The two
  34  halves of this module do not touch formally. Only with that
  35  unformalized premise added does "clean null refutes the package"
  36  extend to "clean null refutes the framework". The framework-level
  37  falsification reading is therefore MODEL/OPEN, not THEOREM.
  38
  39## Honest tier
  40
  41* THEOREM: all the algebra and the certified numeric bands in this file
  42  (kernel-checked, `norm_num` on exact rational literals; zero sorry,
  43  zero new axioms, no `native_decide`). The entanglement statement
  44  proved is exactly `det != 0`, the non-product criterion for the pure
  45  two-qubit branch state; no entanglement-entropy statement is used or
  46  claimed anywhere in this module.
  47* MODEL: the Newtonian weak-field phase formula, the choice of
  48  experimental geometry (masses, coherence time, branch separations),
  49  and the CODATA values of G and hbar, which are measured inputs, not
  50  RS derivations.
  51* MODEL/OPEN: the bridge premise that the RS channel reproduces the
  52  Newtonian weak-field phase magnitudes at this geometry (see above).
  53* The amplitude-channel forcing statement carries the exact structural
  54  premises of the existing Track 2.C/2.D modules; see the docstring of
  55  `rs_amplitude_channel_unique` for the honest premise list. Nothing is
  56  axiomatized here.
  57
  58## Contents
  59
  601. `rs_bmv_witness_band`: at one named representative geometry
  61   (Bose-et-al-2017-style mass and time scales in a parallel
  62   two-interferometer configuration; see Section 1), the entangling
  63   invariant
  64   `dPhi = (G m1 m2 T / hbar)(1/r_LL + 1/r_RR - 1/r_LR - 1/r_RL)`
  65   equals the exact rational `26696 / 47475` (about `0.5623` rad), lies
  66   in the certified band `[1/2, 7/10]` with `0 < 1/2` and
  67   `7/10 < 2 pi`, and therefore the joint two-mass state at this
  68   geometry is non-product (nonzero amplitude-matrix determinant), via
  69   `BMVPositive.entangled_of_branchPhase_in_open_period`.
  702. `rs_amplitude_channel_unique`: the strongest honest composition of
  71   the existing AmplitudeLinearForced* results tying the RS
  72   gravitational channel to the amplitude-linear one.
  733. `bmv_band_entanglement`: the band-robust falsifier. ANY four branch
  74   phases whose entangling invariant lands in `[1/2, 7/10]` give a
  75   non-product state; `clean_null_refutes_rs` is its model-point
  76   instantiation at the exact rational geometry values.
  774. `same_branch_phases_same_BMV_witness`: the non-discrimination
  78   disclosure. Any mediator model producing the same four branch phases
  79   yields the same amplitude matrix, determinant, and witness.
  805. `BMVFalsifierStatus`: documentation status record, including the
  81   permanent pillar-3 exclusion flag.
  82-/
  83
  84namespace IndisputableMonolith
  85namespace Gravity
  86namespace QuantumChannel
  87namespace BMVFalsifierBand
  88
  89noncomputable section
  90
  91/-! ## Section 1. Named experimental geometry and physical constants
  92
  93All values are exact rational literals in SI units so that `norm_num`
  94can certify every band without floating point or `native_decide`.
  95-/
  96
  97/-- CODATA Newtonian constant of gravitation,
  98`G = 6.674e-11 m^3 kg^-1 s^-2`, as the exact rational `6674 / 10^14`.
  99Provenance: CODATA recommended value, rounded to four significant
 100figures. MEASURED input, not an RS derivation. -/
 101def G_SI : ℝ := 6674 / 10 ^ 14
 102
 103/-- Reduced Planck constant `hbar = 1.055e-34 J s`, as the exact
 104rational `1055 / 10^37`. Provenance: CODATA (exact SI hbar is
 1051.054571817e-34 J s), rounded to four significant figures. MEASURED
 106input, not an RS derivation. -/
 107def hbar_SI : ℝ := 1055 / 10 ^ 37
 108
 109/-- MODEL: representative parallel two-interferometer geometry, mass 1.
 110`m1 = 1e-14 kg`, a Bose-et-al-2017-style microdiamond mass scale. -/
 111def m1_SI : ℝ := 1 / 10 ^ 14
 112
 113/-- MODEL: representative parallel two-interferometer geometry, mass 2.
 114`m2 = 1e-14 kg`, equal test masses. -/
 115def m2_SI : ℝ := 1 / 10 ^ 14
 116
 117/-- MODEL: representative parallel two-interferometer geometry,
 118interaction (coherence) time `T = 2.5 s`. -/
 119def T_SI : ℝ := 5 / 2
 120
 121/-- MODEL: representative parallel two-interferometer geometry,
 122branch-pair distance `r_LL = 250e-6 m` (the inter-interferometer
 123distance; the LL and RR pairs sit directly across from each other).
 124
 125Configuration note: `r_LL = r_RR = 250 um` with `r_LR = r_RL = 450 um`
 126violates the collinear-adjacent identity `r_LL + r_RR = r_LR + r_RL`,
 127so this is NOT the adjacent linear Bose et al. 2017 configuration. It
 128is realizable as the parallel two-interferometer BMV variant:
 129inter-interferometer distance `d = 250 um`, in-interferometer branch
 130separation `sqrt(450^2 - 250^2) um`, approximately `374 um`, so that
 131the cross pairs sit at `sqrt(d^2 + dx^2) = 450 um`. -/
 132def r_LL_SI : ℝ := 250 / 10 ^ 6
 133
 134/-- MODEL: representative parallel two-interferometer geometry,
 135branch-pair distance `r_RR = 250e-6 m` (directly-across pair; see the
 136configuration note on `r_LL_SI`). -/
 137def r_RR_SI : ℝ := 250 / 10 ^ 6
 138
 139/-- MODEL: representative parallel two-interferometer geometry,
 140branch-pair distance `r_LR = 450e-6 m` (diagonal cross pair; see the
 141configuration note on `r_LL_SI`). -/
 142def r_LR_SI : ℝ := 450 / 10 ^ 6
 143
 144/-- MODEL: representative parallel two-interferometer geometry,
 145branch-pair distance `r_RL = 450e-6 m` (diagonal cross pair; see the
 146configuration note on `r_LL_SI`). -/
 147def r_RL_SI : ℝ := 450 / 10 ^ 6
 148
 149/-! ## Section 2. The four weak-field branch phases and the invariant -/
 150
 151/-- The weak-field branch phase `phi_LL` at the named geometry. -/
 152def phase_LL : ℝ :=
 153  BMVPositive.weakFieldPhase G_SI hbar_SI m1_SI m2_SI T_SI r_LL_SI
 154
 155/-- The weak-field branch phase `phi_LR` at the named geometry. -/
 156def phase_LR : ℝ :=
 157  BMVPositive.weakFieldPhase G_SI hbar_SI m1_SI m2_SI T_SI r_LR_SI
 158
 159/-- The weak-field branch phase `phi_RL` at the named geometry. -/
 160def phase_RL : ℝ :=
 161  BMVPositive.weakFieldPhase G_SI hbar_SI m1_SI m2_SI T_SI r_RL_SI
 162
 163/-- The weak-field branch phase `phi_RR` at the named geometry. -/
 164def phase_RR : ℝ :=
 165  BMVPositive.weakFieldPhase G_SI hbar_SI m1_SI m2_SI T_SI r_RR_SI
 166
 167/-- The entangling invariant
 168`dPhi = (G m1 m2 T / hbar)(1/r_LL + 1/r_RR - 1/r_LR - 1/r_RL)`
 169evaluated at the named geometry, via the weak-field formula of
 170`BMVPositive`. -/
 171def deltaPhi : ℝ :=
 172  BMVPositive.weakFieldBranchInvariant G_SI hbar_SI m1_SI m2_SI T_SI
 173    r_LL_SI r_LR_SI r_RL_SI r_RR_SI
 174
 175/-- The `BMVPositive.branchPhaseInvariant` of the four named phases is
 176definitionally the weak-field invariant `deltaPhi`. -/
 177theorem branchPhaseInvariant_eq_deltaPhi :
 178    BMVPositive.branchPhaseInvariant phase_LL phase_LR phase_RL phase_RR
 179      = deltaPhi := rfl
 180
 181/-! ## Section 3. The certified value and band (THEOREM) -/
 182
 183/-- **Exact value.** At the named geometry the entangling invariant is
 184the exact rational `26696 / 47475`, approximately `0.562317` rad.
 185Kernel-checked rational arithmetic: the prefactor is
 186`G m1 m2 T / hbar = 16685 / 105500000 m = 1.5815e-4 m` (dimensions of
 187length: `[m^3 kg^-1 s^-2][kg][kg][s] / [kg m^2 s^-1] = m`) and the
 188geometric bracket is `2/(250e-6) - 2/(450e-6) = 32000/9 m^-1`. -/
 189theorem deltaPhi_eq_rat : deltaPhi = 26696 / 47475 := by
 190  unfold deltaPhi BMVPositive.weakFieldBranchInvariant
 191    BMVPositive.weakFieldPhase G_SI hbar_SI m1_SI m2_SI T_SI
 192    r_LL_SI r_LR_SI r_RL_SI r_RR_SI
 193  norm_num
 194
 195/-- Certified lower band edge: `1/2 <= deltaPhi`. -/
 196theorem deltaPhi_ge_half : (1 / 2 : ℝ) ≤ deltaPhi := by
 197  rw [deltaPhi_eq_rat]; norm_num
 198
 199/-- Certified upper band edge: `deltaPhi <= 7/10`. -/
 200theorem deltaPhi_le_seven_tenths : deltaPhi ≤ (7 / 10 : ℝ) := by
 201  rw [deltaPhi_eq_rat]; norm_num
 202
 203/-- Strict positivity of the invariant. -/
 204theorem deltaPhi_pos : (0 : ℝ) < deltaPhi := by
 205  rw [deltaPhi_eq_rat]; norm_num
 206
 207/-- The upper band edge is strictly below one period:
 208`7/10 < 2 pi` (using `3 < pi`). -/
 209theorem seven_tenths_lt_two_pi : (7 / 10 : ℝ) < 2 * Real.pi := by
 210  have h := Real.pi_gt_three
 211  linarith
 212
 213/-- The invariant is strictly inside the open period `(0, 2 pi)`. -/
 214theorem deltaPhi_lt_two_pi : deltaPhi < 2 * Real.pi :=
 215  lt_of_le_of_lt deltaPhi_le_seven_tenths seven_tenths_lt_two_pi
 216
 217/-- **Not congruent to zero mod 2 pi.** For every integer `n`, the
 218invariant differs from `n * (2 pi)`: the band `[1/2, 7/10]` excludes
 219`n <= 0` (those multiples are nonpositive) and `n >= 1` (those are at
 220least `2 pi > 6`). This is the formal content of "bounded away from 0
 221mod 2 pi". -/
 222theorem deltaPhi_not_congruent_zero (n : ℤ) :
 223    deltaPhi ≠ (n : ℝ) * (2 * Real.pi) := by
 224  intro h
 225  have hπ := Real.pi_gt_three
 226  have hlo := deltaPhi_ge_half
 227  have hhi := deltaPhi_le_seven_tenths
 228  rcases le_or_gt n 0 with hn | hn
 229  · have hn' : (n : ℝ) ≤ 0 := by exact_mod_cast hn
 230    have hmul : (n : ℝ) * (2 * Real.pi) ≤ 0 :=
 231      mul_nonpos_of_nonpos_of_nonneg hn' (by positivity)
 232    rw [h] at hlo
 233    linarith
 234  · have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
 235    have hmul : 2 * Real.pi ≤ (n : ℝ) * (2 * Real.pi) :=
 236      le_mul_of_one_le_left (by positivity) hn1
 237    rw [h] at hhi
 238    linarith
 239
 240/-! ## Section 4. Target 1: the certified witness band (THEOREM) -/
 241
 242/-- **RS BMV witness band.** At the named representative geometry
 243(MODEL inputs of Section 1), the entangling invariant lies in the
 244certified band `0 < 1/2 <= deltaPhi <= 7/10 < 2 pi`, and consequently
 245the joint two-mass state is entangled: the branch amplitude matrix has
 246nonzero determinant (non-product state), by
 247`BMVPositive.entangled_of_branchPhase_in_open_period`.
 248
 249The band is THEOREM-grade (exact rational arithmetic, kernel checked);
 250the geometry itself is a MODEL choice. The witness magnitude is
 251`deltaPhi = 26696 / 47475`, approximately `0.562` rad. -/
 252theorem rs_bmv_witness_band :
 253    ((0 : ℝ) < 1 / 2 ∧ (1 / 2 : ℝ) ≤ deltaPhi ∧
 254      deltaPhi ≤ (7 / 10 : ℝ) ∧ (7 / 10 : ℝ) < 2 * Real.pi) ∧
 255    Matrix.det
 256      (BMVPositive.branchAmplitudeMatrix
 257        phase_LL phase_LR phase_RL phase_RR) ≠ 0 := by
 258  refine ⟨⟨by norm_num, deltaPhi_ge_half, deltaPhi_le_seven_tenths,
 259    seven_tenths_lt_two_pi⟩, ?_⟩
 260  apply BMVPositive.entangled_of_branchPhase_in_open_period
 261  · rw [branchPhaseInvariant_eq_deltaPhi]
 262    exact deltaPhi_pos
 263  · rw [branchPhaseInvariant_eq_deltaPhi]
 264    exact deltaPhi_lt_two_pi
 265
 266/-- Convenience extraction: the joint state at the named geometry is
 267entangled (nonzero determinant of the branch amplitude matrix). -/
 268theorem rs_bmv_geometry_entangled :
 269    Matrix.det
 270      (BMVPositive.branchAmplitudeMatrix
 271        phase_LL phase_LR phase_RL phase_RR) ≠ 0 :=
 272  rs_bmv_witness_band.2
 273
 274/-! ## Section 5. Target 2: the amplitude channel is the RS channel -/
 275
 276/-- **RS amplitude channel unique (honest composition).** The strongest
 277statement available from the existing Track 2.C/2.D modules that the RS
 278gravitational channel is the amplitude-linear one. Exact premises:
 279
 2801. Clauses 1 and 2 are conditional on a
 281   `NoClassicalMediator.T0T8ConsistentSubstrate`, which is by
 282   definition an `AmplitudeLinearForced.RecognitionCoupledFactorization`:
 283   the joint substrate is the binary tensor product
 284   `Signal8 (x)[C] Signal8`, the joint operator is `C`-linear and
 285   factorizes on pure tensors (the named factor-product STRUCTURAL
 286   hypothesis of Track 2.C), and the matter side equals the substrate
 287   recognition update `cyclic_shift` (the T0-T8 forcing-chain input).
 288   Under those premises the channel response is forced amplitude-linear
 289   (clause 1) and any density-only (CPTP-classical) response collapses
 290   to the zero response (clause 2). Source:
 291   `NoClassicalMediator.channel_forced_amplitude_linear_under_T0T8` and
 292   `NoClassicalMediator.no_classical_mediator_under_T0T8`.
 2932. Clause 3 replaces global pure-tensor factorization by the substrate
 294   measurement-access premise (`ArisesFromSubstrateAccess`: the channel
 295   response is a nonzero matter-section readout of a `C`-linear joint
 296   operator). Honesty disclosure: `SubstrateSemanticsUnconditional`
 297   proves `IsAmplitudeLinear R_C <-> EXISTS R_J,
 298   ArisesFromSubstrateAccess R_J R_C`, so this premise is provably
 299   equivalent to the conclusion; clause 3 is one direction of that iff
 300   and adds NO forcing content beyond the factor-product clauses 1-2.
 301   It is recorded because it is the semantic reading of
 302   amplitude-linearity used by the source modules, not as extra
 303   evidence. Source:
 304   `AmplitudeLinearForced.isAmplitudeLinear_channel_of_arisesFromSubstrateAccess`.
 305
 306This is a STRUCTURAL THEOREM, conditional exactly on the listed named
 307structural premises. Nothing new is axiomatized here; the unconditional
 308lift (arbitrary joint operators, no access principle) remains open in
 309the source modules and is not claimed. -/
 310theorem rs_amplitude_channel_unique :
 311    (∀ F : NoClassicalMediator.T0T8ConsistentSubstrate,
 312        AmplitudeLinearForced.IsAmplitudeLinear F.R_C) ∧
 313    (∀ F : NoClassicalMediator.T0T8ConsistentSubstrate,
 314        AmplitudeLinearForced.IsDensityOnly F.R_C →
 315          ∀ φ : AmplitudeLinearForced.Signal8, F.R_C φ = 0) ∧
 316    (∀ (R_J : AmplitudeLinearForced.JointSubstrate →ₗ[ℂ]
 317              AmplitudeLinearForced.JointSubstrate)
 318       (R_C : AmplitudeLinearForced.Signal8 →
 319              AmplitudeLinearForced.Signal8),
 320        AmplitudeLinearForced.ArisesFromSubstrateAccess R_J R_C →
 321          AmplitudeLinearForced.IsAmplitudeLinear R_C) :=
 322  ⟨NoClassicalMediator.channel_forced_amplitude_linear_under_T0T8,
 323   fun F hDen φ =>
 324     NoClassicalMediator.no_classical_mediator_under_T0T8 F hDen φ,
 325   fun _ _ hAccess =>
 326     AmplitudeLinearForced.isAmplitudeLinear_channel_of_arisesFromSubstrateAccess
 327       hAccess⟩
 328
 329/-! ## Section 6. Target 3: the falsifier floor (THEOREM) -/
 330
 331/-- **Band-robust falsifier (THEOREM).** ANY four branch phases whose
 332entangling invariant `phi_LL + phi_RR - phi_LR - phi_RL` lands in the
 333certified band `[1/2, 7/10]` produce a non-product joint state: the
 334branch amplitude matrix has nonzero determinant. This is the
 335experimentally meaningful form: the observed phases need not equal the
 336model-point rationals exactly; any measurement or model uncertainty
 337that keeps the invariant inside the band preserves the contradiction
 338with a measured product state. Follows from the open-period witness
 339`BMVPositive.entangled_of_branchPhase_in_open_period` since
 340`0 < 1/2` and `7/10 < 2 pi`. -/
 341theorem bmv_band_entanglement
 342    (φ_LL φ_LR φ_RL φ_RR : ℝ)
 343    (hlo : (1 / 2 : ℝ) ≤
 344      BMVPositive.branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR)
 345    (hhi : BMVPositive.branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR ≤
 346      (7 / 10 : ℝ)) :
 347    Matrix.det
 348      (BMVPositive.branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR) ≠ 0 := by
 349  apply BMVPositive.entangled_of_branchPhase_in_open_period
 350  · linarith
 351  · have h := seven_tenths_lt_two_pi
 352    linarith
 353
 354/-- **Model-point instantiation of the falsifier.** This is the
 355band falsifier `bmv_band_entanglement` evaluated at the exact rational
 356model point: IF the observed branch phases equal the Newtonian
 357weak-field values at the named geometry EXACTLY (the four equality
 358hypotheses), THEN a measured product state (zero determinant, zero
 359entanglement witness) is a contradiction.
 360
 361Honest scope: because the hypotheses are exact equalities to the
 362rational model values, this instantiation has no direct experimental
 363content by itself (its proof is substitution into
 364`rs_bmv_geometry_entangled`); the experimentally meaningful statement
 365is the band-robust `bmv_band_entanglement` above. What a clean null
 366under controlled decoherence at this geometry and coherence time
 367formally refutes is the package {Newtonian weak-field phase model +
 368this geometry}. Extending that to "refutes the framework" requires the
 369unformalized MODEL/OPEN premise that the RS channel produces the
 370Newtonian weak-field phase magnitudes at this geometry; see the module
 371header. The invariant at the model point sits in `[1/2, 7/10]`,
 372bounded away from `0 mod 2 pi` (`deltaPhi_not_congruent_zero`), so the
 373determinant is provably nonzero (`rs_bmv_geometry_entangled`); within
 374the stated package there is no free parameter with which to soften the
 375null. -/
 376theorem clean_null_refutes_rs
 377    (φ_LL φ_LR φ_RL φ_RR : ℝ)
 378    (hLL : φ_LL = phase_LL) (hLR : φ_LR = phase_LR)
 379    (hRL : φ_RL = phase_RL) (hRR : φ_RR = phase_RR)
 380    (hNull :
 381      Matrix.det
 382        (BMVPositive.branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR) = 0) :
 383    False := by
 384  subst hLL; subst hLR; subst hRL; subst hRR
 385  exact rs_bmv_geometry_entangled hNull
 386
 387/-! ## Section 7. Target 4: the non-discrimination disclosure -/
 388
 389/-- **Same branch phases, same BMV witness.** Any mediator model that
 390produces the same four branch phases yields the same amplitude matrix,
 391the same determinant, and the same entangling invariant. The witness is
 392a function of the phases alone. This trivial congruence is stated
 393explicitly so the ledger records WHY the BMV package cannot
 394discriminate RS from GR+QFT (or any other quantum mediator producing
 395the weak-field phases): it is why this package is permanently excluded
 396from the pillar-3 discriminator slot and serves only as the falsifier
 397floor. -/
 398theorem same_branch_phases_same_BMV_witness
 399    {φ_LL φ_LR φ_RL φ_RR ψ_LL ψ_LR ψ_RL ψ_RR : ℝ}
 400    (hLL : φ_LL = ψ_LL) (hLR : φ_LR = ψ_LR)
 401    (hRL : φ_RL = ψ_RL) (hRR : φ_RR = ψ_RR) :
 402    BMVPositive.branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR
 403      = BMVPositive.branchAmplitudeMatrix ψ_LL ψ_LR ψ_RL ψ_RR ∧
 404    Matrix.det (BMVPositive.branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR)
 405      = Matrix.det
 406          (BMVPositive.branchAmplitudeMatrix ψ_LL ψ_LR ψ_RL ψ_RR) ∧
 407    BMVPositive.branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR
 408      = BMVPositive.branchPhaseInvariant ψ_LL ψ_LR ψ_RL ψ_RR := by
 409  subst hLL; subst hLR; subst hRL; subst hRR
 410  exact ⟨rfl, rfl, rfl⟩
 411
 412/-! ## Section 8. Target 5: status record -/
 413
 414/-- Status record for the BMV falsifier-band package. Honest reading:
 415the flags below are set by definition in `bmvFalsifierStatus`; the
 416`rfl` projection theorems only confirm the definition, they carry no
 417mathematical content. This structure is a documentation record; the
 418mathematics lives in the theorems above (`rs_bmv_witness_band`,
 419`bmv_band_entanglement`, `clean_null_refutes_rs`,
 420`rs_amplitude_channel_unique`, `same_branch_phases_same_BMV_witness`).
 421The `excluded_from_pillar3` flag records the permanent panel decision:
 422BMV entanglement cannot discriminate between quantum-mediator models
 423(`same_branch_phases_same_BMV_witness`), so it is a falsifier floor,
 424never a pillar-3 discriminator. -/
 425structure BMVFalsifierStatus where
 426  /-- `rs_bmv_witness_band`: certified band and entanglement witness. -/
 427  witness_band_certified : Bool
 428  /-- `rs_amplitude_channel_unique`: forcing theorems cited with exact
 429  premises. -/
 430  amplitude_channel_theorem_cited : Bool
 431  /-- `bmv_band_entanglement` and `clean_null_refutes_rs`: the
 432  falsifier is a named theorem (band-robust and model-point forms). -/
 433  falsifier_named : Bool
 434  /-- Permanent exclusion from the pillar-3 discriminator slot. -/
 435  excluded_from_pillar3 : Bool
 436
 437/-- The canonical status inhabitant: every flag is set `true` by
 438definition (documentation record, not a proof obligation). -/
 439def bmvFalsifierStatus : BMVFalsifierStatus where
 440  witness_band_certified := true
 441  amplitude_channel_theorem_cited := true
 442  falsifier_named := true
 443  excluded_from_pillar3 := true
 444
 445theorem bmvFalsifierStatus_witness_band_certified :
 446    bmvFalsifierStatus.witness_band_certified = true := rfl
 447
 448theorem bmvFalsifierStatus_amplitude_channel_theorem_cited :
 449    bmvFalsifierStatus.amplitude_channel_theorem_cited = true := rfl
 450
 451theorem bmvFalsifierStatus_falsifier_named :
 452    bmvFalsifierStatus.falsifier_named = true := rfl
 453
 454theorem bmvFalsifierStatus_excluded_from_pillar3 :
 455    bmvFalsifierStatus.excluded_from_pillar3 = true := rfl
 456
 457/-- All four status flags at once. Each `rfl` confirms the definition
 458of `bmvFalsifierStatus` only; see the structure docstring. -/
 459theorem bmvFalsifierStatus_all :
 460    bmvFalsifierStatus.witness_band_certified = true ∧
 461    bmvFalsifierStatus.amplitude_channel_theorem_cited = true ∧
 462    bmvFalsifierStatus.falsifier_named = true ∧
 463    bmvFalsifierStatus.excluded_from_pillar3 = true :=
 464  ⟨rfl, rfl, rfl, rfl⟩
 465
 466end
 467
 468end BMVFalsifierBand
 469end QuantumChannel
 470end Gravity
 471end IndisputableMonolith
 472