|
| 1 | += Identity Claim: Decision Gates |
| 2 | +:toc: macro |
| 3 | +:toclevels: 2 |
| 4 | +:sectnums: |
| 5 | +:sectnumlevels: 2 |
| 6 | +:icons: font |
| 7 | + |
| 8 | +[.lead] |
| 9 | +The identity claim for echo types (see <<readme#,README>>) rests on three |
| 10 | +conditions. Each is treated as a decision gate with an explicit failure |
| 11 | +action. Failure is recorded in `docs/retractions.adoc` rather than |
| 12 | +silently revised. |
| 13 | + |
| 14 | +[NOTE] |
| 15 | +==== |
| 16 | +Gates are reassessed at each tagged release. An identity claim that |
| 17 | +survives one round of scrutiny is not immune in the next. |
| 18 | +==== |
| 19 | + |
| 20 | +toc::[] |
| 21 | + |
| 22 | +== Gate summary |
| 23 | + |
| 24 | +[cols="1,3,2,2", options="header"] |
| 25 | +|=== |
| 26 | +| Gate | Condition | Artefact | Failure action |
| 27 | + |
| 28 | +| <<gate-1,1. Distinct phenomenon>> |
| 29 | +| Echo types name a phenomenon not already covered by neighbouring frameworks. |
| 30 | +| `docs/adjacency/` |
| 31 | +| Drop identity claim; retain as Agda exposition. |
| 32 | + |
| 33 | +| <<gate-2,2. Characteristic theorems>> |
| 34 | +| At least two theorems are naturally echo-shaped and not reducible to generic sigma lemmas. |
| 35 | +| `docs/characteristic.adoc` |
| 36 | +| Drop claim of a distinct theorem family; modules remain. |
| 37 | + |
| 38 | +| <<gate-3,3. Canonical examples>> |
| 39 | +| At least one worked example where echo types are the right explanatory unit. |
| 40 | +| `proofs/agda/examples/` |
| 41 | +| Reframe as theoretical scaffolding awaiting application. |
| 42 | +|=== |
| 43 | + |
| 44 | +[[gate-1]] |
| 45 | +== Gate 1: Distinct phenomenon |
| 46 | + |
| 47 | +.Claim |
| 48 | +**** |
| 49 | +Echo types name structured loss under non-injective computation as a |
| 50 | +phenomenon distinct from existing treatments — refinement types, |
| 51 | +lens/optic theory, HoTT fibers, setoid quotients, provenance semirings. |
| 52 | +**** |
| 53 | + |
| 54 | +=== Test |
| 55 | + |
| 56 | +For each neighbouring framework, produce a short note in |
| 57 | +`docs/adjacency/` answering: |
| 58 | + |
| 59 | +. What is the nearest existing construction? |
| 60 | +. What do echo types add? |
| 61 | +. What do echo types _not_ add? |
| 62 | + |
| 63 | +A framework fails the test if every claimed addition is already present |
| 64 | +elsewhere under another name. |
| 65 | + |
| 66 | +[IMPORTANT] |
| 67 | +==== |
| 68 | +*Gate 1 fails* if no neighbouring framework survives this test. |
| 69 | +==== |
| 70 | + |
| 71 | +=== Failure action |
| 72 | + |
| 73 | +. Record outcome in `docs/retractions.adoc`. |
| 74 | +. Reframe the repository as an Agda exposition of fiber-based structured |
| 75 | + loss. |
| 76 | +. Remove the identity claim from README and Zenodo metadata. |
| 77 | + |
| 78 | +[[gate-2]] |
| 79 | +== Gate 2: Characteristic theorem family |
| 80 | + |
| 81 | +.Claim |
| 82 | +**** |
| 83 | +There exist theorems whose statements are naturally echo-shaped and are |
| 84 | +not reducible to generic sigma/fiber lemmas. |
| 85 | +**** |
| 86 | + |
| 87 | +=== Test |
| 88 | + |
| 89 | +Nominate at least three theorems from the development as characteristic. |
| 90 | +For each, write a one-paragraph justification in |
| 91 | +`docs/characteristic.adoc` answering: |
| 92 | + |
| 93 | +[quote] |
| 94 | +Would this theorem be stated, or stated in this form, without the |
| 95 | +echo framing? |
| 96 | + |
| 97 | +A theorem that survives only as "fiber lemma X with renamed components" |
| 98 | +does not count. |
| 99 | + |
| 100 | +=== Current candidates for nomination |
| 101 | + |
| 102 | +[cols="1,3", options="header"] |
| 103 | +|=== |
| 104 | +| Module | Candidate theorem |
| 105 | + |
| 106 | +| `EchoCharacteristic` |
| 107 | +| `visible-constraint` — retained-constraint under projection. |
| 108 | + |
| 109 | +| `EchoGraded` |
| 110 | +| Compositional degradation law. |
| 111 | + |
| 112 | +| `EchoIntegration` |
| 113 | +| Knowledge preservation under choreography with graded degradation. |
| 114 | +|=== |
| 115 | + |
| 116 | +[IMPORTANT] |
| 117 | +==== |
| 118 | +*Gate 2 fails* if fewer than two candidates survive. |
| 119 | +==== |
| 120 | + |
| 121 | +=== Failure action |
| 122 | + |
| 123 | +. Record outcome in `docs/retractions.adoc`. |
| 124 | +. Retain the modules as useful Agda. |
| 125 | +. Drop the claim that echo types carry their own theorem family. |
| 126 | + |
| 127 | +[[gate-3]] |
| 128 | +== Gate 3: Canonical examples |
| 129 | + |
| 130 | +.Claim |
| 131 | +**** |
| 132 | +There exist concrete cases where "echo type" is the right explanatory |
| 133 | +unit — preferable to, not merely compatible with, existing framings. |
| 134 | +**** |
| 135 | + |
| 136 | +=== Test |
| 137 | + |
| 138 | +Produce at least one fully worked example in `proofs/agda/examples/` |
| 139 | +that is: |
| 140 | + |
| 141 | +* small enough to read end to end; |
| 142 | +* formalised, not narrated; |
| 143 | +* accompanied by an honest comparison to how the same example would be |
| 144 | + handled under the nearest existing framing. |
| 145 | + |
| 146 | +"Preferable" means shorter, clearer, or proves something the alternative |
| 147 | +does not. |
| 148 | + |
| 149 | +[IMPORTANT] |
| 150 | +==== |
| 151 | +*Gate 3 fails* if zero examples survive. |
| 152 | +==== |
| 153 | + |
| 154 | +=== Failure action |
| 155 | + |
| 156 | +. Record outcome in `docs/retractions.adoc`. |
| 157 | +. Reframe as theoretical scaffolding awaiting application. |
| 158 | + |
| 159 | +== Gate resolution |
| 160 | + |
| 161 | +[cols="1,3", options="header"] |
| 162 | +|=== |
| 163 | +| Outcome | Action |
| 164 | + |
| 165 | +| All three gates pass |
| 166 | +| Identity claim upheld. Proceed to submission for peer review. |
| 167 | + |
| 168 | +| Any gate fails |
| 169 | +| Identity claim retracted in README and on Zenodo (as a new version |
| 170 | + with revised abstract). Modules remain available; the claim does not. |
| 171 | +|=== |
| 172 | + |
| 173 | +[TIP] |
| 174 | +==== |
| 175 | +Retractions are not failures of the repository. They are the mechanism |
| 176 | +by which the identity claim is made falsifiable in the first place. |
| 177 | +==== |
0 commit comments