|
2 | 2 |
|
3 | 3 | -- Pillar C of docs/echo-types/establishment-plan.adoc. |
4 | 4 | -- |
5 | | --- SCAFFOLD ONLY. Documentation module (no declarations → no |
6 | | --- postulates, no holes; typechecks under `--safe --without-K`, |
7 | | --- tracked in `All.agda`). |
| 5 | +-- REAL MODULE (separating model landed 2026-05-17). |
8 | 6 | -- |
9 | | --- Goal: a SEPARATING MODEL. Construct a structure that satisfies |
10 | | --- generic Σ-functoriality (the `map-over` id/comp laws) but in which |
11 | | --- the loss-grade composition law `EchoGraded.degrade-compose` |
12 | | --- (equivalently `degrade-via-join`) FAILS. This is the gold-standard |
13 | | --- answer to the only objection every referee raises: "isn't this all |
14 | | --- Σ-lemmas with renamed components?" A model where the generic laws |
15 | | --- hold and the characteristic law does not proves the characteristic |
| 7 | +-- Goal: a SEPARATING MODEL. The only objection every referee raises |
| 8 | +-- is "isn't this all Σ-lemmas with renamed components?" The |
| 9 | +-- gold-standard answer is a model in which the *generic* Σ/Echo |
| 10 | +-- functoriality laws (`Echo.map-over-id` / `map-over-comp`) still |
| 11 | +-- hold, yet the *characteristic* loss-grade composition law |
| 12 | +-- `EchoGraded.degrade-compose` (equivalently `degrade-via-join`) |
| 13 | +-- FAILS — at a concrete, decidable witness. That proves the graded |
16 | 14 | -- family is genuine structure, not bookkeeping. |
17 | 15 | -- |
18 | | --- This continues the existing negative-exhibit discipline of |
19 | | --- `characteristic/VisibleConstraintAudit.agda` and |
20 | | --- `characteristic/IntegrationAudit.agda` (which collapse pseudo- |
21 | | --- theorems to `proj₂` / products of disjoint facts), but in the |
22 | | --- positive direction: an explicit countermodel object. |
| 16 | +-- The precise pin. `EchoGraded.degrade-compose` holds for exactly |
| 17 | +-- one reason: `≤g-prop` — the loss order `_≤g_` is propositional, so |
| 18 | +-- the chosen factoring `p12 ∙ p23` and the direct `p13` are forced |
| 19 | +-- equal, and `degrade-comp` then closes it. This model is `EchoGraded` |
| 20 | +-- with that single hypothesis removed: a "loss order" `_⊑_` with TWO |
| 21 | +-- distinct arrows `s₀ , s₁ : lo ⊑ hi` (so `sep-order-not-prop`), a |
| 22 | +-- reindexing `deg` that distinguishes them (`s₀ ↦ id`, `s₁ ↦ not`). |
| 23 | +-- Nothing else changes; in particular the Σ/`map-over` layer is the |
| 24 | +-- *same generic layer* and its laws still hold here (`sep-map-over-*`). |
| 25 | +-- The path-independence law breaks (`sep-degrade-compose-fails`). |
23 | 26 | -- |
24 | | --- Intended shape (to be filled): |
25 | | --- |
26 | | --- -- A concrete small carrier with a non-lattice "grade" so the |
27 | | --- -- join universal property is unavailable. |
28 | | --- record SepModel : Set where ... |
| 27 | +-- This continues the negative-exhibit discipline of |
| 28 | +-- `characteristic/VisibleConstraintAudit.agda` / |
| 29 | +-- `characteristic/IntegrationAudit.agda` (collapsing pseudo-theorems |
| 30 | +-- to `proj₂`), but in the positive direction: an explicit |
| 31 | +-- countermodel object, with the failure a checked `true ≢ false`. |
| 32 | + |
| 33 | +module EchoSeparating where |
| 34 | + |
| 35 | +open import Echo using (Echo; MapOver; map-over; map-over-id; map-over-comp) |
| 36 | +open import Data.Bool.Base using (Bool; true; false; not) |
| 37 | +open import Data.Product.Base using (_,_) |
| 38 | +open import Data.Unit.Base using (⊤; tt) |
| 39 | +open import Function.Base using (id; _∘_) |
| 40 | +open import Relation.Nullary using (¬_) |
| 41 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans) |
| 42 | + |
| 43 | +---------------------------------------------------------------------- |
| 44 | +-- The model: `EchoGraded` minus `≤g-prop`. |
29 | 45 | -- |
30 | | --- -- Generic Σ-functoriality still holds here. |
31 | | --- sep-map-over-id : ... |
32 | | --- sep-map-over-comp : ... |
| 46 | +-- Two grades and a NON-propositional loss order — two distinct |
| 47 | +-- arrows from `lo` to `hi`. (Contrast `EchoGraded._≤g_`, where |
| 48 | +-- `≤g-prop` makes every hom a singleton.) |
| 49 | + |
| 50 | +data G : Set where |
| 51 | + lo hi : G |
| 52 | + |
| 53 | +data _⊑_ : G → G → Set where |
| 54 | + rfl-lo : lo ⊑ lo |
| 55 | + rfl-hi : hi ⊑ hi |
| 56 | + s₀ s₁ : lo ⊑ hi -- two distinct lo→hi arrows: not a prop |
| 57 | + |
| 58 | +-- Grade-indexed carrier (mirrors `EchoGraded.GEcho`). |
| 59 | +Obj : G → Set |
| 60 | +Obj lo = Bool |
| 61 | +Obj hi = Bool |
| 62 | + |
| 63 | +-- Reindexing along the loss order (mirrors `EchoGraded.degrade`). |
| 64 | +-- The two lo→hi arrows act differently — this is the whole point. |
| 65 | +deg : ∀ {g₁ g₂} → g₁ ⊑ g₂ → Obj g₁ → Obj g₂ |
| 66 | +deg rfl-lo b = b |
| 67 | +deg rfl-hi b = b |
| 68 | +deg s₀ b = b |
| 69 | +deg s₁ b = not b |
| 70 | + |
| 71 | +---------------------------------------------------------------------- |
| 72 | +-- The loss order here is NOT propositional. This is the *single* |
| 73 | +-- hypothesis whose presence (`EchoGraded.≤g-prop`) makes |
| 74 | +-- `degrade-compose` true and whose absence breaks it below. |
| 75 | + |
| 76 | +sep-order-not-prop : ¬ (s₀ ≡ s₁) |
| 77 | +sep-order-not-prop () |
| 78 | + |
| 79 | +-- The functorial UNIT law still holds (the generic graded-structure |
| 80 | +-- part is untouched): identity arrows reindex by the identity. |
| 81 | +sep-deg-unit-lo : (b : Obj lo) → deg rfl-lo b ≡ b |
| 82 | +sep-deg-unit-lo _ = refl |
| 83 | + |
| 84 | +sep-deg-unit-hi : (b : Obj hi) → deg rfl-hi b ≡ b |
| 85 | +sep-deg-unit-hi _ = refl |
| 86 | + |
| 87 | +---------------------------------------------------------------------- |
| 88 | +-- Generic Σ/Echo functoriality STILL HOLDS in this model. |
33 | 89 | -- |
34 | | --- -- The characteristic graded law is refuted at a named witness. |
35 | | --- sep-degrade-compose-fails : |
36 | | --- ¬ (∀ {…} → <degrade p23 (degrade p12 e) ≡ degrade p13 e in SepModel>) |
| 90 | +-- Instantiate the generic `Echo` machinery at a model map (the |
| 91 | +-- `s₁`-action `not`, viewed as a `MapOver` over the point base `⊤`). |
| 92 | +-- `map-over-id` / `map-over-comp` hold here verbatim — they are the |
| 93 | +-- model-independent Σ laws, and this model is a bona-fide Echo |
| 94 | +-- setting. Only the *grade* law (next section) is what fails. |
| 95 | + |
| 96 | +sep-f : Bool → ⊤ |
| 97 | +sep-f _ = tt |
| 98 | + |
| 99 | +sep-MO : MapOver sep-f sep-f |
| 100 | +sep-MO = not , (λ _ → refl) |
| 101 | + |
| 102 | +sep-map-over-id : |
| 103 | + (e : Echo sep-f tt) → map-over (id , (λ _ → refl)) e ≡ e |
| 104 | +sep-map-over-id = map-over-id |
| 105 | + |
| 106 | +sep-map-over-comp : |
| 107 | + (e : Echo sep-f tt) → |
| 108 | + map-over ((not ∘ not) , (λ _ → trans refl refl)) e |
| 109 | + ≡ map-over sep-MO (map-over sep-MO e) |
| 110 | +sep-map-over-comp e = map-over-comp not (λ _ → refl) not (λ _ → refl) e |
| 111 | + |
| 112 | +---------------------------------------------------------------------- |
| 113 | +-- The characteristic law FAILS. |
37 | 114 | -- |
38 | | --- The witness must be concrete (finite carrier, decidable) so the |
39 | | --- failure is a checked inequality, not an appeal to non-derivability. |
| 115 | +-- `SepDegradeCompose` is `EchoGraded.degrade-compose` transcribed |
| 116 | +-- with `_⊑_` / `deg` for `_≤g_` / `degrade`. It is refuted at the |
| 117 | +-- concrete witness g₁=lo, g₂=lo, g₃=hi, p₁₂=rfl-lo, p₂₃=s₀, p₁₃=s₁, |
| 118 | +-- e=true: deg s₀ (deg rfl-lo true) = true, deg s₁ true = false. |
40 | 119 |
|
41 | | -module EchoSeparating where |
| 120 | +SepDegradeCompose : Set |
| 121 | +SepDegradeCompose = |
| 122 | + ∀ {g₁ g₂ g₃} |
| 123 | + (p₁₂ : g₁ ⊑ g₂) (p₂₃ : g₂ ⊑ g₃) (p₁₃ : g₁ ⊑ g₃) (e : Obj g₁) → |
| 124 | + deg p₂₃ (deg p₁₂ e) ≡ deg p₁₃ e |
| 125 | + |
| 126 | +true≢false : ¬ (true ≡ false) |
| 127 | +true≢false () |
| 128 | + |
| 129 | +sep-degrade-compose-fails : ¬ SepDegradeCompose |
| 130 | +sep-degrade-compose-fails law = true≢false (law rfl-lo s₀ s₁ true) |
| 131 | + |
| 132 | +-- Conclusion (for the establishment plan). The generic Σ-functoriality |
| 133 | +-- laws (`sep-map-over-id` / `sep-map-over-comp`) and the functorial |
| 134 | +-- unit (`sep-deg-unit-*`) hold in this model exactly as in |
| 135 | +-- `EchoGraded`; the only difference is `sep-order-not-prop` (no |
| 136 | +-- `≤g-prop`), and that alone is enough to refute the characteristic |
| 137 | +-- composition law. Therefore `EchoGraded.degrade-compose` is NOT a |
| 138 | +-- generic Σ-consequence — it is carried precisely by propositionality |
| 139 | +-- of the loss order. The graded-loss structure is real. |
0 commit comments