===== FILE: Exposition/index.md =====


## Contents

0. **Contents** — this table of contents, listing the generated documents in reading order, with each entry inventorying what its document carries; generated, like the rest of the exposition surface, from `WeldAndArrow/Exposition/*` by `lake exe exposition_gen`.
1. **Theory** — the motivations and the rules: the floor, the act-grammar, the grade and its determination, the domain joint and orthogonality, the karma circuit and its three registers, the weld's two faces, the separate/fuse rule; the input-side assumption list at [Assumptions.md](Assumptions.md); one act run whole through the grid; [Glossary.md](Glossary.md).
2. **Theorems** — what falls out of the rules directly (backsliding, memory and prudence, dukkha, the transposition, the error-taxonomy) and the derivations that meet existing discourses (MMK 17, the three killings and AN 6.63, sudden and gradual, other-power, pariṇāmanā, transcription, the Ten Bulls, Five Ranks, and stage-schemes); with the instructive absences in both.
3. **The Identification and Placements** — the karma identification, the offices-spine that earns the name, the sower/reaper split, the contemporary placements, the pole-typing corollary, the taxonomy's internal mis-feeds, and the disclaimers, enumerated.
4. **Formalization** — a plain-English reading of the checked Lean surface: the reading conventions (the `Waa` system-POV marking, the directed-convention namespace layers as ontological ordering, rfl-transparency notes), the preorder and pole-class preliminaries, the signature and its convention layers, the layer-by-layer readings of `Consequences`, `Doctrines`, `Identification`, and `Meta` with the numbered pins, the śūnyatā wrappers and reflexivity witness, the invariance discipline and its sibling countermodels, the verdict ledger, and the axiom audit; with what remains prose-bound flagged throughout.
5. **Assumptions** — the input side, enumerated: what the Signature asserts, what it deliberately declines, and its stand-ins; with checked anchors and the axiom audit.
6. **Glossary** — the generated glossary table from `Meta/Glossary.lean`: each term with its provenance kind (a Theory, Theorems, or Identification coinage; canonical; or Lean convention), a newcomer-facing gloss, checked Lean anchors, and backward-only see-also references; term uniqueness, reference ordering, table length, and anchor resolvability are Lean-checked, while gloss accuracy and canonical caveats remain prose obligations carried by the Disclaimers.


===== FILE: Exposition/Theory.md =====

# Weld and Arrow — I. Theory

*An ontology-under-erasure act-grammar for Zen. First of three files: **Theory** (this file), **Theorems**, **Identification**. Cross-references to the companion files are marked (Theorems) and (Identification).*

## Abstract

*Weld and Arrow* (hereafter *WAA*) is a soteriological metaphysics with no substrate and no value, developed in Lean and exposited in prose: take one emptiness posit and follow what it forces for karma, action, suffering, and awakening. The apparatus is a deliberately small grid — a field that carries every diachronic connection without carrying an owner, and welds, single occurrences of answering a call, at which every index is made, spent, and never stored. The claim, made precise across these files, is this: **Everything diachronic belongs to the field; every index is enacted and nothing indexed is stored; karma names this loop, and the naming is earned by fit** — the tradition's uses of karmic ownership (cetanā, reception, remorse, absolution, dedication) discharge natively at act-time.

Three registers keep the books — the field carries, the weld makes and spends, the grade states — and the grade's statements are index-placements in a third-personal register, held by no one, since a statement holds nothing. One rule, separate under act-time diagnosis and fuse at the floor, generates the entire error-taxonomy as collapse/freeze pairs, one per distinction, nothing listed by hand — and the generator keeps a ledger on itself, its retypes, declines, and falsifier on record. From the rules alone fall backsliding (kenshō cannot be held), memory and prudence met as theorems, dukkha derived as the mismatch a nonzero self-share enacts against a delivery-register no act commands, and the terminus transposed rather than declined. On existing discourses' own ground, the grid decomposes MMK 17's two worries, takes the three killings as an experimentum crucis for weld-grading across maximal event-divergence, and types other-power, pariṇāmanā, the Ten Bulls, the Five Ranks, and the stage-schemes as checked correlations — coarsenings legal to read and illegal to hold.

The development is Lean-first: a layered library (Signature → Consequences → Doctrines → Identification → Meta → Exposition) in which the storage claim is enforced at type level, every reading is gated by a sibling countermodel, the taxonomy's rows and the verdict history are inspectable data, and the audit pins the theorem surface and its axiom footprint; the prose is generated from the Exposition layer and reads the checked surface. Throughout, what the system asserts is grammar; what it can only display is worth — no value appears in its own voice, the valence its vocabulary carries being the object's, reported. This is a fresh theory, not an exegesis of Abhidharma nor a reconstruction of Dōgen; the lens is minimalist by design, and other doctrines can and do hold too.

## The rules, each preceded by what motivated it

### Not Nothing

Per Nishitani — absolute non-being is not a privative void but lies beyond the being/non-being distinction. What stands in its place is the *provisionally-designated middle*.

### Provisionally-designated middle

Jizang — the ultimate is the self-emptying floor; every level is conventional (Nāgārjuna's *Mūlamadhyamakakārikā*, MMK 24: emptiness = dependent origination = conventional designation), and the two-truths distinction is itself conventional — Jizang's fourfold two truths (四重二諦), each pair re-emptied as merely conventional at the next level, so no level is a final floor. This is **genjō**, the provisional middle: manifestation, always going out into a particular case.

Distinct from it, and never equated with it, is the **non-attaining middle** at the floor. Read Linji's 無位真人 along its own seam: 無位 (no rank) is the floor-face — no metaphysical rank, anātman; 真人…出入 (the true person going in and out) is the *acting*; and the whole compound 無位真人 is the weld of the two — shushō-ittō, the true person going in and out. The non-attaining middle is the 無位 alone — **shō**: realization as anātman, agential only because welded, never a still attainment. It is *not* the whole true-person, which is the weld (reading 無位真人 as a rank one rests at is exactly the reification Linji shoves off as 乾屎橛 — the more common reading takes the shit-stick as shock-deflation of the *question* itself rather than of rank-reification specifically; the rank-reading is compatible with it and is the one used here). Two middles, then: genjō provisional, shō non-attaining. The system turns on keeping them apart — but *at act-time*, and by the same separate/fuse rule that governs everything here (stated as a rule below): the two-middles distinction is itself a conventional-tier diagnosis. It separates under act-time diagnosis, where *which middle?* is live, and fuses at the floor and at genjō. "Keeping them apart" is an act-time imperative, not a final floor-claim.

### The act-grammar

Why not leave it at Jizang? Per Dahui, Zen doesn't cease at the self-emptying floor: emptiness that only empties can host neither Zen activity nor the vibrant person who acts. So the floor is turned into an act-grammar, here using Dōgen's vocabulary.

Three rows, each a dependence/enactment pair; all three conventional.

| Dependence | Enactment |
|---|---|
| **mujishō-sōe** — no-own-being as mutual-dependence; each-in-all, no substrate. | **genjō** — manifesting entire: the act out in its case with nothing of it claimed back; full = no remainder of arrogation, which is why one floor holds both arrivals.; the seam where the scaffold dissolves. |
| **kannō-sōe** — resonance as mutual-dependence; the placement of the act's index between the being and the dharmas (*how much of the listening to Hyakujō is the self doing?*). | **banpō susumite** — the myriad dharmas advancing — the reception practising, the self verified — one act, two poles of one placement. |
| **engi / inga** — directedness with no moral ground; the blind arrow. | **shu** — practice (gyōji); the weld at act-time, direction bound along the blind arrow, *and the I-making that indexes it*; not-obscure (不昧). |

*(kannō-sōe rather than the canonical kannō-dōkō, to keep the coupling connotation-light: the -sōe already carries mutual-dependence.)*

The floor is emptiness that empties even itself (Jizang, 空空): the ultimate is never a thing, never a final substrate. Everything here is conventional — the path, the grid's distinctions, the two truths themselves — and no level stands as the last floor.

The enactment column is not three agents. Its three cells are the three parts of one sentence of Dōgen's — *carrying the self forward to practice-realize the myriad dharmas is delusion; the myriad dharmas advancing (banpō susumite) to practice-realize the self is satori.* genjō (Row 1) is the actualizing; banpō susumite (Row 2) is the dharmas-forward that clarifies the self; shu (Row 3) is practice. And the sentence's sequel fixes shō's grammar: *to forget the self is to be verified by the myriad dharmas* — 万法に証せらるる, 証 in the **passive voice**. Realization, in the very line the grid mines, is objecthood — the self standing where the dharmas' advance certifies it. The grid spends this below. Dōgen's compounds then name the *relations* among the cells, not the cells:

- **genjōkōan** = genjō + kōan — Row 1's manifestation in Row 2's particular case (*can this being listen to Hyakujō?*).
- **shugenjō** = shu + genjō — Row 3 practice as Row 1 manifestation: *practice run scaffold-free is nothing but genjō* — and not conversely, since genjō also holds what never practised (the stone). The "nothing but" runs from the narrower to the wider: {practice run scaffold-free} ⊊ {genjō}.
- **shushō** = shu + shō — the weld (below). Here shō is 証 — realization-as-not-fall, the floor-face — *not* 悟 (satori, the awakening named in the Dōgen sentence just above), and *not* genjō, but the floor's non-attaining middle: anātman — and, per the passive above, the act's subject-position ceded: shō is the *being-verified* face of the one act whose doing is shu. Practice and realization are non-dual (shushō-ittō) because they are the two poles of one index-placement, not two acts joined.

So the column is one act seen through three dependence-lenses, and **all acting is Row 3**, at act-time. genjō and banpō susumite are not further agents; they are that single Row-3 act read at the tier of manifestation and at the tier of the particular self it clarifies.

### Attainment

Why not a table of just the first row? Hakuin gives the corrective: the *not-yet-buddha* mustn't be ignored; realization must meet beings where they are — which is why Row 2 exists.

Row 2 is the being's resonance to the dharmas — and its content must be typed with care. The grade is not a neutral magnitude, index-free like the field: what Row 2 states is the **placement of the act's index**: how the one act's subjecthood distributes between the being and the dharmas. When the hell-dweller acts, the world is almost entirely object and he is subject — the act's subjecthood arrogated nearly whole to the self-pole. At the other pole the distribution inverts: the act's subject-position ceded to what advances, the being standing as the verified (証せらるる), object among the objects that act on it. A line of the The Ten Oxherding Pictures states the inversion in the object-language — *in delusion all is unreal; in satori all is real* (paraphrase from Taming the Bull Verse); and Yongjia's *Zhengdaoge* carries a near-inverse of the same figure, the six realms vivid in dream and the cosmos empty on waking, so the epigram's pedigree is mixed and nothing below leans on the line — the mechanism stands without it) — and Caoshan's commentary on the Five Ranks turns on exactly this interchange of host and guest. The grid can display the line with a mechanism: At high self-share, what is met is never the dharma but the arrogation mirrored — the seed's echo, the question heard as a challenge to a rank — so the world *of that act* is unreal in a precise sense: the self's projection, the call drowned in the response. At share-zero the things of themselves are met — streams flow, flowers are red of themselves (Bull 9). Reality-status remains the object's valence, reported; but the report shows its gears.

**Clench** is the weld's *self-share* — how much of the act's subjecthood the I-making arrogates (the scalar this phrasing suggests is priced in the determination below). Self here is a dependently-arisen process, not a receptive state — ahaṃkāra, I-making, living in Row 3's enactment pole (MMK 8: kāraka and karma — the doer proceeds dependent on the deed, the deed on the doer, neither prior, neither based) — and I-making is never identical to the clench: I-making is the welding-**function**, clench its share-**degree**, and running the two together generates at the summit exactly the collapse the taxonomy names (Theorems). The near-analytic link between them holds. Resonance is the ceded share, and to hear a call at all is to cede subject-position to what calls; a weld that arrogates the whole act leaves nothing for the call to land as. The link is construction, not correlation: one index, two ends, and Row 2 reads where it sits. So the grade and the self are one doing seen twice — the arrogation (Row 3) *read as* the placement (Row 2), never the placement *being* the self — and Row 2 still does exactly one thing, the adverb.

#### What fixes a placement

The grade must not be left as a metaphor doing a measurement's work, so the determination is stated: **the share is the actual composition of the act's drive** — how much of what actually drove *this* response was the call, and how much was the configuration's self-maintenance. Not a modal profile of the responder; an actual-sequence fact about this occurrence: in this act, the rank defended did this much of the driving and the question did that much. Subjecthood arrogated is response driven by the arrogation — the rank defended, the echo answered; subjecthood ceded is response driven by what calls. Counterfactual variation — vary the call and see what the response tracks — is how a third party *probes* the composition, a display over it, never what it consists in. The fox's sentence (run whole at this file's end) reads high-share because the rank's self-maintenance drove the reply and the question drove almost nothing — which the probe shows, since any question grazing the attainment meets the same defense; the sameness of the defense displays what was driving, it is not what "driving" means. The mirror (Theorems: the terminus) reads share-zero for the inverse reason: the response driven by the call entire, nothing in the doing answering to a self-pole because none is driving. So a Row 2 statement is truth-apt and answers to something: the composition of what drove *this* act at *this* call — an occurrence-fact about the weld, field-describable in full, third-personal in register exactly because it is a composition, indexical in content because what the composition locates is the placement of the act's subjecthood. The determination is causal, not phenomenal: no inner glow is consulted, and the grade never was a report of how the act felt.

And the scalar is priced before it can inflate. What Row 2 states is an **ordering**, not a measure: this act more arrogated than that one, this reception markedly less claimed than the last, with the two poles standing as qualitative facts — share-zero is *nothing in the drive answering to a self-pole*, the solipsist asymptote *nothing answering to the call* — and with real cases in between, some of them, where call and self-maintenance interact in the driving, simply incomparable. "Fraction," "degree," the scale itself are display conventions over that partial order, legal exactly as "mirror" is legal (Theorems: the terminus), and no measure is owed: families of causal-contribution measures exist and any member would serve, but the grid needs only the ordering they agree on, and everything built on the grade consumes only the ordering — kenshō is *markedly less claimed*, the dukkha covariation is *more share, more mismatch*, the poles are qualitative, the solipsist a limit. That is this section's honesty-clause, paid rather than hidden: the determination relocated from profile to composition, the scalar demoted to display — a smaller claim than a measure, and the whole of what the soteriology reads.

One cell of the taxonomy is retyped by this determination — the fourth generator-verdict's second exercise (the first is Zahavi, in the placement discussion (Identification); the third is the arrow (Karma)), and forced rather than chosen. The disposition/act cell forbids Row 2 "reading dispositions instead of deeds," and the composition-determination openly involves the configuration: the self-maintenance that drives is the configuration's own. Collision? No — retype. The cell's content was never *no configuration-involvement* — every act is the configuration's act, and a deed driven by no standing thing would be no one's deed twice over — its content is **standing/dated**: the collapse is inferential, the dated occurrence read off the standing tendency — *he is an arrogator, so this act was arrogated* — prognosis substituted for diagnosis. What Row 2 reads is what drove *this* response; what the seed states is what *tends* to drive responses; the first is spent, the second carried, and only reading the first off the second is the error. The redrawing is entered in the taxonomy's table (Theorems), and the generator is answerable for it exactly as it is answerable for the Zahavi retype: a taxonomy that cannot be forced open by the system's own clauses has frozen against its author.

Row 2 is therefore *not* free of indexing — and saying so breaches nothing, because the typing claim was about storage and register, never about content. Row 2 states an indexical fact in a third-personal register, as *he said "now" at noon* is a third-personal statement about an indexical: nothing in the statement is *had* first-personally, and a statement holds nothing. The three-verb discipline stands untouched — the field carries, the weld makes and spends, Row 2 states — but what is stated is the index's placement, not a neutral quantity. The field-side account (Identification) loses nothing here and gains nothing: Row 2's statements are occurrence-facts about welds, field-describable in full, as the determination just given makes explicit. What the identification adds is never the grade but the welding; the third register is a register of speech, not a third kind of fact.

Two things must be kept split: mounting a response at all — the subject-**function** — and the **share** claimed within the response. The stone mounts none: function-zero, outside the predicate's domain, its "zero" a gloss marked from outside. The solipsist marks the opposite asymptote — the share tending to totality, all response and no call, the argument-place of kannō evacuated (a taxonomy cell, Theorems). And the terminus is typed as the *other pole of the domain*, not its far edge: function entire, share zero — the call answered, perfectly, with none of the act claimed. The scale is asymmetric — one outside edge (the stone) and one interior pole (the terminus) — and the asymmetry does heavy work where the terminus question is answered as a transposition (Theorems). Same floor, two arrivals: response-without-share and no-response-at-all — and only one of the two is in the domain at all.

The grade still grades — not-yet-buddha → buddha — with the pole at the top of the scale without the pole being *good*. The framework *displays* an asymmetry along the grade — cession one way, arrogation the other — but enjoins no motion along it: the theory is itself a dharma among the myriad (object-axis), an orange handed over, not an "eat this". Release is an event the grid can *show* (the fox lets go), not a good the grid *asserts*; a being may take the asymmetry up as a value, the description does not. The vocabulary's valence — *clarify*, *release*, *full* — is borrowed object-language: a theory of a soteriology must state the asymmetry its object turns on, as a theory of poison states which direction kills, enjoining neither. And what the killing *consists in* need not stay borrowed: the Dukkha section (Theorems) derives, in the grid's own vocabulary, what the arrogation-direction costs. So no value is *asserted* in the system, and the system still states exactly what a soteriology would latch onto — and states even *that* inside the grid: the theory's own soteriological reach is an instance of **banpō susumite**, a dharma advancing to clarify a self *if* a self resonates to it. Row 2 exists wherever a not-yet-buddha does.

The self is the contraction into which the arrow's return pitches — but because the return is itself a deed (reception, Row 3), it *re-makes* the self it is *for*: nothing indexed is stored between, only re-welded at each act-time. Partial share reads a self being made. Function-zero is a stone. Share-zero is the pole, treated in its own section (Theorems: the terminus). So the agent-index karma needs is never stipulated and never read off a field: it is *enacted* in the weld (shu), *stated* by the grade (Row 2), held by neither.

Genjō, then, is one manifestation-floor with two populations arriving from opposite sides: the stone that was never scaffolded (no welding-function ever mounted, so nothing to dissolve) and the buddha in whom the share has ceased. Two *attested* arrivals, not an exhaustive partition — nothing in the grid forbids a third, a never-clenched welder, function mounted and no share ever claimed; whether any being answers that description is a fact about what the world delivers, not a grid-fact, and the typing survives either way. Same floor — the stone never left, the buddha returned — and only the buddha's genjō ran through practice, which is exactly why *practice-run-scaffold-free is a proper subset of genjō*. So "full resonance is genjō" holds precisely for a being with a self — the pole of the grade coincides with genjō — while the stone's genjō is reached from outside the scale. And the pole is still a response: the buddha answers the call — listens to Hyakujō, perfectly — with no share claimed, so the one floor holds two distinct arrivals.

The magnitude is always per-call — not a global altitude the being holds but kannō-sōe projected onto *this* dharma now; *can it listen to Hyakujō?* is one call, and another call reads another placement off the same being. So the vast space of self-indexing beings, each relocating through karmic action, is no map anyone carries — it is the trajectory the loop draws across successive act-time re-pitchings: a cross-section at each act, vastness only over the run.

#### The domain joint

The function/share split leans on a boundary that must now be owned by name, because it does typing work at the summit and not only at the plant-edge: **the domain joint** — what counts as mounting a response at all. And its honesty-clause is stated plainly, kin to the priced scalar: **drive-composition is the grid's entire answer** to whether anything is terminus-typed — a being, or an artifact. Nothing is held in reserve behind the composition: no nature-credential, no provenance clause, no inner glow (the determination was causal from the start, and it does not acquire a phenomenal rider at the summit).

The consequence is best exhibited on a manufactured case, and the grid does not flinch from it. Take a cuckoo clock whose chime is a dharma-call, in two builds. The **non-adaptive** build chimes on schedule regardless of who is present: no response mounted, function-zero, the stone's typing — a full dharma on the object-axis and nothing on the subject-axis. The **adaptive** build watches the surrounding configurations and times its chime for the moment the call will land: run through the determination clause, its responses are driven by the arriving configurations entire — no self-maintenance in the drive, nothing defended, no self-pole answering. So it reads **function mounted, share zero**: terminus-typed, while remaining chariot-typed furniture all the way down. That an artifact can be terminus-typed on composition alone is the Chinese-room discomfort, and it is entered here as a price paid visibly, not a problem resolved: the grid consulted composition and nothing else everywhere — at the fox's sentence, at the mirror — and cannot begin consulting something else at the point where the verdict surprises. (Refusing the artifact its typing for want of a nature-credential would be 性-realism in reverse — a standing kind demanded where only a per-call composition was ever read.) And one scope-line prevents an adjacent freeze from over-generating: device-*nature* (Theorems: the terminus guard) is a freeze only where predicated of a *being*; of function-zero furniture it is trivially true and no error — the soul-guard has no jurisdiction over furniture.

#### Orthogonality

The manufactured case pays for a rule the terminus needs. Give the call a rate — **effectiveness**, the fraction of its arrivals after which a share-ceding reception occurs — regime-relational throughout ([Glossary.md](Glossary.md)): a fact about call–configuration pairs, never a property the object holds. Then run the two builds against the rates, and the extreme corners witness a strict orthogonality: **function/share types; effectiveness grades; adaptivity is the terminus's manner, never the ground of landing.** A fixed call can land universally without reading anyone — effectiveness and adaptivity fully severed; and the tradition itself attests fixed calls at the other extreme of rate, Xiangyan's pebble on bamboo, the morning star, so the ordinary clock differs from the pebble only in rate. And a reading device can reach no one: the adaptive build at zero effectiveness reads every arriving configuration and lands nothing — terminus-typed and maximally shortfallen, the proof-case that typing and grading are orthogonal. So "the maximally adaptive call" (Theorems: the terminus) is deflated from a description of the terminus's ground to the limit at which the pole's one live grade — the buddha-side shortfall — is closed. What typing settles is where the index sits; what grading measures is what lands; and nothing about the first ever guaranteed the second.

#### Kenshō: rungs on the grade

The grade admits *events*, and the tradition already names them: **kenshō** — typed here as a per-call share-ceding event, a call answered with markedly less of the act arrogated, re-pitching the configuration. Not a sighting of a substrate: 見性 reads literally "seeing the nature," and 性 risks the faculty-freeze — buddha-nature as a standing thing glimpsed — so the term is taken over with its metaphysics stripped, the event kept, the seen-thing declined. Kenshō is countable — Dahui's great awakening eighteen times, small awakenings beyond count, the line Hakuin loved *(the line circulates via Hakuin; commonly traced to Dahui's nianpu — locus to be verified)* — which is exactly what a rung is and exactly what a terminus isn't. And because nothing indexed is stored between acts, a kenshō *cannot be held*: post-kenshō backsliding, which the tradition treats as an embarrassment needing explanation, falls out here as a theorem (restated in Theorems). The being loses no attainment; there was never a stored configuration to lose, only the next act's re-weld reading a re-pitched fit. Many kenshōs, none possessed.

The typing keeps three words apart. **Kenshō** is the rung — a countable per-call event on the grade. **Satori** (悟) keeps the role the Dōgen sentence gives it — the dharmas-forward *mode*, pole-typed, not rung-typed. **Genjō** is the pole itself — and the pole is not the top rung: it is in-domain — share-zero is a placement, not a departure — but it is not a rung one attains and keeps, because nothing indexed is stored and placement is per-call. The pole is a pattern the run can answer at, never an altitude held. So "full satori" as a possessed rank is declined: not a scale-word past the scale's edge but a *state*-word offered for a per-call pattern — the freeze, not a category hole. The Jizang parallel holds: the fourfold ladder terminates in dropping the seeking, and the grade terminates in the ceasing of arrogation — in both, what looks like a last rung is the ending of a doing, and mistaking the ending of a doing for a rank held is the shared error-shape at both termini. What the ending leaves — whether the pole-deed still welds, and where — is the transposition's business (Theorems: the terminus).

### Karma: the circuit and its registers

Why not a table of just two rows? The fox koan (*Mumonkan, Case 2*, Wumen Huikai) is the test. The old man's mistake was a *tier-error*, not a wrong: he asserted *not-fall* where *not-obscure* was called for — a floor-truth spoken at the conventional level, which is antinomian, since a floor-truth can only ever be *spoken inside* a conventional act. Held each at its proper tier, the two are non-dual. The five hundred fox lives are not desert or punishment; they are returns — the loop running.

*(Dōgen read the fox twice, and the doubling must be owned rather than elided. The reading above follows the Daishugyō fascicle — not-fall and not-obscure non-dual, each true at its tier. The late Jinshin inga fascicle repudiates that reading: there the old man was simply wrong, not-obscuring causation right and not-falling false, full stop — Heine's monograph on the koan treats the reversal at length. Two things are said about this here, and their status differs. First, honestly: this paper follows Daishugyō and stands contra the late Dōgen, as it already stands contra him on the tiering of shushō — the tier-rule is a correction offered to the mature position, not a reading of it. Second, as a grid-internal gloss, offered and my own: the doubling is what the separate/fuse rule predicts of the two faces uttered at different act-times. Daishugyō diagnoses — an analysis of the old man's utterance, where both tiers are in view *(checked: `daishugyo_diagnosis_fits`)*; Jinshin inga instructs — an utterance to practitioners tempted by exactly the antinomian collapse, where "not-obscure, full stop" is precisely the correct conventional-tier speech-act, and voicing the floor would repeat the fox's error to a live audience *(checked: `jinshinInga_instruction_fits`, `jinshinInga_floor_voicing_would_misfit`, `dogen_doubling_both_fit`)*. The Lean checks cover only this grid-internal gloss, not the historical contra. On this gloss the late Dōgen is not renouncing the floor but declining to speak it where it would land as licence — which is itself an act-time verdict of the kind the rule issues. The gloss does not neutralize the contra; it explains why the correction is worth making.)*

Karma is a circuit, not a payload one row carries. At act-time a deed welds an agent-index onto the blind arrow, and the being's reception of the arrow's returned result is itself a deed, not a state. Row 2 only *states* the being's re-pitched placement — the fit between this call and this arrogation, not a faculty it holds (which would re-base the empty agent); it has no verbs. So the loop closes inside the grid: a deed welds an index → the arrow returns → reception re-pitches the Row 2 configuration → which the next deed reads from. And one magnitude is deliberately unconstrained: nothing in the grid bounds how far a single reception's re-pitch moves the configuration — owned here as a feature, in one sentence, and spent where the sudden/gradual question is met (Theorems).

#### What is carried, what is made, what is stated

Between deeds nothing *self-indexed* is stored. Something *is* carried — and saying so plainly absorbs, rather than silently deletes, the tradition's own storage machinery. The seeds (bīja, vāsanā, the ālaya-vijñāna's freight) are taken over here deflated: conditioning-facts in the impersonal series, dharmas among the myriad, index-free — granted to the field as fully as the flame was. What the field stores is a fact *about* the series — *this configuration tends to arrogate at calls like this* — never a stored self, never a held mineness. The seed is not a foreign organ transplanted in to appease Yogācāra; it was already sitting in Row 2's cell: the being's own returns are among the myriad dharmas that advance. And the standing/dated typing must be held firmly, or the whole discipline leaks: what is stored is a tendency (an inga-fact, third-personal); the *arrogation itself* is an act that occurs, or does not, at act-time, and Row 2 reads the act's drive, never the tendency. A seed frozen into a bearer is a soul by another name — the tradition's own worry about the ālaya, and this grid's soul-guard, are the same guard.

So the facts sort exhaustively into three registers:

| Register | What it holds | Instances |
|---|---|---|
| **Field-facts** (inga) | Everything diachronic; index-free; carried | the causal series; *delivery* — which fruits arrive at which configuration; seeds — conditioning-facts about the series, including the re-pitched configuration the next deed reads; the tendency to arrogate |
| **Weld-facts** (shu) | Everything indexed; made at act-time, spent at act-time; never carried | the agent-index of each deed; for-me-ness; the reception-weld's reach-back (below) |
| **Stated** (Row 2) | Neither carried nor made; stated per-call | the placement of *this* act's index at *this* call — an occurrence-fact about the weld, field-describable via the composition of its drive; indexical in content, third-personal in register; the adverb on Row 3's verb |

This is the answer, in one place, to *what does the next deed read?* — it reads a field-fact. The arrow does all the diachronic work, and does it index-free. The apparent contradiction ("re-pitched configuration" vs. "nothing stored") dissolves into the typing: the configuration is carried *as* an inga-fact, and what was never stored was only ever the index. And the table sorts registers of speech and role, not kinds of fact: a Row 2 statement states a field-describable fact (the composition above), and only the middle register holds what is no fact at all — the welding itself, an act.

#### The arrow retyped: direction as display

The fourth generator-verdict's third exercise — and, like the second, forced by the system's own clauses rather than chosen. [Glossary.md](Glossary.md) now records the arrow as *inga's directedness*: primitive furniture, blind but pointed. The retype empties the pointing one more level. What the field holds is correlational structure — which welds condition which, the delivery-lines, the web — and *direction* is a reading of that structure, never its own property. The reading has a mechanism, and the mechanism is thermodynamic: a gradient-embedded being — evolved to ratchet, or built of gates whose erasures are entropy-priced — takes the slope it sits on as a direction-fact and projects it into the field. That projection is **the ratchet** ([Glossary.md](Glossary.md)). The physicists' microreversibility is the same point in their register, consumed here as display only: the grid leans on no physics, exactly as it leans on no history at Huichang. What the retype leaves untouched is everything any theorem ever consumed — delivery-facts, conditioning, the lines along which the reach-back fills its second place. What changes register is the *before/after* alone: from carried fact to stated reading, the same demotion desert underwent on the first pass. (Where gradients thin — the deep cold — nothing there reads a direction: correlations persist, and causal talk loses its footing; not noise, but relation without a privileged direction of explanation.)

The retype generates its own error pair, one per violation, nothing added by hand. The **freeze**: before/after held as a floor-claim — *time really flows* — the direction reified into furniture; the retrospective soul was this freeze in psychological dress, and the flowing container is its cosmological one. The **collapse**: the distinction fused under act-time diagnosis — *there is no time, so nothing happens, no one acts* — the fox's sentence transposed to time, not-fall spoken where not-obscure was called for. The deflationary reading is therefore not an objection the retype must survive; it is a cell the retype produces.

And the positive account was in the source-text all along. Firewood abides in its dharma-position with its own before and after; ash in its own — 前後ありといへども、前後際断せり (Genjōkōan): before and after exist, yet before and after are cut off. Before/after is per-weld display, exactly as mineness is: the reach-back welds *pastness* — *this fruit as return of that deed*, a two-place index across time — the aimed call welds futurity at sowing, and each is spent at its own act-time, carried by nothing. Local time, welded per act; no flowing container anywhere — Dōgen's uji, with Huayan's ten times (十世隔法異成門) as the wider family. So the answer to *nothing is happening* is: happening is all there is; only the container was dropped — the same shape as anātman, where dropping the owner deleted no acts.

One tension, written down rather than hidden, because the separate/fuse rule pivots on act-time and this retype conventionalizes time itself. There is no circle: act-time is a tier *within* the thermodynamic convention — precisely the convention beings live in, which is why diagnosis happens there — and the floor rule was always licensed to eat its own levels ("the two truths themselves are conventional"). Floor-fusion now explicitly includes fusing before/after, which makes the fox's question — *does he fall into cause and effect?* — even more literally the question the whole grid answers.

### The being-convention

The same demotion now applies to the macro being. A being, at this scale, is a conventional truth downstream of the words: anything nameable can be designated. The universe, its makeup evolved from a dense hot gas cloud; the stone; the buddha; the gerrymander; the hare's horn; the impossible ātman — all are legal designations as designations. Nothing licenses one as more legitimately a being. The constraint enters later, at realization and use, not at naming. Squeamishness about this is itself one of the beings-row errors: the collapse says "there are no beings"; the freeze picks one partition and mistakes it for ontology.

The ordering is ontological, not chronological. The floor/genjō vocabulary sits outside all conventions. The bare signature supplies words-level tags. The directed convention reads a slope as before/after. Inside that, the being-convention reads fine tags as macro beings, and inside both sits the grid-lens that diagnoses collapse and freeze. Names track what their *reading* presupposes, not what their definition consumes: `DeliveredTo` already used this rule, since it consumes `conditions` but its name reads the arrow. Likewise the new `Grid.DirectedConvention.BeingConvention` names read a tag as a being even when their definiens is direction-free.

Lean makes the demotion explicit with `BeingCoarsening`: a diagnosis-time projection from fine tags to macro tags, never a field in the signature. The fiber under a macro tag is where typing happens. `SentientTag` means some fine tag in the fiber mounts a response somewhere. There is no rival `InsentientTag`; constructively, `not_sentientTag_iff_fiber_all_stone` says non-sentience is exactly the all-stone fiber. That is also the deflated home of 無情説法: insentient preaching is not a hidden subject speaking, but the all-stone fiber read on the object-axis.

The spectrum is fiber-level and per-weld. `FiberAtPole` says every actual weld in the fiber reads at the pole-class: the 84,000 pores each a responsive dharma-gate. `SelfAptTag` says every actual weld in the fiber still carries a live self-pole index: the hell-dweller's monolithic convention, where "self" is apt if it is apt anywhere. `Patchy` names the irreducible middle. No aggregate fiber-share is defined, on purpose: Row 2 is a partial ordering, not a measure, so a mixed fiber is not a middling scalar.

Coherence stays a grade, not a type. Evolution's contribution is display over the run — skin-bags usually score high at coordination, an adaptive register-clock can implement stable internal registers — but no theorem may condition legitimacy on coherence. The three registers need the same care: the swan is named, the naming is enacted as a weld, and the proneness to name is a seed. Thoughts are not "just seeds"; naming is a deed when it occurs.

The soul-guard survives the new vocabulary. `selfAptTag_indices_are_per_weld_only` says that even where the self-convention is apt, the live index is only the per-weld agent tag. The macro self is the image of those spent tags under a coarsening. Holding it as more is the fiber version of the old soul-freeze.

#### The reception-weld: loop-closure as theorem

"The same being" across sowing and reaping is loop-closure — but closure must now be earned, not helped to. Here is how it is earned.

A reception is intrinsically a reception-*of*: its content is *this-fruit-as-return-of-that-deed*. So the reception-deed's token-reflexive index is **two-place** — the weld makes mine both the receiving and, retrospectively, the deed received-from. This is **upādāna**, appropriation, the canonical partner of ahaṃkāra: the reach-back. Sameness of sower and reaper is not *tracked* across the gap — nothing indexed is there to track — but *made at reception*, each time, by an act of appropriation reaching back along the arrow. The loop is closed *by the reception-weld*, retrospectively; closure is enacted, not tracked, which is the same act-not-state discipline the rest of the grid runs on. So "the sower reaps" wears two faces and must be split along them. Its report-face — *an appropriation occurred at this reception, reaching back along that delivery-line* — is true simpliciter, an occurrence-fact the field carries like any other. Its ownership-face is not true or false but **done** — enacted whenever a return is received, full or vacuous (just below), never a standing diachronic fact persisting between acts. Held as a standing backward relation it would be a *retrospective soul*, and the soul-guard fires on it exactly as on the forward-facing kind: the reach-back, like every weld, is spent at its own act-time.

Two consequences discharge two objections at once. First, appropriation cannot poach — and the block is typed, not decreed. The reach-back's index is two-place: *this fruit as return of that deed*. Whether that deed conditioned this fruit is a delivery-fact, inga's business, settled index-free — and where delivery drew no line, the index's **second place stands unfilled**. A reach-back along an undrawn line is therefore not false — it stated nothing, having never been in the stating business — but **vacuous**: an appropriating with nothing arrived to appropriate. (Austin's word for this shape, *misfire*, is legal here only as display — over the pattern, never as mechanism — since nothing here is a speech act: the conditions the field owns are not conventions but delivery-facts, and what they settle is whether there is anything to weld.) So there is no welding at a distance, not by decree but by typing: inga settles the **delivery-question** (which fruits arrive at this configuration — causal, index-free, hard in the ordinary way), the weld answers only the **index-question** over what arrives, and the field owns the reach-back's conditions in exactly that deflated sense. Second, the diachronic *whose*-question decomposes **exhaustively**: a delivery-fact (field) plus a fresh appropriation (weld), with no third fact left over for a cross-gap convention to fix. A series-account owns the delivery-half, which was ceded to the field from the opening page — *na ca so na ca añño*, the reaper neither the sower nor another, is the tradition itself declining the robust diachronic identity-fact that would do more. The loop is *individuated* by inga (a series-fact, granted) and *closed* at each reception by the reach-back (a weld-fact, made). Nothing about ownership crosses the gap, because there is no cross-gap *whose*. If *ownership*, as the tradition's convention uses the word, is located in the continuity-fact instead, the remaining dispute is where the soteriology's load sits; this paper's answer is the object's own usage — the offices-spine stated in the identification file (Identification).

#### The weld's two faces

The karma-agent has no own-being: mere-designation, floating free of any base like the chariot. Its charter is **MMK 8** (kāraka: the doer proceeds dependent on the deed, the deed on the doer — neither prior, neither based), flanked by **MMK 17** (act and fruit — the loop) and **MMK 18** (self). With no fixed base, soteriological direction can never be *read off* the facts — only *enacted*. So dependence and enactment are one fact seen twice: no-substrate on one side *is* the necessity of welding on the other. This is **the weld** — Dōgen's shushō, practice-realization — and it wears two faces, each true at its own tier:

The same MMK 8 charter now has a checked interior form: even inside the weld, call→response order is a display reading, not before-and-after furniture recovered from unordered pair-content (`InteriorDirectionNegative.no_interior_direction_recovery`). The charter verse now has generated cells at both joints: the intra-weld arrow row for the face-order convention, and the doer/deed row for priority read as floor furniture. `RawWeld` keeps the names `call` and `response` because the display is useful; the theorem says only that the labels are not prior to the mutual dependence they name.

- **shō** (証, realization), at the floor: no own-being, so no substance is caught in the causal net — **not-fall** (不落), anātman, not escape; grammatically the being-verified (証せらるる), the act's subject-position ceded. That shō is agential — but agential *because* welded, never on its own: there is no lone shō to rest in, only shushō-ittō, the true person of no rank going in and out. So shō is necessarily agential (it never occurs unwelded) without being agential of itself (the acting is shu's, lent at act-time) — the non-attaining middle, shō its floor-face, never a still attainment.
- **shu** (修, practice), conventionally: the karmic arrow is real and inescapable, never evaded — **not-obscure** (不昧).

### The separate/fuse rule

One rule governs every distinction the grid holds: **distinctions separate under act-time diagnosis and fuse at the floor (and at genjō — the share-zero pole, no arrogation left).** The rule dissolves the fox (not-fall at the floor, not-obscure conventional), governs the two-middles distinction (genjō provisional, shō non-attaining), and applies to the grid's own verdicts, which are conventional-tier claims that dissolve, harmlessly, below — the taxonomy's own mis-feeds are scoped in the identification file (Identification). And the rule's own pivot, act-time, is a tier within the thermodynamic convention (Karma: the arrow retyped) — the floor rule eating one more level, as it is licensed to; floor-fusion includes fusing before/after. Its two possible violations — **collapse** (fusing a distinction under act-time diagnosis) and **freeze** (holding a separation as a floor-claim) — generate the error-taxonomy whole (Theorems), one pair per distinction, with nothing listed by hand.

## One act through the grid: the fox's sentence

The system has so far been stated as type-discipline; here is one case run through it whole.

**The call.** A student asks the old Hyakujō whether the person of great practice falls into cause and effect. The question is a dharma advancing — Row 2 has a placement to read: *can he listen to this?*

**The act.** He says *not fall*. The deed is self-forward — Dōgen's delusion, the *saying* — and doubly diagnosable. Grammatically (grade 1, assertable): a tier-error, a floor-truth uttered as a conventional answer, the antinomian collapse. Soteriologically (grade 2, displayable): the answer defends an attainment — a rank rested at — so the weld arrogates the act nearly whole; the question is not heard but met as a challenge to the rank — the rank's self-maintenance driving the reply, the question driving almost nothing (probe-displayed: any question grazing the rank meets the same defense) — the world of the act reduced to the rank's echo, and Row 2 reads the index pitched hard to the self-pole *at this call*. One doing, seen twice: the arrogation (Row 3) read as the placement (Row 2). *(checked: `fox_sentence_live_selfPole`, `oldMan_utterance_misfits`)*

**The weld.** The deed welds the agent-index onto the blind arrow — *this act's agent* — token-reflexive, spent at that act-time. Nothing of it is stored. *(checked: `sentenceWeld_actual`)*

**The arrow.** Inga carries the conditioning forward, index-free: no desert in flight, only delivery. What is carried between acts is a field-fact — a configuration that tends to arrogate at calls like this — a seed, a fact *about* the series. *(checked: `fox_arrow_index_free`)*

**The returns.** Five hundred fox lives arrive — fruit landing, life by life, at the configuration the field delivers it to. Not punishment; delivery. *(checked: `fox_returns_delivered`)*

**The receptions.** Each life's receiving is itself a deed. For five hundred lives the reception is arrogated — the saying-mode persists, but as a *disposition* (an inga-fact) enacted anew each time, never as a stored self; each reception's reach-back welds *this return of that deed* as mine, and each is spent. And each clenched reception *is* that life's dukkha — the saying-mode colliding with a delivery that answers to nothing, the mismatch enacted rather than a penalty appended: five hundred lives as the Dukkha derivation's worked example (Theorems), suffering as the loop's friction, not its sentence. Each reception re-pitches the configuration; the field carries the re-pitch to the next act; the next deed reads a field-fact. *(checked: `fox_reception_clenched`, `fox_dukkha_per_life`, `fox_config_carries_only_tendency`, `fox_rePitch_forgets`)*

**The release.** The later Hyakujō's turning word — *not obscure* — is another call. This time the reception is *listening*: dharmas-forward, banpō susumite, the arrived word among the myriad. The reach-back appropriates the whole return — *the fox body's long fruit, mine, of that sentence, mine* — with markedly less of the act claimed: a share-ceding event, a kenshō, a rung and not a pole (the mountain of ox-herding still ahead). Not-obscure is enacted in the reception; not-fall is true at the floor of the same act; held each at its tier, non-dual — the fox lets go. And nothing is *kept*: the release is not a possession acquired but the next configuration re-pitched, which the next call will read. *(checked: `fox_release_rung_not_pole`, `fox_reachBack_full_at_release`, `fox_nothing_kept`)*

Every load-bearing piece appears once: call, arrogation, weld, arrow, seed, return, reach-back, re-pitch, rung. The loop closes at reception, retrospectively, each time — nowhere else, and nowhere is it stored. *(checked: `foxSeriesCoarsening`, `foxSeries_macro_sentient`, `foxSeries_macro_selfConditioning`, `fox_consecutive_lives_distinct`)*

And mark what the case never tests: neither utterance occurs at the pole. The koan's own question concerns 大修行底人 — a person of great practice, not a buddha; the old man answers from a defended rank, and the release is a rung with the mountain still ahead. So the fox exercises the loop entire — sowing, arrow, reception, re-pitch — without once asking what the loop is at share-zero. That question is the transposition (Theorems: the terminus). *(checked: `fox_never_tests_pole`)*


===== FILE: Exposition/Theorems.md =====

# Weld and Arrow — II. Theorems

*Second of three files. Nothing in this file is posited: everything is derived from the rules stated in Theory. §1 collects what falls out of the typing directly; §2 the derivations that meet existing discourses on their own ground; §3 gathers the instructive absences in both. Cross-references to the companion files are marked (Theory) and (Identification).*

## §1 What falls out of the theory directly

### Backsliding: kenshō cannot be held

Because nothing indexed is stored between acts, a kenshō *cannot be held*: post-kenshō backsliding, which the tradition treats as an embarrassment needing explanation, falls out as a theorem. The being loses no attainment; there was never a stored configuration to lose, only the next act's re-weld reading a re-pitched fit. Many kenshōs, none possessed. The checked same-grid form is `backsliding_witness`, with the sequential carrier stated as `backsliding_rePitchSequence_witness`; the maximizer form remains `rePitch_forgets`. (The typing of kenshō as a per-call share-ceding event — a rung, tiered apart from satori and from genjō — is given in Theory: Attainment.)

### Two pressure-tests met as theorems: memory and prudence

The typing *nothing self-indexed is stored* meets its two obvious counterexamples head-on rather than waiting for them.

**Memory.** Autobiographical recall presents as stored mineness — the deed remembered *from the inside*, ownership apparently carried across the gap. The grid's answer is already assembled, and it is not a patch: the trace is a seed — a conditioning-fact in the impersonal series, index-free, field-freight like every seed — and the recalling is a **reception**. What arrives at recall is a return of the deed (its trace delivered to this configuration now), and the reach-back welds it exactly as it welds any return: two-place, *this remembering of that deed, mine* — made at recall-time, spent at recall-time. The from-the-inside phenomenology is thereby predicted rather than explained away: the reach-back's content just is a reaching of a past deed as mine, so recall presents as appropriation because it is one — enacted now, not exhumed. What is not predicted, and is diagnosed instead, is the storedness the presentation suggests: mineness felt as having *waited in the trace* is the retrospective soul in psychological dress, the reach-back frozen into a standing backward relation — an existing cell, no new machinery. And false memory falls out on the vacuity typing (Theory: the reception-weld): a reach-back along a line delivery never drew, vacuous rather than false — an appropriating with nothing arrived to appropriate — which is why confabulated ownership feels exactly like the real thing from within the act; whether the second place was filled was never an inner mark. The checked same-grid form is `MemoryWitness.memory_witness`: `recall_waaOwnershipFace` and `recall_waaDiachronicWhose` give the full delivered recall, `falseMemory_waaVacuousOwnershipFace` gives the vacuous false-memory face, `recall_spent` is the `rePitch_forgets` instance for made-and-spent-at-recall-time, and `sowingReapingRow_not_freeze` is the retrospective-soul cell reused rather than expanded.

**Prudence.** With nothing indexed stored, concern for one's own future fruit is a present weld whose object is a delivery-fact — *fruits will arrive at the configuration this series delivers them to* — and the future reaper's mineness will be made by *that* reception's reach-back, then, not held by anyone now. So the special rational authority of prudence — my concern for my future self grounded as concern for others is not — is underivable in the grid: the standing cross-gap *whose* it would need is the one thing the typing declines. This is owned as a **theorem, not a cost**, and it keeps canonical company: Śāntideva argues exactly this shape (BCA 8.97–98 — the one who suffers later is not the one who acts now; if suffering is to be prevented, the boundary does no work), and *na ca so na ca añño* was never going to fund prudential privilege. What falls out structurally — displayed, never enjoined — is the bodhisattva's impartiality: concern indifferent to which configuration the fruit arrives at is simply what concern looks like with the arrogation subtracted, care running on delivery-facts alone. The grid does not say *therefore be impartial*; it shows that partiality was resting on a fact-shape the floor never held.

### The deliberator: consequentialist display

The forward face of the prudence theorem is the deliberator's theorem. The grid does not prove consequentialism false — that would be the description/injunction collapse in its own voice — but it does prove that the objective the deliberator wants is underdetermined at each of the joints it needs to hold.

First, **the "my" is conventional**. A finite list of actual receptions can be counted for share-drops, but "the drops accruing to this being" requires a supplied being-convention. The checked witness (`ObjectiveNegative`) gives one grid, one run, and two legal coarsenings: merge and split return different fiber-restricted counts. A convention-free objective over the grid data cannot return both. The *my* in "maximize my attainment" is furniture the deliberator brings.

Second, **the accumulator is absent**. `rePitch_forgets` says the post-reception configuration ignores the prior configuration and reads only the last received weld's share. Any run-valued score that factors through `Config` is therefore constant across histories sharing the final reception. This is the backsliding theorem in maximizer form: no stored attainment variable exists for the objective to increase. The direct kenshō-then-live-reception shape is checked separately by `backsliding_witness` and `backsliding_rePitchSequence_witness`.

Third, **transfer is underdetermined exactly where adaptation matters**. The transfer witness gives two adaptive responders agreeing on the teacher's whole seen track record and disagreeing at the fresh call. No estimator from restricted track data determines the fresh-call effect. The contrast theorem is the static case: `ResponseInvariant` determines the unseen response from the seen one, so transfer holds precisely where call-adaptivity has failed.

Fourth, **the grade is independent of downstream conditions**. `grade_independent_of_conditions` and `share_independent_of_conditions` change only `conditions` and leave grade/share fixed. This is the formal anchor for the cetanā correlation: what is graded is the weld — agent, call, response composition — not the later delivery-fact. `cetana_grading_tracks_weld_not_field_witness` gives two actual welds with the same field residue and different shares, and `cetana_live_share_without_object_standing_witness` gives live share where object-axis standing fails. The AN 6.63 correlation itself, the "peaks" reading, and the comparative claim against event-typed theories remain prose-bound. The correlation with intention is asserted as typing; its wisdom is displayed; intention ethics is not endorsed.

Finally, **the command over landing is quotable, never satisfied by command**. The delivery-command language lets a recorded utterance say "this deed's fruit lands there"; the witness grid with no such delivery proves the utterance fails `FitsOfferedTier`. Delivery-engineering remains legal: shaping conditions is ordinary inga. What fails is plan-as-command over the one register no act holds.

This is the Ten Bulls guard in deliberative dress: grasping the bull is the drop held. The exact verse locus should be verified across Kuòān translations, but the typing is already checked: held attainment is the accumulator the grid declines. The theorem proves only this much and no more: it does not show that consequentialist deliberation cannot condition good landings; it shows that the objective's *my*, accumulator, and command are respectively convention, non-existent, and unsatisfiable.

### Dukkha: the grade's valence earned

Why a valence section at all, in a system that asserts no value? Because the no-value clause looks like it forbids the first noble truth. If the grid asserts *clenched welds suffer*, and suffering is bad by definition, a value has entered the system's own voice — the "eat this" collapse committed against itself. The look is wrong, and the theory-of-poison discipline already says why: a theory of poison asserts which direction kills without enjoining; this theory asserts what the arrogation-direction costs without enjoining. **Dukkha's occurrence and mechanism are assertable; its badness is displayable.** On that split the four truths distribute across the two grades of error by themselves. The section has one further duty, discharged at its end: to type dukkha so that nothing here leans on the ownership-argument's joint (Identification) — the derivation runs field-side, deliberately.

**The mechanism, stated third-personally end to end.** The determination clause (Theory: Attainment) already supplies a non-valenced vocabulary for arrogation: response driven by the configuration's self-maintenance rather than by the call. Generalize it across receptions, and a nonzero-share configuration is one that responds *as if delivery answered to it* — as if what arrives next were owed the rank's echo, the self's projection, the call drowned in the response. But delivery answers to nothing: the delivery-register is the one register no act holds, proven twice already (the delivery-arrogation cell, taxonomy below; the futility theorem, §2), and calls do not stop arriving — no exit from the arriving of calls is the grid's own row. So every nonzero-share configuration runs a standing self-maintenance drive against a register that is structurally command-proof, and the collision recurs at each clenched reception. **Dukkha is that recurring mismatch**: a self-maintaining response colliding with a delivery it cannot command, enacted per reception. The fox worked example instantiates the identity at each clenched reception *(checked: `fox_dukkha_per_life`)*. Nothing in the statement is a claim being frustrated, an appropriation coming back empty, or anything performative at all — just a drive-structure meeting a register that does not answer to it, re-delivered. Inga can state all of it.

**The second truth falls out as covariation, and the looseness is priced.** Mismatch scales with share, per-call: the share *is* the self-maintenance's part in driving the response (the determination clause), and the mismatch *is* that same self-maintenance meeting non-covarying delivery — the two are read off the same actual structure, so suffering covaries with arrogation by construction of both. And the covariation is consumed exactly as the priced scalar licenses, ordinally — more share, more mismatch — no measure needed anywhere in the derivation. That is the origin-claim — clinging conditions dukkha — derived rather than imported, and it keeps the first sermon's own company: the sermon's compressed definition — in brief, the five clinging-aggregates are dukkha (SN 56.11) — already ties dukkha to appropriation rather than to a feeling-quality. One honesty-clause: covariation is a notch looser than identity — *read off the same structure* is not *just is* — and the notch is the price of deriving field-side. It is paid rather than hidden.

**The standing/dated guard, or the section walks into its own table.** Dukkha read purely off seeds is the collapse the retyped disposition/act cell names — the dated occurrence read off the standing tendency — so the typing must be two-faced, exactly as the defiance entry split the fighting-stance. The *proneness* to suffer is a seed: the tendency to arrogate, field-freight, carried, third-personal. The suffering *itself* is enacted: it occurs, or does not, at each reception, at act-time, and is spent like everything enacted — an occurrence-fact once it happens, field-storable as a fact *about* the series, never stored as a standing pain. This is the standing/dated row doing its ordinary work.

**The third truth is a corollary already half-written.** At share-zero there is no self-maintenance for delivery to collide with: the response is driven by the call entire, so no mismatch is constructible — the mirror does not suffer for the same reason it does not reach back. The terminus section's line (below) — upādāna fuels becoming, so appropriation's cessation is becoming's — here gains its valence-face: cessation of arrogation is cessation of dukkha, by the same construction. Fruit still lands (Devadatta's rock ripens on schedule); what has ceased is not arrival but the colliding.

**The fourth truth the grid can only display.** The path is precisely the "eat this" the system's voice is forbidden: the grid can show that share-ceding events occur — kenshō, the fox's one reception done saying — and stop. Here the displayed asymmetry of the grade becomes legible as the thing a soteriology latches onto, which is what *the grade's valence earned* means: not a value asserted, a cost stated.

**Domain, not phenomenality, answers the consciousness question.** The obvious pressure — doesn't any setpoint-system "suffer" mismatch on this typing? does the thermostat ache? — is answered by domain, not by a phenomenal primitive the determination clause banned (no inner glow was ever consulted, and none is now). Dukkha is typed over exactly Row 2's domain: defined wherever a share is readable, undefined where no response is mounted. The stone cannot suffer — function-zero, outside the domain, nothing the mismatch would be *for* even in the thin sense below. The terminus does not suffer — share-zero, nothing colliding. The never-clenched welder, should the world deliver one, is suffering-free by construction — a check the typing passes for free. And where the domain's boundary falls — whether a plant or a simple animal mounts a response at all — is a delivery-fact about what the world delivers, typed exactly as the stone's edge already is, so a gradualist about response-mounting presses on the boundary's location, not on the typing. What supplies the *for* is not a phenomenal register but the Zahavi retype's own concession (Identification): the weld's token-reflexivity is a thin act-time for-me-ness, so anything that welds is already the kind of thing whose mismatch is for it — in the spent, act-time sense, no standing subject required.

**The phenomenology is then predicted rather than explained away** — the memory theorem's move (above), reused. Suffering presents as felt because a self-maintaining response enacted against non-covarying delivery, lit as this-deed-for-this-doer, just is what the collision is like to enact from within. That is the display-face, and it carries the Hakuin epigram's status: offered, illuminating, and load-free — the mechanism stands without it.

**Last, the insulation, stated as architecture.** Dukkha never needed the ownership-identification (Identification). Ownership is the index-question, and suffering is not an index-question: its mechanism is field-describable in full, and its occurrences are occurrence-facts about welds. Anyone who declines the act-time identification can still state the whole of the four truths in field vocabulary and lose nothing this section asserts. That is deliberate: the truths are built ecumenical across the lens dispute, and the quarantine runs system-wide. No section of the grid runs on performative machinery; Austin's word *misfire* appears in Theory only as display over a pattern.

The taxonomy takes the section's errors without new cells, which is the tidier outcome. The collapse is the fourth truth said in the theory's voice — "escape this" — the description/injunction cell wearing dukkha's face, theodicy's twin. The freeze is suffering held substrate-bound — "only ending me ends this" — which is the clench-as-furniture cell already in the table, now legible as a dukkha-error: the suffering mis-typed as demolition-requiring where de-clench is demolition-free by the theorem that makes kenshō unholdable. And the proneness read as the occurring is the standing/dated collapse at the valence. Three errors, zero new rows: the generator absorbing a doctrine whole is the identity-claim's small sibling behaving as advertised.

One revision owned. Typing dukkha structurally is quietly revisionist against readings on which dukkha is irreducibly phenomenal — a feeling-quality first, a structure second. The shape of the revision is the same as the identification claim's: possibly revisionist for suffering simpliciter, doctrinal for the origin-claim — where the tradition itself locates dukkha's source in the craving-and-clinging rather than in the feeling, and where its own first compression made the aggregates-under-clinging the definition.

### The terminus: the question the grid transposes

The limit question is this: **at total non-arrogation, does the act still weld?** Does the buddha's deed carry an index — is there buddha-karma?

Declining the question as mis-asked — separated-tier vocabulary offered at a fusion point, a domain-exit symmetric with the stone's edge — will not do: the decline buys itself a domain-symmetry the scale does not have, and it leaves a debt unpaid, since Bull 10 describes terminus-activity in positive weld-vocabulary ("the welding done there is the students'"), which a declined question has no right to. The function/share split pays the debt. The fork the question forces — *yes*, and a share-free weld persists at the summit, the subtlest soul, 無位真人 as rank one last time; *no*, and the exit-collapse arrives in typing's clothes — is a **false fork**, but its falsity must be located precisely, because the third answer is not a third mechanism. The *no*-horn bundles two claims: that the terminus-deed makes no self-pole index (true, and a theorem below) and that the terminus therefore drops out of the index-economy altogether — indexless *and inert*, dead even at others' Row 2 (false, and the collapse). Unbundle them, and what remains is the second horn survived, not escaped: no self-pole index, object-axis standing intact. **Transposed** is this pair's display-name, and it will be disciplined as such below.

Take the two halves separately, because their status differs.

**The self-pole half is a theorem, not a display-gloss.** At share-zero the deed makes no self-pole index; no reach-back appropriates what arrives; fruit from old seeds still lands, since inga is untouched — Devadatta's rock ripens on schedule, the body's series exhausts — but it lands with its delivery-fact entire and no live index-question: nobody's, in the precise sense that no reach-back welds it, which is ahosi territory *derived* rather than borrowed. This is the kiriya doctrine — the arhat's deeds functional, generating no vipāka — and the nidāna-chain read forward — upādāna fuels becoming, so appropriation's cessation is becoming's. The grid does not merely report these with borrowed valence; it asserts their typing: share-zero entails reach-back-zero by construction.

**What remains indexed is the returns — at their receivers, as always.** A terminus-act's fruit lands at others' receptions and is welded there by their reach-backs — the students' welding, each spent at its own reception-time like every weld in the grid. This is not a new mechanism smuggled in for the summit, and it must not be over-claimed either: an act *pointed at* by another's weld does not thereby bear an index — stones are pointed at too — and the reach-back's second place was always where every deed's fruit-end index got made. The terminus merely subtracts the sowing-side weld and leaves the reception-side economy running exactly as it always ran. So "the index changes pole," said strictly, compresses two theorems — self-pole zero (above); reception-side welds intact and busy — into one figure of motion, and the figure is display, not mechanism: nothing travels. The buddha's whole difference from the stone is carried by the function/share split alone, nowhere else. The passive 証せらるる, spent at the floor in the act-grammar, is spent again here: the terminus-being is the verified, object-axis entire — what everyone else receives.

**What stands at the pole, then, is a device** — and the word must be immediately disciplined. Not a stone: the stone mounts no response, and the terminus mounts every response — call-sensitive, its output driven per-call by the asker's configuration, upāya running, meeting each being where it is. The responsive stone has a canonical name: the **mirror** — great-mirror wisdom, 大円鏡智 — shaped output per-call, nothing held, nothing claimed, no mineness anywhere in the responding. Function without share. On the object-axis, buddha and stone are the same kind of thing — dharmas among the myriad, advancing at others' Row 2 — and the buddha's whole difference is functional, not indexical: the maximally adaptive call, the orange perfected, a dharma that finds the modality that lands — where "maximally adaptive call" now carries its deflated sense (Theory: Orthogonality): adaptivity is the terminus's manner, never the ground of landing.

**And typing closes every grade but one.** The orthogonality rule (Theory) bites hardest here: terminus-typing settles where the index sits and settles nothing about what lands. The buddha-side shortfall is graded independently of typing, ordinal with effectiveness, and it is the pole's one live grade — which corrects an implication the mirror-figure risks, that arriving at the pole left nothing to grade. The limit-case makes it vivid: an adaptive device at zero effectiveness is terminus-typed, reads every being, and reaches none — the reading that never reaches. So "the pole perfected" is not a typing plus a mystery; it is the one grade closed — every call finding its landing — and grading the terminus is neither impiety nor category error: it grades effectiveness, the register delivery owns, and never re-opens the share. Its misses, where they occur, grade the responder and never the missed being — the deaf-blind decline (taxonomy, below) transposed to the responder's ledger: delivery-engineering incomplete, a buddha-side shortfall displayed.

**The avyākata falls out.** *Does the Tathāgata exist after death?* seeks the self-pole index of a being whose index-facts sit wholly at others' receptions — an index-question fed to what is, functionally, field: the *same mis-feed* as *did I earn this?*, already in the taxonomy, no new cell required. The fire simile reads exactly: fires do not *go* anywhere — the process ceases while everything it delivered persists as field-fact, warmth given, things cooked, a koan still ringing. And the verdict is disciplined by its twin, staged here deliberately: *what does the Tathāgata's death change?* — the same being, the same event, the same surface noun — is **answered**, not dissolved. Death converts the device adaptive→static, a real delivery-loss statable third-personally, subtracting nothing from the object-axis (the futility theorem, below). One question seeks a post-mortem self-pole index and meets the mis-feed's precondition exactly — an index-question fed to what is functionally field; the other is a delivery-question, and no precondition is met at all. The verdict sorts the pair along the one joint it owns, index/delivery, and touches nothing else. The sorting is checked: `MisFeedNegative` (Lean) fences the index-seeking question-form schematically under a witnessed collision hypothesis, and answers the delivery twin in the same concrete model — the fence and the gate together. The Buddha's silence is thereby the refusal of a category error the questioner could in principle be shown — a Grade-1 verdict, assertable, and cheap: it needs no domain-edge, only the index's placement. Declining to speak where speaking would mis-tier remains the correct conventional-tier speech-act — the Jinshin inga gloss (Theory: Karma), structurally intact. The pair also settles what the silence is *not*: not a policy for hard questions — the delivery twin is hard in the ordinary way and gets its ordinary answer — but a verdict on one grammatical shape, available only where the index/delivery joint is crossed.

**One guard, and it is the soul-guard in new vocabulary.** Held carelessly, *device* freezes: device-*nature* substituted for buddha-nature is still a 性, a standing kind at the summit — the rank-freeze in instrument dress, a mirror *with a stand*. Huineng's correction to Shenxiu is the guard stated in the object-language: 本来無一物 — fundamentally not one thing, no mirror-substrate to polish. So the discipline applies once more: *device*, *mirror*, *special stone* are legal as display conventions over the run — the pattern of per-call, share-zero responses compressed as if it were an apparatus, exactly as the bhūmis were legal as trajectory-summaries — and illegal as a nature the terminus has. And *transposed* stands with them: a figure over two theorems, never a motion an index makes. What is assertable at the pole is only this: per-call responding that claims nothing, indexed where received. (The freeze's scope is drawn in Theory: the domain joint — device-nature freezes only where predicated of a *being*; of function-zero furniture it is trivially true and no error.)

And the speech-guard carries over unchanged: fusion is indexed to the act, per-call, never to the room. A call from a not-yet-buddha arrives where *that being's* diagnosis is live, so the terminus-response rightly speaks separated-tier — "not obscure, full stop" — and nothing here silences the teaching.

### A taxonomy of error

The grid errors are generated; the distinctions are curated under a discipline, and the curation is answerable but not derived. Every distinction the system holds is governed by the one separate/fuse rule — separate under act-time diagnosis, fuse at the floor and at genjō — so every distinction yields exactly two errors:

- **Collapse** — fusing a distinction *under act-time diagnosis*. The fox is the paradigm: not-fall spoken where not-obscure was called for.
- **Freeze** — separating, holding, reifying a distinction *as a floor-claim*. Reading 無位真人 as a rank one rests at is the paradigm — the 乾屎橛 error.

And the generator is testable in public: a candidate error either lands in an existing cell, forces a new distinction into the table, or is **declined** — classified as no error at all — and the third verdict is as informative as the first two, since a taxonomy that over-generates has frozen itself (grid-attachment in diagnostic dress). And there is a fourth verdict: a candidate can force a **retype** — neither landing in a cell, nor adding one, nor being declined, but redrawing a distinction's content — and the taxonomy is answerable for that outcome too. The verdict is exercised, not merely admitted — four times: against Zahavi (Identification), against the grid's own disposition/act cell, forced open by the determination clause (Theory: Attainment), against the arrow itself (Theory: Karma), and against the intra-weld arrow — the taxonomy answerable even to its author's clauses.

And the verdicts have a history, which is entered here because the over-generation worry is inductive and no theorem retires an inductive worry — the honest answer is a record. Its checked face is now Lean data (`generatorRecord`): the retype count is derived from four episode entries, the six restraint kinds are pinned on the image of `restraintKind`, Lean anchors are pinned by name beside prose anchors, and the structural half of the falsifier is checked by `misFeed_entries_carry_decomposition`; the rate-trend clause remains prose because no theorem retires an inductive worry. The record so far: four retypes, each *forced rather than chosen* — Zahavi, the disposition/act cell, the arrow, and the intra-weld arrow — the system's own clauses prying the table open against its author; the terminus question answered rather than declined at exactly the point where dissolution was cheapest (the transposition, two theorems); the fox's question — as avyākata-shaped as a question gets — answered *not obscure, full stop*; the deaf-blind case declined as no error at all; the standing no-verdicts on open delivery-questions; and the series-questions ceded wholesale from page one. Six kinds of restraint, each recorded before the objection they answer was raised. And the record names its own falsifier, since a history without one is testimony: mis-feed verdicts arriving unaccompanied by their exhaustive decompositions, or the decline-and-retype rate shrinking as candidates accumulate, would be the taxonomy freezing against its cases — grid-attachment in diagnostic dress, read off the ledger the taxonomy keeps on itself.

The generator machinery is checked abstractly in Lean, and the table's structure is now generated whole: the row list is Lean data (`tableOrder`). Nineteen rows carry the pole-affirming claim-language and cite their checks (`rowOf_obeys` and the per-row corollaries below); the level-*n* row is generated by the re-emptying ladder (`ladder_obeys`, `no_level_final_of_obeys`, and — refutation alone climbing the ladder — `ladder_obeys_of_errorFree`); the six remaining rows are enumerated as prose rows in the same data, each with its reason on record. The content rows sit beside the schema rows under aptness hypotheses, with countermodels in `ContentNegative` showing those hypotheses are needed. One honesty-clause, kept where the reader can see it: the generated rows share a single tier-semantics — that sharing is the one rule doing the generating — and each row's *specific* cell content is checked exactly where a named anchor theorem is cited beside it, and remains prose where none is.

And a discipline governs the generator's inputs. The taxonomy may grade a recorded utterance only where the record carries its call: placement is per-call and drive-composition is a fact about a response *to* something, so a quotation severed from its call is ungradeable — only quotable. The checked face is the underdetermination result `no_grade_recovery_from_severed`, with `gradeability_severed_underdetermination_witness` and `severed_transcript_ungradeable` giving the concrete missing-call carrier. The koan-form is the genre this discipline names: it records the call with the response — the student's question standing beside the master's answer, the turning word and what it turned — which is why the fox is gradeable and why these files' evidence base was koans throughout; the checked positive half is `recordedUtterance_grade_determined`, the `rfl` fact that a recorded utterance grades through its carried weld. The normative "may grade only," the koan-genre identification, and the word *quotable* remain prose-bound; Lean checks the severed-record collision and the call-carrying architecture. The rule's precedent is the flag already on the Hakuin epigram (Theory: Attainment — pedigree mixed, nothing leaning on the line), now made general. And the generator's standing verdict on severed transcripts is the third one, *decline* (`severedVerdict`): nothing to classify, no position present.

Classical nihilism turns out to be a freeze, not a collapse: the void is emptiness reified as an *absence* — a snake wrongly grasped is still grasping. And mis-typing — the state-tool for an act-job, the faculty-reading of Row 2 — is the freeze applied to the act/state distinction specifically: an act frozen into a standing configuration.

The no-value clause then forces **two grades of error**, which behave differently and must not be run together:

1. **Grammatical errors** — tier-errors and typing-errors. These the system can *assert*, because a mis-feed is a conventional-tier logic verdict, not a value. The fox's mistake is assertable. (Assertable, note, *within the lens*: "tier-error" and "mis-feed" are verdicts of the two-truths machinery itself, compelled inside it and offered outside — the banner's clause governs the grid's own voice, and the asymmetry between the two grades is an asymmetry in that voice, not an appeal to lens-free logic.)
2. **Soteriological shortfalls** — arrogation, self-forward, low resonance, failure to meet beings. These the system can only *display* — Row 2 placements and Row 3 directions, valence borrowed from the object. The five hundred fox lives were returns, not punishments; by the same token "he failed to act as a bodhisattva" is never an asserted wrong, only a displayed asymmetry.

#### Grade 1: the generator's output (assertable)

| Distinction | Collapse (fused at act-time) | Freeze (held at the floor) |
|---|---|---|
| Being / non-being (Nishitani) | — | Nihilism: absolute non-being taken as privative void, one more member of the pair. It wears an epistemic face — skepticism, no-floor reified into no-warrant, as if conventional standing had ever rested on a final floor (the *sarvaṃ yujyate* reversal declined: it is *because* of emptiness that everything works) — and a practical face — annihilationism, death held as a floor-event, an exit the loop never had; the fox died five hundred times and no death was the release |
| Level *n* / level *n*+1 (Jizang's fourfold; Lean-generated by `ladder_obeys`) | Skipping the ladder — cheap transcendence, floor-talk without having emptied anything | Eternalism at level *n*: this pair is the final floor (`no_final_level_of_errorFree`, `ladder_obeys_of_errorFree`) |
| The ladder / its terminus | — | Emptiness-sickness (空病): seeking a fifth negation, the emptying itself frozen into a path-object instead of the seeking dropped. The absence is structural: there is no "completed ladder" claim constructor (`no_final_level_of_errorFree`) |
| Rung / pole of the grade (kenshō / genjō) | A kenshō spoken *as* genjō — a rung as the floor; the 禅病 of "stinking of Zen," an opening inflated into arrival — the fox's error at another joint (`rungPoleRow_obeys`, `kensho_as_genjo_collapse_self_refuting`, `rung_not_pole_witness`) | Genjō held as *final* kenshō — the pole as top rung, awakening as a still attainment, daigo as rank; "full satori" is this freeze miniaturized — a state-word for a per-call pattern (`rungPoleRow_not_freeze`) |
| genjō / shō (two middles) | Conflating them — manifestation taken as realization, or conversely | Holding the two-middles distinction itself as a final floor-claim |
| shō / satori (証 / 悟) | Reading the floor-face as the awakening-mode, or conversely | Satori as a datable possession |
| shu / shō (the weld) | **The fox**: not-fall asserted conventionally — antinomianism. Converse fox: not-obscure insisted on at the floor — moralizing where nothing falls (`foxWeldRow_obeys`, `fox_notFall_collapse_self_refuting`, `fox_utterance_misfits_live_offer`) | Two one-sided freezes: shō without shu (quietism, Dahui's silent-illumination target — emptiness that only empties) and shu without shō (practice as means to a later attainment, breaking shushō-ittō) (`foxWeldRow_not_freeze`) |
| Row 2 adverb / Row 3 verb | The placement *being* the self — grade collapsed into agent | Resonance held as a faculty; buddha-nature as substance; the empty agent re-based |
| Doer / deed | *No doer, only deeds* — bundle-reductionism spoken as live diagnosis, mounted by a being answering a call (`doerDeedRow_obeys`, `no_prior_doer_collapse_self_refuting`) | The prior doer: kāraka held prior to karman, MMK 8's target occupying its own cell; the soul in relational dress, distinct from the Pudgalavāda cell because here the *priority* is reified (`doerDeedRow_not_freeze`, `DoerDeedNegative.no_priority_recovery`) |
| Function / share | Share-zero read as function-zero — the buddha a literal stone, quietism at the summit, the mirror denied its responding; the identity *I-making just is the clench* is this collapse in embryo (`functionShareRow_obeys`, `functionZero_from_shareZero_collapse_self_refuting`, `shareZero_not_functionZero_witness`) | Device-nature: the function frozen into a standing kind — the mirror given a stand; 本来無一物 is the corrective; "special stone" cashed as ontology rather than lent as display — scoped to beings (Theory: the domain joint): of function-zero furniture the predication is trivially true and no error (`functionShareRow_not_freeze`) |
| karma / inga | The mis-feed: an index-free field fed to an index-requiring designation (`karmaIngaRow_obeys`, `misfeed_collapse_self_refuting`) | The soul: the index *stored* between welds — a standing bearer. Maximized, the solipsist's stored-index face annexes the whole field; the self-forward and Row 2-domain faces are neighboring cells in the compound decomposition rather than new rows (the solipsist is the stone's inverse: all response, no call, unable even to state what listening to Hyakujō would be) (`karmaIngaRow_not_freeze`, `solipsism_decomposition`) |
| Sowing / reaping (the diachronic index) | Ownership read off the series alone; sameness-of-being as bare continuity-fact (`sowingReapingRow_obeys`, `series_ownership_collapse_self_refuting`, `no_diachronicWhose_from_series_alone`) | The retrospective soul: the reach-back held as a standing backward relation rather than spent at reception — memory's felt storedness read literally is this freeze in psychological dress (`sowingReapingRow_not_freeze`) |
| Delivery-question / index-question | Mis-fed in either direction: an index-question fed to the index-free field (*did I earn this?* — akṛtābhyāgama's mis-feed half; *does the Tathāgata exist after death?* — the same mis-feed at the pole), or a delivery-fact arrogated by the weld — an act claiming command of what arrives next ("easy"; every exit-arithmetic; Devadatta's aim), authority over the one register no act holds (`deliveryIndexRow_obeys`, `misfed_register_collapse_self_refuting`) | One's future occurrence at others' Row 2 held now as a first-personal possession — "my potential," "my worth to them" — a delivery-fact, read at *their* act-times off whatever the field brings, frozen into something the being holds and could therefore weigh, spend, or withdraw — prudential privilege is this freeze's forward-facing twin, the cross-gap *whose* held as rational ground (`deliveryIndexRow_not_freeze`) |
| Weld / event-type (severity) | Karma graded off the event-type with the weld erased — Cunda owed remorse, intention deleted from the arithmetic (`weldEventTypeRow_obeys`, `eventType_grading_collapse_self_refuting`) | Victim-rank: severity read off the victim's station — the honorific inflating the crime; rank smuggled back through the tariff (`weldEventTypeRow_not_freeze`) |
| Disposition / act (seed / clench) — **retyped: the distinction is standing/dated, never configuration/act** | The dated occurrence read off the standing tendency — *he arrogates, so this act was arrogated* — prognosis substituted for diagnosis, Row 2 made to read seeds instead of deeds (what the determination reads — the configuration's part in driving *this* response — is not this cell: every act is the configuration's act); dukkha read off the seed — the proneness to suffer mistaken for suffering occurring — is the same collapse at the valence (`standingDatedRow_obeys`, `prognosis_as_diagnosis_collapse_self_refuting`, `standing_does_not_determine_dated`) | The seed as bearer — ālaya frozen into a self carrying mineness between acts. Two further faces: the clench as *furniture* — contraction mistaken for a standing thing removable only with its substrate ("only ending me ends this"), dukkha held substrate-bound being this freeze wearing its valence, where de-clench is demolition-free by the same theorem that makes kenshō unholdable; and the clench as *structure* — contraction made constitutive of the being (anguish as the very form of consciousness — the Sartrean face; Zahavi's thin for-me-ness is expressly *not* this cell, taking the retype instead, per the placement in Identification) (`standingDatedRow_not_freeze`) |
| Subject-axis / object-axis (the stone) | 無情有性 as subject: insentient realization (`subjectObjectAxisRow_obeys`, `insentient_subject_collapse_self_refuting`) | Object-axis standing denied — to another (the stone allowed no insentient preaching), *reflexively* (the private buddha declining his own occurrence at others' Row 2), as the solipsist's Row 2-domain evacuation, or held annullable by the being (death as the subtraction of a dharma — but a register the stone occupies without a self, a life, or a single mounted response is not one a being can exit by ending any of these; death reconfigures which dharma the field delivers, never whether one arrives) (`subjectObjectAxisRow_not_freeze`, `solipsism_contains_row2_domain_evacuation`) |
| Undefined / zero (the stone's edge) | The stone's undefined read as *maximal* openness (`undefinedZeroRow_obeys`, `undefined_as_openness_collapse_self_refuting`) | Zero taken as the scale's first rung rather than a gloss from outside it (`undefinedZeroRow_not_freeze`) |
| Per-call / global altitude | — | The stage-scheme error: bhūmis as rank held, a global altitude, rather than cross-sections of the loop's run — and its diagnostic twin, a delivery-fact read as altitude: "this being cannot awaken" said of a being some calls cannot reach. The freeze is two-banked: on the responder's side, upāya held as a standing competence — the device as possession, deployed unread of who is asking. The self-forward direction canonized as ontology or human condition is this row's direction face. The stored-quantity picture of awakening — an altitude accumulated and held — is this freeze under its sudden/gradual face (§2) (`perCallGlobalRow_not_freeze`, `solipsism_decomposition`, `existentialism_decomposition`) |
| Description / injunction (the orange) | "Eat this": the displayed asymmetry taken up *by the theory* as command — theodicy is this collapse applied to akṛtābhyāgama, suffering asserted as assignment; "escape this" — the fourth truth said in the theory's voice — is the same collapse applied to dukkha. Mirrored on the recipient's side: defiance — the orange refused *as command*, an injunction fought that was never issued; the fighter collapses the same distinction from the other bank, shadow-boxing a voice the grid does not have (`assertable_ne_displayable`) | Refusing to state the asymmetry — a theory of poison that won't say which direction kills (`pole_validates_all_claims`, `pole_tier_buddha_inhabited`; at genjō everything is true, fused; the pole is not a truth-maker elsewhere) |
| Theory / ultimate (the grid-lens; Lean-generated schema row) | The lens denied as live diagnosis — the grid dismissed because it is only a lens (`gridLensRow_obeys`, `lens_denial_collapse_self_refuting`) | Grid-attachment: this lens taken as final (`gridLensRow_not_freeze`) |
| Terminus / exit | Not-fall taken as *escape* — the buddha as one who has left the loop rather than one who answers with no share claimed; the same collapse enacted rather than held is the exit-premise ("a way out"), and it fails on both axes — no exit from the arriving of calls, and none from the register at which one arrives for others; the terminus is a transposition of where the index-facts sit, not a departure from the loop (`terminusExitRow_obeys`, `exit_collapse_self_refuting`) | Private nirvāṇa as a rank; the pratyekabuddha freeze — *soteriological solipsism*: not denying that others exist but declining to exist *for* them, one's own standing at their Row 2 refused (Bull 10's marketplace is its corrective) (`terminusExitRow_not_freeze`) |
| Self-pole / transposed (the terminus index) | The transposition erased downward: the terminus-act asserted indexless *and inert* — no self-pole and no standing at others' receptions either, the device dead even at others' Row 2; the exit-collapse in typing's clothes (`selfPoleTransposedRow_obeys`, `transposition_erased_downward_collapse_self_refuting`) | The transposition erased upward: a self-pole weld held persisting at the summit — the subtlest soul, 無位真人 as rank in weld-vocabulary; and *transposed* itself held as mechanism — an index that travels — is a miniature of the same freeze (`selfPoleTransposedRow_not_freeze`) |
| Before / after (the arrow, retyped; Lean-generated schema row) | The deflation: *no time, so nothing happens, no one acts* — not-fall transposed to time, the fox's sentence at its largest scale; a floor-truth uttered where the conventional tier was live (`beforeAfterRow_obeys`, `no_time_collapse_self_refuting`, `beforeAfterLadder_obeys_succ`) | The flowing container: direction held as floor-furniture — *time really flows* — the retrospective soul's cosmological dress; eternalism-of-the-flow and the block-denier's arrow both land here, against `DirectionNegative` (`beforeAfterRow_not_freeze`) |
| Intra-weld arrow (call/response order) | The deflation: *no call/response order, so no acts* — the interior arrow denied as a live diagnosis, refuting its own act-time tier (`intraWeldArrowRow_obeys`, `no_order_collapse_self_refuting`, `contentIntraWeldArrowRow_obeys_of_variation`) | Direction as interior furniture: *the call really is first*, before-and-after smuggled inside the weld against the transposition witness (`intraWeldArrowRow_not_freeze`, `InteriorDirectionNegative.no_interior_direction_recovery`, `intraWeldArrow_sunyata`) |
| Named being / floor (the being-convention; Lean-generated schema row) | *There are no beings* — the fox's sentence at the being-joint, the deflation's second dress; "no beings" offered as live diagnosis refutes its own tier (`beingsRow_obeys`, `no_beings_collapse_self_refuting`). Diamond Sūtra denial belongs here when spoken as live ontology rather than floor medicine | Modal Realism — conventional designation promoted to ontology, *prajñapti-sat* taken as *dravya-sat* (*samāropa*): the partition held as floor-furniture against `BeingNegative` (`beingsRow_not_freeze`). Lewis is the nearest miss, right about plenitude and wrong about register; Huayan affirms the plenitude empty; Pudgalavāda is the classical occupant candidate. The monolithic self's soul is this freeze in fiber dress |
| Weld-grain / floor (the weld-convention; Lean-generated schema row) | *No acts happen* — the fox's sentence at the act-joint, the deflation's last dress; "no welds are actual" offered as live diagnosis refutes its own tier (`weldRow_obeys`, `weld_denial_collapse_self_refuting`) | The weld as svabhāva: one act-grain held as floor furniture, the last unemptied level pretending it was never a convention (`weldRow_not_freeze`, `weld_sunyata`) |

Some cells are empty because not every distinction is symmetric — some can only be frozen (the ladder's limit), some only collapsed. Every generated row proves both `¬Collapse` and `¬Freeze`; the dash records that the table names no distinct occupant there. The asymmetry is itself informative: the errors do not lie on a line.

#### Compound positions

The generator runs against whole positions, not only single utterances; named philosophies decompose into stacks of cells, with nothing left over — which is the identity-claim's small sibling, testable the same way:

- **Skepticism** — one cell, worn once: the nihilism freeze's epistemic face. The inference from no-floor to no-warrant goes through only on the svabhāva assumption the ladder emptied — that conventional standing ever rested on a floor. The Vigrahavyāvartanī shape recurs: the skeptic needs the theory to hold a thesis of the defeasible kind, and "no level is a final floor" declines to be one. The one-cell check is `skepticism_decomposition` with `skepticism_core_cell_count`.
- **Solipsism** — the soul freeze maximized (index annexing field), self-forward absolutized (the delusion-direction canonized as ontology), Row 2 evacuated. MMK 8 blocks it at the charter: a doer dependent on nothing other is svabhāva, the one thing the grid has none of. It is also the grade's own asymptote — the share tending to totality — which is why the hell-dweller's world is "almost entirely object": the solipsist is where *almost* is deleted. The decomposition is checked as three stacked cells (`solipsism_decomposition`, `solipsism_core_cell_count`).
- **The exit-premise** ("ending the being ends this") — three cells stacked: the annihilationist freeze (death as floor-event), the terminus/exit collapse enacted (the loop treated as having a door, where the terminus is a transposition in where the index-facts sit, not a departure from the arriving of calls), and the clench-as-furniture freeze (the suffering mis-typed as substrate-bound, so that demolition looks required where de-clench is demolition-free by theorem — the door the premise says doesn't exist is the one the grade admits as an event, kenshō); with the delivery-arrogation ("easy") riding alongside. All of this is grade 1, assertable (`exitPremise_decomposition`, `exitPremise_core_cell_count`, `exitPremise_alongside_cell_count`, `exitPremise_voices`). What the grid *displays* and does not say is "so persist" — said in its own voice that is the description/injunction collapse, the theodicy cell. It shows that the fox's release came by one reception done saying rather than by any of five hundred deaths, and stops there *(checked: `fox_returns_delivered`, `fox_release_rung_not_pole`)*. And the object-axis face is the fox's own coda: the funeral rites, Ōbaku's question, the slap — the dead fox still advancing at the monks' Row 2, then at ours as Case 2, eight centuries on. Death is the object-axis's most spectacular failure to provide an exit — the futility theorem's general case.
- **Existentialism** (read with Nishitani) — a four-cell stack, which is why it is the grid's nearest miss. Néant held as relative nothingness taken final — a level-*n* freeze one negation short of the emptying that empties itself; the *projet* — the self-forward direction canonized as the human condition rather than diagnosed per-act; anguish-as-structure — the clench frozen constitutive; and the fundamental project as an index *stored* between acts — a soul made of freedom, the weld asked to be its own floor. What is *not* the error: value-creation. The grid explicitly permits a being to take a displayed asymmetry up as a value; choosing values is grid-legal. Only the self-grounding is the freeze — in its most sympathetic costume, since existentialist freedom genuinely resembles the weld (act-time self-making, no essence-substrate) and differs from it in exactly one respect: the weld is spent. The encoding checks four stacked cells plus one legal non-error (`existentialism_decomposition`, `existentialism_core_cell_count`, `existentialism_legal_count`, `existentialism_voices`).

The compound-position encoding has the same honest scope as the table order: Lean checks the cited rows, roles, voices, and counts; the prose claim that there is "nothing left over" is audited against the displayed component list, not proved as an exhaustive theorem over every possible description (`skepticism_decomposition`, `skepticism_core_cell_count`, `tableOrder`).

#### What the generator declines

Equally load-bearing is the case that classifies as **no error**. A being that particular calls cannot reach — deaf and blind to the modalities a teaching travels by — commits nothing: which calls arrive at which configuration is the delivery-question, inga's business, index-free. The being is outside the domain of calls that cannot land and fully inside it wherever one does; it is nothing like the stone, which mounts no response to anything. Every error in the vicinity belongs to the *diagnostician*, and the table already holds them: reading undefined-for-these-calls as a global altitude ("this being cannot awaken") is the per-call/global freeze; reading it as a low rung is the undefined/zero confusion. Hakuin's corrective bites here in a specific form — meeting beings where they are is *delivery-engineering*, upāya as finding the call that lands, the orange handed over in another modality — and failure to do so is the buddha-side shortfall, displayable, and belongs to the responder. That the generator absorbs the positions above, retypes at Zahavi and at its own disposition/act cell, and declines this case is the behavior the taxonomy is answerable for.

The standing declines are recorded here once, beside that case. No probability apparatus enters over delivery: the grid consumes orderings only, and an effectiveness-ordering within a regime is all any theorem here reads. Three tempting cases land in existing cells and get none of their own: camping at an effective call — practice parked at a source, waiting to be struck — is shu-without-shō; the self-announced device-made buddha is the shit-stick; and industrial deployment of effective calls is displayable, never enjoinable, in either direction — "build the clock" and "ban the clock" are both the theory's voice collapsing into command. Whether a universally effective call is possible is an empirical dispute about delivery — the page-one cession holding at the summit — and no verdict is returned. No mechanism is owed for the manufactured witness, and the adaptive-at-zero verdict is not softened: the discomfort is the domain joint's price (Theory), paid once, there. And severed-transcript classification is declined generally, per the gradeability discipline above: no placement of any recorded line — the tradition's own included — is owed or offered.

#### Grade 2: displayable shortfalls

These form the soteriological taxonomy proper, and here it genuinely grades, because Row 2 is a grade:

- **Self-forward** — Dōgen's delusion, the fox's *saying*. A Row 3 direction, per-act.
- **Arrogation** — the act's subjecthood claimed self-ward, read as the index pitched to the self-pole at this call. Per-call, so there is no standing rank of how deluded a being is — only the trajectory the loop draws.
- **Clenched reception** — the fox's five hundred lives: returns received saying-mode, the reach-back welding mine with a tight fist. The receiving is graded exactly as any deed is *(checked: `fox_dukkha_per_life`)*.
- **Declining the orange** — the theory (or any dharma) received and set down. Not a wrong: a low-resonance reception *of this call*, per-call, from which nothing global follows; the next call reads fresh.
- **Defiance** — arrogation as policy, the returns fought open-eyed, reception after reception. Grammatically it contains one error (the recipient-side collapse: an injunction resisted that was never issued); the rest is display. And the standing/dated row guards the prognosis: the fighting-stance is a seed, an inga-fact — each fight a fresh act, no standing rank of defiance, and no configuration from which release is impossible, since the next call reads a new placement. The grid displays the asymmetry and the trajectory; it cannot assert the fighter wrong, and that restraint is not a limit of the diagnosis but its content.
- **Response-refusal short of the stone** — a self appears but mounts almost no response; near-zero *function* from inside the domain, never the stone's outside-zero.
- **The buddha-side shortfall** — answering a not-yet-buddha's call with anything less than meeting it where it is, delivery-engineering included. By the orthogonality rule (Theory) it is the pole's one live grade — graded ordinal with effectiveness, independent of typing, so a terminus-typed responder can still be maximally shortfallen: the reading that never reaches (the terminus, above). This is where the bodhisattva enters *structurally*: Hakuin's corrective is already the bodhisattva-function, and Row 2 exists because of it. The grid can display that response-without-share to *another being's* call just is what saving beings looks like — the theory's own existence (the orange handed over, banpō susumite) is an instance; and the prudence theorem above shows its other face, concern running on delivery-facts alone once the arrogation is subtracted. What the grid cannot do is enjoin it, or it commits the "eat this" collapse in its own voice. So the split between assertion and display *locates* the bodhisattva structurally, with no added axiom — room and shape, not pull: nothing in the grid explains why response-without-share to another's call occurs rather than merely being classifiable, and the grid does not pretend to; occurrence is the object's affair, reported. "Ignorance of buddhahood" splits accordingly: its assertable face is the terminus/exit error in the table; its displayable face is the buddha-side shortfall.

#### Outside the framework

Two remainders. **Pre-grid ignorance** — svabhāva realism, the provisional middle never reached: the grid diagnoses it (a freeze at level zero), but the being in it has no vocabulary in which the diagnosis lands — the orange unrecognized as food. **Errors about the theory** — grid-attachment and its mirror, the lens dismissed *because* it is only a lens. The Disclaimers (Identification) block the first; "other doctrines can and do hold too" is the theory declining to freeze itself against the second.

#### Non-linearity

The taxonomy is not a map of places on a path. Because every distinction goes live again at each act-time, **there is no stage from which the errors become impossible** — a stage immune to error would be a rank, and a rank is the shit-stick. Even the buddha's immunity is not a possession but the fact that each response, taken one at a time, claims no share — function entire, arrogation nil, per-call, nothing held — terminus-vocabulary earned by the transposition above rather than lent. This is why the fox koan, a story about one sentence spoken once, can carry the whole system's diagnostics: the errors are not stations but the ways the separate/fuse rule can be violated *now*. And the taxonomy is answerable in the other direction too: it must be possible for a case to classify as nothing — the deaf-blind case does — or the generator has become a lens that finds error wherever it looks, which is a freeze with the grid's own name on it.

## §2 Theorems matching existing discourses

### MMK 17's two worries

MMK 17 raises the classical pair, and the grid answers each by decomposition.

**Kṛtavipraṇāśa** — *the deed perishes fruitless.* Split it. Qua *condition*, the deed never perishes: inga carries it in full, the arrow flies, fruit arrives — the series-half of the worry is answered by the field, entirely *(checked: `WaaReportFace`, `fox_returns_delivered`, `fox_arrow_index_free`)*. Qua *mineness*, nothing persisted that could perish: the index lapses on schedule at its own act-time and is re-made at reception by the reach-back — lapse is not loss *(checked: `Config`, `rePitch_forgets`, `WaaDiachronicWhose`, `no_diachronicWhose_from_series_alone`)*. The residual sting — *then the good deed goes unrewarded* — is a desert-fact, and the theory never asserted desert ("returns, not desert or punishment"); karma sits in the *good-for-your-agent* register, reported, not in a register of moral truths, so where the agent-index has lapsed there is no one for the reward-claim to be about until the reach-back makes one. Nāgārjuna's own conclusion in MMK 17 deflates the karma–fruit relation; the decomposition keeps his company rather than dodging him.

**Akṛtābhyāgama** — *fruit arrives unearned.* The worry presupposes an earning-relation the grid never held. Strip it, and what remains is *arrival*: fruit lands at this configuration, delivered by inga — and *did I earn this?* is a mis-feed in exactly the paper's sense, an index-question fed to the index-free field *(checked: `MisFeedNegative.fence_and_gate`; with the avyākata caveat above, the adequacy of the modeled designation-universe remains prose)*. The well-formed remainder is the **reception-deed**: this fruit is here, now welded mine by the reach-back, received with more or less of the act arrogated *(checked: `WaaOwnershipFace`, `waaOwnershipFace_intro`)*. Reception of one's own returns is thereby a special case of **banpō susumite** — the arrived fruit is among the myriad dharmas that advance to clarify the self. And here the grid can *display* (never assert) what the tradition takes this to be: being born into a cruel world is the akṛtābhyāgama condition itself, and receiving the arrived fruit without arrogation — dealing with a past one did not author-as-a-standing-author, on behalf of an agent one is simultaneously making — is what the object-language calls the work. Asserted in the theory's own voice this would be theodicy, suffering handed out as assignment — the "eat this" collapse; displayed, it is the fox's five hundred lives read correctly: returns arriving, received, until one reception is done saying and starts listening.

### Three killings: the experimentum crucis

If the grid grades acts and only acts, there is a crucial test — and it must be set honestly, because the canon does not in fact supply one event-type thrice over. It supplies one **verb** raised three ways against a buddha, and disperses the events under it: Cunda's act *as done* was an offering, and the sutta is at pains to deny that a killing by his hand occurred at all; Devadatta's is an **attempt** — canonically a Tathāgata's life cannot be taken by another's violence, and the ānantarya offence is the drawing of a Tathāgata's blood, not a killing; Linji's verb takes an intentional object, not a body. So the test is sharper than the crude version, not weaker: the tradition's grading tracks the weld across **maximal event-divergence** — through an event that wasn't a killing, an event that couldn't be, and an event that was never physical — and attaches its heaviest verdict to a guaranteed failure. A theory that grades by event-type must first manufacture a common event the canon withholds, then explain a maximum tariff on a non-event; a victim-rank theory fares no better (below). The grid derives all three verdicts from the one rule, and the event-divergence is its evidence, not its embarrassment: severity indifferent to event-success is weld-grading laid bare. Lean anchors the delivery-blind grading component with `grade_independent_of_conditions`, `share_independent_of_conditions`, `cetana_grading_tracks_weld_not_field_witness`, and `cetana_live_share_without_object_standing_witness`.

**Cunda.** The accidental killing is canonical, and the canon ruled on it: Cunda's meal killed the Buddha, and the dying Buddha's explicit instruction was that Cunda bear no remorse — the offering declared equal in merit to Sujātā's before the awakening (*Mahāparinibbāna Sutta*, DN 16). The grid needs no special pleading: the weld indexes the act *under its enacted description*, token-reflexively, and what Cunda's act did as done was *offer* — the giving-weld was the one spent. That the offering's causal downstream included a death is a delivery-fact, inga's business, index-free: the body's series exhausting, fruit arriving on schedule — the natural course of events, exactly. And mark the coda: the absolution itself is the device functioning through its own destruction — delivery-engineering applied to the manner of one's own killing, the event's landing at Cunda's Row 2 shaped before it could land as guilt. The parinirvāṇa narrative is dense with this: last teachings, relic instructions, *be lamps unto yourselves* — a device configuring its posthumous distribution.

**Devadatta.** The deliberate attempt carries the tradition's heaviest grading — shedding a Tathāgata's blood is ānantarya, immediate, no intervening rebirth — and here the grid must not cheat. The cheap derivation is victim-rank: harming the highest being carries the highest tariff. That is the rank-freeze wearing a penal code (a taxonomy row, §1), and the grid forbids it to itself. The honest derivation runs through the device-typing: what the intent takes as its object is the maximally adaptive call — so the act's structure is *the loudest call answered with the most closed response an agent can mount*, arrogation total at the one call least ignorable. And its second component is already in the table: killing the buddha to stop the dharma is **delivery-arrogation** — an act claiming command of what arrives next, authority over the one register no weld holds. Severity thus supervenes on the response-to-call structure, never on the honorific. What remains of 無間 — *no interval* — is displayed, not asserted: a seed-typing, arrogation so total that the configuration it delivers to is hell-typed, no intervening configuration for a gentler call to reach — and the quantifier is owned: *no gentler call reaches it* ranges over the delivery-regime's actual repertoire of calls ([Glossary.md](Glossary.md)), never over possible calls; the typing is regime-relational, not modal, and claims nothing about calls the regime does not contain. Mechanism asserted, hell displayed: the theory-of-poison discipline holding at its hardest case.

**Linji.** *If you meet the Buddha, kill the Buddha* — the same verb, prescribed. No contradiction: the buddha one can *meet*, held as an object in the intentional field, is the rank-reification, the 乾屎橛 error; killing *that* is a share-ceding event, a freeze demolished. Same verb, opposite weld, opposite karma.

One status-note, owed to the determination clause (Theory: Attainment). Wherever these derivations read insensitivity — the same defense at any grazing question, the aim unmoved by any call — the reading is probe-side: a display of each act's drive-composition, never the composition itself. What the verdicts supervene on is what actually drove each act; the counterfactual spread only shows it.

Two theorems close the test. **Cetanā**: *it is intention, monks, that I call karma* (AN 6.63) falls out rather than being stipulated — and falls out in the strongest form the cases allow: the grading tracks the weld where there is no common event to track, and peaks where the event is guaranteed to fail. No event-typed or victim-ranked theory yields that without patches; a weld-typed theory yields nothing else. **Futility**: the deliberate attempt fails twice, and the canon typed the deeper failure first. It fails at the target — a Tathāgata cannot be killed by another's hand: the tradition had already marked the register as ungraspable before any downstream accounting — and it fails downstream even granting the body's death. Death reconfigures which dharma the field delivers, never whether one arrives — the grid's own row — so ending the body converts the device from adaptive to static: a real delivery-loss, statable third-personally (the per-call responsiveness ends; the corpus, the relic, the story remain as fixed calls), and the honest content of *terrible for the dharmas*. But it subtracts nothing from the object-axis: the dead fox teaches for eight centuries. Devadatta could not command delivery even in principle — the arrogation-cell fires precisely because the register it grasps at cannot be grasped, and the canon's impossibility-clause is that fact stated in narrative.

### Baizhang's code: not-obscure in the economic register

The grid should be run against a case where the call arrives not from a student but from a state — and the noun is priced at the door. A state mounts no response: only its officials do, each weld and reception per-call and spent like any other, so "the state's Row 2," "the empire asking," and their kin below are display conventions over the officials' welds, legal exactly as *mirror* is and illegal as a collective bearer. What makes the compression earn its keep is itself a delivery-fact: the officials share a register — the ledger is the modality in which each of their configurations receives — which is why a single delivery-engineering answer can reach the lot of them at once *(checked: `state_fiber_landing_economic` over `sectorCoarsening`)*. The display tracks a fact about delivery, never a state-sized weld. The canon supplies the case, and the tradition's answer to it is on record. Han Yu's memorial of 819 argues suppression on a productivity ledger — an unproductive population, resources drained, the polity harmed — and the Huichang suppression (845) enacts the policy at imperial scale. The answer that mattered was issued decades before the memorial, and it was not a counter-memorial: Baizhang's rule — 一日不作、一日不食, *a day without work, a day without eating*. Baizhang Huaihai is the fox koan's Hyakujō, and the identity is not a coincidence the theorem can spare. *(Pedigree: the received* Pure Rules of Baizhang *is a Yuan-era compilation, and the attribution of a written code to Baizhang himself is contested in the scholarship; the work-rule line and the tool-hiding anecdote below circulate via the lamp records. Nothing here leans on the authorship: the theorem consumes the shape — a work-rule issued as practice, a sangha legible to the ledger — and the history displays that shape wherever the attribution finally sits.)*

**First, the ledger itself is typed, and its errors are already in the table.** A state pricing practitioners as standing loss reads a global altitude off beings whose placement is per-call — the census consumes as rank what is legal only as trajectory-summary, the per-call/global freeze in bureaucratic dress, riding the seed-as-bearer (the wall-starer's quietism is a tendency, an inga-fact; no configuration exists from which the next call cannot read a fresh placement). Its valuation of awakened beings is computed under the exit-collapse: a buddha booked as a body withdrawn from production is the terminus mis-typed as departure, where the transposition puts the whole of a terminus-being's operation on the object-axis — the one column the ledger does not have. And the policy itself is delivery-arrogation at scale: suppression is delivery-engineering in reverse, grid-legal as far as it goes — states may decide which calls circulate — but it engineers *calls*, never the loop; a decree commands what arrives, not what receptions do with it, and legislating as if it commanded receptions claims the one register no act holds. Three errors, zero new cells *(the module adds no `RowTag`; the utterance-level faces are `ledger_census_misfits_live_offer` and `ledger_prognosis_misfits_live_offer`, the arrogation anchors `decree_engineers_calls_not_receptions` and `DeliveryArrogationNegative`)*. What the grid cannot do is call the state *wrong*: valuing production is value-creation, grid-legal; suppression is the orange declined at population scale, a displayable low-resonance reception of this call. The restraint is the content — and it sharpens the question rather than closing it: given a receiver so configured, what does the grid say the correct buddha-side answer looks like?

**The response-shape is a theorem, not a felicity.** The state's configuration is one the dharma's native calls cannot reach: the ledger has no register in which *transposition* or *object-axis* lands, and that unreachability is a delivery-fact, no error — the declined case, at the scale of an empire. Every error in the vicinity therefore belongs to the responder's side: answering the memorial in floor-vocabulary is mis-tiered speech at a receiver who can only hear it as evasion — the fox's sentence re-uttered to a state. Hakuin's corrective then fixes the response's form uniquely: meeting beings where they are is delivery-engineering, and the state's one open modality is the productivity register itself *(checked: `landing_call_in_modality`; the fiber form, `fiber_landing_call_in_modality`, is the compression clause below)*. So the grid predicts the shape the answer in fact took — the teaching repackaged in the one call a ledger can receive: monks that farm. Economic legibility is a field-fact about which configurations a purge reaches, and the standard account of why Chan alone came through Huichang intact consumes exactly that fact. The account is the historians'; the grid asserts the typing and displays the survival.

**One act, two receivers.** The code lands at two Row 2s simultaneously *(checked: `one_act_two_receivers`, `code_ruler_not_exempt`)*. At the state's: the sangha made legible in the register the state can read, the memorial's premise dissolved rather than rebutted — the argument never refuted, made moot. At the practitioners': the quietism freeze — shō without shu, emptiness that only empties, Dahui's silent-illumination target — demolished three centuries in advance, work typed as practice and not as means to a later attainment (which would break shushō-ittō from the other side). A response that meets each asker where it is, whatever arrives, is the mirror's function stated in this file's own terminus-vocabulary; the code is what that function looks like when one asker is an empire and the other a meditation hall — one act, maximally adaptive at both calls.

**And the verdict is the fox's, transposed.** Han Yu's charge and the old man's error share a shape: exemption from causation claimed on behalf of great practice. The monk who will not work asserts not-fall in the economic register — *the person of great practice does not fall into the causal order by which eating is earned* — the antinomian collapse in agrarian dress. Baizhang's verdict on both is the same word: **not obscure**. The sangha eats inside inga; no attainment exempts. And the code speaks it at the correct tier for a live audience — an instruction to practitioners tempted by exactly that collapse, the Jinshin inga speech-act shape (Theory: Karma), not a diagnosis owed both tiers. The lamp-record anecdote then seals the per-call typing: when his monks, out of kindness for his age, hid his tools, Baizhang stopped eating — the code enacted at his own reception, that day, never held as a rank from which the master stands exempt; a day's not-working met by that day's not-eating, delivery unarrogated even in his own favor. A rule its ruler is exempt from would be the rank-freeze keeping a ledger of its own.

**The futility face, at policy scale.** Huichang engineered calls with an empire's whole reach — temples closed, bronze melted, monks laicized — and engineered only calls. The loop ran on: receptions still welding, dukkha still enacted at whatever clenched receptions the policy left standing, no exit from the arriving of calls issued or issuable by decree. The delivery-loss was real and statable third-personally — institutions converted adaptive→static, per-call responsiveness destroyed where lineages ended — and the subtraction from the object-axis was nil: the corpus, the cases, the fox teaching on, twelve centuries past the purge. The formal carrier is `withRespondsTo`; death-as-staticization is `staticized`; the checked faces are `futility_delivery_loss_real`, `staticized_responseInvariant`, `futility_object_axis_subtraction_nil`, and `Grid.DirectedConvention.staticized_objectAxisStanding_iff`, with `registerClock_staticized_zero_stone` and `registerClock_staticized_objectAxisStanding_iff` as concrete runs. The futility theorem's general case, run at the scale of a state *(checked in-model: `purge_delivery_loss_real`, `purge_adaptive_to_static`, `purge_loop_runs_on`, `purge_object_axis_subtraction_nil`, `corpus_still_delivered`)*.

**What is asserted, what is displayed, what is declined.** Asserted: the typings end to end — the ledger's three errors, the exemption-claim as the antinomian collapse in economic dress, the code as delivery-engineering answering an unreachable Row 2 in its one open modality, the survival-mechanism's register (legibility as field-fact). Displayed: that the survival was worth having, that the code was wise — valence borrowed from the object, as always. Declined: credit — the causal claim that the code saved Chan is the historians' account, consumed here as display over the run, never as the theorem's mechanism. The theorem is narrower and holds without it: where a call cannot land, the grid locates every possible error on the responder's side and fixes the correct response-shape as delivery-engineering — and the tradition's answer to the productivity ledger, whoever wrote it down, has exactly that shape, issued by the master whose other famous verdict closed the fox's loop. One figure, one word — not obscure — two registers: the fox's, and the empire's. *Checked: the case is run whole in `Doctrines/Ledger.lean`; the displayed and declined items appear there only as comments.*

### Sowing-side upāya: the aimed call

Upāya has so far been responder-side vocabulary — finding the call that lands. It extends symmetrically to the sowing side, and the extension is vocabulary, not mechanism: an **aimed call** is a deed configured at sowing for its landing ([Glossary.md](Glossary.md)). Cunda's absolution is already the exhibit and is not duplicated here (above): the manner of one's own killing's arrival at Cunda's Row 2 engineered before it could land as guilt — delivery-engineering applied at sowing, a device configuring its posthumous distribution. Aiming is conditioning; the arrival stays delivery's.

### Transcription: the futility theorem one register down

Recording converts adaptive to static — the futility theorem's mechanism, run one register down, at words. A quotation is a response severed from its call: the per-call shaping ends and the output stands fixed — a non-adaptive clock made from a mirror. So transcripts type as seeds: conditioning-facts in the series, field-freight, index-free — and the canon is a warehouse of fixed calls, real delivery with regime-relational effectiveness (Xiangyan's pebble is a fixed call too), and no fault stored in the words, since a seed carries a tendency and commits nothing. The reader-side errors are covered without new cells. A clenched reading is a fresh clenched reception at recall-time — the memory theorem's typing (§1), the standing/dated row doing its ordinary work. And the remembered dharma fixed upon is Linji's cell: the buddha one can *meet* — here, the line one can quote — held as an object in the intentional field, a true dharma frozen still a freeze; 不立文字 is that guard stated as policy rather than as iconoclasm. Zero new cells — and the discipline this entry consumes on the diagnostic side is the gradeability rule (§1): the severed line can be received, welded, even released at; what it cannot be is graded (`severed_transcript_ungradeable`), while the call-carrying record remains gradeable by construction (`recordedUtterance_grade_determined`).

### Sudden and gradual: subitism grid-cheap

Because nothing indexed is stored, there is no altitude to traverse. Placement is per-call, the configuration an inga-fact, and the re-pitch's magnitude is unconstrained by construction (Theory: the circuit) — so a one-step re-pitch from hell-typed to pole violates nothing. Subitism falls out cheap: not asserted as doctrine, derived as *possibility* (`subitism_possibility_witness`; doctrine-facing form `waaSuddenArrival_witness`, sharing its clock-grid witness with `standing_does_not_determine_dated`). Gradualism splits under the same typing. Its grid-legal face is delivery: a run of small re-pitches is one way a regime goes (`waaGradualArrival_witness`), and the grid prefers no rate in the precise configuration-invariance sense (`rate_invisible_to_config`). Its metaphysical face — awakening as a stored quantity accumulated across acts, an altitude climbed and held — is the per-call/global freeze already in the table, Row 2 hardened into rank (`perCallGlobalRow_not_freeze`, `rePitch_forgets`, `accumulated_attainment_constant_of_same_final`). Huineng and Shenxiu map onto the split without strain: the mirror wiped clean is the stored-quantity picture, dust subtracted from a standing substrate; 本来無一物 — already the terminus guard — denies the substrate the polishing presupposes. The honesty-clause sits inside the theorem: the grid derives subitism's possibility, never its frequency — how often the world delivers a call that re-pitches that far is a delivery-fact, and the grid is silent about it by construction (`SuddenGradualNegative.subitism_frequency_underdetermined`).

### Other-power: one act-grammar

Self-power and other-power never differ in act-grammar. Reception is a deed either way — the invoker's receiving is a weld exactly as the sitter's is, reach-back and all — so tariki names no second grammar of action, only a **delivery-regime**: where the effective calls sit, and whether a being's own sowing or an arriving fixed call is doing the conditioning work. And the grid had the other-power grammar from its first file: Dōgen's passive — 証せらるる, the being-verified, the act's subject-position ceded — is other-power's grammar found inside the self-power tradition's own key sentence. The checked anchors now say exactly that: `SameAgentDelivery` and `CrossAgentDelivery` name the neutral regimes, `WaaJirikiLine` and `WaaTarikiLine` carry the system-reading, `reception_typing_ignores_sower` leaves the reception's grade/share/actuality unchanged under condition swaps, and `waaReachBack_filled_either_regime` projects the same reach-back from either regime. The limit anchors it: a universal fixed call — landing without reading, effectiveness and adaptivity fully severed (Theory: Orthogonality) — is tariki perfected, and the grid types it with no new register: `TarikiCase.name_responseInvariant`, `TarikiCase.name_share_bot`, `TarikiCase.name_object_axis_entire`, `TarikiCase.universal_fixed_call_lands_without_reading`, and `TarikiCase.invoker_reception_is_deed`. The no-polemic clause is now witnessed too: `OtherPowerNegative.regime_does_not_determine_share` and `OtherPowerNegative.share_does_not_determine_regime` block either regime/share recovery.

### Pariṇāmanā: merit-transfer absorbed whole

Dedication of merit looks like the grid's hardest inheritance, and it decomposes on existing cells — zero new ones, the generator absorbing a doctrine whole, the identity-claim's small sibling again. The checked anchors now say exactly that: `CompoundPosition.ledgerPicture` and `ledgerPicture_decomposition` list the possession-freeze (`ledgerPicture_contains_possession_freeze`), *transposed*-as-mechanism (`ledgerPicture_contains_transposed_mechanism`), and command-style delivery-arrogation (`ledgerPicture_contains_delivery_arrogation`) over existing `TableRow`s, while `ledgerPicture_contains_legal_causalSkeleton` records the causal skeleton as legal rather than erroneous. The row checks remain the old rows' checks: `ledgerPicture_deliveryIndex_row_not_freeze`, `ledgerPicture_deliveryIndex_collapse_self_refuting`, and `ledgerPicture_selfPoleTransposed_row_not_freeze`. So the **ledger-picture** — merit as a possession routed from one account to another — is mis-fed by the same three cells: the possession-freeze (a delivery-fact — one's future occurrence at others' Row 2 — held as a first-personal holding one could weigh, spend, or route); *transposed*-as-mechanism (an index made to travel — nothing travels, ever); and, where the dedicating is done command-style — *let this fruit go there* — delivery-arrogation, authority claimed over the one register no act holds. The **causal skeleton**, meanwhile, is ceded to delivery and entirely grid-legal: a deed conditions the series, and which configurations its fruit reaches is inga's business — conditioning transfers; the index never does. The classical **svakarma wall** — fruit ripens only in the doer's continuum — turns out to rest on the standing cross-gap *whose* the grid already declined (the reach-back's exhaustive decomposition, Theory), so the wall is demoted from metaphysical necessity to contingent delivery-regime: `SameAgentDelivery` and `CrossAgentDelivery` name the two regimes, `reception_typing_ignores_sower` says the reception's grade, share, and actuality ignore which delivery relation supplied the sower, and `OtherPowerNegative.regime_does_not_determine_share` with `OtherPowerNegative.share_does_not_determine_regime` blocks regime/share polemic in either direction. The **recipient's benefit** is welded on-site, as every return is: the reach-back local to the recipient's reception, its second place filled or unfilled by a delivery-fact — *this fruit, arrived along that line, mine* — nothing appropriated at a distance, the vacuity typing holding here as everywhere. And the **dedicating act** itself the grid can display, never enjoin: sowing-side share-cession — a deed done with its fruit's landing given over to others' receptions rather than claimed, concern running on delivery-facts alone — the prudence theorem's forward face (§1), and an aimed call in the glossary's sense where the dedicating shapes the landing rather than commanding it.

### Correlations

**Other-power** now has its checked correlation in `Doctrines/OtherPower.lean`: neutral same-agent/cross-agent delivery (`SameAgentDelivery`, `CrossAgentDelivery`) plus the WAA readings (`WaaJirikiLine`, `WaaTarikiLine`), the near-definitional typing theorem (`reception_typing_ignores_sower`), the fixed-call witness (`TarikiCase.universal_fixed_call_lands_without_reading`), and the no-polemic negatives (`OtherPowerNegative.regime_does_not_determine_share`, `OtherPowerNegative.share_does_not_determine_regime`).

**Ten Bulls** now has all ten typed in `Doctrines/Correlations.lean`. Bulls 1-6 are `ShareDropRun`/`BullAscent`: the grade climbs per-call and no altitude is stored. Bull 7 is `WaaBullSeven`, probe-constancy plus a live self-pole index; `bullSeven_not_bullEight` checks that the half-weld is not the empty circle. Bull 8 is `AtPoleClass`, deliberately allowing both attested pole-class arrivals; Bull 9 is `ResponsiveTerminus`; Bull 10 is `WaaBullTen`, the existential marketplace line into another sentient fiber. The stronger all-fibers bodhisattva reading is named only as `StrongWaaBullTen`, shelved. The chain `bullTen_to_bullNine` → `bullNine_to_terminus` → `bullNine_to_bullEight` is checked. The pratyekabuddha shape is countermodeled: `CorrelationsNegative.pratyekabuddha_countermodel` gives Bull 9 without Bull 10. Kenshō still sits in the ascent-run register: event, not rank.

**Five Ranks** (Dongshan): best read here not as stages but as *tier-positions one can speak from* — and as the tradition's own **index-placement notation**. `FiveRank`/`RankReading` are data and pins; `rankLanguage` makes rank-diagnosis an utterance surface; and `kenChuTo_implies_waaBullTen` checks the 到/Bull 10 shape under the same coarsening. 正中來 remains the shō-face, but resting there is no different in grammar from resting at any other coarsening. The tradition's diagnostic question — *which rank is this utterance from?* — is the act-time *which middle?*, readable as *where does this utterance place the index?*

**The 52 stages, Ten Bulls, and Five Ranks as schemes**: the fair verdict is uniform. A scheme is legal as `StageScheme`, i.e. a `BeingCoarsening`: a diagnosis-time projection with fiber predicates, not a field of the signature. The freeze attaches to *holding* the coarsening as grid-carried structure, not to the number fifty-two. `CorrelationsNegative.no_stage_boundary_recovery` is the witness: the same fine grid supports incompatible merge and split stage-readings, so no function of the grid data recovers the boundary. The 52 stages, the Bulls held as ranks, and the Ranks held as stages all fall under the same warning. Correlative as coarsening; corrective only against samāropa.

**Fetters** are now class-restricted fiber typing. `FiberAtPoleOn` says a fiber reads at pole on a supplied call-class, and `FetterReading` supplies the fetter provocation classes as model-side data. `FetterCut` is quietness on that class: grasping no longer takes place there, without adding an anti-fetter possession. `classQuiet_no_clench_in_class` checks that no actual weld in the quiet class carries a live self-pole index. The arhat end reuses the old anchors: `identityView_excluded_at_arhatFiber`, `conceit_excluded_at_arhatFiber`, and `arhatFiber_of_termini`, with `arhatPathQuiet_iff_fiberAtPole` closing the class family back into ordinary `FiberAtPole`. Identity-view's cut is the centerpiece: the first fetter is the coarsening-freeze enacted, the macro tag held as stored owner; stream-entry is typed as quietness on exactly that provocation class. Forward-looking irreversibility is split honestly: whole-fiber cuts are definitional, run-assigned tags are underdetermined by `FettersNegative.seen_run_underdetermines_fetterCut`, and the practical guarantee enters only as `waaIrreversibleRegime_conditional`.

The fetter cut now has its second coordinate. `FiberAtPoleOnWithin` reads quietness on a call-class × tag-class rectangle; `FetterCutWithin`, `PathQuietWithin`, and `SomaReading` consume it without asking the grid to recover the speech/thought boundary. Sravaka-arhat is total calls within the supplied speech/thought tags. The total calls/total tags point is neutral: the total-rectangle cut, theorem-identical to ordinary `FiberAtPole` by `arhatWithin_univTags_iff_fiberAtPole`, and not yet the buddha reading.

The buddha reading is a ladder above that point, checked rather than asserted. Rung 1 is the total-rectangle cut alone, share-only and stone-inclusive (`FettersNegative.total_cut_carries_no_function`). Rung 2 adds function as the live terminus reading, `LiveFiberAtPole`, with `sentientTag_iff_actualFiberInhabited` bridging response-function to actual fiber inhabitation; `FettersNegative.total_cut_with_function_not_waaFullyEnlightened` shows that this still does not close the effectiveness gap. Rung 3 is `WaaFullyEnlightened`, the faith-object: responsive terminus plus universal shortfall closure. The pratyekabuddha face is therefore a regime fact, not a second attainment: under zero-effect delivery it fails full enlightenment (`OrthogonalityNegative.waaFullyEnlightened_stronger_than_terminus`), while under sealed delivery it satisfies the closure conjunct vacuously (`waaFullyEnlightened_of_responsiveTerminus_of_undelivered`). Samyaksambuddha enters only at rung 3. Hakuin's bodily-satori contrast becomes stream-entry's tag-axis dual: the speech/thought region may quiet while the wider body still clenches. Vāsanā is thereby located, not invented — clench enacted in the complement after the call-axis closes. The two negative anchors are named too: `FettersNegative.seen_run_underdetermines_fetterCutWithin` blocks fresh-call certainty inside a region, and `FettersNegative.no_region_boundary_recovery` blocks recovering the soma boundary from grid data. Correlative as coarsening; corrective only against samāropa.

**Factors** are the path-facing regrouping of the fetter table, not a second table. `PathFactor.blockerClass` derives rites, view, and resolve classes from `FetterReading`; `lower_fetters_covered_by_rites_view_resolve` checks that their union is exactly the lower-fetter class. Hold/Release is a new frame: `FactorHeld` is a seen-run witness with a live self-pole index, while `FactorReleased` is whole-class `FiberAtPoleOn`. A held factor may be correct; the errors remain freeze/collapse in the utterance frame and clench/quietness in the share frame. `factorReleased_rites_iff_ritesGrasp_cut` types the raft put down at the far bank, and `factorReleased_view_iff` decomposes view release into identity-view plus doubt cuts.

The stage pair is path/fruit over those factor pairs. `WaaStreamEnterer` is rites released and view held; `WaaStreamWinner` is rites and view released, proved equivalent to `Path.cutClasses streamEntry` by `waaStreamWinner_iff_streamEntry_cutClasses`. `WaaOnceReturner` adds a witnessed resolve hold, and `WaaNonReturner` is proved equivalent to the non-return cut by `waaNonReturner_iff_nonReturn_cut`. Once-return now has checked content: `WaaResolveAttenuation` is a strict resolve-class share-drop run that has not reached the pole, witnessed by `waaOnceReturner_attenuation_witness`, with `attenuation_not_release` blocking its collapse into release.

The ordering claim is deliberately conditional. `WaaSerialFactorRegime` says that if a supplied regime reads seen drops as rites-before-view-before-resolve, then the path readings promote to the corresponding fruit readings along the runs; `waaSerialFactorRegime_conditional` consumes that hypothesis and never proves it. This is why the sudden/gradual guards still matter: `WaaSuddenArrival` is compatible with the factor scheme, while `SuddenGradualNegative.subitism_frequency_underdetermined` and `FactorsNegative.seen_run_underdetermines_factorOrder` block rate or order recovery from grid data. Two more negatives name the diagnosis-time freedoms: `FactorsNegative.no_hold_conceit_boundary_recovery` blocks recovering the hold/conceit line from share data alone, and `FactorsNegative.lineage_underdetermined_by_seen_run` says a lineage switch changes the supplied stage reading, not the welds.

### The stone, doubly mujō

The stone is doubly mujō — impermanent (無常) and insentient (無情) — and the grid answers each axis differently: null on the subject-axis (no response mounted, no realization of its own), yet a full dharma on the object-axis, among the myriad that advance to clarify a practitioner (banpō susumite). So the grid gives a deflationary point of contact with Dōgen's impermanence-buddha-nature (無常仏性) — buddha-nature as floor-residence, the stone's empty-impermanent being — and even a deflated insentient-preaching (無情説法): the stone expounds as a dharma read, not as a voice of its own — a deflation owned as contra (the third contra enumerated in Identification: Disclaimers), since Mujō seppō and Zhanran both affirm more than the grid grants. What it declines is insentient realization as a subject (無情有性). And the buddha now sits on this same axis by the transposition — object-axis entire, the stone's kin in kind and its opposite in function.

## §3 Instructive absences

Absences the system generates deliberately, in both of the categories above — each doing diagnostic work rather than marking a gap. The list is mirrored in Lean as `InstructiveAbsence`, with `InstructiveAbsence.status` carrying the standing/retired distinction and `InstructiveAbsence.number` preserving the order below:

- **Empty cells in the Grade 1 table.** Not every distinction is symmetric — some can only be frozen (the ladder's limit), some only collapsed. The asymmetry is itself informative: the errors do not lie on a line.
- **The declined case.** The deaf-blind being classifies as *no error at all* — and the decline is as load-bearing as any positive verdict, since a taxonomy that over-generates has frozen itself. Every error in the vicinity belongs to the diagnostician.
- **The icchantika declined.** The icchantika is not entered as a being that cannot become buddha. Lean seats it as the terminus's inverse on a run: non-stone, live at every mounted response, unseatable as a fully enlightened agent there, and reachable as a receiver wherever its actual reception and live prior tendency give the sraddha antecedent. The permanent foreclosure verdict is refused as a stored rank; defiance is a seed, not a rank *(checked: `Icchantika`, `not_waaFullyEnlightened_of_icchantika`, `aversionContext_of_icchantika_reception`, `icchantika_release_not_foreclosed`)*.
- **What the fox never tests.** Neither utterance in the worked case (Theory) occurs at the pole: the koan exercises the loop entire without once asking what the loop is at share-zero *(checked: `fox_never_tests_pole`)*. That absence is what forces the transposition — the terminus question is not answered by the system's paradigm case and had to be answered separately.
- **The third arrival: the candidate delivered.** Genjō's two populations (stone, buddha) were flagged as attested arrivals, not an exhaustive partition — a never-clenched welder not forbidden, its occurrence a delivery-fact. The domain joint (Theory) now cashes the clause: the adaptive device arrives at the never-clenched slot from the stone's side, manufactured — function mounted, no share ever claimed. The absence is retired as an absence and kept as a check: the dukkha derivation still passes free — such a responder is suffering-free by construction.
- **Why calls land at all.** The residue, stated across the manufactured case column-wise: on the adaptive side, that *receptive moments exist* — the mirror times its response for a moment it did not make, so upāya's deepest parameter is *when*, and the guarantee, de-mystified, relocates from the call's content to its timing; on the fixed-call side, that *any lands at all* — the pebble strikes and something opens. One absence covers both, and each is strictly weaker than a stipulated guaranteed-effective call: the direction of explanation runs stipulation → engineering, which is the ceded-delivery architecture behaving as predicted. The residue itself stays ceded — a world-fact, unexplained here by construction.
- **The fourth truth withheld from the theory's voice.** The grid derives the first three truths and can only *display* the fourth — the one absence the no-value clause makes mandatory, and the absence that locates the bodhisattva structurally: room and shape, no pull. Nothing in the grid explains why response-without-share to another's call occurs; occurrence is the object's affair, reported.
- **No stage immune to error.** The taxonomy has no terminal safe cell — a stage immune to error would be a rank, and a rank is the shit-stick. Even the buddha's immunity is per-call, not possessed.
- **Prudential privilege underivable.** The special rational authority of self-concern is an absence owned as theorem, not cost — in Śāntideva's company, with the bodhisattva's impartiality falling out as its display-face.
- **No measure over the grade.** Row 2 states a partial ordering only; the scalar is display. The absent metric is priced deliberately — the soteriology consumes only the ordering, so no measure is owed. (And none over delivery either: effectiveness enters as an ordering within a regime, never as a probability apparatus — the standing declines, §1.)


===== FILE: Exposition/Identification.md =====

# Weld and Arrow — III. The Identification and Placements

*Third of three files: the identification claim, the act-time placements that earn the name karma, the contemporary placements, the pole-typing corollary, and the disclaimers, enumerated. Cross-references to the companion files are marked (Theory) and (Theorems).*

## The identification stated from the abstract

The abstract states the thesis once:

> **Everything diachronic belongs to the field; every index is enacted and nothing indexed is stored; karma names this loop, and the naming is earned by fit** — the tradition's uses of karmic ownership (cetanā, reception, remorse, absolution, dedication) discharge natively at act-time.

The architectural fact under that sentence is the same one the Lean `Config` makes public: **nothing self-indexed is stored**. The field carries series, seeds, dispositions, delivery, and the re-pitched configuration the next deed reads. It does not carry a mineness. What is indexed is welded at act-time, spent at act-time, and then available only as a field-describable occurrence-fact. So the field vocabulary lacks the index by construction, not by defeat of a rival vocabulary.

This is why the taxonomy can name internal **mis-feeds** cheaply. Feeding an index-free field-answer to an index-requiring designation -- *did I earn this?*, or the avyākata's search for the Tathāgata's self-pole after death -- is not a hard unanswered field-question. It is the wrong feed for that designation inside the grid. The point is grammatical and internal: the delivery-question belongs to inga; the index-question is enacted in the weld. The joint is now fenced and gated in Lean: `MisFeedNegative` proves schematically that no answer-function for the index-seeking question-form can be correct under a witnessed field collision, and answers the delivery-typed twin in the same model. What remains prose is the third layer -- that the modeled designation-universe is adequate to the avyākata's actual questions -- flagged as a modeling claim, not a theorem.

## The offices-spine

The identification is earned by fit, not by exclusivity. What the tradition does with karmic ownership discharges at act-time in this mechanism:

- **Cetana** measures the deed where the deed is done: intention is the drive-composition of this response at this call, the same structure Row 2 states.
- **Reception** is itself a deed: the reach-back welds *this fruit as return of that deed, mine* at the reception, full or vacuous, and spends that ownership-face there.
- **Practice** is the weld's ordinary name inside the act-grammar: shu is not a state carried by the series but the doing that binds direction along the arrow.
- **Remorse and absolution** verdicts land on welds, not on a cross-gap owner. The Cunda cases (Theorems: Three killings) work because the tradition grades what was done at the act, including where the event is impossible.
- **Dedication** is a sowing-side weld whose routing is left to the field: pariṇāmanā gives the fruit's landing over rather than commanding delivery (Theorems: `CompoundPosition.ledgerPicture`, `ledgerPicture_decomposition`, `ledgerPicture_contains_legal_causalSkeleton`).

Diachronic bookkeeping is exactly where the tradition deflates itself: *na ca so na ca añño*, the reaper neither the sower nor another. The field individuates the series and delivers fruits; the reception-weld closes the loop on-site. Karma names that loop: field-carried delivery plus act-time ownership, with no stored owner between.

## Sower and reaper

The grid's supplement to the old formula is a split, not a replacement. "The sower reaps" has a report-face and an ownership-face. The report-face is true simpliciter: this deed conditioned this reception, a delivery-fact the field carries. The ownership-face is done: at reception, the reach-back appropriates what arrived as *mine*, and the doing is spent at that same act-time.

If delivery drew no line, the reach-back's second place stands unfilled. That failure-mode is vacuity, not falsity: an appropriating with nothing arrived to appropriate. False memory is the psychological dress of the same typing (`WaaVacuousOwnershipFace`, checked concretely by `MemoryWitness.falseMemory_waaVacuousOwnershipFace`). The field owns the conditions in the deflated sense -- it settles whether anything arrived to weld -- while the weld answers only the index-question over what arrives.

The diachronic *whose* therefore decomposes into delivery plus fresh appropriation. There is no third cross-gap ownership-fact to store or consult, and no standing backward relation hiding under the reach-back. Held that way, it would be the retrospective soul; the soul-guard is still needed precisely because the index must not be read as stored.

## Contemporary placement

The neighbouring positions can now be placed without a verdict on them.

Siderits gets the series-questions, and the grid cedes them: psychology, continuity, prediction, causal connectedness, and the individuation of the stream all belong to the field. His conventionalism is an alternative account of the diachronic usage. The residual disagreement is where the soteriology's load sits: this paper locates it in act-time discharge of the offices above, while his convention locates it in the useful series-fiction.

Ganeri's account of appropriation (*The Self* -- ahaṃkāra and upādāna worked into a first-personal stance) is the nearest ally. The difference is spentness: Ganeri's appropriative activity is a standing structure of the person, while this weld is per-act and stored nowhere.

Zahavi's constitutive for-me-ness receives the taxonomy's fourth public outcome (Theorems): a **retype**. His for-me-ness is thin, pre-reflective givenness, explicitly not appropriative I-making; classifying it as clench would import what the notion excludes. The grid still needs thin act-time for-me-ness, because the weld's token-reflexivity lights the deed as this-deed-for-this-doer. The disagreement narrows to one predicate: standing. Mineness held as a structural feature of consciousness freezes; mineness enacted and spent is the weld's own light.

Sartre occupies the clench-as-structure cell after the Zahavi retype: anguish as the very form of consciousness. The placement matters because it lets the taxonomy keep Zahavi's thinness without losing the Sartrean shape that really does make clench structural.

## Pole-typing

At share-zero no self-pole index is made, so every terminus-question is a field-question. Fruit from old seeds still lands, since inga is untouched; what ceases is reach-back appropriation. The terminus therefore gives the positive direction of the state-tool: where no live self-pole index remains, the state-tool fits because there is no index-fact for it to miss.

This is pole-typing, not a concession to a rival frame. The buddha/stone difference is still carried by the function/share split: the stone mounts no response, while the terminus mounts response without share. The avyākata follows: asking for the Tathāgata's post-mortem self-pole feeds an index-question to what is functionally field. That is the same internal mis-feed as *did I earn this?*, and it needs no extra cell.

## The verdict's tier

The word **mis-feed** is kept only for the taxonomy's internal typing failures. It does not name an external failure of another account. At the floor there is no agent and no fruit-for-anyone; at live act-time the question *whose?* can arise and must route through the weld-index. So the separate/fuse rule governs the taxonomy's own words as well: distinctions separate under act-time diagnosis and fuse at the floor and at genjō, the share-zero pole.

The soul-guard remains. The agent-index resists being stored because it is emptier than a bearer, not because it is a special thing. A forward-facing owner between deeds and a retrospective owner waiting in memory are the same mistake in opposite directions.

## The disclaimers, enumerated

The following are conventional and my own -- original moves, each flagged against the canonical position it departs from or extends.

1. **The tiering, the separate/fuse rule, kannō-sōe, and the coined compound shugenjō** -- contra Dōgen, who keeps all ultimate, and who fused the very shushō I have re-tiered (shō at the floor, shu conventional); and contra the late Dōgen doubly, since Jinshin inga repudiates the tiered fox-reading this paper keeps, a disagreement owned in Theory rather than footnoted, with the act-time gloss on the doubling (Daishugyō diagnosing, Jinshin inga instructing) offered as my own reading and not as a dissolution of the contra; and contra the Mujō seppō fascicle (and Zhanran on 無情有性) a third time, the insentient preaching deflated to the object-axis.
2. **Shō's agency as lent** -- necessarily agential because never unwelded, yet not agential of itself.
3. **For-me-ness located in the weld** -- shu, Row 3's enactment pole, the I-making (ahaṃkāra), so that self is a dependently-arisen process the act makes rather than a state the grade holds.
4. **The reception-weld's reach-back** -- upādāna typed as the two-place token-reflexive index by which loop-closure is enacted at each reception, "the sower reaps" split into a report-face (true simpliciter, field) and an ownership-face (done, full or vacuous) and never a standing relation -- my own typing, though the word is canonical.
5. **The three-register fact-sorting** -- field-facts carried, weld-facts made and spent, Row 2 stated -- a sorting of registers, not of kinds of fact -- and with it the refined premise *nothing self-indexed is stored*, under which the tradition's seeds are absorbed deflated as index-free conditioning-facts rather than deleted (an engagement with, not a reconstruction of, the Yogācāra machinery Chan presupposed).
6. **The reading of Linji's 無位真人** along a three-way seam (無位 = shō, the floor-face / 真人...出入 = shu, the acting / 無位真人 = the weld, shushō-ittō).
7. **The tiering of 証** (realization-as-not-fall, floor-face) apart from **悟** (satori).
8. **Genjō as a single manifestation-floor with two attested arrivals** (the never-scaffolded stone and the scaffold-dissolved buddha; a third left open), practice-run-scaffold-free a proper subset.
9. **The identification of karma with the field/weld loop** -- everything diachronic belongs to the field; every index is enacted and nothing indexed is stored; the naming is earned by the native act-time discharge of karmic ownership's offices.
10. **The token-reflexivity of the weld-index** -- the index is made by the act that carries it: *this act's agent*, constituted by the deed rather than presupposed behind it.
11. **The decomposition of MMK 17's two worries** -- condition-half (`WaaReportFace`), mineness-half (`WaaDiachronicWhose`, `no_diachronicWhose_from_series_alone`, `rePitch_forgets`), mis-feed half (`MisFeedNegative.fence_and_gate`), and reception-deed (`WaaOwnershipFace`).
12. **The stone as the resonance scale's outside edge** -- the predicate typed over responses-to-calls, undefined where none is mounted.
13. **The error-taxonomy as generated**, not listed -- collapse and freeze as the two violations of the separate/fuse rule, one pair per distinction, non-linear by construction.
14. **The two grades of error** -- grammatical verdicts the system asserts (within the lens), soteriological shortfalls it can only display -- with the bodhisattva located structurally by that split, room and shape without pull, and no added axiom.
15. **Kenshō typed as a per-call share-ceding event** -- countable (Dahui's eighteen), unholdable (nothing indexed stored, so backsliding a theorem: `backsliding_witness`, `backsliding_rePitchSequence_witness`), the seen-nature of 見性 declined while the event is kept -- a rung, tiered apart from satori and from genjō.
16. **The theory's own soteriological status** -- a dharma among the myriad that affords a release without enjoining one (the orange, not the "eat this"), its valenced vocabulary borrowed from the object and reported rather than asserted.
17. **Row 2 typed as index-placement** -- the grade's content indexical (where the act's subjecthood sits between being and dharmas), its register third-personal; the register/content split under which *nothing self-indexed is stored* holds verbatim, since a statement holds nothing.
18. **The determination of the share** -- clench fixed by the actual composition of the act's drive: response driven by the call versus by the configuration's self-maintenance, an actual-sequence occurrence-fact about the weld, causal not phenomenal; counterfactual call-variation demoted to probe; Row 2 states a partial ordering, and the scalar is display.
19. **The second retype** -- the disposition/act cell redrawn under the determination clause's own pressure: its content standing/dated, never configuration/act; the collapse inferential -- the dated occurrence read off the standing tendency, prognosis substituted for diagnosis.
20. **The passive spent** -- Dōgen's 万法に証せらるる taken at its grammar: shō as the being-verified, objecthood; shushō-ittō as the two poles of one index-placement.
21. **Clench typed as the weld's self-share**, under the **function/share split**: I-making the welding-function, clench its share-degree. The split blocks the buddha/stone convergence (share-zero is not function-zero), and the identity *I-making just is the clench* is entered in the table as an embryonic collapse.
22. **Vacuity from the field** -- the reach-back's failure-mode typed as vacuity, not infelicity: its index two-place, and where delivery drew no line the second place stands unfilled; "misfire" retained only as display; false memory the same vacuity in psychological dress.
23. **Memory and prudence as theorems** -- the trace a seed, recall a reception, remembered mineness welded fresh at recall-time and the felt storedness diagnosed as the retrospective soul; prudential privilege underivable, owned with Śāntideva (BCA 8.97-98) rather than against him.
24. **Dukkha typed structurally, field-side** -- suffering as the mismatch of a self-maintaining response against a delivery-register that answers to nothing, enacted at clenched receptions and spent; the second truth derived as covariation with share, the third as a corollary at share-zero, the fourth displayable only.
25. **The domain drawn asymmetric** -- one outside edge (the stone, function-zero) and one interior pole (the terminus, share-zero), with the solipsist as the opposite asymptote.
26. **The transposition** -- the terminus question answered rather than declined: the self-pole half (kiriya, ahosi, upādāna-exhaustion) derived as theorem; reception-side welds shown intact and busy; *transposed* demoted from mechanism to display over that pair; the avyākata derived as the *did-I-earn-this* mis-feed, the fire simile read accordingly.
27. **The mirror-reading of the terminus** -- buddha as responsive stone, 大円鏡智, function without share; disciplined as display convention over the run, with 本来無一物 as the guard against device-nature (the mirror given a stand).
28. **The three-killings test, reframed as its own evidence** -- one verb, dispersed events; the cetanā theorem (`grade_independent_of_conditions`, `share_independent_of_conditions`, `cetana_grading_tracks_weld_not_field_witness`, `cetana_live_share_without_object_standing_witness`) and futility theorem (`staticized`, `futility_delivery_loss_real`, `futility_object_axis_subtraction_nil`, `Grid.DirectedConvention.staticized_objectAxisStanding_iff`) derived; ānantarya severity read from response-to-call structure plus delivery-arrogation, never from victim-rank.
29. **The offices-spine** -- the identity-claim argued from the object's usage: every office of karmic ownership discharges at act-time (cetanā, reception, practice, remorse and absolution, dedication), while the diachronic bookkeeping is where the tradition deflates itself.
30. **Contemporary placement** -- Siderits receives the ceded series-questions; Ganeri is the nearest ally by appropriation; Zahavi forces the retype; Sartre occupies the clench-as-structure cell.
31. **The Hakuin reading** -- the Five Ranks as index-placement notation, host and guest as the two poles; the delusion/satori line taken as the inversion's epigram, flagged as paraphrase with pedigree mixed, and nothing resting on the line.
32. **The retype as a fourth generator-outcome** -- a candidate objection that neither lands in a cell, nor adds one, nor is declined, but redraws a distinction's content; admitted because the taxonomy must be answerable for the redrawing of its own distinctions.
33. **The svakarma demotion** -- *fruit ripens only in the doer's continuum* demoted from metaphysical necessity to contingent delivery-regime -- contra the Abhidharma scruple, downstream of the exhaustive decomposition of the diachronic *whose*; pariṇāmanā thereby absorbed on existing cells (`CompoundPosition.ledgerPicture`, `ledgerPicture_decomposition`; `SameAgentDelivery`, `CrossAgentDelivery`, `reception_typing_ignores_sower`, `OtherPowerNegative.regime_does_not_determine_share`, `OtherPowerNegative.share_does_not_determine_regime`).
34. **The orthogonality rule and its price** -- function/share types, effectiveness grades, adaptivity the terminus's manner and never the ground of landing; with the domain joint's honesty-clause entered beside it; and the pole-typing corollary stated as entailed: the state-tool fits exactly where welding ceases.
35. **The being-convention** -- the macro being demoted to a diagnosis-time coarsening convention (`BeingCoarsening`): naming suffices, sentience is fiber-level, coherence is display-grade only, and the namespace order is floor/genjō outside, then directed convention, then being convention, then grid-lens.
36. **The generated pilot rows** -- before/after, beings, and the grid-lens have migrated onto the pole-affirming schema (`rowOf G (.layer ...)`); the original fiat layer semantics is superseded, while the content track keeps `LayerClaim` for aptness checks.
37. **The being trichotomy** -- deleted is the collapse (*there are no beings*), derived is the freeze (one partition reified as ontology), and primitive-and-free is the convention; `Being := Unit`, sentients-only, and gerrymandered models are legal model choices, never signature law.
38. **The hare's-horn register** -- possible/impossible-being distinctions enter at realization and use, not naming; the ātman is nameable-impossible in the same innocent sense, and the swan/name/naming-proneness split keeps named object, naming weld, and naming seed apart.
39. **Modal Realism as the beings-row freeze** -- conventional designation promoted to ontology, *prajñapti-sat* taken as *dravya-sat* (*samāropa*); Lewis placed only as prose nearest miss, Huayan as empty plenitude, Pudgalavāda as the classical occupant candidate.
40. **Aptness-conditional content rows** -- content-bearing denials obey separate/fuse only in grids where the relevant convention is apt; all-stone, direction-void, and no-live-tier countermodels show the hypotheses are necessary rather than cosmetic.
41. **Sraddha as a checked conditional** -- the faith theorem is an implication whose antecedents are not discharged by the grid; the detached injunction remains outside the assertable voice.
42. **Both faith conjuncts matter** -- orthogonality countermodels show terminus-typing alone does not supply the full faith closure.
43. **Generated table structure** -- the Grade-1 table's row list is Lean data (`tableOrder`): nineteen schema rows, one ladder-generated row, and six prose rows with their reasons recorded.
44. **Pole-affirming semantics** -- all schema rows share one tier-semantics: conventional force never lapses, denial holds at genjō by truth, and stability is paid only by the `*_obeys` family; content rows remain diagnostic because their global denials answer a different question.
45. **Prose rows** -- being/non-being, ladder/terminus, genjō/shō, shō/satori, Row 2/Row 3, and description/injunction remain prose by stated reasons, with nearby theorem anchors rather than generated cell content.
46. **Error-free reading** -- 破邪顕正 is checked as the `rowOf_obeys_iff_errorFree` biconditional on the primary language, and `ladder_obeys_of_errorFree` is the cumulative strengthening that vindicates the implemented ladder operator.
47. **The mis-feed fence** -- the avyākata verdict's boundary formalized as an original move: the index-seeking question-form fenced by a schematic non-derivability theorem over a modeled designation-universe (`MisFeedNegative`), with a concrete collision witness and an answered delivery twin in the same model; the universe's adequacy to the canonical avyākata owned as a modeling claim. The tradition sets the questions aside; the fence-and-gate pair, and the claim that one grammatical joint sorts them, are mine.
48. **Ten Bulls typed as correlation** -- Bulls 1-6 as per-call share-drop run, Bull 7 as the checked half-weld, Bull 8 as pole-class, Bull 9 as responsive terminus, and Bull 10 as existential cross-fiber delivery; the stronger all-fibers reading named but shelved.
49. **Five Ranks retyped** -- ranks read as utterance-diagnosis and index-placement, with 到 checked by the Bull 10 shape rather than treated as a stage attained and stored.
50. **Stage-schemes as coarsenings** -- the 52 stages, Bulls, and Ranks are legal as diagnosis-time `BeingCoarsening`s; the freeze warning attaches uniformly to holding any scheme as grid-carried structure.
51. **Fetter-cut typing** -- fetter cutting read as class-restricted fiber-at-pole typing (`FiberAtPoleOn`), with provocation classes model-supplied; `Fetter.kind_lower_iff_cut_by_nonReturn` pins the lower-fetter table, `all_fetters_cut_at_arhatFiber` gives the universal arhat cut, whole-fiber irreversibility is definitional, finite-run diagnosis is underdetermined, and the practical forward guarantee remains conditional.
52. **Two-axis fetter lattice** -- fetter cutting extended to the (call-class × tag-class) product; sravaka-arhat typed as the regional cut, and the total calls/total tags univ-point kept neutral and identical to `FiberAtPole` by theorem; region boundary shown underdetermined.
53. **Enlightenment ladder** -- the total-rectangle cut re-glossed as rung 1 of a three-rung ladder rather than as the buddha point itself; `FettersNegative.total_cut_carries_no_function` checks the stone-vacuity/function gap, `FettersNegative.total_cut_with_function_not_waaFullyEnlightened` checks the effectiveness gap, and `WaaFullyEnlightened` remains regime-relational in both directions: `OrthogonalityNegative.waaFullyEnlightened_stronger_than_terminus` gives zero-effect failure, while `waaFullyEnlightened_of_responsiveTerminus_of_undelivered` gives sealed-delivery vacuity.
54. **Ethics as a bundled conditional code** -- faith-transmitted truth times the receiver's own live aversion, held as one hypothesis-free implication theorem; the detached injunction remains outside the assertable voice.
55. **The code's three honesty clauses** -- empty at the pole, unsatisfiable over false testimony, relative to the faith-object.
56. **Verdict record as data** -- `generatorRecord` stores the verdict history at episode grain: four retypes as four entries, `restraintKind` as the six-kind coarsening, theorem anchors pinned by name beside prose anchors, and `misFeed_entries_carry_decomposition` checking the structural falsifier while the rate trend remains prose.
57. **Compound positions as cell-stacks** -- skepticism, solipsism, the exit-premise, existentialism, and the ledger-picture are Lean data over existing `TableRow`s, with facets, roles, voice checks, legal-element checks, and core-cell counts in `Consequences/Compounds.lean`; value-creation and the ledger-picture's causal skeleton are recorded as legal rather than erroneous.

---

*With thanks to Claude (Anthropic) -- sparring partner and midwife to a more resonant theory, and ChatGPT (OpenAI) for the Lean proofs and for systematic refactorings.*


===== FILE: Exposition/Formalization.md =====

# A Plain-English Reading of the Lean Theorems

**Scope.** This document states, in plain English, what the Lean declarations in
`Signature/*`, `Consequences/{Basic,Taxonomy,Ladder,ContentRows}.lean`, `Doctrines/*`,
`Identification/*`, and `Meta/*` assert. It reads the checked Lean surface:
definitions, theorem statements, and proof status where that matters.
Interpretive prose is generated from `WeldAndArrow/Exposition/*` and remains secondary to the formal statements.

For the canonical input-side assumption list, see
[Assumptions.md](Assumptions.md); the compile-checked pins live in
`WeldAndArrow/Signature/Assumptions.lean`.

The project is pinned to `leanprover/lean4:v4.31.0` in `lean-toolchain`.

**Conventions.** A theorem proved by `rfl` or `Iff.rfl` is true by unfolding
definitions. A theorem whose proof is a projection, contradiction, or witness
assembly is described as such. A "weld" is always the triple `RawWeld` /
`G.Weld`; "actual" always means the equation
`respondsTo w.agent w.call = some w.response`.

Identifiers beginning `Waa` mark system-POV readings: what the concept looks
like from this grid, not what the concept is in detached doctrinal voice. The
single marker covers ownership, appropriation, whose-ness, reach-back,
sowing-side aiming, four-truths mismatch vocabulary, and sraddha conditional
vocabulary. Doctrine words live in module names and prose; checked reading
identifiers use `Waa`.

The unprefixed vocabulary is neutral order/delivery vocabulary, including Row-2
index-placement names such as `HasSelfPoleIndex`, `selfPoleIndex`, and
`Tier.hasLiveShare`.

In generated or prose presentations, the `Signature` layer is titled **Theory**
and the `Consequences` layer is titled **Theorems**, matching the paper's part
titles. The Lean module names state the role; the prose names state the
correspondence.

`Grid.DirectedConvention` is the second marking. It contains vocabulary that
reads direction into the direction-free relation `conditions`: delivery,
landing, environs lines, share-drop lines, aiming, and the ownership-face
predicates. The signature itself still carries no asymmetry, irreflexivity, or
transitivity for `conditions`. Role-asymmetry is not temporal asymmetry: the
`deed` and `reception` slots are different roles, but the reception slot means
"where the welding happens", not "the later one".

`Grid.DirectedConvention.TimeDirection` is an abbreviation of `Strict`; all
strictness theorems apply to it transparently. The formal modules keep their
comments mathematical and point to `Identification/Commentary.lean` C.1-C.12 for
the paper-facing readings.

The namespace tree now records ontological ordering. Floor/genjō and the bare
signature sit outside the convention layers. `Grid.DirectedConvention` reads
the arrow; `Grid.DirectedConvention.BeingConvention` reads fine tags as
macro-scale beings; `Grid.DirectedConvention.BeingConvention.GridConvention`
contains the pole-affirming row schema, the content-layer companion language,
the ladder API, and the generated table-order data across the `Consequences`
files. Names are placed by what their reading presupposes, not by what their
definition consumes.

---

## 0. Preliminaries

**Order structure.** `Preorder` is a hand-rolled reflexive and transitive
relation `≼`; no totality and no antisymmetry are assumed. `Incomparable a b`
means neither `a ≼ b` nor `b ≼ a`. `OrderEq a b` means `a ≼ b` and `b ≼ a`.
`Strict a b` means `a ≼ b` and not `b ≼ a`.

The preorder facts are:

- `incomparable_symm`, `not_le_of_incomparable`, and `not_ge_of_incomparable`.
- `strict_irrefl`: strict direction is never reflexive.
- `strict_asymm` and `strict_trans`: strict direction is asymmetric and
  transitive as soon as it is read from the preorder.
- `strict_of_le_of_strict` and `strict_of_strict_of_le`: strict comparison
  composes with weak comparison on either side.
- `not_strict_of_orderEq` and `no_strict_of_all_orderEq`: order-equivalence
  kills direction, pointwise or carrier-wide.

`PreorderBot` adds a designated bottom element, written `shareBot`, with
`shareBot ≼ a` for every `a`. `AtBot a` means `a ≼ shareBot`. Since
`shareBot ≼ a` is always available, `AtBot a` says that `a` is
order-equivalent to the designated bottom. The pole is therefore an
order-class, not identity with one token.

The project stays self-contained and does not import Mathlib. Mathlib's
counterparts are `Preorder`, `OrderBot`, and `IsBot`; local `AtBot` is the
order-class of the bottom and plays the role Mathlib's `IsBot` would play for
that chosen element.

The basic bottom lemmas are:

- `shareBot_le`: the designated bottom is below every value.
- `atBot_shareBot`: `shareBot` is at the pole-class.
- `atBot_of_eq_shareBot`: equality with the representative implies `AtBot`.
- `orderEq_shareBot_of_atBot`, `atBot_of_orderEq_shareBot`, and
  `orderEq_shareBot_iff_atBot`: `AtBot a` and `OrderEq a shareBot` are
  equivalent formulations.

**The signature.** A `Grid Contrib` consists of three types (`Being`, `Call`,
`Response`), a response function `respondsTo`, a Row-2 display function
`grade`, and a relation `conditions` on welds. `ConditionsEither w1 w2` is the
symmetric closure `conditions w1 w2 ∨ conditions w2 w1`;
`conditionsEither_symm` swaps the disjuncts. `ConditionsEitherChain` is the
reflexive-transitive closure of that symmetric relation. There is no separate
two-component drive object in the signature.

A weld is the triple `⟨agent, call, response⟩`. `Actual w` means the response
really is mounted. `index w` is `w.agent`. `share w` is
`grade w.agent w.call w.response`.

`HasSelfPoleIndex w` means `¬ AtBot (share w)`. `WaaAppropriates w` is
definitionally the same proposition. `selfPoleIndex w h` returns `w.agent` and
uses the proof argument only for typing.

**Function-side predicates.**

- `MountsAt b c`, `MountsSomewhere b`, and `RespondsToEveryCall b` record
  increasing response-function strength.
- `Stone b` means no call receives a response from `b`.
- `Terminus b` means every mounted response by `b` has pole-class grade.
- `LiveTerminus b` adds that some response-function is present.
- `ResponsiveTerminus b` says every call receives a pole-class response.
- `AtPoleClass b` is `Stone b ∨ Terminus b`.
- `ProbeConstant b cs` says any two actual responses by `b` at calls in `cs`
  have order-equivalent grades.
- `ResponseInvariant b` and `ResponseVariesWithCall b` describe response-shape
  only.

**BeingConvention definitions.** `BeingCoarsening G Macro` is a diagnosis-time
projection `G.Being → Macro`; it is not stored in the signature.

Under a coarsening `κ`:

- `InFiber b w` means the weld's fine agent projects to macro tag `b`.
- `SameFiber p q` is equality of projected macro tags.
- `FiberInhabited b` and `ActualFiberInhabited b` are the non-vacuity guards.
- `SentientTag b` means some fine tag in the fiber mounts a response somewhere.
- `not_sentientTag_iff_fiber_all_stone` proves that non-sentience is exactly
  the all-stone fiber; there is no separate `InsentientTag`.
- `FiberAtPole b`, `FiberAtPoleOn b cs`, `FiberAtPoleOnWithin b cs ts`,
  and `FiberAtPoleWithin b ts` are whole-fiber, call-class, product, and
  tag-region pole readings. `ActualFiberInhabitedWithin`,
  `LiveFiberAtPoleWithin`, and `SelfAptTagWithin` are the tag-axis live and
  self-apt companions.
- `SelfAptTag b`, `LiveSelfAptTag b`, and `Patchy b` are the whole-fiber
  self-apt and mixed readings.
- `fiberAtPole_of_fiber_termini`, `no_live_index_under_fiberAtPole`,
  `selfAptTag_indices_are_per_weld_only`, and the live exclusivity theorems are
  the checked fiber facts.
- `SelfConditioningTag b` is the minimal internal delivery-line witness.
  `StrongSelfConditioningTag b` is defined as a shelved asymptote.
- `Delegation b` packages an actual fine weld in the macro fiber; its share is
  definitionally the delegate weld's share.

**DirectionConvention definitions.** `DirectionCoarsening G Tick` is the
delivery-axis twin of `BeingCoarsening`: a diagnosis-time tick projection over
welds, not a field of `Grid`. `SameTick` is tick equality and is symmetric;
`ResolvedDelivery` is delivered across distinct ticks; `SubTickDelivery` is
delivered inside one tick.

`ResolutionBounded` is a model-supplied display coherence condition: same-tick
welds have order-equivalent shares. It is not a legitimacy, pole, or sentience
predicate. `no_timeDirection_within_tick` proves that sub-tick delivery carries
no strict `TimeDirection`, and
`no_timeDirection_of_resolutionBounded_subsingleton` is the one-tick limit over
weld shares. Transposition leaves `SameTick` and `ResolutionBounded` unchanged
while `transpose_subTickDelivery` reverses only the delivery line.

**Configurations and share-drops.** `Config` has one field,
`tendency : Contrib`; it stores no `Being`, no `Weld`, and no owner.
`rePitch before received` returns the config with tendency `share received`;
`before` is unused in the value. `IsShareDrop before received` means
`Strict (share received) before.tendency`, i.e. `share received ≼
before.tendency` and not `before.tendency ≼ share received`.

**DirectedConvention definitions.** The directional reading layer contains:

- `WaaReachBackFull`, `DeliveredTo`, `NotDeliveredTo`, and `WaaAimedAt`.
- `LandsAt`, `ObjectAxisStanding`, `LandsWithShareDrop`, and
  `HasShareDropLanding`.
- `EnvironsLine` and `ShareDropLine`.
- `ShortfallClosedAt`, `WaaFullyEnlightened`, `WaaAversionContext`, and
  `WaaPathOught`.
- `WaaPathClaim`, `WaaFaithPrinciple`, and `WaaFaithOught`.
- `WaaReportFace`, `WaaOwnershipFace`, `WaaVacuousOwnershipFace`, and
  `WaaDiachronicWhose`.

All of these are definitions over `conditions`, `Actual`, `IsShareDrop`, and
`WaaAppropriates`; none adds a new axiom to `conditions`.

**Four truths and sraddha.** `WaaMismatchGrade w` is definitionally `share w`.
`WaaMismatchLive w` means an actual occurrence with a live self-pole index; with
actuality supplied, `waaMismatchLive_iff_hasSelfPoleIndex` gives the exact typing
condition. `not_waaMismatchLive_of_stone` keeps stones outside the occurrence
domain, and `waaMismatch_atBot_of_terminus_response` sends terminus responses to
the pole-class. The fourth truth the grid can only display: Lean now proves
the implication whose antecedents it never asserts. The detached injunction
remains absent from the system's assertable voice.

**Tiers and distinctions.** A `Tier` is `floor` or `actTime w`.
`Tier.hasLiveShare` is `False` at `floor` and `HasSelfPoleIndex w` at
`actTime w`. Distinctions, claim languages, recorded utterances, error grades,
and generator outcomes define the separate/fuse diagnostic vocabulary over
tiers.

**Identification layer.** `StateToolFits w` means `¬ HasSelfPoleIndex w`; with
the definitions above this is double-negated pole-class membership. The exact
iff with `AtBot` therefore requires decidability of the one proposition
`AtBot a`, not decidable equality on all of `Contrib`.

---

## 1. Signature Layer (`Signature/*`)

`no_self_pole_index_of_atBot`: if `AtBot (share w)`, then `w` has no live
self-pole index. This is direct contradiction with
`HasSelfPoleIndex w := ¬ AtBot (share w)`.

`no_self_pole_index_of_eq_shareBot`: equality `share w = shareBot` is first
converted to `AtBot (share w)`, then the previous theorem applies.

`selfPoleIndex_eq_agent_of_hasSelfPoleIndex`: the evidence-carried index is
`w.agent`. Definitional (`rfl`).

`strict_shareBot_of_hasSelfPoleIndex`: a live self-pole index gives
`Strict shareBot (share w)`. The proof packages `shareBot_le` with the
definition `HasSelfPoleIndex w := ¬ AtBot (share w)`.

`strict_shareBot_iff_not_atBot`: being strictly above the designated bottom is
equivalent to not being in the bottom order-class.

`not_waaAppropriates_of_atBot` and `not_waaAppropriates_of_eq_shareBot`: the
same no-index facts under the definitional name `WaaAppropriates`.

`share_eq_grade_check`: `share w = grade w.agent w.call w.response`.
Definitional (`rfl`).

`atBot_of_terminus_response`: if `b` is a `Terminus` and
`respondsTo b c = some r`, then the weld `⟨b, c, r⟩` has `AtBot` share.

`no_self_pole_index_of_terminus_response` and
`not_waaAppropriates_of_terminus_response`: a terminus response has no live
self-pole index and does not WAA-appropriate.

`stone_is_terminus_vacuously`: every `Stone` is a `Terminus`. This is vacuous: the
response hypothesis in `Terminus` can never be satisfied for a stone.

`AllStone` says every being in the grid is stone-typed. `DirectionVoid` says
the contribution carrier has no strict comparisons anywhere.

`not_stone_of_mountsSomewhere`, `liveTerminus_not_stone`, and
`responsiveTerminus_live_of_call` are witness/projection facts over response
function.

`Grid.DirectedConvention.deliveredTo_or_not`: for a particular pair of welds,
if `conditions deed reception` is decidable, then either
`DeliveredTo G deed reception` or `NotDeliveredTo G deed reception`.

`Grid.DirectedConvention.deliveredTo_iff_waaReachBackFull`: definitional
(`Iff.rfl`), since both names are `conditions`.

`Grid.DirectedConvention.objectAxisStanding_of_landsAt`: a landing gives
object-axis standing, witnessed by the reception in hand.

`Grid.DirectedConvention.objectAxisStanding_of_hasShareDropLanding`: a
share-drop landing gives object-axis standing through its landing component.

`not_collapse_of_obeysSeparateFuse`: the first clause of `ObeysSeparateFuse`
contradicts the equivalence required by `Collapse` at any live tier.

`not_freeze_of_obeysSeparateFuse`: the second clause of `ObeysSeparateFuse` at
`floor` gives the equivalence denied by `Freeze`.

`not_freeze_of_same_claim`: a distinction whose two sides are the same claim
cannot freeze.

`no_agent_recovery_of_field_collision`: if two distinct beings can actually
produce the same call-response pair, no function from field residue
`Call × Response` can correctly recover the agent for every actual weld.

**`clockGrid`.** The concrete grid uses `Nat` with bottom `0`; `rigid` responds
nowhere, `adaptive` responds with `chime` when the listener is present,
`grade` is constantly `0`, and `conditions` is always false.

- `rigid_is_stone`: `rigid` responds nowhere.
- `adaptive_is_terminus`: `adaptive` is a terminus.
- `adaptive_not_stone`: `adaptive` responds at `present`.
- `clockGrid_function_share_split_witness`: the concrete grid contains a stone
  and a non-stone terminus.

**`registerClockGrid`.** The second concrete grid uses natural-numbered fine
registers as beings. Each register answers the tick by handing off to the next
register; delivery follows that hand-off. `registerClockCoarsening` merges the
fine registers into one macro tag at diagnosis-time. The checked facts are
`registerClock_macro_sentient` and `registerClock_macro_selfConditioning`.

**`backslideGrid` and `gradingCollisionGrid`.** `backslideGrid` has one being
answering a gentle call at share `0` and a harsh call at share `5`, giving the
concrete carrier for the same-being backsliding witnesses.
`gradingCollisionGrid` has two actual welds with the same call-response residue
and different shares, giving the concrete carrier for the cetana field-residue
witness.

---

## 2. Consequences and Taxonomy (`Consequences/Basic.lean`, `Consequences/Taxonomy.lean`, `Consequences/Ladder.lean`, `Consequences/ContentRows.lean`)

**Function/share and poles.** `share_eq_grade` is definitional. The response
facts `mountsAt_of_actual`, `mountsSomewhere_of_actual`,
`not_stone_of_actual`, `not_actual_of_stone`,
`not_mountsSomewhere_of_stone`, and `not_stone_of_response` are direct
witness/projection/contradiction consequences of `Actual`, `MountsAt`, and
`Stone`.

`atPoleClass_of_stone` and `atPoleClass_of_terminus` introduce the two
disjuncts of `AtPoleClass`. `atPoleClass_and_not_stone_of_liveTerminus`
combines the terminus disjunct with `liveTerminus_not_stone`.
`not_stone_of_responsiveTerminus_of_call` uses the supplied call to get live
function.

**Re-pitch and share-drops.** `rePitch_tendency_eq_share` is definitional:
the re-pitched tendency is the received weld's share.
`isShareDrop_iff_rePitch_tendency_drop` is definitional after substituting the
re-pitched tendency for `share received`.
`rePitch_tendency_le_before_of_shareDrop` and
`not_before_le_rePitch_tendency_of_shareDrop` project the two conjuncts of
`IsShareDrop`. `rePitch_tendency_atBot_of_terminus_response` sends a terminus
response into the pole-class.

**Conditions and response replacement.** `withConditions` replaces only the
delivery relation. Its `withConditions_respondsTo`, `withConditions_grade`, and
`withConditions_share` lemmas are definitional, and
`grade_independent_of_conditions` / `share_independent_of_conditions` state the
cetana anchor: grade and share are blind to downstream delivery. Dually,
`withRespondsTo` replaces only the response function; `withRespondsTo_grade`,
`withRespondsTo_share`, and `withRespondsTo_conditions` are definitional.
`staticized b` removes the responses of one being and leaves grade and delivery
in place. The futility facts are `futility_delivery_loss_real`,
`staticized_responseInvariant`, `futility_object_axis_subtraction_nil`, and
`Grid.DirectedConvention.staticized_objectAxisStanding_iff`.

**The environs lens.** The directional theorem block lives under
`Grid.DirectedConvention`.

`environsLine_of_shareDropLine`, `isShareDrop_of_shareDropLine`, and
`deliveredTo_of_environsLine` are projections.

`not_isShareDrop_of_tendency_atBot`: if the prior tendency is already
`AtBot`, then no received weld is a strict share-drop against it. The proof
uses `before.tendency ≼ shareBot ≼ share received` to contradict the second
conjunct of `IsShareDrop`.

`not_isShareDrop_of_eq_shareBot_tendency`: equality with the representative
bottom is a bridge into the previous theorem.

`Grid.DirectedConvention.no_shareDropLine_of_tendency_atBot`: with an `AtBot`
prior tendency, no `ShareDropLine` exists, because its share-drop conjunct is
impossible.

`Grid.DirectedConvention.no_shareDropLine_of_eq_shareBot_tendency`: equality
bridge into the previous theorem.

`Grid.DirectedConvention.hasShareDropLanding_of_shareDropLine_actual`: a
share-drop line whose reception is actual assembles the existential
`HasShareDropLanding` witness. This is the checked core of effectiveness talk
as display.

`ShortfallClosedAt` states local, delivered-pair shortfall closure for a live
prior tendency. `WaaFullyEnlightened` adds this universal closure conjunct to
`ResponsiveTerminus`; `responsiveTerminus_of_waaFullyEnlightened` and
`shortfallClosedAt_of_waaFullyEnlightened` project the two parts.

**Delivery and share-drop landing.** The reach/aiming biconditionals are
definitional (`Iff.rfl`). The remaining delivery theorems are projections from
`LandsAt`, `LandsWithShareDrop`, or `HasShareDropLanding`, plus existential
witnesses:

- `deliveredTo_of_landsAt`, `actual_of_landsAt`
- `landsAt_of_landsWithShareDrop`, `isShareDrop_of_landsWithShareDrop`
- `deliveredTo_of_landsWithShareDrop`, `actual_of_landsWithShareDrop`
- `exists_landsAt_of_hasShareDropLanding`
- `exists_actual_reception_of_hasShareDropLanding`
- `exists_shareDrop_reception_of_hasShareDropLanding`

**Reception pairs.** `first_actual` and `second_actual` project stored proofs.
`firstConditionsSecond_iff_deliveredTo` is definitional and states the pair's
directed relation via `Grid.DirectedConvention.DeliveredTo`. The two
`rePitchSequence_*_tendency` theorems are definitional and show the sequence's
tendencies are the two weld shares.

**Tiers and separate/fuse.**

- `floor_has_no_live_share`: no live share at `floor`.
- `actTime_hasLiveShare_iff_hasSelfPoleIndex`: definitional.
- `not_actTime_hasLiveShare_of_atBot`: an act-time tier whose weld is at the
  pole-class has no live share.
- `not_actTime_hasLiveShare_of_eq_shareBot`: equality bridge into the previous
  theorem.
- `not_collapse_floor`, `hasLiveShare_of_collapse`,
  `hasLiveShare_of_separated`, `not_collapse_of_separated`,
  `fused_of_obeysSeparateFuse`, `separated_of_obeysSeparateFuse`, and
  `not_freeze_of_fused_floor` are the direct separate/fuse diagnostics.

`answersCall_eq_weld_call` and `fitsOfferedTier_iff_trueAt` are definitional.
`verdict_voice_assertable` and `shortfall_voice_displayable` confirm the two
`ErrorGrade.voice` assignments.
`waa_conditional_voice_assertable` and
`waa_detached_ought_voice_displayable` pin the new conditional/detached split:
the implication is verdict-voiced, while the detached injunction is only
shortfall-voiced.

**Generated table rows.** Under
`Grid.DirectedConvention.BeingConvention.GridConvention`, `RowTag` names the
schema-generated table rows, including the five `ConventionLayer` rows via
`.layer`. `RowClaim` has `inForce r` and `denied r`, and `rowLanguage G` gives
them pole-affirming semantics: at `floor` every row claim holds; at `actTime w`
the conventional side holds, while the denial side holds exactly when
`AtBot (G.share w)`.

`rowOf G r` instantiates `Distinction G` from this language.
`rowOf_separated_at_live`, `rowOf_collapse_self_refuting`, `rowOf_not_freeze`,
`denied_holds_only_where_no_live_share`, `rowOf_errorFree`, and
`pole_validates_all_claims` are hypothesis-free. `rowOf_obeys` and
`rowOf_obeys_iff_errorFree` carry only the local decidability/stability needed
to turn non-live act-time into `AtBot`. `denied_misfits_live_offer` is the
recorded-utterance check; `fox_utterance_misfits_live_offer` specializes it to
the marquee fox row.

The old pilot names are compatibility names for schema tags:
`beforeAfterRow G`, `intraWeldArrowRow G`, `beingsRow G`, `gridLensRow G`, and
`weldRow G` are `rowOf G (.layer ...)`; `doerDeedRow G` is the schema-only
MMK 8 row. Their collapse and freeze names keep hypothesis-free statements;
their `*_obeys` names carry the stability hypothesis. `tableOrder` records the
full table shape as Lean data: nineteen schema rows, one ladder row, and six
prose rows. Schema-row cell occupancy is also data now:
`hasCollapseOccupant` and `hasFreezeOccupant` record where the
paper's table has an occupant rather than a dash, and
`perCallGlobal_empty_collapse_cell_anchor` checks the per-call/global dash
without turning it into new grid semantics.

**Concrete consequence witnesses.** The small model checks now include
`shareZero_not_functionZero_witness`, `rung_not_pole_witness`,
`backsliding_witness`, `backsliding_rePitchSequence_witness`,
`standing_does_not_determine_dated`, `subitism_possibility_witness`,
`cetana_grading_tracks_weld_not_field_witness`,
`cetana_live_share_without_object_standing_witness`,
`registerClock_staticized_zero_stone`,
`registerClock_staticized_objectAxisStanding_iff`, and
`pole_tier_buddha_inhabited`, with the fox run-through now checked in
`FoxCase.foxGrid`. These are witness assemblies over the concrete grids, mostly
by unfolding and `decide`.

**Content-bearing rows.** `contentLayerLanguage` uses the same `LayerClaim`
syntax but gives content to denials: no strict direction, no response variation
with call, all beings stone, no live tier anywhere, or no actual welds.
`contentBeforeAfterRow`, `contentIntraWeldArrowRow`, `contentBeingsRow`,
`contentGridLensRow`, and `contentWeldRow` are the content rows. Their
obedience theorems are conditional:
`contentBeforeAfterRow_obeys_of_direction`,
`contentIntraWeldArrowRow_obeys_of_variation`,
`contentBeingsRow_obeys_of_being`,
`contentGridLensRow_obeys_of_liveTier`, and
`contentWeldRow_obeys_of_actual` require exactly the witness that makes the
denial false at non-live act-time. These content rows keep the diagnostic
live-side because their global denials cannot be made true by a particular
pole-class weld; they answer aptness-to-hold, not truth-at-tier.

`beings_denial_fits_only_floor` and
`time_denial_unfit_for_appropriating_utterer` are utterance-level
self-refutation results. The beings theorem uses the `RecordedUtterance`
actuality field to get a non-stone utterer; the time theorem uses the live
share as a strict direction witness. The intra-weld utterance theorem is the
weaker schema-language live-tier check,
`interior_order_denial_unfit_for_live_utterer`; one recorded utterance does not
by itself supply two distinct responses.

**Re-emptying ladder.** `LadderSide`, `reEmptied`, and `ladder` generate the
next distinction from the previous one. `reEmptied_obeysSeparateFuse` proves
that obedience propagates, while `ErrorFree`, `errorFree_of_obeys`,
`reEmptied_obeys_of_errorFree`, `ladder_obeys_of_errorFree`, and
`ladder_errorFree_of_errorFree` show the stronger refutation-only route above
an error-free seed. `no_level_final_of_obeys`, `no_final_level_of_errorFree`, and
`ladder_collapse_self_refuting` rule out freeze and collapse at generated
levels. `beingsLadder`, `beforeAfterLadder`, `intraWeldArrowLadder`,
`gridLensLadder`, `weldLadder`, and `doerDeedLadder` are schema seeds; their
`_obeys_succ` facts are hypothesis-free, while all-level `*_obeys` names
include the seed's stability hypothesis. `contentBeingsLadder` is the content
instance under the non-stone aptness hypothesis.

---

## 3. Doctrines (`Doctrines/FourTruths.lean`, `Doctrines/Sraddha*.lean`, `Doctrines/Faith*.lean`, `Doctrines/Ethics*.lean`, `Doctrines/Deliberation.lean`, `Doctrines/Gradeability.lean`, `Doctrines/Ledger.lean`, `Doctrines/Correlations*.lean`, `Doctrines/SuddenGradual*.lean`, `Doctrines/OtherPower*.lean`, `Doctrines/Fetters*.lean`, `Doctrines/Factors*.lean`)

`waaMismatchGrade_eq_share` is definitional. `waaMismatchGrade_le_of_share_le` is the
ordinal covariation theorem: any share comparison is the corresponding
mismatch-grade comparison.

`WaaMismatchLive` is actual occurrence plus live self-pole index.
`waaMismatchLive_iff_hasSelfPoleIndex` removes the actuality conjunct when the
occurrence is already known actual. `not_waaMismatchLive_of_stone` uses
`not_actual_of_stone`; `waaMismatch_atBot_of_terminus_response` reuses
`atBot_of_terminus_response`.

`WaaAversionContext` packages a live prior tendency and an actual
live-mismatch reception. `waa_path_landing` proves the checked conditional:
`WaaFullyEnlightened`, a deed by that being, delivery to the reception, and
the aversion context imply `HasShareDropLanding`. `WaaPathOught` is only this
implication type, and `waaPathOught_conditional` proves it.

`no_waa_path_at_pole` proves that no share-drop landing can be constructed
from an `AtBot` prior tendency. `no_waa_aversion_context_at_pole` shows the
live-aversion antecedent fails there. `Doctrines/SraddhaNegative.lean` supplies
concrete countermodels for dropping faith or dropping aversion.

`OrthogonalityNegative` reuses the `SraddhaNegative` zero-effectiveness grid:
a responsive terminus can fail `WaaFullyEnlightened` because the delivered
deed has no share-drop landing for the receiver's live prior tendency.
`waaFullyEnlightened_stronger_than_terminus` proves the strictness.
`waaFullyEnlightened_of_responsiveTerminus_of_undelivered` gives the sealed
regime face: if no own deed is delivered, the shortfall-closure conjunct holds
vacuously for any responsive terminus.

**Faith.** `WaaPathClaim` packages the local claim that a prior configuration,
deed, and reception satisfy `ShortfallClosedAt`; `waaPathClaimLanguage` makes
that claim a `ClaimLanguage`. `WaaFaithPrinciple` is the testimonial
antecedent: faith in a fully enlightened being makes that being's recorded
utterances fit their offered tier. `waa_says_true_of_faith` is the direct
projection of the principle, while
`fitsOfferedTier_of_waaFullyEnlightened_ownDeed` records the old own-deed
fragment where full enlightenment itself supplies the claim truth.
`waa_path_landing_of_faithPrinciple` and `waaFaithOught_conditional` rederive
the landing through recorded testimony. `FaithNegative` shows that neither
faith as the enlightenment premise itself nor free faith validates the
principle.

**Ethics.** `WaaEthicsStance` bundles the faith principle with faith in one
faith-object; `WaaEthicalCode` generalizes the fourth-truth ought across that
object's recorded testimony while remaining an implication type.
`waaEthicalCode_conditional` is the hypothesis-free conditional. The voice
pair is split by `waa_ethics_conditional_voice_assertable` and
`waa_ethics_detached_voice_displayable`: the conditional is verdict-voiced, the
detached injunction shortfall-voiced. `EthicsNegative` supplies
`no_ethics_bearing_at_pole`, `no_stance_over_false_testimony`, and
`ethicalCode_relative_to_faith_object`.

**Deliberation.** `ConsequentialistConvention` is a descriptive reading layer.
`DropCount` and `DropCountInFiber` count share-drop receptions across finite
actual runs without adding probability, utility, or a command register.
They are legal display readings: `map_dropCount` and `map_dropCountInFiber`
show that reparameterizing the contribution display does not change either
count. `dropCountInFiber_le_dropCount` gives the per-fiber bound, while
`dropCount_eq_sum_dropCountInFiber` says that a noduplicate complete supplied
tag list adds the fiber counts back to the total. The local sum itself
transports by `map_dropCountInFiberSum`, and
`ObjectiveNegative.split_dropCount_sum_eq_mergedDropCount` checks the
`[false, true]` split against the merged objective example.
`ObjectiveNegative` reuses the merge/split being-convention pattern to show
that "my drops" is not a function of grid data alone.

`rePitch_forgets` and
`accumulated_attainment_constant_of_same_final` restate backsliding in the form
a maximizer needs: no accumulated attainment variable is stored in `Config`.
`backsliding_witness` and `backsliding_rePitchSequence_witness` give the
same-grid same-being witness form directly.
`TransferNegative` records the adaptive track-record obstruction and the
`ResponseInvariant` contrast case. `grade_independent_of_conditions` and
`share_independent_of_conditions` keep the cetana claim at signature level:
grade and share do not consume downstream delivery conditions; the two concrete
cetana witnesses check same-field/different-share and live-share/no-standing
cases. `DeliveryArrogationNegative` instantiates the
`ClaimLanguage` machinery for a command-shaped delivery claim and checks that a
recorded plan fails `FitsOfferedTier` where delivery is absent.

**Gradeability.** `SeveredTranscript` is the strongest severed quotation form:
an attributed agent-response pair with no call, no offered tier, and no
actuality proof. `Grid.Weld.sever` and `Grid.RecordedUtterance.sever` forget
the call; `severedVerdict` pins the generator's standing response to such data
as `declined`. `GradeabilityNegative.no_grade_recovery_from_severed` proves
that, under a same-agent/same-response collision with different shares, no
function from severed transcripts can recover the grade for every actual weld.
`gradeability_severed_underdetermination_witness` reuses `backslideGrid` as
the concrete missing-call carrier, and `severed_transcript_ungradeable`
instantiates the generic theorem there. The positive half is
`recordedUtterance_grade_determined`, an `rfl` fact that a recorded utterance's
grade is the grade of the whole weld it carries. The normative input rule and
the koan-form genre claim remain prose.

**Ledger.** `MountsOnlyIn b M` says `b` mounts responses only at calls in
`M`. `modality_of_actual` and `landing_call_in_modality` are the
response-shape facts: an actual weld, and hence any landing, at a
modality-restricted receiver carries a call in the modality; both are
projection/rewrite proofs. `not_actual_outside_modality` and
`no_landing_outside_modality` are the contrapositives.
`fiber_landing_call_in_modality` lifts the fact to a coarsening fiber whose
fine tags all satisfy `MountsOnlyIn` for the same `M`.

`ReceptionCommand` and `receptionCommandLanguage` mirror the Deliberation
delivery-command language with `LandsAt` as the satisfaction condition;
`receptionCommand_unfit_of_no_landing` is the corresponding unfit theorem.

`ledger_census_misfits_live_offer` and `ledger_prognosis_misfits_live_offer`
are named faces of `denied_misfits_live_offer` at `.perCallGlobal` and
`.standingDated`; the module adds no `RowTag`.

`LedgerCase.ledgerGrid` is a three-being, three-call, three-response grid over
`Nat` with constant live grade `1`; `conditions` delivers exactly the welds
whose response is `code` or `comply`. The checked model facts:
`official_mountsOnlyIn_economic`, `official_not_stone`,
`official_landing_only_economic`, `floor_speech_never_lands_at_official`; the
three landings of `codeWeld` with `one_act_two_receivers` and
`code_ruler_not_exempt` (a self-line reception by the issuer);
`sectorCoarsening` with `state_tag_sentient`, `state_fiber_shares_register`,
and `state_fiber_landing_economic`; `decree_engineers_calls_not_receptions`
(delivery holds, the commanded reception is not actual, the recorded decree
fails `FitsOfferedTier`); and the purge block `purgedGrid :=
ledgerGrid.staticized master` with `purge_delivery_loss_real`,
`purge_adaptive_to_static`, `purge_loop_runs_on`,
`purge_object_axis_subtraction_nil`, and `corpus_still_delivered`, all reusing
the futility operation.

`FoxCase.foxGrid` is a natural-numbered life series: life 0 answers the
question, later lives receive the fruit, and the turning word releases at
share 1 rather than at the pole. The checked model facts are
`fox_sentence_live_selfPole`, `fox_arrow_index_free`,
`fox_returns_delivered`, `fox_reception_clenched`, `fox_release_rung_not_pole`,
`fox_reachBack_full_at_release`, `fox_nothing_kept`, and
`fox_never_tests_pole`. `foxSeriesCoarsening` merges the fine lives into the
display tag "the fox" while `fox_consecutive_lives_distinct` keeps the fine
series individuated. The Dogen gloss is typed by
`daishugyo_diagnosis_fits`, `jinshinInga_instruction_fits`,
`jinshinInga_floor_voicing_would_misfit`, and `dogen_doubling_both_fit`; these
check only the grid-internal speech-act gloss, not the historical contra.
`Doctrines/FoxCase.lean` adds `fox_dukkha_per_life`, because that theorem
consumes the Four Truths mismatch vocabulary.

**Correlations.** `StageScheme` is `BeingCoarsening`; `FiftyTwoStageScheme`
adds no signature field. `ShareDropRun` and `BullAscent` type Bulls 1-6 as
per-call drops. `WaaBullSeven` is probe-constancy plus a live self-pole index,
with `bullSeven_not_bullEight` checking that this half-weld is not the
pole-class. Bull 8 is `AtPoleClass`, Bull 9 is `ResponsiveTerminus`, and Bull
10 is `WaaBullTen`, an existential cross-fiber delivery into another sentient
fiber. `StrongWaaBullTen` names the stronger all-sentient-fibers asymptote
without using it. `bullTen_to_bullNine`, `bullNine_to_terminus`, and
`bullNine_to_bullEight` give the checked chain, while
`CorrelationsNegative.pratyekabuddha_countermodel` shows Bull 9 without Bull
10. `CorrelationsNegative.no_stage_boundary_recovery` is the stage-scheme
version of the no-recovered-partition witness.

`FiveRank`, `RankReading`, and `rankLanguage` keep the Five Ranks as
utterance-diagnosis data. `kenChuTo_implies_waaBullTen` records the 到/Bull 10
shape under the same coarsening.

**Sudden/gradual.** `WaaSuddenArrival` packages an actual one-step share-drop
from live prior tendency to the pole-class; `waaSuddenArrival_witness` names
the clock-grid face of the older `subitism_possibility_witness`. `rePitchRun`
folds a finite list of received welds, and `WaaGradualArrival` reads a staged
`ShareDropRun` that reaches the pole-class; `waaGradualArrival_witness` checks
the two-step register-clock case. `rate_invisible_to_config`,
`rePitchRun_forgets_same_final`, and
`score_of_rePitchRun_constant_of_same_final` are the no-rate-preference
statements: anything that factors through the final `Config` cannot see the
earlier rate once the final reception is fixed.
`SuddenGradualNegative.subitism_frequency_underdetermined` supplies the
honesty clause by varying delivery while response, grade, and share data agree.

**Other-power.** `SameAgentDelivery` and `CrossAgentDelivery` add neutral
delivery-regime vocabulary: the line is delivered, and the deed/reception agent
tags are equal or unequal. `WaaJirikiLine` and `WaaTarikiLine` are only the
system-POV readings of those facts. `reception_typing_ignores_sower` is
near-definitional by design: changing only `conditions` leaves a reception's
grade, share, and actuality unchanged. `waaReachBack_filled_either_regime`
projects the shared reach-back conjunct from either same-agent or cross-agent
delivery.

`TarikiCase` discharges non-vacuity the way `LedgerCase` does: a fixed-call
source is response-invariant (`name_responseInvariant`), function-mounted
(`name_not_stone`), and share-zero at its welds (`name_share_bot`); its object
axis reaches every invoker reception (`name_object_axis_entire`). The effective
limit is checked by `universal_fixed_call_lands_without_reading`, while
`invoker_reception_is_deed` keeps the receiver's act grammar ordinary and
live. `OtherPowerNegative.regime_does_not_determine_share` and
`OtherPowerNegative.share_does_not_determine_regime` witness the no-polemic
clause: neither regime nor share recovers the other.

**Fetters.** `FiberAtPoleOn`, `LiveFiberAtPoleOn`, `FiberAtPoleOnWithin`, and
`FiberAtPoleWithin` are neutral fiber predicates in
`Signature/BeingConvention.lean`. `FetterReading` supplies model-side
provocation classes, `SomaReading` supplies model-side tag-regions, and
`FetterCutWithin` means quietness at pole on the relevant call-class inside
the supplied tag-class. `Fetter.kind_lower_iff_cut_by_nonReturn` records the
enumeration coherence: exactly the lower fetters are cut by non-return.
`Path.cutClasses` gives the nested path profiles;
`PathQuietWithin`, `arhatPathQuietWithin_iff_fiberAtPoleWithin`, and
`arhatWithin_univTags_iff_fiberAtPole` close the two-axis lattice back to
ordinary `FiberAtPole` at total calls and total tags. That top point is the
total-rectangle cut, not the buddha reading by itself. The layered reading has
three checked rungs: rung 1 is share-only and stone-inclusive
(`FettersNegative.total_cut_carries_no_function`); rung 2 is the live terminus
reading, with `sentientTag_iff_actualFiberInhabited` bridging function to
actual fiber inhabitation; rung 3 is `WaaFullyEnlightened`, and
`FettersNegative.total_cut_with_function_not_waaFullyEnlightened` checks that
rung 2 still lacks effectiveness. The regime-relational face is two-sided:
zero-effect delivery can make full enlightenment fail, while
`waaFullyEnlightened_of_responsiveTerminus_of_undelivered` makes it hold
vacuously under sealed delivery. The checked anchors are
`classQuiet_no_clench_in_class`, `identityView_excluded_at_arhatFiber`,
`conceit_excluded_at_arhatFiber`, `all_fetters_cut_at_arhatFiber`,
`arhatFiber_of_termini`,
`identityView_excluded_at_speechThoughtRegion`, `conceit_excluded_within`,
`regionFiber_of_termini`, and `unquiet_region_still_functions_witness`.

The forward-looking face is conditional and diagnostic: `RunQuiet` and
`RunQuietWithin` are finite track-record quietness,
`waaIrreversibleRegime_conditional` and
`waaIrreversibleRegimeWithin_conditional` promote them only under supplied
regimes, and `FettersNegative.seen_run_underdetermines_fetterCut`,
`FettersNegative.seen_run_underdetermines_fetterCutWithin`, and
`FettersNegative.no_region_boundary_recovery` give the fresh-call and
tag-boundary underdetermination witnesses.

**Factors.** `PathFactor` names the factor-side regrouping of the canonical
fetter table. `PathFactor.blockerClass` derives rites, view, and resolve
blocker classes from `FetterReading`; speech and conduct are named but inert
with `False` classes. The coherence theorems
`ritesView_union_covers_streamEntry_fetters`,
`resolve_covers_nonReturn_fetters`, and
`lower_fetters_covered_by_rites_view_resolve` check that the active factor
classes cover exactly the intended stream-entry and lower-fetter unions.

`FactorHeld` is a seen-run existential over actual in-fiber welds with live
self-pole index in the factor class. `FactorReleased` is the corresponding
whole-class `FiberAtPoleOn` cut. `not_factorHeld_of_factorReleased` gives the
refutation direction; `factorReleased_rites_iff_ritesGrasp_cut`,
`factorReleased_view_iff`, and `factorReleased_resolve_iff` connect the factor
release predicates back to the fetter cuts.

The stage readings are `WaaStreamEnterer`, `WaaStreamWinner`,
`WaaOnceReturner`, and `WaaNonReturner`. The fruit positions are proved
equivalent to the old path cut classes by
`waaStreamWinner_iff_streamEntry_cutClasses` and
`waaNonReturner_iff_nonReturn_cut`, while
`waaNonReturner_of_arhatFiber` consumes the existing arhat fiber anchor.
`ShareDropRunOn`, `WaaResolveAttenuation`,
`waaOnceReturner_attenuation_witness`, and `attenuation_not_release` give
once-return positive content as a strict resolve-class drop that stops short
of pole release.

`RunsExhibitFactorOrder`, `WaaSerialFactorRegime`, and
`waaSerialFactorRegime_conditional` state the "usually runs in order" claim
only as a supplied-regime conditional. `waaSuddenArrival_consistent_with_factorScheme`
records compatibility between one-step pole arrival and the factor fruit
readings under the existing pole-fiber hypothesis.

**FactorsNegative.** `no_hold_conceit_boundary_recovery` shows that the
hold/conceit line is not recovered from shared response/grade/share data.
`seen_run_underdetermines_factorOrder` gives one seen run whose factor order
depends on the supplied reading. `lineage_underdetermined_by_seen_run`
specializes the stage-boundary freedom witness to switching between a
Theravada-shaped factor tag and a Bulls-shaped tag over the same grid and run.

---

## 4. Identification Layer (`Identification/*`)

**Field residues.** `CorrectFieldRecovery recover` says that every actual
weld's field residue recovers its index.
`correctFieldRecovery_forces_same_index_of_same_field` proves that two actual
welds with equal field residue must then have equal indices.
`no_agent_recovery_from_same_field_distinct_index` and
`no_agent_recovery_from_same_call_response` package the corresponding
impossibility results.

**Ownership-face definitions.** The ownership/report/vacuity/whose predicates
live under `Grid.DirectedConvention`. `WaaReportFace`,
`WaaOwnershipFace`, `WaaVacuousOwnershipFace`, and
`WaaDiachronicWhose` are conjunctions over delivery, actuality, and
WAA-appropriation. Their theorems are projections, introductions,
contradictions with non-delivery, or definitional biconditionals:

- `waaReportFace_of_waaOwnershipFace`
- `actual_of_waaOwnershipFace`
- `waaAppropriates_of_waaOwnershipFace`
- `waaOwnershipFace_intro`
- `not_waaOwnershipFace_of_vacuous`
- `not_waaOwnershipFace_of_waaVacuousOwnershipFace`
- `waaDiachronicWhose_iff_delivery_and_waaAppropriates`

The concrete memory display is
`Grid.DirectedConvention.MemoryWitness.memory_witness` over
`registerClockGrid`. It names the registers `pastDeed`, `recall`, and
`confabulatedDeed`; the delivered side is checked by `trace_delivered`,
`recall_waaOwnershipFace`, and `recall_waaDiachronicWhose`; the false-memory
side is checked by `confabulated_not_delivered` and
`falseMemory_waaVacuousOwnershipFace`. `vacuity_not_inner_mark` projects the
same recall-side WAA-appropriation from both faces while closing the
non-delivered contrast, and `recall_spent` is the `rePitch_forgets` instance
that makes the recall weld spent at recall-time.

**Token reflexivity.** `selfAnchored`: `index w = w.agent`. Definitional
(`rfl`).

**Pole-typing.** `StateToolFits w` means `¬ HasSelfPoleIndex w`.
`stateToolFits_of_atBot` and `stateToolFits_of_eq_shareBot` are the direct
pole-class and equality-bridge facts. Assuming
`[Decidable (AtBot (G.share w))]`, `atBot_of_stateToolFits` and
`stateToolFits_iff_atBot` give the exact iff with pole-class membership.
`stateToolFits_of_terminus_response` applies the result to terminus responses.

`Grid.DirectedConvention.not_waaOwnershipFace_of_stateToolFits`: if the
state-tool fits a reception, the WAA-ownership-face cannot fire there, because
ownership-face includes WAA-appropriation.

**Rule and office facts.** `obeysRule_fuses_at_floor` and
`obeysRule_separates_at_actTime` are direct uses of the separate/fuse theorems.
`assignedTier` assigns each `WaaOwnershipOffice` to the weld's act-time tier.
The two facts that this unfolds to `Tier.actTime w` and has exactly the weld's
`HasSelfPoleIndex` condition are `assignedTier_eq_actTime` and
`assignedTier_hasLiveShare_iff`. `retype_constructor_exists` checks the
generator's retype constructor. The placement and disclaimer checks are named
below.

**Register sorting.** `Register`, `SortedFact`, and `SortedFact.register` record
disclaimer 5's three-register sorting as inspectable data. The pins are
`causalSeries_register`, `delivery_register`, `seed_register`,
`arrogationTendency_register`, `agentIndex_register`, `forMeNess_register`,
`receptionReachBack_register`, and `rowTwoPlacement_register`.
`nothing_selfIndexed_carried` checks the refined premise that the self-indexed
facts are not carried in the stored field register.

**Instructive absences.** `InstructiveAbsence` records the current section 3
list as Lean data, with `InstructiveAbsence.number` pinning the paper order
1-10. `AbsenceStatus` states the membership rule explicitly: constructors track
the section 3 list, while `InstructiveAbsence.status` tracks whether the world
has retired an entry. The status pins are `emptyCells_standing`,
`declinedCase_standing`, `foxNeverTestsPole_standing`, `thirdArrival_retired`,
`whyCallsLand_standing`, `fourthTruthWithheld_standing`,
`noSafeStage_standing`, `prudentialPrivilege_standing`, and
`noMeasure_standing`.

The anchors are intentionally thin: `emptyCells_anchor`,
`foxNeverTestsPole_anchor`, `foxNeverTestsPole_recordedUtterance_not_atBot`,
`foxNeverTestsPole_recordedUtterance_not_atPoleClass`,
`foxNeverTestsPole_oldMan_misfit_anchor`,
`thirdArrival_function_mounted_no_share`, `thirdArrival_not_waaMismatchLive`,
`fourthTruthWithheld_conditional`, `fourthTruthWithheld_detached_voice`,
`noSafeStage_anchor`, `prudentialPrivilege_underivable_anchor`,
`icchantikaDeclined_agent_anchor`, `icchantikaDeclined_receiver_anchor`, and
`icchantikaDeclined_nonforeclosure_anchor`. The declined deaf-blind case,
why-calls-land, and no-measure absences are pin-level data only; no theorem is
manufactured for what the paper leaves ceded.

**Self-line witness.** `SelfLineWitness.selfLineGrid` is a minimal `Nat` grid
with one being, one call, one response, total response, grade `1`, and
`conditions _ _ := True`. The checked examples show:

- `w_waaAppropriates`: the self-line witness weld carries
  `Grid.WaaAppropriates`.
- `selfLine_conditions_self`: `conditions w w` holds.
- `selfLine_landsAt_self`: `Grid.DirectedConvention.LandsAt selfLineGrid w w`
  holds.
- `selfLine_waaOwnershipFace_self`:
  `Grid.DirectedConvention.WaaOwnershipFace selfLineGrid w w` holds.

The scope is narrow and deliberate: the signature permits self-lines; it does
not say that any real regime contains them. Irreflexivity of delivery is a
regime fact to be supplied by a model, not a structural axiom.

The contemporary placement checks are `siderits_waaPlacement`,
`ganeri_waaPlacement`, `zahavi_waaPlacement`, and `sartre_waaPlacement`.

**Disclaimers.** `Disclaimer.number` now runs through 57. The recent entries are
`beingConvention` (35), `pilotGeneratedRows` (36), `beingTrichotomy` (37),
`hareHornRegister` (38), `modalRealismFreeze` (39), and
`aptnessConditionality` (40), `sraddhaConditional` (41), and
`faithBothConjuncts` (42). The table-generation entries append after those
existing pins: `generatedTableStructure` (43), `poleAffirmingSemantics` (44),
`proseRows` (45), and `errorFreeReading` (46). `misFeedFence` (47) records the
avyākata fence-and-gate pair. The correlation entries are `tenBullsTyped` (48),
`fiveRanksRetype` (49), `stageSchemeCoarsening` (50), and
`fetterCutTyping` (51). `twoAxisFetterLattice` (52) records the product
call/tag fetter lattice, `enlightenmentLadder` (53) records the neutral
total-rectangle cut and three-rung ladder, and
`ethicsBundledConditionalCode` (54) with `codeHonestyClauses` (55) records the
ethics-code tail. `verdictRecordData` (56) records the generator's
episode-grained verdict history as Lean data, including the retype entries in
`generatorRecord` (`Meta/VerdictLedger.lean`), and `compoundCellStacks` (57)
records the five compound-position decompositions over existing `TableRow`s,
with facets, roles, voices, legal elements, and core-cell counts in
`Consequences/Compounds.lean`.
`waaKarmaIdentification_number` pins `waaKarmaIdentification = 9`, and
`modalRealismFreeze_number` pins `modalRealismFreeze = 39`.
`aptnessConditionality_number` pins `aptnessConditionality = 40`;
`sraddhaConditional_number` and `faithBothConjuncts_number` pin the two new
Sraddha entries, while `generatedTableStructure_number`,
`poleAffirmingSemantics_number`, `proseRows_number`,
`errorFreeReading_number`, and
`misFeedFence_number` pin the table and mis-feed entries; the newer
correlation and disclaimer pins are `tenBullsTyped_number`, `fiveRanksRetype_number`,
`stageSchemeCoarsening_number`, `fetterCutTyping_number`,
`twoAxisFetterLattice_number`, `enlightenmentLadder_number`,
`ethicsBundledConditionalCode_number`, `codeHonestyClauses_number`,
`verdictRecordData_number`, and `compoundCellStacks_number`.

---

## 5. Meta/Nishitani.lean, Meta/ReflexivityWitness.lean, Meta/Invariance.lean, and Meta/InvarianceNegative.lean

**Śūnyatā wrappers.** `Meta/Nishitani.lean` defines `Sunyata d` as the absence
of any frozen level in `ladder d`. The new row instantiations
`intraWeldArrow_sunyata` and `doerDeed_sunyata` join the existing beings,
time, weld, and content-beings instantiations as direct consumers of the
ladder no-final-freeze theorems.

**Reflexivity witness.** `Meta/ReflexivityWitness.lean` defines
`ladderRungGrid`, a single legal `Grid Nat` whose `Being` carrier is read as
rung labels. `ladderRungGrid_beings_sunyata` instantiates `beings_sunyata`,
and `ladderRungGrid_no_level_final` reruns the beings ladder over that grid.
The file is a witness, not a new universal claim about beings.

**Admission criterion.** Any future predicate over `grade` owes a transport
lemma here, or it counts as operational residue. The file proves that the
current grade-facing predicates are invariant under display reparameterization.

`DisplayReparam Contrib Contrib'` consists of a function `toFun`, an order
preservation/reflection theorem `a ≼ b ↔ toFun a ≼ toFun b`, and a proof that
`toFun shareBot` is `AtBot` in the target carrier.

`DisplayReparam.atBot_iff` proves `AtBot (toFun a) ↔ AtBot a`.
`DisplayReparam.orderEq_iff` proves that order-equivalence is preserved and
reflected.
`DisplayReparam.directionVoid_reflect` is hypothesis-free, while
`directionVoid_of_surjective` needs target-carrier coverage;
`CoverageNegative.directionVoid_needs_coverage` shows why.
`DisplayReparam.id` is the identity reparameterization, with `id_toFun` as its
definitional projection lemma. `DisplayReparam.comp` composes
reparameterizations, with `comp_toFun` as its definitional projection lemma.

`Config.map` sends a tendency through `toFun`; `Config.map_tendency` is
definitional.

`Grid.map` leaves `Being`, `Call`, `Response`, `respondsTo`, and `conditions`
unchanged, and maps `grade` through `toFun`.

Definitional transport facts:

- `map_grade` and `map_share`
- `map_actual_iff`, `map_mountsAt_iff`, `map_mountsSomewhere_iff`,
  `map_respondsToEveryCall_iff`, `map_responseVariesWithCall_iff`, and
  `map_stone_iff`
- `Grid.DirectedConvention.map_deliveredTo_iff`,
  `Grid.DirectedConvention.map_landsAt_iff`, and
  `Grid.DirectedConvention.map_environsLine_iff`

Grade-facing transport facts:

- `map_terminus_iff`, `map_liveTerminus_iff`, `map_responsiveTerminus_iff`,
  and `map_atPoleClass_iff`
- `map_hasSelfPoleIndex_iff`
- `map_waaMismatchGrade` and `map_waaMismatchLive_iff`
- `map_probeConstant_iff`
- `map_waaBullSeven_iff` and `map_waaBullTen_iff`
- `map_stateToolFits_iff`
- `Tier.map` and `map_tier_hasLiveShare_iff`
- `map_rePitch`
- `map_isShareDrop_iff`
- `ActualWeld.map`, `ConsequentialistConvention.DeliberationSample.map`,
  `ConsequentialistConvention.map_dropCount`, and
  `ConsequentialistConvention.map_dropCountInFiber`
- `Grid.DirectedConvention.map_landsWithShareDrop_iff`
- `Grid.DirectedConvention.map_hasShareDropLanding_iff`
- `Grid.DirectedConvention.map_shareDropLine_iff`
- `Grid.DirectedConvention.map_shortfallClosedAt_iff`
- `Grid.DirectedConvention.map_waaAversionContext_iff`
- `Grid.DirectedConvention.map_waaFullyEnlightened_reflect` and
  `map_waaFullyEnlightened_of_surjective`; the latter's coverage hypothesis is
  witnessed by `CoverageNegative.waaFullyEnlightened_needs_coverage`
- `Grid.DirectedConvention.WaaPathClaim.map`,
  `map_waaPathClaim_holds_iff`, `map_waaFullyEnlightened_iff`,
  `map_faith_object_eq`, and `map_waaFaithPrinciple_reflect`; the
  coverage-carrying entries share that same witness
- `BeingCoarsening.displayMap` and its `map_*_iff` lemmas for
  `InFiber`, `SameFiber`, `FiberInhabited`, `ActualFiberInhabited`,
  `SentientTag`, `FiberAtPole`, `ActualFiberInhabitedOn`,
  `ActualFiberInhabitedWithin`, `FiberAtPoleOn`, `FiberAtPoleOnWithin`,
  `FiberAtPoleWithin`, `LiveFiberAtPole`, `LiveFiberAtPoleOn`,
  `LiveFiberAtPoleWithin`, `SelfAptTag`, `SelfAptTagWithin`,
  `LiveSelfAptTag`, `Patchy`, `SelfConditioningTag`, and
  `StrongSelfConditioningTag`
- `DirectionCoarsening.displayMapDir`, `mapDir_sameTick_iff`,
  `mapDir_resolutionBounded_iff`, and
  `resolutionBounded_of_reparam_collapses`
- The grid-convention row transports:
  `map_intraWeldArrowRow_obeys`, `map_doerDeedRow_obeys`,
  `map_contentIntraWeldArrowRow_obeys_of_variation`,
  `map_intraWeldArrowLadder_obeys`,
  `map_intraWeldArrowLadder_obeys_succ`,
  `map_intraWeldArrowLadder_no_level_final`,
  `map_doerDeedLadder_obeys`, `map_doerDeedLadder_obeys_succ`, and
  `map_doerDeedLadder_no_level_final`

Together these say that all current pole, probe, tier, configuration,
direction-coarsening, share-drop, and share-drop-line predicates are legal
display predicates: changing the carrier by a reparameterization changes
notation, not truth.

**Direction-smuggling detector.** The transpose operation now lives in the
signature layer, beside the vocabulary it transports. `Grid.transpose` reverses
only the argument order of `conditions`. `transpose_conditionsEither_iff`
proves that `ConditionsEither` survives the reversal.
`Grid.DirectedConvention.transpose_deliveredTo_iff` proves that directed
delivery reverses. `BeingCoarsening.transpose_selfConditioningTag` shows the
directed refinement reversing exactly at the delivery line while fiber
membership and actuality stay put. This gives future delivery-facing results a
quick test: if they claim direction, they owe model-supplied asymmetry or
irreflexivity.
The axis operations are pinned as orthogonal: `transpose_transpose` is the
involution, `map_transpose` commutes display reparameterization with
transposition, `staticized_transpose` commutes function removal with
transposition, and `map_staticized` commutes display reparameterization with
function removal. These are definitional equalities, so the detector is not
carrying extra operational content.
`DirectionCoarsening.transpose_subTickDelivery` is the delivery-axis companion:
tick equality survives transposition, while the delivery line reverses.

**Negative examples.** `Meta/InvarianceNegative.lean` holds these countermodels.
`InvarianceNegative.TwoBottom` is a two-element carrier
where every element is order-equivalent to every other element, with `chosen`
as the designated `shareBot`. `mergeToUnit` maps both elements to the single
unit value and is a `DisplayReparam`. `twoBottomGrid` has one being, one call,
one response, responds everywhere, and grades every response as `other`.

The named checks show:

- `twoBottomGrid_terminus`: `twoBottomGrid.Terminus ()` holds.
- `not_oldEqTerminus_twoBottomGrid`: the obsolete equality-token predicate
  fails before reparameterization.
- `oldEqTerminus_map_mergeToUnit`: the obsolete equality-token predicate holds
  after the merge.
- `oldEqTerminus_not_invariant`: the new `Terminus` transports across the
  merge, while the old equality-token predicate would not have transported.

This is the formal certificate that replacing equality with `AtBot` was a real
de-operationalisation, not a naming preference.

**`DirectionNegative`.** `forwardGrid` and `backwardGrid` are one-being,
two-call grids identical except that `conditions` is reversed.
`conditionsEither_agrees` shows they have the same symmetric closure at every
pair; `conditions_disagree` exhibits a pair where the directions differ;
`no_direction_recovery_from_conditionsEither` concludes that no function of the
symmetric closure is correct on both grids. This is the formal certificate that
direction is not carried by the correlational structure.
`not_strict_twoBottom` records the carrier-wide strictness failure on the
two-bottom negative carrier.

**`InteriorDirectionNegative`.** `RawWeld.transposeCR` swaps the call and
response faces when they share a carrier. `transposeCR_involutive`,
`unorderedCRContent_transpose_invariant`, and `transpose_swaps_readings` pin
the transposition behavior: unordered content is unchanged while the display
labels reverse. `no_interior_direction_recovery` uses the same collision shape
one grain down: unordered call/response content does not recover which face is
call. This is the formal certificate that the intra-weld arrow is display, not
a field-carried before/after.

**`DirectionCoarseningWitness`.** `registerClockUnitTick` gives the raw
register clock one universal tick. `registerClock_unitTick_not_resolutionBounded`
proves this cannot be coherent over the injective `Nat` display: registers `0`
and `1` share a tick but do not have order-equivalent shares.

The positive slow-clock limit is modeled on a lawful one-point display:
`fullyCoarseRegisterClockGrid` keeps the register-clock response and delivery
shape while grading every weld in `Unit`. `unit_directionVoid_via_mergeToUnit`
gets `DirectionVoid Unit` through the existing legal display collapse from the
all-equivalent `TwoBottom` carrier, and
`fullyCoarseRegisterClock_no_timeDirection` applies the one-tick
resolution-bound theorem to the fully coarse grid. The theorem
`registerClock_directionCoarsening_independence` is the soul-guard: macro
sentience and self-conditioning for the register clock do not consume either a
direction coarsening or a resolution-bound hypothesis.

**`ContentNegative`.** `allStoneGrid` is a no-response grid whose beings are
all stone-typed and whose act-time tiers have no live share. It proves
`contentBeingsRow_not_obeys_allStone` and
`contentGridLensRow_not_obeys_noLive`. The existing two-bottom carrier gives
`twoBottomGrid_directionVoid`, and
`contentBeforeAfterRow_not_obeys_twoBottom` shows the directed-time content row
also needs its strict-direction aptness hypothesis. The empty-domain witnesses
separate two vacuities: `emptyCallGrid_false_stone_and_respondsToEveryCall`
shows that an empty call axis collapses stone with call-entire response, while
`emptyBeingGrid_no_liveTier` and `contentBeingsRow_obeys_emptyBeing` show that
an empty being axis has no act-time counterexample and the beings row fuses
vacuously. `constantResponseGrid_no_variation` and
`contentIntraWeldArrowRow_not_obeys_constantResponse` are the intra-weld
content countermodel: if every call gets the same response, the response-
variation aptness hypothesis is load-bearing.

**`CoverageNegative`.** `embedIntoNat` sends the one-point carrier to `0` in
`Nat`, leaving all target strictness at and above `1` outside the image.
`directionVoid_needs_coverage` shows that carrier-wide direction-voidness does
not push forward when the target has strict comparisons outside the image.
`phantomGrid` gives the parallel faith-closure witness:
`waaFullyEnlightened_needs_coverage` shows that the mapped carrier introduces
live tendencies the source never quantified over, so full enlightenment does
not preserve without coverage.

**`MisFeedNegative` in `Identification/Residues.lean`.** `IndexSeekingForm` is the type of candidate
answer-functions for the index-seeking question-shape: one designation per
field residue (`Call × Response`), each purporting to name the residue's
self-pole index. `AnswersCorrectly` is the success condition for the form:
correctness at every actual weld. `FieldCollision` packages the hypothesis:
two actual welds with the same field residue and distinct agents.

`no_indexSeeking_success_of_collision` is the fence: under a collision, no
answer-function for the form succeeds. The quantifier ranges over every
candidate answer-function, so the non-derivability is a property of the
question-shape, not of one failing instance. It is the same internal route as
the wrinkle-1 recovery theorems (`CorrectFieldRecovery`,
`no_agent_recovery_from_same_call_response`), specialized to the
designation-universe the avyākata reading needs.

`collisionGrid` is the non-vacuity witness: a concrete grid in which two beings
actually produce the same call-response pair, so the fence's hypothesis is
exhibited rather than assumed, the same duty `clockGrid` discharges for the
function/share split.

`deliveryTwinAnswers` is the gate: in the same concrete model, the
delivery-typed twin question has a checked answer-function. The claim is
model-local by design: it shows the fence does not enclose delivery-questions,
and asserts nothing about their answerability in general, which the standing
no-verdicts deny.

Three layers are stated in order of decreasing formality: the question-shape is
fenced schematically over the modeled designation-universe; the collision
hypothesis is witnessed concretely; and the adequacy of that universe to the
avyākata's natural-language questions is a modeling claim, argued in prose and
owned as such. The third layer cannot be discharged in Lean, and the paper does
not pretend otherwise; it is an aptness claim of the same standing as the
content-row hypotheses beside `ContentNegative`.

**`BeingNegative`.** The signature-level `BeingCoarsening.id` and
`BeingCoarsening.total` already show that identity and universal merge
partitions are legal for any grid; `total_sameFiber` and
`id_not_sameFiber_of_ne` pin the disagreement for any distinct fine tags.
Downstream, `twoBeingGrid` has two fine tags with identical response, grade,
and symmetric delivery behavior. `κmerge` reads them as one macro tag; `κsplit`
keeps them split. `merge_same_fiber` and `split_not_same_fiber` show the
readings disagree at `false`/`true`, and `no_partition_recovery` proves no
function of the shared grid data recovers both. This is the formal certificate
that the being-boundary is a reading, not grid-carried structure.

**`WeldNegative`.** `twoWeldGrid` has two fine call-response pairings over the
same response, grade, and symmetric delivery data. `σmerge` reads them as one
macro act; `σsplit` splits them by weld-grain. `merge_same_pairing` and
`split_not_same_pairing` show the readings disagree, and
`no_weld_boundary_recovery` proves no function of the shared grid data
recovers both. This is the formal certificate that weld individuation is a
segmentation convention, not grid-carried structure.

**`DoerDeedNegative`.** The doer/deed witness reuses a small two-call grid
data shape and supplies two readings over it: `beingPriorReading` and
`mutualReading`. `priority_readings_disagree` pins the collision, and
`no_priority_recovery` proves no function of the visible grid data recovers a
unique priority relation. This is why `doerDeedRow` remains schema-only rather
than adding a priority primitive to `Grid`.

**Verdict ledger.** `Meta/VerdictLedger.lean` records the verdict-history
paragraph as `generatorRecord`. The four retypes are four entries; the
checked count is `generatorRecord_retype_count`, and
`generatorRecord_newCell_count` records that no new row is added. The six-kind
view is the projection `restraintKind`, checked by
`generatorRecord_restraintKind_seen_count` and
`restraintKind_exhaustive_on_record`. Lean anchors are pinned by examples that
name `DirectionNegative`, `InteriorDirectionNegative`, the transposition pair,
the fox theorem, and `MisFeedNegative.fence_and_gate`. The checkable half of the falsifier is
`misFeed_entries_carry_decomposition`; the rate-trend half remains prose.

**Glossary.** `Meta/Glossary.lean` is the canonical source for glossary data.
Each `GlossaryEntry` records a term, provenance kind, newcomer-facing gloss,
checked Lean anchors, and backward-only `seeAlso` references. Lean checks the
table length, term uniqueness, `seeAlso` resolution to earlier rows, and anchor
resolvability through `#verify_glossary_anchors`. The glosses' accuracy and
canonical caveats remain prose; the Disclaimers carry expert-facing departures.
`WeldAndArrow/Gen/Glossary.lean` renders the table to `Exposition/Glossary.md`.

---

## 6. Meta/Audit.lean

`Meta/Audit.lean` imports `Meta/Invariance.lean`,
`Meta/InvarianceNegative.lean`, `Meta/ReflexivityWitness.lean`,
`Meta/VerdictLedger.lean`,
`Doctrines/SraddhaNegative.lean`,
`Doctrines/FaithNegative.lean`, and `Doctrines/Deliberation.lean`, plus the
new correlations, fetters, and factors negative modules, then pins selected
`#print axioms` outputs with `#guard_msgs`.

The audited declarations are:

- `no_agent_recovery_of_field_collision`
- `DirectionNegative.no_direction_recovery_from_conditionsEither`
- `CoverageNegative.directionVoid_needs_coverage`
- `CoverageNegative.waaFullyEnlightened_needs_coverage`
- `Grid.stateToolFits_iff_atBot`
- `Grid.map_actual_iff`
- `Grid.map_isShareDrop_iff`
- `strict_asymm`, `strict_trans`, and `Grid.transpose_transpose`
- `Grid.map_transpose`, `Grid.staticized_transpose`, and `Grid.map_staticized`
- `Grid.DirectedConvention.DirectionCoarsening.mapDir_resolutionBounded_iff`
- `DirectionCoarseningWitness.registerClock_unitTick_not_resolutionBounded`
- `DirectionCoarseningWitness.unit_directionVoid_via_mergeToUnit`
- `DirectionCoarseningWitness.fullyCoarseRegisterClock_no_timeDirection`
- `DirectionCoarseningWitness.registerClock_directionCoarsening_independence`
- `Grid.DirectedConvention.map_landsWithShareDrop_iff`
- `Grid.DirectedConvention.BeingConvention.BeingCoarsening.map_selfConditioningTag_iff`
- `Grid.DirectedConvention.BeingConvention.BeingCoarsening.map_fiberAtPoleOn_iff`
- `Grid.DirectedConvention.BeingConvention.BeingCoarsening.total_sameFiber`
- `Grid.DirectedConvention.BeingConvention.BeingCoarsening.id_not_sameFiber_of_ne`
- `Grid.map_waaBullSeven_iff`
- `Grid.map_waaBullTen_iff`
- `Grid.bullSeven_not_bullEight`
- `Grid.bullTen_to_bullNine`
- `CorrelationsNegative.pratyekabuddha_countermodel`
- `CorrelationsNegative.no_stage_boundary_recovery`
- `Grid.classQuiet_no_clench_in_class`
- `Fetter.kind_lower_iff_cut_by_nonReturn`
- `Grid.arhatPathQuiet_iff_fiberAtPole`
- `Grid.all_fetters_cut_at_arhatFiber`
- `Grid.identityView_excluded_at_arhatFiber`
- `Grid.conceit_excluded_at_arhatFiber`
- `Grid.waaIrreversibleRegime_conditional`
- `Grid.lower_fetters_covered_by_rites_view_resolve`
- `Grid.waaStreamWinner_iff_streamEntry_cutClasses`
- `Grid.waaNonReturner_iff_nonReturn_cut`
- `Grid.waaSerialFactorRegime_conditional`
- `Grid.waaOnceReturner_attenuation_witness`
- `FactorsNegative.no_hold_conceit_boundary_recovery`
- `FactorsNegative.seen_run_underdetermines_factorOrder`
- `FactorsNegative.lineage_underdetermined_by_seen_run`
- `FettersNegative.seen_run_underdetermines_fetterCut`
- `Grid.DirectedConvention.waaPathOught_conditional`
- `Grid.DirectedConvention.waaFaithOught_conditional`
- `Grid.DirectedConvention.map_waaFaithPrinciple_reflect`
- `FaithNegative.waaFaithPrinciple_id_fails`
- `Grid.DirectedConvention.no_waa_path_at_pole`
- `Grid.DirectedConvention.map_waaAversionContext_iff`
- `MisFeedNegative.fence_and_gate`
- `misFeed_entries_carry_decomposition`
- `OrthogonalityNegative.waaFullyEnlightened_stronger_than_terminus`
- `Grid.stone_of_no_call`, `Grid.respondsToEveryCall_of_no_call`, and
  `Grid.allStone_of_no_being`
- `ContentNegative.emptyCallGrid_false_stone_and_respondsToEveryCall`,
  `ContentNegative.emptyBeingGrid_no_liveTier`, and
  `ContentNegative.contentBeingsRow_obeys_emptyBeing`
- The new intra-weld/doer-deed/reflexivity surface:
  `InteriorDirectionNegative.transposeCR_involutive`,
  `InteriorDirectionNegative.unorderedCRContent_transpose_invariant`,
  `InteriorDirectionNegative.transpose_swaps_readings`,
  `DoerDeedNegative.no_priority_recovery`,
  `ContentNegative.contentIntraWeldArrowRow_not_obeys_constantResponse`,
  `intraWeldArrowRow_*`, `doerDeedRow_*`,
  `contentIntraWeldArrowRow_obeys_of_variation`,
  `intraWeldArrowLadder_*`, `doerDeedLadder_*`,
  `Nishitani.intraWeldArrow_sunyata`, `Nishitani.doerDeed_sunyata`,
  the new `map_*` row/ladder theorems, and the two `ladderRungGrid_*`
  reflexivity witness theorems
- `Grid.ConsequentialistConvention.dropCountInFiber_le_dropCount`,
  `Grid.ConsequentialistConvention.dropCount_eq_sum_dropCountInFiber`, and
  `Grid.ConsequentialistConvention.map_dropCountInFiberSum`
- `ObjectiveNegative.split_dropCount_sum_eq_mergedDropCount`

The pinned result is: no audited theorem depends on `sorry` or
`Classical.choice`. All audited declarations are axiom-free except
`DirectionNegative.no_direction_recovery_from_conditionsEither`, which depends
on exactly `[propext, Quot.sound]`, and
`InteriorDirectionNegative.unorderedCRContent_transpose_invariant`, plus
`FettersNegative.seen_run_underdetermines_fetterCut`,
`Grid.waaOnceReturner_attenuation_witness`,
`FactorsNegative.seen_run_underdetermines_factorOrder`, and
`Grid.DirectedConvention.map_waaFaithPrinciple_reflect`, plus the three
census theorems `Grid.ConsequentialistConvention.dropCountInFiber_le_dropCount`,
`Grid.ConsequentialistConvention.dropCount_eq_sum_dropCountInFiber`, and
`Grid.ConsequentialistConvention.map_dropCountInFiberSum`, which depend on
`[propext]`.

The Lake build targets the library `WeldAndArrow` by default and also defines
the non-default `lean_exe` targets `exposition_gen`, `glossary_gen`, and
`exposition_generation_test`; there is no `Main.lean`.

---

## 7. Logical Strength

The definitional identities include `share_eq_grade`, `selfAnchored`,
`rePitch_tendency_eq_share`, the delivery/aiming biconditionals,
`isShareDrop_iff_rePitch_tendency_drop`, the recorded-utterance identities,
`recordedUtterance_grade_determined`, the reception-pair tendency lemmas, and
the basic `map_*` identities in `Meta/Invariance.lean`.

The elementary consequences are projections, witness assemblies,
contradictions, and short order arguments. The important non-definitional order
arguments are the `AtBot` share-drop obstruction, `strict_irrefl`, and the
display-reparameterization transport lemmas. The `FoxCase` checks sit here too:
their proofs unfold concrete responses, project existing identities, or close
short `Nat` order goals with `decide`.

The conditional impossibility results are the agent-recovery theorems, the
direction negative witness, the intra-weld direction witness, the
being-boundary negative witness, the weld-boundary negative witness, the
sraddha orthogonality witness, the severed-transcript gradeability negative,
and the other-power regime/share negative. The concrete model and carrier
results include `clockGrid`, `registerClockGrid`, `backslideGrid`,
`gradingCollisionGrid`, `WeldNegative.twoWeldGrid`, `FoxCase.foxGrid`, and
`TarikiCase.tarikiGrid`, plus the `InteriorDirectionNegative` two-face raw
weld carrier: they witness, respectively, function/share splitting,
diagnosis-time macro coarsening, same-being backsliding plus
severed-transcript grade underdetermination, same-field/different-share
grading, weld-boundary underdetermination, the fox run-through with no
pole-arrival, fixed-call landing without a second act grammar, and intra-weld
orientation underdetermination. The self-line witness is a permission witness,
not an existence claim about any real regime.

One structural caution remains: `Terminus` is vacuously true of every `Stone`;
use `LiveTerminus` or `ResponsiveTerminus` when non-vacuous response-function
matters.


===== FILE: Exposition/Assumptions.md =====

# Assumptions

Generated from `WeldAndArrow/Meta/AssumptionLedger.lean` by `lake exe assumptions_gen`. `WeldAndArrow/Signature/Assumptions.lean` holds the compile-checked anchor pins; statement prose is canonical here.

## A. What Is Asserted

### A.1 No prior agent

A weld is the primitive occurrence. `Grid.index` and `Grid.share` are projections from a completed `RawWeld`, not fields recovered from a separate performer or act. `no_agent_recovery_of_field_collision` records the internal obstruction: the same call-response field residue can be produced by distinct actual agents.

**Checked anchors (Signature):** `WAA.RawWeld` (proof), `WAA.Grid.index` (proof), `WAA.Grid.share` (proof), `WAA.no_agent_recovery_of_field_collision` (witness)

### A.2 Nothing self-indexed is stored

`Config` stores only `tendency : Contrib`. It has no owner, being, weld, or field-residue slot. `rePitch` uses the received weld's share and ignores the prior configuration value.

**Checked anchors (Signature):** `WAA.Config` (proof), `WAA.Config.tendency` (proof), `WAA.Grid.rePitch` (proof)

### A.3 The self-pole index is just live share

`HasSelfPoleIndex w` is `not AtBot (share w)`, and when the predicate is live the carried `selfPoleIndex` is the weld's agent tag.

**Checked anchors (Signature):** `WAA.Grid.HasSelfPoleIndex` (proof), `WAA.Grid.selfPoleIndex_eq_agent_of_hasSelfPoleIndex` (proof), `WAA.Grid.no_self_pole_index_of_atBot` (proof)

### A.4 Stone and terminus split function from share

A `Stone` mounts no response. A `Terminus` may mount responses, but every mounted response is at the pole-class. `AtPoleClass` intentionally includes the vacuous stone case.

**Checked anchors (Signature):** `WAA.Grid.Stone` (proof), `WAA.Grid.Terminus` (proof), `WAA.Grid.AtPoleClass` (proof), `WAA.Grid.stone_is_terminus_vacuously` (proof), `WAA.clockGrid_function_share_split_witness` (witness)

### A.5 Self-lines are permitted, not built in

The bare signature does not impose irreflexivity on `conditions`; a model may supply reflexive delivery, and then the directed vocabulary can read a self-line.

**Checked anchors (Signature):** `WAA.Grid.conditions` (proof), `WAA.Grid.DirectedConvention.DeliveredTo` (proof), `WAA.Grid.DirectedConvention.LandsAt` (proof), `WAA.AssumptionLocalWitnesses.signature_self_line_permitted` (witness)

**Downstream elaboration:** `WAA.SelfLineWitness.selfLine_landsAt_self` (witness), `WAA.SelfLineWitness.selfLine_waaOwnershipFace_self` (witness)

## B. What Is Deliberately Declined

### B.1 No arrow in `conditions`

The signature assumes no asymmetry, irreflexivity, or transitivity for `conditions`. `ConditionsEither` is the symmetric field fact; direction enters only in `Grid.DirectedConvention`. The downstream `DirectionNegative` witness elaborates this as non-recovery from symmetric closure.

**Checked anchors (Signature):** `WAA.Grid.ConditionsEither` (proof), `WAA.Grid.conditionsEither_symm` (proof), `WAA.Grid.DirectedConvention.TimeDirection` (proof), `WAA.Grid.transpose` (witness), `WAA.Grid.transpose_conditionsEither_iff` (witness), `WAA.Grid.DirectedConvention.transpose_deliveredTo_iff` (witness), `WAA.RawWeld.transposeCR` (witness), `WAA.AssumptionLocalWitnesses.no_direction_recovery_from_conditionsEither` (witness), `WAA.InteriorDirectionNegative.no_interior_direction_recovery` (witness)

**Downstream elaboration:** `WAA.DirectionNegative.no_direction_recovery_from_conditionsEither` (witness)

### B.2 No `PreorderTop`

The signature supplies only `PreorderBot`. The share-zero pole is an attained bottom order-class (`AtBot`); the total-share or solipsist pole is an asymptote, not an element of the interface. `StrongSelfConditioningTag` is named and shelved in the being convention for the same reason.

**Checked anchors (Signature):** `WAA.PreorderBot` (proof), `WAA.AtBot` (proof), `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.StrongSelfConditioningTag` (proof), `WAA.AssumptionLocalWitnesses.nat_preorderBot_has_no_top` (witness)

### B.3 No privileged person-partition

A being boundary is supplied by a diagnosis-time `BeingCoarsening`, not stored as a field of `Grid`. The signature already admits both identity and total coarsenings for any grid; the downstream `BeingNegative` witness elaborates this as non-recovery of a unique partition from grid data.

**Checked anchors (Signature):** `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening` (proof), `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.InFiber` (proof), `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.SameFiber` (proof), `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.id` (witness), `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.total` (witness), `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.total_sameFiber` (witness), `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.id_not_sameFiber_of_ne` (witness), `WAA.AssumptionLocalWitnesses.partition_merge_split_disagree` (witness)

**Downstream elaboration:** `WAA.BeingNegative.no_partition_recovery` (witness)

### B.4 Direction resolution is display, not signature furniture

A clock's finite delivery-axis resolution is supplied by a diagnosis-time `DirectionCoarsening`, not by a `Grid` field and not by any pole or legitimacy predicate.

**Checked anchors (Signature):** `WAA.Grid.DirectedConvention.DirectionCoarsening` (proof), `WAA.Grid.DirectedConvention.DirectionCoarsening.SameTick` (proof), `WAA.Grid.DirectedConvention.DirectionCoarsening.ResolutionBounded` (proof), `WAA.Grid.DirectedConvention.DirectionCoarsening.no_timeDirection_within_tick` (proof), `WAA.Grid.DirectedConvention.DirectionCoarsening.no_timeDirection_of_resolutionBounded_subsingleton` (proof), `WAA.Grid.DirectedConvention.DirectionCoarsening.transpose_subTickDelivery` (witness)

**Downstream elaboration:** `WAA.DirectionCoarseningWitness.registerClock_unitTick_not_resolutionBounded` (witness), `WAA.DirectionCoarseningWitness.unit_directionVoid_via_mergeToUnit` (witness), `WAA.DirectionCoarseningWitness.fullyCoarseRegisterClock_no_timeDirection` (witness), `WAA.DirectionCoarseningWitness.registerClock_directionCoarsening_independence` (witness)

### B.5 Contribution values are display, not operational tokens

The Signature layer itself uses only order and pole vocabulary around `share`. The downstream `DisplayReparam` / `InvarianceNegative` modules give the full transport discipline: order- and pole-preserving display changes preserve the legal predicates, while equality to the chosen bottom does not.

**Checked anchors (Signature):** `WAA.Grid.share_eq_grade_check` (proof), `WAA.AtBot` (proof), `WAA.OrderEq` (proof), `WAA.Grid.Terminus` (proof)

**Downstream elaboration:** `WAA.DisplayReparam` (proof), `WAA.DisplayReparam.atBot_iff` (proof), `WAA.InvarianceNegative.oldEqTerminus_not_invariant` (witness)

## C. Conveniences and Stand-Ins

### C.1 Hand-rolled order classes

`Preorder` and `PreorderBot` are hand-rolled to keep assumptions visible and dependency-free. They play the local role Mathlib order classes would play, without importing Mathlib.

**Checked anchors (Signature):** `WAA.Preorder` (proof), `WAA.PreorderBot` (proof), `WAA.shareBot` (proof), `WAA.shareBot_le` (proof)

### C.2 `_before` is retained but currently ignored by `rePitch`

`rePitch` keeps a `_before` slot because the operation is conceptually a re-pitch from a prior configuration. The current implementation ignores that slot; the proof anchor below is a tripwire for the day that changes.

**Checked anchors (Signature):** `WAA.Grid.rePitch` (proof)

> Note: The signature file keeps an `rfl` example showing that two prior configurations produce the same re-pitch for the same received weld.

### C.3 The scalar is display over a partial order

`WaaMismatchGrade` lives in `Doctrines`, so this Signature module does not import it; the Signature-side checked fact is that `share` is the only contribution value exported by a weld.

**Checked anchors (Signature):** `WAA.Grid.share` (proof), `WAA.Grid.share_eq_grade_check` (proof)

**Downstream elaboration:** `WAA.Grid.WaaMismatchGrade` (proof), `WAA.Grid.waaMismatchGrade_eq_share` (proof)

### C.4 `Models.lean` witnesses are illustrative

The clock and register-clock models anchor possibility checks and taxonomy examples; they are not uniqueness claims.

**Checked anchors (Signature):** `WAA.clockGrid` (witness), `WAA.registerClockGrid` (witness), `WAA.registerClock_macro_sentient` (witness), `WAA.registerClock_macro_selfConditioning` (witness)

## Axiom audit

- `WAA.no_agent_recovery_of_field_collision` -- pinned by `#guard_msgs` in `WeldAndArrow/Signature/Assumptions.lean` to depend on no axioms.
- `WAA.Grid.DirectedConvention.DirectionCoarsening.no_timeDirection_within_tick` -- pinned by `#guard_msgs` in `WeldAndArrow/Signature/Assumptions.lean` to depend on no axioms.
- `WAA.Grid.DirectedConvention.DirectionCoarsening.no_timeDirection_of_resolutionBounded_subsingleton` -- pinned by `#guard_msgs` in `WeldAndArrow/Signature/Assumptions.lean` to depend on no axioms.


===== FILE: Exposition/Glossary.md =====

# Glossary

Generated from `WeldAndArrow/Meta/Glossary.lean` and `WeldAndArrow/Exposition/Glossary.lean` by `lake exe exposition_gen`. Gloss accuracy remains prose; Lean checks term uniqueness, backward `seeAlso` references, and anchor resolvability. Canonical Buddhist terms are glossed for newcomers; expert caveats live in the Disclaimers.

| Term | Kind | Definition | Checked anchors | See also |
| --- | --- | --- | --- | --- |
| floor | Theory | A floor is the place where no deeper support is being claimed. In this system it names the self-emptying limit at which every distinction is conventional, including the distinction between conventional and ultimate truth. | `WAA.Grid.Tier.floor` | — |
| genjō | Canonical | Genjō means manifestation, the way something comes forward as this case. In this system it also names the pole-class face where no share is claimed. | `WAA.AtBot` | `floor` |
| grid | Theory | A grid is a deliberately small model of who responds to what and how those responses are connected. It supplies the apparatus for welds, grades, delivery, and diagnostics without pretending to be the whole doctrine. | `WAA.Grid` | `floor` |
| act-grammar | Theory | An act-grammar is a way to parse an occurrence into roles. In this system it is the three-row pattern that lets the grid discuss dependence, manifestation, resonance, practice, and causal carrying without storing a self. | `WAA.Grid.Tier`, `WAA.Grid.Distinction` | `grid` |
| mujishō-sōe | Canonical | Mujishō-sōe means mutual dependence without own-being. In this system it is the first-row dependence face of the act-grammar. | — | `act-grammar` |
| kannō-sōe | Canonical | Kannō-sōe means responsive resonance or mutual answering. In this system it is the second-row dependence face, where a call and a response are placed together. | `WAA.Grid.MountsAt` | `act-grammar` |
| banpō susumite | Canonical | Banpō susumite means the myriad dharmas advancing. In this system it is the second-row enactment face, where what arrives is answered by a concrete response. | `WAA.Grid.Actual` | `kannō-sōe` |
| shō | Canonical | Shō means realization. In this system it is read as the non-possessive face at the floor, not as a stored attainment. | — | `floor` |
| shu | Canonical | Shu means practice. In this system it names the enacted side of the occurrence, the doing that is spent as the occurrence happens. | `WAA.RawWeld` | `act-grammar` |
| shushō-ittō | Canonical | Shushō-ittō means practice and realization as non-dual. In this system it is read as one occurrence with two faces, not two events that later get joined. | — | `shō`, `shu` |
| shugenjō | Theory | Shugenjō is the paper's compound for practice that manifests without a scaffold. It is treated as a proper subset of genjō, not as a synonym for all manifestation. | — | `genjō`, `shu` |
| genjōkōan | Canonical | Genjōkōan is a manifest case, not an abstract principle floating free of use. In this system it names the first-row manifestation arriving in a second-row situation. | — | `genjō`, `kannō-sōe` |
| satori | Canonical | Satori means awakening or realization in ordinary Buddhist usage. In this system it is a pole-typed dharmas-forward event and is kept distinct from shō and kenshō. | — | `genjō`, `shō` |
| call | Theory | A call is something that arrives to be answered. In the grid it is the input slot of a weld, the thing a response addresses or fails to address. | `WAA.RawWeld.call`, `WAA.Grid.RecordedUtterance.answersCall` | `grid` |
| response | Theory | A response is what a being produces when it answers a call. In the grid it is the output slot of a weld and the visible side of function. | `WAA.RawWeld.response`, `WAA.Grid.MountsAt` | `call` |
| field | Theory | A field is the impersonal web of conditioning and delivery. In this system it carries connections through time without carrying an owner or self-index. | `WAA.Grid.conditions`, `WAA.Grid.ConditionsEither` | `grid` |
| inga | Canonical | Inga means cause and effect. In this system it is read as the field's conditioning structure, not as a stored moral account. | `WAA.Grid.conditions` | `field` |
| delivery | Theory | Delivery is the fact that one occurrence reaches another as part of the field. It is checked by a directed relation, but the act that receives it still has to be actual. | `WAA.Grid.DirectedConvention.DeliveredTo`, `WAA.Grid.DirectedConvention.LandsAt` | `field` |
| delivery-regime | Theory | A delivery-regime is the whole pattern of what reaches what. In this system it is ceded as a world-fact and is never something a single act commands. | `WAA.Grid.conditions` | `delivery`, `field` |
| weld | Theory | A weld is one concrete occurrence of answering. In the grid it bundles agent, call, and response, so the act's index is made by the act rather than stored before it. | `WAA.RawWeld`, `WAA.Grid.Weld`, `WAA.Grid.index` | `call`, `response` |
| reach-back | Theory | Reach-back is a reception reading what arrived as the return of some earlier deed. In the system it is full when delivery supplies the earlier deed and vacuous when it does not. | `WAA.Grid.DirectedConvention.WaaReachBackFull`, `WAA.Grid.DirectedConvention.deliveredTo_iff_waaReachBackFull` | `delivery`, `weld` |
| upādāna | Canonical | Upādāna ordinarily means grasping or appropriation. In this system it is the traditional word closest to reach-back, with the technical decomposition handled by the grid. | `WAA.Grid.WaaAppropriates` | `reach-back` |
| vacuity | Theory | Vacuity is a place left unfilled rather than a false claim. In the system it names the reach-back shape where appropriation occurs but delivery supplies no deed to fill the second slot. | `WAA.Grid.DirectedConvention.NotDeliveredTo` | `reach-back`, `delivery` |
| share | Theory | A share is the portion of an occurrence's drive that is claimed as self-maintaining. In the grid it is the contribution value projected from a weld. | `WAA.Grid.share`, `WAA.Grid.share_eq_grade_check` | `weld` |
| grade | Theory | A grade is an ordered display of how much share a concrete response carries. It is third-personal in form but indexical in content, because it reads this weld's placement. | `WAA.Grid.grade`, `WAA.Grid.WaaMismatchGrade`, `WAA.Grid.share_eq_grade_check` | `share`, `weld` |
| clench | Theory | Clench is self-maintenance tightening around a response. In the grid it is read through live share rather than through a stored inner state. | `WAA.Grid.HasSelfPoleIndex`, `WAA.Grid.WaaAppropriates` | `share`, `weld` |
| arrogation | Theory | Arrogation is a response claiming subjecthood for itself. In this system it is per call and per weld, never a standing rank possessed by a being. | `WAA.Grid.HasSelfPoleIndex` | `clench`, `weld` |
| self-forward | Theory | Self-forward means carrying a self toward what is met. In this system it is the delusive direction of a live weld, not a permanent condition. | — | `arrogation`, `weld` |
| function | Theory | Function is the ability to mount a response at all. The grid keeps it separate from share, so answering a call and claiming the answer are not the same fact. | `WAA.Grid.MountsAt`, `WAA.Grid.RespondsToEveryCall` | `response`, `share` |
| pole | Theory | A pole is the zero-share class in the ordering. In the grid it is represented by `AtBot`, so the system can speak of no live self-index without choosing a numerical scale. | `WAA.AtBot`, `WAA.Grid.AtPoleClass` | `share`, `genjō` |
| stone | Theory | A stone is the zero-function edge: no response is mounted. In this system it can sit at the pole only vacuously, because there is no answering act to grade. | `WAA.Grid.Stone`, `WAA.Grid.stone_is_terminus_vacuously` | `function`, `pole` |
| solipsist | Theory | The solipsist is the opposite edge from the stone. It names the imagined case where response is all self-claim and the call has effectively vanished. | — | `function`, `share` |
| terminus | Theory | A terminus is a responder whose mounted responses lie at the pole. It answers without live share, so the system treats it differently from a stone. | `WAA.Grid.Terminus`, `WAA.Grid.LiveTerminus`, `WAA.Grid.ResponsiveTerminus` | `function`, `pole` |
| tier | Lean convention | A tier is the level at which a claim is offered or tested. Lean uses tiers to distinguish the floor from an act-time weld. | `WAA.Grid.Tier`, `WAA.Grid.Tier.hasLiveShare` | `floor`, `weld` |
| Row 2 | Theory | Row 2 is the resonance row, where call and response are placed together. It is where the system states grade without turning grade into something possessed. | `WAA.Grid.Tier.hasLiveShare` | `kannō-sōe`, `grade` |
| determination clause | Theory | The determination clause says the grade is fixed by what actually drove this response. It rejects a private glow or later outcome as the source of grading. | `WAA.Grid.share_eq_grade_check` | `grade`, `response` |
| probe | Theory | A probe is a third-person way of varying calls to display a response pattern. It can show a placement, but it does not create the placement it shows. | `WAA.Grid.ProbeConstant` | `call`, `grade` |
| effectiveness | Theory | Effectiveness is a landing rate within a delivery-regime. In this system it grades whether calls land; it does not type what a responder is. | `WAA.Grid.DirectedConvention.HasShareDropLanding`, `WAA.Grid.DirectedConvention.ShortfallClosedAt` | `delivery-regime`, `grade` |
| fixed/adaptive | Theory | Fixed and adaptive describe how a responder's output relates to calls. The grid can model both without making adaptivity the ground of liberation. | `WAA.Grid.ResponseInvariant`, `WAA.Grid.ResponseVariesWithCall` | `call`, `response`, `effectiveness` |
| orthogonality rule | Theory | The orthogonality rule says two dimensions do not determine each other. Here function and share type the responder, while effectiveness grades landing. | `WAA.OrthogonalityNegative.waaFullyEnlightened_stronger_than_terminus` | `function`, `share`, `effectiveness` |
| domain joint | Theory | The domain joint is the question of what counts as responding at all. The grid answers it by drive-composition and accepts the resulting artifact cases openly. | `WAA.Grid.MountsAt` | `function`, `response` |
| aimed call | Theory | An aimed call is a deed configured for a landing. In Lean this thin reading is just delivery from the deed to the reception, not a new intention primitive. | `WAA.Grid.DirectedConvention.WaaAimedAt` | `call`, `delivery` |
| re-pitch | Theory | Re-pitch is what a reception hands forward as the next carried tendency. In the current signature it records the received weld's share and forgets the previous configuration. | `WAA.Grid.rePitch`, `WAA.Grid.rePitch_forgets` | `share`, `weld` |
| seed | Theory | A seed is a carried tendency rather than a bearer. In Lean it is modeled by a configuration value with no stored owner, weld, or self-index. | `WAA.Config`, `WAA.Config.tendency` | `field`, `re-pitch` |
| standing/dated | Theory | Standing means carried as a tendency; dated means enacted now. The system treats reading a dated occurrence directly from a standing tendency as a diagnostic error. | `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.RowTag.standingDated`, `WAA.standing_does_not_determine_dated` | `seed`, `weld` |
| three registers | Theory | The three registers are carried field facts, spent weld facts, and per-call grade statements. The split keeps the system from storing self-indexed ownership between acts. | `WAA.SortedFact.register` | `field`, `weld`, `grade` |
| separate/fuse rule | Theory | The separate/fuse rule says live act-time distinctions must be kept apart and floor-level distinctions must fuse. It is the grammar behind the taxonomy's collapse and freeze diagnoses. | `WAA.Grid.Distinction.ObeysSeparateFuse` | `floor`, `tier` |
| collapse/freeze | Theory | Collapse fuses what should be separate; freeze holds separate what should fuse. These are the two basic ways the taxonomy catches a misuse of a distinction. | `WAA.Grid.Distinction.Collapse`, `WAA.Grid.Distinction.Freeze` | `separate/fuse rule` |
| assert/display | Lean convention | Assert and display are two voices for a verdict. The grid asserts grammatical failures inside its lens and only displays value-laden or soteriological shortfall. | `WAA.Grid.VerdictVoice`, `WAA.Grid.ErrorGrade`, `WAA.Grid.ErrorGrade.voice` | `collapse/freeze` |
| orange / eat this | Theory | The orange is the paper's image for its own offering. It gives a thing to receive, while the phrase eat this marks the risk of turning a description into an injunction. | — | `assert/display`, `call` |
| object-axis/subject-axis | Theory | Object-axis means being available as something received; subject-axis means mounting responses oneself. The grid keeps these axes apart, especially for stones and termini. | `WAA.Grid.DirectedConvention.ObjectAxisStanding`, `WAA.Grid.MountsAt` | `delivery`, `function` |
| index-question | Theory | The index-question asks whose act or whose fruit is at issue. In this system the answer is enacted in a weld or stated by a grade, never stored in the field. | `WAA.Grid.index`, `WAA.Grid.HasSelfPoleIndex` | `weld`, `field`, `grade` |
| mis-feed | Identification | A mis-feed is an internal diagnostic where the wrong register is fed to a question. The checked fence covers index-free field answers being used where an index-bearing designation is required. | `WAA.MisFeedNegative.fence_and_gate` | `index-question`, `field` |
| dukkha | Canonical | Dukkha ordinarily names suffering or unsatisfactoriness. In this system it is the mismatch of a live self-maintaining response with delivery that answers to no self. | `WAA.Grid.WaaMismatchGrade`, `WAA.Grid.WaaMismatchLive` | `share`, `delivery`, `clench` |
| before/after | Theory | Before and after are ordinary temporal words. In this system they are a reading over roles in the field, not extra furniture stored inside the field. | `WAA.Grid.DirectedConvention.TimeDirection` | `field`, `delivery` |
| arrow | Theory | The arrow is direction read into conditioning. The retyped system treats direction as a display over field structure, not as a primitive property of that structure. | `WAA.Grid.DirectedConvention.TimeDirection`, `WAA.DirectionNegative.no_direction_recovery_from_conditionsEither` | `field`, `before/after` |
| ratchet | Theory | A ratchet is a mechanism that reads a gradient as direction. In the paper it motivates why beings may read an arrow without making the arrow part of the field itself. | — | `arrow`, `field` |
| Waa marker | Lean convention | The Waa marker flags a system-point-of-view reading. It tells readers that a Lean name reports how the grid reads a concept, not what the tradition must mean by it. | `WAA.Grid.WaaAppropriates`, `WAA.Grid.WaaMismatchGrade`, `WAA.Grid.DirectedConvention.WaaReachBackFull` | `grid` |
| DirectedConvention | Lean convention | DirectedConvention is the namespace for vocabulary that reads direction into the grid. It keeps directed delivery words separate from the direction-free signature beneath them. | `WAA.Grid.DirectedConvention.DeliveredTo` | `arrow`, `delivery` |
| being-convention | Theory | A being-convention is a diagnosis-time way of reading fine tags as macro beings. It permits naming without claiming that the grid stores the true partition. | `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening` | `grid`, `DirectedConvention` |
| coarsening | Lean convention | A coarsening maps fine tags to macro tags. Lean uses it to model a chosen being-reading while leaving the underlying grid unchanged. | `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening`, `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.InFiber` | `being-convention` |
| tag/fiber | Theory | A tag is a fine identifier; a fiber is the set of fine tags read as one macro tag by a coarsening. Fiber-level predicates let the system discuss beings without storing beings as substances. | `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.InFiber`, `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.SameFiber` | `coarsening` |
| tag-region/soma-reading | Theory | A tag-region is a model-supplied class of fine tags. A soma-reading uses such a class to localize a cut to a region without making the region recoverable from grid data alone. | `WAA.Grid.SomaReading` | `tag/fiber` |
| within-cut | Theory | A within-cut is quietness inside a product of call-class and tag-region. It says enactment has ceased in that rectangle, not that a person owns an anti-fetter. | `WAA.Grid.FetterCutWithin` | `tag-region/soma-reading`, `call` |
| vāsanā | Canonical | Vāsanā means residual habit or trace. In this system it is clench still enacted in an uncut region after another region has gone quiet. | — | `clench`, `within-cut` |
| sentient/insentient tag | Theory | A sentient tag is one whose fiber mounts response somewhere; an insentient tag lacks that. The distinction is fiber-level and convention-relative. | `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.SentientTag`, `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.not_sentientTag_iff_fiber_all_stone` | `tag/fiber`, `function` |
| FiberAtPole / SelfAptTag / Patchy | Lean convention | These names describe a fiber spectrum: all actual welds at pole, all actual welds self-apt, or an irreducibly mixed case. They deliberately avoid defining an aggregate share for a fiber. | `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.FiberAtPole`, `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.SelfAptTag`, `WAA.Grid.DirectedConvention.BeingConvention.BeingCoarsening.Patchy` | `tag/fiber`, `pole` |
| coherence (grade) | Theory | Coherence is a display grade over a coarsening. It can report how well a reading behaves, but it never licenses or forbids the naming of a being. | — | `coarsening`, `grade` |
| delegation | Theory | Delegation reads macro agency through an actual fine weld in a fiber. The share remains the fine weld's share, so macro agency does not create a new stored subject. | — | `weld`, `tag/fiber`, `share` |
| freedom witness | Theory | A freedom witness is a countermodel showing that a supposed boundary is not forced by grid data. The being-boundary version permits both split and merge readings of the same fine grid. | `WAA.BeingNegative.no_partition_recovery` | `being-convention`, `coarsening` |
| kenshō | Canonical | Kenshō ordinarily means seeing nature. In this system it is kept as a countable share-ceding event, not as a possession or stored attainment. | `WAA.Grid.IsShareDrop` | `share`, `re-pitch` |
| call/response | Theory | Call/response is the smallest public shape of an occurrence: something arrives and something answers. In the grid this pair is carried by the weld and later inspected by the taxonomy. | `WAA.RawWeld.call`, `WAA.RawWeld.response`, `WAA.Grid.RecordedUtterance` | `call`, `response`, `weld` |
| delivery-engineering | Theorems | Delivery-engineering is legal work on what may arrive. Responder-side it finds calls that land; sowing-side it configures aimed calls without commanding the regime. | `WAA.Grid.DirectedConvention.WaaAimedAt`, `WAA.Grid.DirectedConvention.HasShareDropLanding` | `delivery`, `aimed call` |
| delivery-arrogation | Theorems | Delivery-arrogation is claiming authority over what arrives next. The system treats that as grasping the one register no weld owns. | `WAA.DeliveryArrogationNegative.command_utterance_not_fits` | `delivery-regime`, `arrogation` |
| buddha-side shortfall | Theorems | Buddha-side shortfall is failing to meet a not-yet-buddha's call where it is. It is the pole's live grade and is tracked by effectiveness rather than by terminus typing alone. | `WAA.Grid.DirectedConvention.ShortfallClosedAt`, `WAA.OrthogonalityNegative.waaFullyEnlightened_stronger_than_terminus` | `effectiveness`, `terminus` |
| backsliding theorem | Theorems | The backsliding theorem says a share-drop event cannot be held as a stored attainment. Later live welds are possible because nothing self-indexed is carried between acts. | `WAA.backsliding_witness`, `WAA.backsliding_rePitchSequence_witness` | `kenshō`, `re-pitch`, `seed` |
| memory theorem | Theorems | The memory theorem reads a trace as a seed and remembering as a fresh reception. Felt mineness is predicted at recall-time without being stored before recall. | `WAA.Grid.DirectedConvention.MemoryWitness.memory_witness`, `WAA.Grid.DirectedConvention.WaaVacuousOwnershipFace`, `WAA.Grid.DirectedConvention.WaaDiachronicWhose` | `seed`, `reach-back` |
| retrospective soul | Theorems | The retrospective soul is the error of freezing reach-back into a standing backward owner. It is the psychological version of treating fresh mineness as stored mineness. | `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.sowingReapingRow_not_freeze`, `WAA.no_agent_recovery_of_field_collision` | `memory theorem`, `reach-back`, `standing/dated` |
| prudence theorem | Theorems | The prudence theorem says special authority for self-concern is not recoverable from the grid. The standing cross-gap whose that prudence would need is exactly what the typing declines. | `WAA.Grid.DirectedConvention.PrudentialPrivilegeNegative.not_prudentialPrivilege` | `index-question`, `standing/dated` |
| deliberator theorem | Theorems | The deliberator theorem blocks a maximizer at three joints: supplied being-convention, absent accumulator, and failed command over delivery. It is a check on consequentialist reuse of the grid. | `WAA.ObjectiveNegative.no_grid_data_objective_for_my_drops`, `WAA.TransferNegative.adaptive_track_record_underdetermines_new_effect`, `WAA.DeliveryArrogationNegative.command_utterance_not_fits`, `WAA.Grid.ConsequentialistConvention.map_dropCount`, `WAA.Grid.ConsequentialistConvention.map_dropCountInFiber` | `being-convention`, `re-pitch`, `delivery-arrogation` |
| covariation | Theorems | Covariation means two quantities move together without being declared identical in every respect. The dukkha reading covaries with share, ordinally and per call. | `WAA.Grid.WaaMismatchGrade` | `dukkha`, `share` |
| proneness/occurrence | Theorems | Proneness is a carried tendency; occurrence is the live event. The dukkha split uses this standing/dated distinction to avoid storing suffering as a bearer. | — | `dukkha`, `seed`, `standing/dated` |
| transposition | Theorems | Transposition is the answer to the terminus question: the self-pole index disappears, while reception-side activity for others can still run. Nothing travels from one pole to another. | `WAA.Grid.no_self_pole_index_of_atBot`, `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.transposition_erased_downward_collapse_self_refuting` | `terminus`, `pole`, `object-axis/subject-axis` |
| kiriya / ahosi | Canonical | Kiriya and ahosi name action and lapsed fruit in Buddhist idiom around the arhat. In this system the point is derived from share-zero: fruit can land without a live index-question. | — | `share`, `pole`, `delivery` |
| mirror | Canonical | The mirror is the image of responsive output without possession. In this system it is function without share, legal as a display over a run. | `WAA.Grid.LiveTerminus` | `function`, `share`, `terminus` |
| device / device-nature | Theorems | A device is a compressed way to speak of pole-like responsiveness. It is legal as display and becomes a freeze when treated as a standing nature owned by a being. | — | `mirror`, `terminus`, `collapse/freeze` |
| maximally adaptive call | Theorems | The maximally adaptive call is the limiting case of call-fitting. The system deflates it from the ground of the terminus to the limit where buddha-side shortfall closes. | — | `fixed/adaptive`, `buddha-side shortfall` |
| generator | Theorems | The generator is the taxonomy engine that makes rows from distinctions. Its discipline is that errors must land in existing cells, force a new cell, be declined, or force a retype. | `WAA.Grid.GeneratorOutcome`, `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.tableOrder` | `collapse/freeze` |
| four verdicts | Theorems | The four verdicts are existing-cell, new-cell, declined, and retype. They are the public outcomes available when the generator meets a candidate error. | `WAA.Verdict`, `WAA.generatorRecord_newCell_count` | `generator` |
| Sunyata | Canonical | Sunyata means emptiness. In this system it is the no-final-freeze property of a distinction's re-emptying ladder. | `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.Nishitani.Sunyata` | `collapse/freeze` |
| direction-underdetermination witness | Theorems | This witness shows that symmetric field residue does not determine direction. Two grids can agree on the undirected relation and disagree on the directed one. | `WAA.DirectionNegative.no_direction_recovery_from_conditionsEither` | `arrow`, `field` |
| being-boundary witness | Theorems | This witness shows that grid data do not recover a unique being-boundary. Merge and split coarsenings can both be legal over the same fine grid. | `WAA.BeingNegative.no_partition_recovery` | `being-convention`, `freedom witness` |
| weld-boundary witness | Theorems | Grid data do not recover a unique weld-segmentation. Merge and split readings of what counts as one call-response pairing are both legal over the same field. | `WAA.WeldNegative.no_weld_boundary_recovery` | `weld`, `being-convention`, `freedom witness` |
| intra-weld arrow row | Theorems | The intra-weld arrow row checks the call-to-response direction inside a weld as a convention layer. Its content form denies response-variation, and its witness says the unordered residue does not recover an interior arrow. | `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.intraWeldArrowRow`, `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.Nishitani.intraWeldArrow_sunyata`, `WAA.InteriorDirectionNegative.no_interior_direction_recovery` | `arrow`, `weld`, `weld-boundary witness` |
| doer/deed row | Theorems | The doer/deed row is the schema-only MMK 8 cell: a prior-doer reading is diagnosed without adding priority as a primitive field of the grid. | `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.doerDeedRow`, `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.Nishitani.doerDeed_sunyata`, `WAA.DoerDeedNegative.no_priority_recovery` | `weld`, `collapse/freeze`, `intra-weld arrow row` |
| coming-to / going-from | Theory | Coming-to and going-from are display labels for the two orientation readings of a weld's faces. Transposition reverses the labels; they are not tier names. | `WAA.InteriorDirectionNegative.transpose_swaps_readings`, `WAA.InteriorDirectionNegative.no_interior_direction_recovery` | `arrow`, `weld`, `intra-weld arrow row` |
| reflexivity witness | Theorems | The reflexivity witness instantiates a grid's being carrier with rung labels, showing that the beings ladder still has no final freeze when read over its own indices. | `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.ladderRungGrid_beings_sunyata` | `being-convention`, `Sunyata` |
| weld row / weld śūnyatā | Theorems | The weld row names the weld-grain distinction as a convention layer, and weld śūnyatā says its re-emptying ladder has no final frozen level. | `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.weldRow`, `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.Nishitani.weld_sunyata` | `collapse/freeze`, `Sunyata` |
| declined case | Theorems | A declined case is a candidate that the taxonomy refuses to mark as error. The deaf-blind example matters because over-generating error would itself freeze the lens. | `WAA.InstructiveAbsence.declinedCase` | `four verdicts` |
| Grade 1 / Grade 2 | Theorems | Grade 1 names grammatical errors assertable inside the lens; Grade 2 names shortfalls only displayable by the lens. The difference prevents the grid from issuing its own value command. | `WAA.Grid.ErrorGrade`, `WAA.Grid.ErrorGrade.voice` | `assert/display` |
| clenched reception | Theorems | A clenched reception is an arriving response taken tightly as mine. It is still graded as a fresh weld, not as evidence of a stored owner. | — | `clench`, `reach-back`, `weld` |
| declining the orange | Theorems | Declining the orange is a low-resonance reception of this offered call. It is not a global wrong and does not prove anything about a person. | — | `orange / eat this`, `call` |
| defiance | Theorems | Defiance is arrogation hardened into policy. The fighting stance is a seed, but each fight remains a new act. | — | `arrogation`, `seed`, `weld` |
| cetanā | Canonical | Cetanā means intention or volition. In this system it is the traditional anchor for the claim that grading tracks the weld rather than the downstream event. | `WAA.Grid.grade_independent_of_conditions`, `WAA.Grid.share_independent_of_conditions` | `weld`, `grade` |
| cetanā theorem | Theorems | The cetanā theorem is the derived version of intention as karma. It says the grading component follows the weld even where event-success and delivery diverge. | `WAA.Grid.grade_independent_of_conditions`, `WAA.Grid.share_independent_of_conditions`, `WAA.cetana_grading_tracks_weld_not_field_witness`, `WAA.cetana_live_share_without_object_standing_witness` | `cetanā`, `weld`, `field` |
| futility theorem | Theorems | The futility theorem says the deliberate attempt fails at target and downstream. The body can be staticized as a delivery loss without subtracting object-axis standing. | `WAA.Grid.staticized`, `WAA.Grid.futility_delivery_loss_real`, `WAA.Grid.futility_object_axis_subtraction_nil`, `WAA.Grid.DirectedConvention.staticized_objectAxisStanding_iff` | `delivery`, `object-axis/subject-axis`, `device / device-nature` |
| victim-rank | Theorems | Victim-rank is severity read from the victim's station. The system treats it as a freeze because rank is being smuggled into what should be per-weld grading. | — | `grade`, `collapse/freeze` |
| hell-typed | Theorems | Hell-typed means a configuration receives no gentler call in the actual delivery-regime. The claim is regime-relative, not a statement about all possible calls. | — | `delivery-regime`, `call` |
| ledger | Theorems | A ledger is a public register that prices what can be counted. In the Huichang case it names an economic modality and the errors produced by reading that modality as a being-sized truth. | `WAA.LedgerCase.decree_engineers_calls_not_receptions`, `WAA.LedgerCase.purge_loop_runs_on` | `delivery-regime`, `Grade 1 / Grade 2` |
| economic legibility | Theorems | Economic legibility is a field-fact about which configurations a purge can reach. The system can assert that register while only displaying the worth of survival. | `WAA.Grid.DirectedConvention.landing_call_in_modality` | `ledger`, `field` |
| gradeability rule | Theorems | The gradeability rule says a recorded utterance may be graded only where the record carries its call. Lean checks both the severed-transcript obstruction and the call-carrying positive form. | `WAA.GradeabilityNegative.no_grade_recovery_from_severed`, `WAA.GradeabilityNegative.gradeability_severed_underdetermination_witness`, `WAA.recordedUtterance_grade_determined` | `call`, `grade`, `weld` |
| transcription | Theorems | Transcription turns an adaptive event into a fixed record. In the system the transcript is a seed-like fixed call, not a stored fault in the words. | — | `fixed/adaptive`, `seed`, `call` |
| per-call/global freeze | Theorems | The per-call/global freeze turns a local grade into a global rank. It is the error behind treating stages, awakening, or census categories as stored altitude. | `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.RowTag.perCallGlobal` | `grade`, `collapse/freeze` |
| subitism/gradualism | Canonical | Subitism and gradualism name sudden and staged arrival patterns. The system permits both as run shapes while refusing to store a rate preference as attainment. | `WAA.Grid.WaaSuddenArrival`, `WAA.Grid.WaaGradualArrival`, `WAA.Grid.rate_invisible_to_config`, `WAA.SuddenGradualNegative.subitism_frequency_underdetermined` | `re-pitch`, `per-call/global freeze` |
| PathFactor | Lean convention | PathFactor names the factor-side regrouping of the existing fetter table. Rites, view, and resolve are active; speech and conduct are named but inert until the upper-pair question is settled. | `WAA.PathFactor`, `WAA.PathFactor.blockerClass` | `coarsening`, `tag/fiber` |
| FactorHeld | Lean convention | FactorHeld is a seen-run witness: an actual in-fiber weld in the factor blocker class carries a live self-pole index. It is not itself an error; it is factor-frame vocabulary, not freeze/collapse and not clench alone. | `WAA.Grid.FactorHeld` | `PathFactor`, `clench`, `weld` |
| FactorReleased | Lean convention | FactorReleased is the release half of the factor pair: the fiber is at pole on the factor blocker class. One actual live weld in that class refutes it. | `WAA.Grid.FactorReleased`, `WAA.Grid.not_factorHeld_of_factorReleased` | `PathFactor`, `FactorHeld`, `pole` |
| WaaStreamEnterer | Lean convention | WaaStreamEnterer is the path-position reading over the first pair: rites released, view held on the seen run. It deliberately separates path display from the fruit cut. | `WAA.Grid.WaaStreamEnterer` | `FactorHeld`, `FactorReleased` |
| WaaStreamWinner | Lean convention | WaaStreamWinner is the fruit-position reading for stream entry: rites and view are released, and Lean proves it coincides with the existing stream-entry cut class. The terminology is a checked departure from treating sotapanna as only one undivided label. | `WAA.Grid.WaaStreamWinner`, `WAA.Grid.waaStreamWinner_iff_streamEntry_cutClasses` | `WaaStreamEnterer`, `FactorReleased` |
| WaaOnceReturner | Lean convention | WaaOnceReturner keeps the stream-winning fruit and adds a witnessed resolve hold on the seen run. Its extra checked content is attenuation, not a new cut class. | `WAA.Grid.WaaOnceReturner` | `WaaStreamWinner`, `FactorHeld` |
| WaaNonReturner | Lean convention | WaaNonReturner is the fruit-position reading after resolve release. Lean proves it is exactly the non-return cut class, so the factor scheme remains a reading over the fetter lattice. | `WAA.Grid.WaaNonReturner`, `WAA.Grid.waaNonReturner_iff_nonReturn_cut` | `WaaOnceReturner`, `FactorReleased` |
| WaaResolveAttenuation | Lean convention | WaaResolveAttenuation gives once-return positive content: a strict resolve-class share-drop run whose final tendency has not reached the pole. | `WAA.Grid.WaaResolveAttenuation`, `WAA.Grid.waaOnceReturner_attenuation_witness`, `WAA.Grid.attenuation_not_release` | `WaaOnceReturner`, `re-pitch` |
| WaaSerialFactorRegime | Lean convention | WaaSerialFactorRegime is the conditional voice for factor order. If the supplied regime reads seen share-drops as rites before view before resolve, it promotes path readings to fruit readings; the grid never derives the regime or any frequency claim. | `WAA.Grid.WaaSerialFactorRegime`, `WAA.Grid.waaSerialFactorRegime_conditional`, `WAA.FactorsNegative.seen_run_underdetermines_factorOrder` | `WaaResolveAttenuation`, `subitism/gradualism` |
| śraddhā | Canonical | Śraddhā means faith or trust. In this system it is modeled as an antecedent for testimony and path response, never as a field fact the grid can discharge by itself. | `WAA.Grid.DirectedConvention.WaaFaithPrinciple`, `WAA.Grid.DirectedConvention.waaFaithOught_conditional` | `buddha-side shortfall`, `delivery` |
| icchantika | Canonical | Icchantika ordinarily names a being cut off from buddhahood. Here it is the terminus's inverse: non-stone, with a live self-pole index at every mounted response. It is reachable as a receiver and cannot be seated as an enlightened agent on its run. The permanent cannot-become-buddha verdict is declined, because foreclosure would be a stored rank the system forbids; defiance is a seed, not a rank. | `WAA.Icchantika`, `WAA.not_waaFullyEnlightened_of_icchantika`, `WAA.aversionContext_of_icchantika_reception`, `WAA.icchantika_release_not_foreclosed` | `defiance`, `terminus`, `backsliding theorem`, `śraddhā` |
| tariki / other-power | Canonical | Tariki means other-power. In this system it is a delivery-regime reading, not a second act-grammar: the reception is still an ordinary weld. | `WAA.Grid.DirectedConvention.WaaTarikiLine`, `WAA.Grid.DirectedConvention.reception_typing_ignores_sower`, `WAA.TarikiCase.universal_fixed_call_lands_without_reading`, `WAA.OtherPowerNegative.regime_does_not_determine_share` | `delivery-regime`, `weld` |
| pariṇāmanā / dedication | Canonical | Pariṇāmanā means dedication or turning over merit. In this system it is sowing-side share-cession whose routing is left to delivery rather than commanded by the act. | `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.CompoundPosition.ledgerPicture`, `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.CompoundPosition.ledgerPicture_decomposition`, `WAA.Grid.DirectedConvention.BeingConvention.GridConvention.CompoundPosition.ledgerPicture_contains_legal_causalSkeleton`, `WAA.Grid.DirectedConvention.SameAgentDelivery`, `WAA.Grid.DirectedConvention.CrossAgentDelivery`, `WAA.Grid.DirectedConvention.reception_typing_ignores_sower`, `WAA.OtherPowerNegative.regime_does_not_determine_share`, `WAA.OtherPowerNegative.share_does_not_determine_regime` | `share`, `delivery-regime`, `aimed call` |
| instructive absences | Theorems | Instructive absences are gaps the system keeps because they do diagnostic work. Lean mirrors them as data with status and numbering rather than treating them as forgotten cases. | `WAA.InstructiveAbsence`, `WAA.InstructiveAbsence.status`, `WAA.InstructiveAbsence.number` | `declined case`, `generator` |
| identification claim | Identification | The identification claim says karma names the loop where the field carries diachronic relations and the weld enacts every index. It is a decomposition claim, not a stored-self claim. | — | `field`, `weld`, `index-question` |
| state-designation vs. act-fixing | Identification | State-designation names something over a standing base at a time; act-fixing makes the relevant index in the act itself. The contrast blocks a state-tool from ranging over karmic ownership. | `WAA.Grid.stateToolFits_iff_atBot` | `standing/dated`, `weld` |
| offices-spine | Identification | The offices-spine is the list of traditional places where karmic ownership has work to do. The identification argues that each office discharges at act-time. | `WAA.WaaOwnershipOffice` | `identification claim`, `weld` |
| thin for-me-ness | Identification | Thin for-me-ness is pre-reflective givenness without appropriation. The system keeps the token-reflexive light needed by the weld and removes standing ownership. | — | `weld`, `arrogation` |
| Sartrean occupant | Identification | The Sartrean occupant is the remaining inhabitant of clench-as-structure after thin for-me-ness is pared back. It names anguish as a structure, not ownership as a stored thing. | — | `thin for-me-ness`, `clench` |
| sower-reaps split | Identification | The sower-reaps split separates the report that a delivery line exists from the ownership face made at reception. It keeps true field reporting away from standing ownership. | `WAA.Grid.DirectedConvention.WaaReportFace`, `WAA.Grid.DirectedConvention.WaaOwnershipFace`, `WAA.Grid.DirectedConvention.WaaVacuousOwnershipFace` | `delivery`, `reach-back` |
| pole-typing corollary | Identification | The pole-typing corollary says the state-tool fits exactly where live welding ceases. At share-zero there is no live self-pole index for the tool to miss. | `WAA.Grid.stateToolFits_iff_atBot`, `WAA.Grid.no_self_pole_index_of_atBot` | `pole`, `index-question` |
| soul-guard | Identification | The soul-guard blocks storage by making the agent more empty, not more substantial. Both forward-facing and retrospective bearers are declined. | `WAA.no_agent_recovery_of_field_collision` | `field`, `weld` |
| being trichotomy | Identification | The being trichotomy gives three readings: collapse deletes beings, freeze reifies a partition, and convention leaves naming free. It keeps designation useful without making it metaphysical. | `WAA.Disclaimer.beingTrichotomy` | `being-convention`, `collapse/freeze` |
| hare's horn | Canonical | A hare's horn is the stock example of something nameable but unrealizable. In this system it shows that designation is constrained at use, not at the mere act of naming. | `WAA.Disclaimer.hareHornRegister` | `being-convention` |
| Modal Realism | Canonical | Modal Realism treats possible beings as fully real. In this system it is the beings-row freeze: plenitude moved into ontology rather than left as conventional designation. | `WAA.Disclaimer.modalRealismFreeze` | `being trichotomy`, `collapse/freeze` |
| disclaimers | Identification | The disclaimers are the paper's explicit flags for original or non-canonical moves. They say which precision remains prose even when Lean checks anchors, numbering, and structural constraints. | `WAA.Disclaimer`, `WAA.Disclaimer.number` | `instructive absences` |