The Mirror Calculus

*3cm The Mirror Calculus 0.8cm A Presence-Only Mathematical Language: Formation, Descent, Geometry, and the Register-Typed Resolution of the Riemann Question 2.2cm Parker M. D. Emmerson

Abstract

This volume develops a mathematical notation in which every mark is kept under left–right reflection and the numeral zero does not occur, and carries that notation from its grammar through geometry, algebra, analysis, and analytic number theory. Formation precedes assertion. The Mirror Calculus enacts presence-only formation: an object-language inscription forms only through a positive witness, trace, relation, transformation, roster, pairing, certificate, or explicit sponsorship event. Non-presentation forms no substitute object-language term. Numerical zero, empty collections, null returns, default falsity, vacuous judgments, and negative records inferred from failed search are analyzed as surrogate-zero devices: they make non-presentation participate as an object, value, or verdict.

The strict Mirror grammar has exactly twelve object constructors:

\[\mathsf{Bal},\ \mathsf{Row},\ \mathsf{Jux},\ \mathsf{Stk},\ \mathsf{Up},\ \mathsf{Dn},\ \mathsf{Lk},\ \mathsf{Ovl},\ \mathsf{Adh},\ \mathsf{Box},\ \mathsf{OBox},\ \mathsf{Frac}.\]

Strict object atoms are fixed by horizontal reflection. Reflection reverses the arguments of \(\mathsf{Bal}\), \(\mathsf{Row}\), and \(\mathsf{Jux}\), and acts pointwise on the remaining constructors. The resulting involution, well-formedness preservation, and renderer equivariance have a full structural proof. A smaller implementation fragment \(\GK\) is represented by the accompanying Lean source; the present edition does not identify that fragment with the whole language. In particular, the current implementation datatype contains a variant named blank. The kernel artifact therefore concerns implementation control syntax and has not yet formalized the stricter discipline adopted here, under which no layer carries any mark for non-emission.

Blank is not a term denoting emptiness, and it is not a metasyntactic control either: every carrier at every layer carries a formed term, and withheld emission is an event of the metalanguage. \(\Eval(t)\downarrow e\) records successful emission and \(\Eval(t)\uparrow\) records the act's non-performance. A one-sided balance or an empty enclosure is thereby excluded from the language by the plenary-emission totality, and the judgment is the whole report of a withholding.

The Riemann question is resolved at explicitly separated registers, each verdict carrying its sponsor on its face. The native axis sentence \(\RHMirror\) is a sentence of \(\Sent(\GP)\); the literal zero-locus sentence \(\RHClassZero\) is formed in the classical register alone. The adopted theory \(\Pdag=\Pbase+\AdmZeta\) derives the native sentence:

\[\Pdag\vdash\RHMirror.\]

Over the declared base, class-wide Admission and its counter-inscription are each witnessed by a finite model in exact rationals: a relative independence theorem with both sides exhibited, and the fork at which \(\AdmZeta\) is adopted, sponsored by \(\alpha_\zeta\). The witnessed semantics sponsors a coherent omega-kept family as a completion postulate, declared as such. Under the named classical interface,

\[I(\AdmZeta)\quad\Longleftrightarrow\quad\RHClass,\]

proved from the definition of the interface, so that \(\RHClass\) holds under the interface with the sponsored adoption printed on the verdict. Independence is here an affirmative method: carried by a proof-reflecting translation to a sound classical theory, \(\Sigma_1\)-completeness converts it into arithmetic truth, and the analytic equivalence converts truth into \(\RHClass\). An explicit polynomial witness carries every reflection and functional-equation symmetry together with an off-axis quartet, and so measures exactly what \(\AdmZeta\) supplies beyond symmetry. The work supplies a presence foundation, a strict mirror grammar, a typed root algebra with its dagger reading, a kernel-certified fragment with its computational record, a research program recorded at exact strength, an external blind-reading audit of the object language, the native derivation, the class-wide model theorem, and the exactly priced analytic interface through which the classical statement is read.

Preface

This book presents the Mirror Calculus: a mathematical notation in which every mark is kept under left–right reflection and the numeral zero does not occur, carried from its grammar through geometry, algebra, analysis, and analytic number theory. It is the full Mirror Calculus volume of the three-paper Against Zero / Counting Back from Infinity / Mirror Calculus program: the first paper defends the thesis that formation precedes assertion and analyzes surrogate-zero devices by role; the second adopts the descent laws and develops native mathematics relative to them; the present volume gives the language, its algebra and geometry, its plates, and the register-typed resolution of the Riemann question. The object language is the protagonist throughout; every classical appearance in the book is an interpretation the interface prices.

The tour is this. The presence foundation opens the book, and the descent mathematics follows it. The strict mirror language is then given exactly: codex, twelve-constructor grammar, well-formedness, reflection metatheory, and the scope of its formal verification. The plate language comes next as current mathematics, closing with the caption-blind decoding audit — the language delivered to a reader without one word of prose. The typed algebra and its geometry follow: the failure of the first junction model and the typed successor, the reading group that folds the page, roots and resolvents, the dagger reading, and positive analytic counting. The cone-chain applications lead into the Riemann architecture, where the controlling chain of the front matter is proved component by component; the explicit formula and the computational record follow; and the book closes with the research directions and their engineering consequences.

Conventions. Classical results imported into proofs are named at the point of use. The metalanguage is ordinary mathematical English and may discuss zero, emptiness, nonformation, classical logic, and standard mathematics. The strict object language is narrower: it does not contain a term whose purpose is to reify non-presentation.

What is new here. Four things, and it is worth separating them from what is imported. First, a reflection-equivariant presence-only grammar with a closed atom inventory, twelve constructors, and a kernel-certified fragment: a formal language in which non-presentation has no object-level term, carried far enough to state and check real mathematics. Second, the resolution of the Riemann question at its own registers: in the presence grammar the native axis sentence is well formed and the adopted theory derives it, while the conventional zero-locus sentence belongs to the classical register, where it converts the withholding of a presence-valued evaluation into equality with a numerical object; the classical statement is read off the native law through one interface at a price stated exactly, and presence-only formation, the grammar in which this is carried out, is argued for in the first chapter and adopted as the grammar of record throughout. Third, the register discipline itself: an assertion-record schema under which every consequential claim names its sponsor, its stratum, and the interface priced for any transfer, applied to a hard subject without remainder. Fourth, the surrogate-zero taxonomy and its engineering transfers, which a fully classical reader may adopt entire.

What sponsors what. Each result of this book is read off its sponsor. \(\Pdag\vdash\RHMirror\) is a derivation. The relative independence of class-wide Admission from the base is a theorem with both sides exhibited by finite models. The interface equivalence \(I(\AdmZeta)\Longleftrightarrow\RHClass\) is proved from the definition of the interface. \(\AdmZeta\) itself is present in \(\Pdag\) by declaration, sponsored by \(\alpha_\zeta\), at a fork the independence theorem proves inhabited on both sides; and under the interface \(\RHClass\) accordingly holds, with the verdict carrying that sponsor on its face. The symmetry no-go formalizes, for the same architecture, a constraint the classical reader already meets. The residue is named and located: faithful reference to the completed prime-fused descent, which the volume shows carries the whole of the remaining classical difficulty.

Claim and Register Convention

Every claim in this book is typed by the register in which it is made. Five registers are used: the grammatical register \(\RegGra\), in which formation in the presence grammar \(\GP\) is judged; the native object register \(\RegObj\), in which the descent laws operate and the adopted theory \(\Pdag\) derives; the omega register \(\RegZen\), in which formation under the registered Omega-Seal rule is judged; the relative register \(\RegRel\), for derivability and independence over the unextended base \(\Pbase\) and for statements conditional on a declared adoption; and the classical register \(\RegCla\), entered only through the named interface \(I\). Statements never migrate silently between registers: a transfer names its interface, and the interface prices it.

Four kinds of claim occur: stipulations, which declare grammar or adoption; theorems, proved in a stated register; computations, exact or carried out at stated truncation and precision; and interpretations, which read one register's content in another and carry theorem strength only componentwise. Where a machine certificate applies, its scope is stated once, where it is used.

The controlling architecture

The object language is sovereign in this book. Its sentences are formed by the twelve-constructor grammar; its theorems are proved in the registers the grammar sustains; and every classical appearance in the volume is an interpretation whose price a named interface states. The mathematical spine is the following chain, proved component by component. Formation:

\[\RHClassZero\notin\Sent(\GP), \qquad \RHMirror\in\Sent(\GP).\]

Native relative independence:

\[\Pbase\nvdash\AdmClass, \qquad \Pbase\nvdash\CounterAdmClass.\]

Explicit foundational selection:

\[\Pdag=\Pbase+\AdmZeta.\]

The resolution, a native proof:

\[\Pdag\vdash\RHMirror.\]

The boundary is native as well: the polynomial witness

\[F(s)= \left((s-\tfrac12)^2-a^2\right) \left((s-\tfrac12)^2-\bar a^{\,2}\right), \qquad a=\tfrac3{10}+7i,\]

satisfies every reflection and functional-equation symmetry the tent group imposes while carrying an off-axis quartet, and it recurs as a central theorem below.

The interface, priced. Through the named analytic interpretation \(I\),

\[I(\AdmZeta)\Longleftrightarrow\RHClass, \qquad\text{so}\qquad I\models\Pdag\ \Longrightarrow\ \RHClass, \qquad \neg\RHClass\ \Longrightarrow\ I\not\models\Pdag.\]

The classical statement enters here and here alone: as the priced shadow of the adopted native law.

Presence Foundation

Formation Before Assertion

The foundational thesis

Formation precedes assertion. A strict inscription enters the object language through a positive formation event: a witness, trace, relation, transformation, nonempty roster, pairing, certificate, or explicit sponsorship. The formation event supplies the inscription and its provenance together.

The thesis is stated positively. The strict language records what a scene presents and how the presentation forms. Evaluation judgments and search control remain in the metalanguage, and implementation control codes remain in the implementation stratum. They do not acquire object status merely because a software datatype or explanatory sentence needs to discuss them, and the language of record carries no counterpart to any of them.

Whenever a formed symbol is assigned the semantic office of representing non-existence, the notation embeds a category conflict: the mark's formation certifies presentation while its assigned role asks it to stand for a failed presentation. Presence-only formation resolves the conflict by retaining the formed mark, when one exists, as implementation or diagnostic control rather than promoting it to a strict semantic object.

This is a claim about type and formation, not a Boolean verdict declaring one mathematical tradition permitted and another forbidden. Classical mathematics and the presence calculus are distinct formal regimes. Their relation is established theorem by theorem through named interfaces.

The positive formation of one

Unity may be positively presented. A natural scene may exhibit a stable singular organization; a counting procedure individuates that presentation and carries it into tally grammar as one. The phrase imposed unity names this individuation operation. It does not mean that nature is incapable of presenting singular form.

The Descent interpretation gives a second realization. In the sweeping geometry, unity forms through the balance between an infinitesimal length carried through an infinite angle and an infinite length carried through an infinitesimal angle. Written schematically in the metalanguage,

\[(\mathrm d\ell)\,\Theta_{\infty} \quad\mathsf{Bal}\quad \ell_{\infty}\,(\mathrm d\Theta).\]

The balance is not a discovery of a context-free numeral floating outside formation. It is a positive relation whose sweep, scene, and trace form a unit carrier.

Counting therefore requires:

1. a presented scene;
2. a positive individuation relation;
3. a trace establishing the unit carrier;
4. a procedure that repeats or compares such carriers;
5. a roster on which the tally is performed.

The numeral one records the first formed unity of that procedure. Genealogical numeration retains the sweep history by which the unity formed.

Root grammar and semantic office

Root grammar governs more than the printed BNF. It governs the semantic office assigned to a formed mark.

A metalanguage may quote or diagnose a privative expression. The root-grammatical violation occurs when that expression is made to perform object-forming or inference-sponsoring work.

Whenever a presented symbol is assigned the meaning “non-existence,” root grammar receives both a positive inscription and a semantic instruction cancelling presentation. This is a root-grammatical contradiction, even where a classical model consistently manipulates the resulting sign.

The strict discipline therefore asks, at every use:

1. Which positive event formed the mark?
2. Which positive relation gives it semantic content?
3. Does the mark carry presented content, or is it functioning as renderer or search control?
4. Has a control-layer event been promoted into a semantic object?

The surrogate-zero test is determined by role, not vocabulary. “Zero,” “empty,” “null,” “none,” and privative prose are equally subject to the test whenever their meanings are applied.

Surrogate-zero roles

device	reifying role	presence-only replacement
numerical zero	a tally returned when no individual was tallied	a tally forms only over a nonempty roster and therefore begins at one
empty collection	a roster with no presented member	no empty roster; roster formation requires at least one sponsored entry
null return	a returned value standing for failure to return a value	successful emission is recorded by \(\Eval(t)\downarrow e\); withheld emission is the metalanguage judgment \(\Eval(t)\uparrow\)
default falsity	a negative verdict inferred from failure to produce an affirmative verdict	a contrary requires its own positive witness or a completed coverage certificate
vacuous judgment	a verdict over an unoccupied domain	the object-language judgment does not form until a domain roster or a separately priced classical interface is supplied
negative record from failed search	a record of exclusion inferred from non-record	non-record is not negative record; exclusion requires positive coverage and completion traces
blank enclosure	a visible frame made to denote an empty object	a diagnostic renderer display about withheld emission, outside the strict sentence language

A positive contrary is not the shadow of a missing affirmation. Rejection, exclusion, failure, incompatibility, and fault are lawful object-language contents when independently witnessed. An instrument fault report is a positive event. A completed search certificate is a positive event. A witnessed clash between two formed inscriptions is a positive event. What is barred is the conversion of silence into any of them without a sponsor.

Three statuses, not three truth values

The notation distinguishes:

1. a positively presented assertion;
2. a positively presented contrary or rejection, with its own witness;
3. no semantic inscription.

Status (iii) is not a third truth value. It is not an object that propagates through connectives, a null member of a result type, or an “unknown” value. It is the metalanguage observation that neither of the first two inscriptions formed. A three-valued logic reifies the third status as a participant in operations. TPN does not.

Classical mathematics and transfer

The foundational thesis does not declare classical mathematics meaningless or useless. It denies automatic transfer.

A positively interpreted fragment of a classical structure may be used when the interpretation presents its elements, domains, and operations. A theorem then transfers only after a separate argument shows that its statement and proof remain inside that fragment. Every use of an empty auxiliary structure, choice over an unpresented family, excluded middle over unformed sentences, or a null element requires a named interface. The price may be worth paying; it may not be hidden.

No theorem in this volume establishes that all classical mathematics has such a transfer. Conversely, no failure of automatic transfer is represented as a refutation of the classical theorem in its own register.

Transcendental Presence Notation

Primitive positive sorts

TPN is the program's trace-bearing decision language. Its primitive sorts are:

• Witness. A presented individual, event, or performed act.
• Scene. A context of presentation: an instrument, procedure, epoch, laboratory, database scope, or other positive setting.
• Trace. A record of the procedure by which a witness, relation, or transformation was presented.
• Inscription. A formed object-language sign carrying its sponsor.
• Nonempty roster. A sequence of one or more presented inscriptions together with apartness or individuation records.
• Tally. A count over a formed nonempty roster.
• Pairing. A presented correspondence between witnesses or scenes.
• Positive transformation. A trace-bearing act carrying presented input to presented output.
• Clash record. A record of two formed inscriptions and a separately witnessed incompatibility between them.
• Certificate. A distinguished inscription recording a completed procedure, its scope, and its coverage traces.
• Sponsorship. A positive adoption event by which a foundational law or completion postulate is entered into the adopted theory.

Formation rules

A witness forms an inscription only with a scene and trace:

\[\frac{ \mathsf{Witness}(w)\qquad \mathsf{Scene}(\sigma)\qquad \mathsf{Trace}(\pi:w\text{ presented in }\sigma) }{ \mathsf{Inscribe}(\ulcorner w\urcorner;\pi) }.\]

A roster requires one or more entries and positive individuation:

\[\frac{ \mathsf{Inscribe}(t_1;\pi_1)\ \cdots\ \mathsf{Inscribe}(t_k;\pi_k) \qquad \mathsf{Sep}(t_i,t_j;\sigma_{ij})\ (i<j) \qquad k\geq 1 }{ \mathsf{Roster} (\langle t_1\frown\cdots\frown t_k\rangle; \pi_1\ast\cdots\ast\pi_k) }.\]

A tally forms only from a roster:

\[\frac{\mathsf{Roster}(R;\pi)} {\mathsf{Tally}(R)\geq 1}.\]

Thus counting begins at one as a consequence of the adopted roster formation rule.

A certificate records positive completion rather than an absence:

\[\frac{ \mathsf{Procedure}(p)\qquad \mathsf{Scope}(S)\qquad \mathsf{Completed}(p,S;\tau)\qquad \mathsf{Coverage}(p,S;\kappa) }{ \mathsf{Cert}(p;S;\tau,\kappa) }.\]

Direct clash and hypothesis-discharging rejection

Direct clash recording and hypothesis-discharging rejection are different acts.

A direct clash requires two formed inscriptions and an independent witness of incompatibility:

\[\frac{ \mathsf{Inscribe}(t;\pi)\qquad \mathsf{Inscribe}(t';\pi')\qquad \mathsf{Clash}(t,t';\kappa) }{ \mathsf{ClashRecord}(t,t';\pi,\pi',\kappa) }.\]

A rejection under a hypothesis requires derivations on both sides of a witnessed clash:

\[\frac{ \mathsf{Assume}(h;\alpha)\qquad \mathsf{Derive}(t\mid h;\pi)\qquad \mathsf{Derive}(t'\mid h;\pi')\qquad \mathsf{Clash}(t,t';\kappa) }{ \mathsf{Reject}(h;\alpha,\pi,\pi',\kappa) }.\]

A term's failure to form is a metalanguage judgment and is not itself a clash. Indirect reasoning remains available, but it must terminate in two positively formed conclusions together with a positive incompatibility witness.

Sponsorship

Foundational laws are not described as unsponsored truths. They enter the adopted theory through a positive adoption event:

\[\frac{\mathsf{Sponsor}(\alpha,\varphi)} {\mathsf{Assert}(\varphi;\alpha)}.\]

The event does not prove \(\varphi\) from weaker laws. It records which theory has been selected and who or what performed the selection.

This rule governs both Native Admission and the omega completion used later. It is the principal device by which the volume separates adopted law from theorem.

Scene composition

Scenes compose only through presented pairings. If witnesses in scenes \(\sigma\) and \(\tau\) are identified by a trace-bearing pairing, the pairing licenses transport between those scenes. No universal ambient scene is given for free.

The frequently used idea that local scenes assemble into a scene-colimit is an interpretation. A formal colimit model is not supplied by the current calculus. Accordingly, this volume does not cite scene-colimit language as a theorem of TPN.

Engineering transfers

The formation rule has direct engineering consequences.

Databases

Absence of a record is not a negative record. Under an open-world reading, a missing row warrants no exclusion. A closed-world inference becomes presence-lawful only when a positive completeness certificate establishes that the relevant relation, sources, and time range were covered. This sharpens the familiar distinction between incomplete information and recorded falsity in database theory.

A semantic schema should therefore store events and relations that formed. A renderer or query layer may withhold a field when no value was emitted; the control path stays control. A domain value called null is formed only by a named interface, and a classical export that requires one is that interface.

AI and missing data

A dislike is a recorded dislike event; a rating is an emitted rating; a feature value is an emitted value; the unobserved cell has status (iii). Implicit-feedback methods that assign a low-confidence signal to unobserved cells install a modeling device, and presence-only reporting keeps the device labelled as one.

Padding tokens, masks, sentinel codes, and withheld emissions belong to the implementation-control layer. They guide tensor shape and control flow, and a semantic report records only what was emitted: the machinery layer's marks reach it, when they do, through a named interface.

Safety and decision systems

A consequential decision should be a positive record such as

\[\mathsf{Approved}(\text{request};\text{sponsor};\text{trace}),\]

\[ \mathsf{Rejected}(\text{request};\text{clash};\text{trace}), \] or

\[\mathsf{ReviewScheduled} (\text{request};\text{trigger};\text{slot}).\]

Failure to produce an approval does not form a rejection. A detector that remains silent does not form the assertion “no hazard.” The presence replacement is a readiness certificate recording scope, test traces, instrument traces, credentials, and coverage. Such provenance accords with the positive-event orientation of the W3C PROV model.

Descent Mathematics

The Adopted Descent Foundation

The laws in this chapter are adopted formation laws. Their status is not empirical, and they are not consequences of the strict grammar. The no-zero result proved from them is therefore relative to them.

Relative no-zero theorem

Proof.

The base formation rules require a positive witness or precipitation event. Every composite rule preserves at least the witnesses and traces of its premises. Roster formation requires at least one entry. An induction over derivations therefore shows that every formed tally has a nonempty sponsoring roster. A null tally has no derivation under these rules.

Genealogy and arithmetic

Juxtaposition of genealogies and nesting of one genealogy through another supply candidate readings of addition and multiplication. This volume uses those readings only where a corresponding evaluation identity is displayed or proved. It does not assert a general arithmetic representation theorem for all genealogical numerals.

The \(n\)-wave reading—that a degree-\(n\) residue family is realized by \(n\)-fold interference—is likewise an interpretation. No complete formal \(n\)-wave model is included in the current artifact set.

Classical completion

Let \(S\) be a semigroup without an identity. Its free identity adjunction is

\[S^{1}=S\sqcup\{e\},\]

with multiplication or addition extended so that \(e\) is an identity and with no further relations imposed.

For the positive additive tally semigroup,

\[(\mathbb Z_{>0},+)^{1}\cong(\mathbb N,+,0).\]

Classical zero is recovered here by an explicit adjunction. A genealogy-forgetting map that sends a formation history to its positive magnitude does not by itself create an identity element. Consequently, any classical passage requiring zero must name the completion or adjunction; it cannot be attributed to projection alone.

The Strict Mirror Language

The Symbol Codex

Everything below is normative. Layer 1 is semantic ground; Layer 2 is the retired linear system (documented for the record and for linearization); Layer 3 is the final strict alphabet with stroke-level constructions; Layer 4 the layout constructors; Layer 5 the derived notational conventions; Layer 6 the metalanguage.

Layer 1 — semantic ground

• Strict-symmetry axiom. Every mark is carried to itself by left–right reflection, enforced by construction (stroke specifications), not by font.
• Mirror reading. \(M(S)\) = order reversal composed with glyph-wise reflection; the semantic requirement is \(\sem{M(S)}=\sem{S}\) where \(\sem{\cdot}\) (kerned double brackets).
• Non-inscription. The empty region is not a symbol; it is the absence of one. Every classical “\(=0\)” is answered by blank paper: annihilation, coincident bounds, closed-manifold accumulation, discriminant balancing blank, the refused basepoint of the indefinite integral.
• Blank is not a name (the non-euphemism clause). Blank is not zero renamed; it differs in syntactic category, not vocabulary. Zero is a term: it takes properties, enters sets, receives operations, and anchors the identity and absorber laws. A blank region emits no glyph, and every term's office is presence: each names a formed presentation, the offices are exhausted by the constructor inventory, and whatever is present in syntax is present in emission — a withholding is the renderer's non-performance of the act, recorded by the judgment \(\Eval(t)\uparrow\) and by it alone. What zero names in the classical register is answered here by an act's non-performance, never by a mark. Eliminability criterion: every well-formed occurrence of Blank paraphrases, meaning-preserved, into presence-talk (coincidence, annihilation, unsatisfiability, keeping); an occurrence that cannot be so paraphrased is smuggled zero and is illegal. Inexpressibility criterion: classical sentences in which zero is essential (“zero is even”; the identity law) have no translation — they are unformulable, not false. Zero is ineliminable and generative of laws; Blank is eliminable and generative of prohibitions. At the level of the classical model the two are co-referential; the system reforms the grammar, not the referent, and whether that reform is discovery is exactly the Faithfulness Question. Corollary (the nominalization ban). Blank admits no plural, no membership, no gradation, no index, and no duration: “the exit loci,” “a set of exit loci,” “blank-depth,” “blank at level \(n\)” are all illegal prose — reifications of absence, the zero-move committed in the metalanguage. All such structure attaches lawfully to sentences (inscriptions) and certifiers (presences): one writes “true \(\Pi_1\) sentence (arithmetical hierarchy, written without the oracle superscript throughout)s,” “sentences undecided by the level-\(n\) certifier,” never their blank-nominal shadows. Discovered as the clause's fourth successful audit: the eliminability test convicted a metatheoretic exposition that had granted absence a census, and every convicted phrase paraphrased losslessly into sentence-and-certifier form — which is the clause functioning as designed: a euphemism cannot be convicted; a typed prohibition can. Sanctioned forms. Each survives the eliminability test: (i) the metalanguage judgment \(\Eval(t)\uparrow\), which records withheld emission as a statement about the evaluation relation, never as a term; (ii) the predicative idiom balances blank, which predicates non-inscription of an evaluation exactly as “is consistent” predicates of a theory — a statement about emission, mirroring no drawn form; (iii) blank-typed as an adjective on sentences and truth-conditions; (iv) blank as an ordinary adjective on physical presences (blank paper, a blank page); (v) sentential nominals of the predicate — non-inscription — which attach to processes and sentences exactly as “consistency” and “non-halting” do. (vi) the copular and elliptical predicatives of the same idiom — “is blank,” “blank \(\Leftrightarrow\),” “ascending or blank” — which predicate non-inscription of an evaluation exactly as balances blank does. (vii) for laws, the positive-act forms are preferred and used natively: keeping law where the classical register writes kept, mirror-fixed and carried to itself where it writes kept-under-reflection; “keeping” remains licensable as a sentential nominal but is reserved for classical-apparatus names, flagged as imports. A law is an act performed at every stage, not a stasis. (viii) every position is an occupation: a drawn layout presents formed content at each of its positions and the page is exhausted by emissions of formed terms, so a one-sided balance or empty enclosure is excluded from \(\Sent(\GP)\) by that totality — the exclusion a fired rejection sponsored by the plenary-emission clause, in the grammar and equally in the drawn layout (WF6, Definition); the renderer's withholding is an event of the metalanguage, recorded by the judgment. Three plate emissions violating this law (a blank fused as an addend) were detected by the blind-reading experiment, whose independent reader — offered a vacant slot in an additive frame — introduced a null object to fill it: the exact category collapse the typing charge indicts, induced by our own layout. The emissions are repaired; the law is enacted; the experiment stands as the register's first external audit instrument. All count-noun uses are abolished: the parameters at which a descent balances blank are named what they always were — exit loci, presences, markable, orbit-bearing; the ledger over them is the exit ledger; the Witness–Blank theorem is renamed the Witness-Typing theorem. The reform sharpens the Riemann chapters rather than weakening them: the hypothesis concerns exit loci — parameters of the strip — and only the misnamed noun was ever absent-shaped. The logic of the volume (judgment forms). The metalogic here is verificationist, in the lineage the Honesty clause names: there are no truth-values as objects — the Boolean pair is the zero–one pair in disguise — and a sentence does not have a value. There are three judgment forms, each an act with an inscription attached: a sentence is inscribed (a derivation exhibited), counter-inscribed (a refutation exhibited), or kept (its channel maintained stage by stage). Excluded middle is accordingly not a law of this logic but a classical import, named where used — in the classical equivalences, and in the dichotomy clause of the Keeping Theorem, whose appeal to soundness and \(\Sigma_1\)-completeness is classical-side reasoning about the transfer. Assertion, in this logic, is not the selection of a value; it is the exhibition of an inscription. Refusals are events. Every “cannot” and “unwritable” in this volume is certified positively: by a fired rejection — the engine prints its refusal text, an inscription — or by an exhibited counter-term, drawn and checked. Negation here is never a name for an absent object; it is always cashed as a presence that does the blocking. The audit obeys the typing. Universal negatives over open domains — “no element of the kind anywhere” — admit no finite certificate and are blank-typed: they may be kept, stage by verified stage, never concluded. This applies to the volume's own purity claims: what is certified is the ledger of convictions and discharges; whether further instances remain is a channel held open, in exactly the posture this volume holds toward its one open axiom. Precedent: \(\neg\exists\) asserts absence without naming an object; Blank is the refused reification of the negated existential.
• WF6 and vinculum canonicality — discovery record. The prediction experiment exposed two forms admitted by an earlier grammar stratum: Blank used as an additive operand and an inscribed unit denominator. Definitive WF6: \(\mathsf{Blank}\) may occur only as a balance side or as the content of \(\mathsf{Box}/\mathsf{OBox}\); it is prohibited in every other constructor position. The former emissions are preserved only as the evidence by which the specification gap was discovered.
• Torsor ground. The number line is an affine line: positions and oriented changes, no origin. Orientation exists and lives on the vertical axis; what the classical register calls sign is read off it.
• Balance form. Equations are written with both sides inscribed as presences; no canonical right-hand side, no “\(=0\)” normalization.
• 1D Collapse (design lemma). Under the stated parsing and layout hypotheses together with the strict axiom a one-line string can express only commutative operations and symmetric relations; hence the notation is necessarily two-dimensional, with exactly two lawful carriers of asymmetry: the vertical axis, and adhesion.

Layer 2 — the retired chiral system, linearized

Achiral glyphs (self-converse denotations): \(+\;\cdot\;=\; \leftrightarrow\;\forall\;\pi\), the vertical stroke, and the provisional digit family. Chiral pairs, each mirroring to its converse:

pair	denotation	converse reading
angle brackets \(\langle\ \rangle\)	grouping	grouping
left/right filled triangles	oriented change “from–to”	“to–from”
lower-corner triangles	division (\(a\) by \(b\))	(\(b\) under \(a\))
\(\nearrow\ /\ \nwarrow\)	power (base–exponent)	(exponent–base)
half-moon anchors	numeral units-position	converse significance
\(<\ /\ >\)	order	converse order
\(\to\ /\ \leftarrow\)	implication	converse implication
tail-arrows	one-sided approach (from below)	(from above)
lens brackets	oriented integral scope	reversed orientation
lollipop pair	positional “below”	converse
turnstiles \(\vdash\ /\ \dashv\)	judgment (departing)	(arriving)

Additional achiral operators of that layer: \(\curlywedge\) (minimum), a vertical-symmetric existential, three-dot digit-three (freeing \(\Delta\) for the differential). Retirement: the pairs violate the strict axiom individually; the layer is retained solely as a typeable linearization of Layer-2 terms, and its two glyph classes are recovered in the final theory as the trivial and sign isotypes of the flat reading group.

Layer 3 — the strict atoms, stroke by stroke

All coordinates are in units of the atom half-size \(s\) (engine value \(s=11\) pt at scale 1), origin at the atom's center, \(x\) rightward, \(y\) upward. Every construction is symmetric under \(x\mapsto -x\) by inspection. “Pip” = filled dot of radius \(0.35s\); “dot” (operator) = filled dot of radius \(0.16s\); “rank dot” = filled dot of radius \(0.3s\).

Digits (bijective values one to ten)

value	name	construction
1	stroke	line \((0,-s)\)–\((0,s)\)
2	chevron	lines \((-0.7s,-s)\)–\((0,s)\) and \((0,s)\)–\((0.7s,-s)\)
3	three bars	horizontals at \(y=-0.8s,0,0.8s\), each \((-0.8s,y)\)–\((0.8s,y)\)
4	four pips	pips at \((\pm0.55s,\pm0.55s)\)
5	quincunx	pips at \((\pm0.6s,\pm0.6s)\) and \((0,0)\)
6	six pips	pips at \((\pm0.5s,\{0.7s,0,-0.7s\})\)
7	branched stem	line \((0,-s)\)–\((0,s)\); arms \((0,\pm0.15s)\)–\((\pm0.75s,\pm s)\), all four
8	double circle	circles radius \(0.52s\) centered \((0,\pm0.52s)\)
9	nine pips	pips at \((\{-0.65,0,0.65\}s,\{-0.65,0,0.65\}s)\)
10	cross	lines \((-0.7s,-s)\)–\((0.7s,s)\) and \((-0.7s,s)\)–\((0.7s,-s)\)

Letters (variables)

Y	stem \((0,-s)\)–\((0,0)\); arms \((0,0)\)–\((\pm0.7s,s)\)
A	legs \((\mp0.7s,-s)\)–\((0,s)\); bar \((-0.38s,-0.15s)\)–\((0.38s,-0.15s)\)
H	verticals at \(x=\pm0.55s\) full height; crossbar at \(y=0\)
T	top bar \((-0.7s,s)\)–\((0.7s,s)\); stem \((0,s)\)–\((0,-s)\)
U	verticals \((\pm0.55s,s)\)–\((\pm0.55s,-0.3s)\); bottom arc (semicircular arc closing below, \(180^\circ\) extent)
V	lines \((\mp0.7s,s)\)–\((0,-s)\)
M	verticals at \(x=\pm0.7s\); inner strokes meeting at \((0,-0.1s)\)
W	four strokes: \((\pm0.8s,s)\)–\((\pm0.4s,-s)\)–\((0,0.2s)\)
\(\Omega\)	open arc \(-60^\circ\) start, \(300^\circ\) extent, in box \((\pm0.6s, -0.45s..0.75s)\); feet \((\pm0.3s..\pm0.62s,-0.55s)\)

Extension rule: further variables by symmetric diacritics (dot, diaeresis, circumflex) glued above these; asymmetric Latin letters are illegal.

Operator and mark atoms

\(+\)	crossbars \((\pm0.7s,0)\) and \((0,\pm0.7s)\); commutative addition
\(\cdot\)	operator dot; commutative multiplication
\(=\)	horizontals at \(y=\pm0.3s\); symmetric relation
\(\oplus\) (fuse)	circle radius \(s\) with internal \(+\) of half-arm \(0.55s\); presence fusion (commutative semigroup, no neutral)
\(\cap\) (cap)	upper semicircular arc, legs to \(y=-0.7s\); meet-junction (commutative by WF3 — the grammar forces the algebra)
rank dot	glued above a digit: one dot \(=\times10\), two dots \(=\times100\), etc.
\(\Delta\)	triangle, apex \((0,s)\), base \((\pm0.85s,-s)\); the differential mark, glued above its variable
\(\infty\)	circles radius \(0.42s\) centered \((\pm0.42s,0)\); the indeterminate-extent mark
sector	upper half-disc radius \(s\) with diameter chord; the positive sector, carries a glued \(+\)
up / dn	vertical arrow marks (stem \(1.5s\), symmetric heads); bare orientation atoms
dots	three pips at \((\{-0.55,0,0.55\}s,0)\); ellipsis / residue marks
disk / rim	circle radius \(1.5s\), solid / dashed; region and boundary
rayV / rayH	long stroke, vertical \((0,\pm2.2s)\) / horizontal \((\pm2.2s,0)\); sweep carriers

Layer 4 — constructors and layout law

Universal metrics: gap \(G=8\) pt\(\times\)scale; adhesion marks render at \(0.55\times\) host scale; box padding \(1.4G\); Up/Dn connector \(2.6s\); Lk connector \(1.8s\).

constructor	layout	reflection action
\(\mathsf{Row}_{\circ}(t_1;t_2)\)	horizontal through operator atom \(\circ\); WF3: \(\circ\) must denote commutative/symmetric content	swaps arguments (harmless by WF3)
\(\mathsf{Jux}(t_1;t_2)\)	operator-free juxtaposition (clusters, free pairs); commutative by fiat	swaps arguments
\(\mathsf{Stk}(t;b)\)	\(t\) above \(b\), common axis	pointwise
\(\mathsf{Up/Dn}(t;b)\)	stack joined by oriented vertical arrow; the oriented change “from \(b\) up to \(t\)” / “from \(t\) down to \(b\)”	pointwise (orientation is vertical: mirror-fixed)
\(\mathsf{Lk}(t;b)\)	plain link; order-by-height	pointwise
\(\mathsf{Ovl}(a;b)\)	superposition at a common center (sweep crossings)	pointwise
\(\mathsf{Adh}_{\uparrow/\downarrow}(h;m)\)	mark \(m\) (atom or term) glued above/below host \(h\); WF2: rank dots on digits; \(\Delta\) on variables; exponents and half-powers above; stage/index marks below	pointwise on host and mark
\(\mathsf{Box}(t)\)	rounded enclosure; definite scope	pointwise
\(\mathsf{OBox}(t)\)	enclosure open at the top; WF4: only for semantically indeterminate content (infinity carriers, missing bounds)	pointwise
\(\mathsf{Frac}(n;d)\)	vinculum stack; division and quotients	pointwise
\(\mathsf{Blank}\)	emits no element; the licensed non-inscription slot	fixed

WF1: all layout axes vertical. Mirror theorem (structural induction): every well-formed term denotes the same proposition as its mirror; the only argument-permuting constructors are Row/Jux, tamed by commutativity. Machine check: render term and reflected term to primitive multisets (lines, circles, discs, arcs, rects); the term passes iff the coordinate-reflection of the first matches the second under bipartite pairing with tolerance \(0.05\) pt (arcs compared with \(\theta\mapsto 180^\circ-(\theta+\mathrm{extent})\)).

Layer 5 — derived notational conventions

• Numerals. Bijective base ten; a number is a cluster (\(\mathsf{Jux}\)) of rank-marked digits, order-free; e.g. thirty-two \(=\{3^{\bullet},2\}\) in either order; one hundred \(=\{9^{\bullet},10\}\); \(1024=\{10^{\bullet\bullet},2^{\bullet},4\}\).
• Oriented change. \(\mathsf{Up}(q;p)\) = “from \(p\) up to \(q\)”; its magnitude is achiral; annihilation \(\mathsf{Up}(p;p)+\mathsf{Dn}(p;p)\) balances blank.
• Roots. A square root is the half-power fraction glued above (\(\mathsf{Adh}\) with mark \(\mathsf{Frac}(1;2)\)). “The” root is never inscribable: the pair is achiral; a root with exhibited orientation carries an up/dn orientation mark — Galois conjugation is arrow reversal. Solving an equation is licensed chirality descent; Vieta (coefficients) is the achiral projection.
• Calculus. Differential: \(\Delta\) glued above the variable. Derivative: \(\mathsf{Frac}(\Delta W;\Delta T)\) — adhesion over vinculum, both vertical; existence \(=\) mirror-coherence of the vertical approach pair. Definite integral: Box with bounds stacked (target above, source below), integrand with glued \(\Delta\) inside; degenerate bounds \(\Rightarrow\) Blank. Indefinite integral: OBox; the result ends “\(+\ \mathsf{Blank}\)” — the classical \(+C\) is the refused basepoint. FTC: the box balances the Up-change of the antiderivative.
• Blanks (the non-inscription family). annihilation; coincident bounds; closed-manifold accumulation; disjoint junction; discriminant balancing blank (repeated roots; symmetric configurations sit on their own branch loci); zero deficit (the fourth right corner); the refused \(+C\); the unsatisfiable \(\omega\)-equation on the flat page.
• Carrier tower. Which roots a form can hold is fixed by its reading group: page — sign roots; corner — adds cube roots of the turn (E-doublet); smooth cone — all turns: the cone is, as carrier language, angularly complete (interpretation; the fundamental theorem of algebra is an import, not derived here) (the FTA reading).

Layer 6 — metalanguage symbols

\(\mathsf G\), \(\mu\), \(M\), \(\sem{\cdot}\)	grammar; glyph reflection; mirror reading; semantics
\(\mathsf{Sw},\mathsf{Res},\mathcal K\)	MJA sorts: sweeps, residues, costs (all zero-free)
\(\oplus,\cap,\kappa,\delta,\varepsilon,\pi^{+},\mathrm{tr}\)	fusion; junction; cost; defect (non-inscribed iff transverse; recoverability iff the defect balances blank); non-inscription (meta-name); positive-sector projection; genealogy trace (free — Chasles lives in evaluation only)
\(t,\kappa=\sin\alpha,\alpha,\gamma,R,h\)	sector fraction; sine; semi-vertical angle; seam angle (\(\sin\gamma=t_1h_2+t_2h_1\): the circle group law); slant; height (\(h^2=(1-t)(1+t)\): deficit times abundance)
\(\nu_{i,n}\)	Bessel order; limit-circle iff \(\nu interior to the unit interval\); rank thresholds \(\kappa=\sqrt{(4n^2+1)/5}\)
\(e_k\), \(\mathrm{disc}\)	symmetric functions (\(e_1=1\) always: the circle as trace); discriminant (the inscribed distinction)
\(A_k\) strata	fold / cusp / swallowtail: balanced di-cone; equilateral tri-form; four quarters — symmetry depth \(=\) multiplicity at the exit locus
\(G\) (reading groups)	\(\mathbb Z/2\) (page), \(C_{2v}\) (tent), \(C_{3v}\) (corner), \(O(2)\) (cone), \(O(3)\); carriers \(=\) kept coordinates; chiralities \(=\) nontrivial irreps
\(U(2)\), \(\Lambda=U\mathrm B U^*\)	seam/apex self-adjoint families; the junction dictionary (spend \(=\) extension parameter/degree)

Terminological convention

The following five words are used throughout in these senses only. An assertion is an inscription entered into \(\Sent(\GP)\) together with its sponsor. A judgment is a metalanguage act about formation or evaluation — \(\vdash\)-statements, \(\Eval(t)\!\uparrow\), formation and well-formedness judgments; a judgment is not a truth-bearer. A value is the output of evaluation, an element of \(\Ctimes\). A verdict is the recorded outcome of a sponsored decision. Truth is reserved for satisfaction in a named classical interpretation: the predicate is two-place, as in true in the standard arithmetic interpretation, and within a section that has already fixed the interpretation the qualifier may be elided. The phrase truth-value names a classical notion and appears below only where that notion is being denied of some object of this calculus; the Boolean pair is the zero–one pair and is named as such. Unqualified truth is not a term of this volume, and no claim here is made in it.

The Strict Grammar

Atoms

Constructors

Reflection and the mirror theorem

Proof.

Structural induction. Atoms: fixed by \(\refl\) and drawn self-symmetric, so the base case is the atom axiom. Vertical constructors (\(\Stk{}{}\), \(\Up{}{}\), \(\Dn{}{}\), \(\Fr{}{}\), \(\mathsf{Box}\), \(\mathsf{OBox}\), \(\Adh{}{}{}\)): \(\refl\) acts pointwise on arguments and preserves the constructor, so the inductive hypothesis closes the case — reflection cannot permute vertically encoded data. The only constructor that permutes arguments is \(\Row{}{}{}\), and WF3 restricts its operator slot to commutative/symmetric denotations, so \(\sem{\Row{\refl t_2}{\circ}{\refl t_1}} = \sem{\refl t_2}\circ\sem{\refl t_1} = \sem{t_2}\circ\sem{t_1} = \sem{t_1}\circ\sem{t_2}\).

The plates as terms

Exactly twelve object constructors

The strict object grammar has exactly twelve constructors over the strict atom set \(\Sigma\):

\[\mathsf{Bal},\mathsf{Row},\mathsf{Jux},\mathsf{Stk}, \mathsf{Up},\mathsf{Dn},\mathsf{Lk},\mathsf{Ovl}, \mathsf{Adh},\mathsf{Box},\mathsf{OBox},\mathsf{Frac}.\]

Blank is outside this count because Blank is not an object constructor.

Atoms are generators, not constructors in the twelve-constructor count.

Constructor table

constructor	layout and typing	reflection action
\(\mathsf{Bal}(l,r)\)	two formed sides separated by the symmetric balance relation	\(\mathsf{Bal}(\refl r,\refl l)\)
\(\mathsf{Row}_{\circ}(l,r)\)	horizontal operator row; \(\circ\) must denote commutative content or a symmetric relation	\(\mathsf{Row}_{\circ}(\refl r,\refl l)\)
\(\mathsf{Jux}(l,r)\)	operator-free multiset-style juxtaposition; order carries no denotation	\(\mathsf{Jux}(\refl r,\refl l)\)
\(\mathsf{Stk}(t,b)\)	\(t\) above \(b\), with a common vertical axis	\(\mathsf{Stk}(\refl t,\refl b)\)
\(\mathsf{Up}(t,b)\)	vertical stack with an upward-oriented connector	\(\mathsf{Up}(\refl t,\refl b)\)
\(\mathsf{Dn}(t,b)\)	vertical stack with a downward-oriented connector	\(\mathsf{Dn}(\refl t,\refl b)\)
\(\mathsf{Lk}(t,b)\)	plain vertical link between presented terms	\(\mathsf{Lk}(\refl t,\refl b)\)
\(\mathsf{Ovl}(l,r)\)	overlay at a common center	\(\mathsf{Ovl}(\refl l,\refl r)\)
\(\mathsf{Adh}_{v}(h,m)\)	typed mark \(m\) adhered above or below host \(h\)	\(\mathsf{Adh}_{v}(\refl h,\refl m)\)
\(\mathsf{Box}(t)\)	closed enclosure of formed content	\(\mathsf{Box}(\refl t)\)
\(\mathsf{OBox}(t)\)	open enclosure of formed but semantically indeterminate content	\(\mathsf{OBox}(\refl t)\)
\(\mathsf{Frac}(n,d)\)	vertical vinculum stack, with formed numerator and denominator	\(\mathsf{Frac}(\refl n,\refl d)\)

Only \(\mathsf{Bal}\), \(\mathsf{Row}\), and \(\mathsf{Jux}\) reverse their arguments. Every strict atom is fixed. The remaining constructors are carried pointwise under horizontal reflection.

Preterms and withheld emission

Arithmetic, membership, parity, magnitude, orientation, duration, index, and genealogy attach to formed terms, and the operand, mark, host, numerator, denominator, roster, and enclosure positions are each occupied by formed terms — the occupancy exhausts the positions. Where a classical renderer prints a placeholder, this one performs the judgment instead, and the judgment is the whole of the record.

Well-formedness WF1–WF6

Numeral canonicality

In bijective base ten, a canonical numeral has a finite rank roster

\[\{(r,d_r):0\le r\le k,\ 1\le d_r\le10\},\]

with every rank \(0,\ldots,k\) represented exactly once, and value

\[\sum_{r=0}^{k}d_r10^{r}.\]

The roster is displayed through \(\mathsf{Jux}\); reflection may reverse the display order, but rank marks retain the value. For example, thirty-two is the cluster consisting of a rank-one digit three and a rank-zero digit two. One hundred is represented by rank-one digit nine and rank-zero digit ten. No placeholder is required.

Proof.

Existence and uniqueness are the usual division-with-remainder proof for bijective numeration, using remainders in \(\{1,\ldots,10\}\). If an ordinary remainder is zero, the preceding quotient is reduced by one and digit ten is used. WF5 records each resulting rank exactly once and excludes all alternative carriers with repeated, omitted, or unit-denominator ranks.

Reflection

Proof.

Structural induction on \(t\). Atoms are fixed. In the \(\mathsf{Bal}\), \(\mathsf{Row}\), and \(\mathsf{Jux}\) cases, two applications of reflection reverse the arguments twice and the inductive hypotheses restore the children. Every remaining constructor is preserved pointwise, so the inductive hypotheses close those cases.

Proof.

Proceed by structural induction. WF1 is preserved because strict atoms are fixed and horizontal reflection preserves vertical axes. WF2 is preserved because host and mark sorts are preserved recursively and the vertical adhesion position is unchanged. WF3 is preserved because the three argument-reversing constructors are restricted to swap-invariant content. WF4 is preserved because horizontal reflection does not change whether a formed enclosure is open or semantically indeterminate. WF5 is preserved because the rank-labelled numeral roster is unchanged as a roster. WF6 is preserved vacuously on strict terms because no control preterm occurs in either \(t\) or \(\refl t\).

Renderer equivariance

Let \(L(t)\) denote the ideal renderer emission as a finite structured family of primitives with exact coordinates, and let \(\mu\) denote coordinate reflection \(x\mapsto-x\) on those primitives.

Proof.

The proof is structural. The atom case follows from the stroke registry. For \(\mathsf{Bal},\mathsf{Row},\mathsf{Jux}\), horizontal reflection exchanges the child placement boxes, exactly matching the recursive argument reversal. For \(\mathsf{Stk},\mathsf{Up},\mathsf{Dn},\mathsf{Lk}, \mathsf{Adh},\mathsf{Frac}\), reflection preserves vertical order and acts on each child. Overlay reflects each superposed primitive. Closed and open enclosure frames are themselves symmetric and carry the reflected child. These are all twelve constructor cases.

Proof.

Structural induction using the displayed interpretation hypotheses. The result is conditional on the semantic dictionary; renderer equivariance alone is not a proof of an arbitrary denotational interpretation.

Formal verification

The reflection metatheorems proved in this chapter apply to the full twelve-constructor grammar \(\mathsf G_{\mathrm P}\). The accompanying Lean development formalizes the implementation fragment \(\mathsf G_{\mathrm K}\), whose constructors are

\[\texttt{atom},\ \texttt{dig},\ \texttt{blank},\ \texttt{row},\ \texttt{bal},\ \texttt{jux},\ \texttt{ovl},\ \texttt{adh},\ \texttt{box},\ \texttt{obox},\ \texttt{lk},\ \texttt{frac}.\]

For this fragment the development proves reflection involutivity, preservation of its implemented well-formedness predicate, and equivariance of its emission algebra.

The implementation constructor blank is an artifact of the implementation grammar \(\mathsf G_{\mathrm K}\) alone; the strict discipline of record carries no counterpart to it at any layer, and it is not interpreted as a term of the strict object language. The full grammar theorem is therefore the structural theorem proved above, while the kernel certificate applies to the explicitly represented fragment \(\mathsf G_{\mathrm K}\). Toolchain information and source checksums are supplied with the accompanying artifacts.

The Plate Language

Plate Grammar and Reading Rules

The plate corpus uses ordinary TikZ primitives embedded directly in this source. The presence of those primitives makes the figures reproducible by TeX, but it does not prove that they were regenerated from the current renderer or checked in the final environment.

The original corpus was divided into:

1. ten founding machine plates;
2. thirty folded and proof plates;
3. continued plates F31–F56.

The following source preserves their drawings and captions under the historical control notice.

The Machine Edition: Original Ten Plates

Plate 1 — carriers of asymmetry

Plate 2 — presence-only numerals

Plate 3 — the torsor

Plate 4 — balance quadratic

Plate 5 — mirror coherence

Plate 6 — integration

Plate 7 — Fubini

Plate 8 — Stokes and Zeno

Plate 9 — descent

Plate X — junction and genealogy

The Folded Plates

Plate F1 — the tent: the dagger made isometry

Plate F2 — three sheets and the cone limit

Plate F3 — the reading-group theorem

Historical caption-only plate. The page, tent, corner, cone, and space were assigned the groups

\[\mathbb Z/2,\quad C_{2v},\quad C_{3v},\quad O(2),\quad O(3).\]

The current fixed-algebra theorem replaces the former claim that every orbit span is irreducible.

Plate F4 — the right-face bound

Plate F5 — roots in folded forms

Plate F6 — the tri-cone partition

Plate F7 — di-cone variables and heights

Plate F8 — tri-form cubic

Plate F9 — heights from coefficients and the historica

Blank stratification

Plate FX — seam law and carrier tower

Plate F11 — differentiation and integration

Plate F12 — the mirror axis

Plate F13 — historical spend-covering display

Plate F14 — historical presence-rendered ledger

Plate F15 — historical native derivation I

Plate F16 — historical native derivation II

Plate F17 — historical Witness–Blank statement

Plate F18 — historical formal proof I

Plate F19 — historical formal proof II

Historical reductio text: the implementation rejected a Blank control as an adhesion host and as an oriented operand. Those rejections do not reject a presented off-axis parameter with a metalinguistic nonemission judgment.

Plate F1X — determinant and turn showcase

Plate F21 — numerical determinant example

Plate F22 — turn algebra

Plate F23 — measure without a native null object

Plate F24 — historical right-folding tower

Plate F25 — historical determinant proofs

Historical Proof I: alternation as orientation reversal.

Historical Proof II: singularity as equality of parity fusions.

Plate F26 — historical Euler turn proof

Historical Proof III: the half-turn annihilation display.

Plate F27 — historical modification theorem

Historical Proof IV: modification on a null event.

Plate F28 — historical Borel–Cantelli and Burnside proofs

Historical Proof V: Borel–Cantelli in the proposed descent display.

Historical Proof VI: the Burnside right-folding criterion.

Historical Lemma B: Selection Jump display.

Historical Lemma C: no occupied Blank control.

Plate F2X — Euclid's infinitude of primes

Historical notation execution of Euclid's theorem.

The Continued Plates: F31–F56

Plate F31 — predicted terms

Plate F32 — predicted terms

Plate F33 — predicted terms

Plate F34 — predicted terms

Plate F35 — predicted terms

Plate F36 — predicted terms

Plate F37 — mined exact identities

Plate F38 — exit-locus retyping

Plate F39 — historical detector

Plate F3X — historical open frontier

Plate F41 — the Symmetry No-Go canonized

Plate F42 — historical genealogy filters

Plate F43 — historical adjudication display

The historical source announced that the external assessment had been adjudicated, the first MJA stratum corrected, Blank discipline tightened, the fixed-algebra theorem adopted, and machine claims rescoped. The claim of completed analytic budgets does not hold at the stratum of record, and Option B Blank is superseded by the strict renderer-control classification.

Plate F44 — historical exclusion filters

Plate F45 — historical discharge specification

Plate F46 — historical Keeping theorem

Plate F47 — Zeno stages and seal

Plate F48 — historical orbifold positivity examination

Plate F49 — historical conservation examination

Plate F4X — historical compressed native argument

Plate F51 — historical sponsored occupation

Plate F52 — finite stages and omega-family

Plate F53 — historical reference clauses

Plate F54 — historical architecture in five displays

Plate F55 — class-wide independence models

Plate F56 — historical transport to an omega-family

The Caption-Blind Decoding Audit

This chapter is a documentary record of a caption-blind trial of the object language, together with its exact evidential status. The trial is part of the volume's provenance: its one conviction is the recorded origin of the stricter Blank control now in force, so the current stratum's discipline cites this chapter as the register's first external audit instrument.

The trial

The glyph corpus — the figures, stripped of every caption, label, and word — was delivered to an independent reader in a fresh context, with staged probes designed to leak neither vocabulary nor target. The reader was caption-blind, not mathematics-blind: the correct condition, since the reference clauses of Section concern informed interpreters. Three rounds; findings at exact strength.

Round one: arithmetic. The bijective numerals, the rank-dot place system, the carry law, commutativity, and the machine edition's quadratic ladder were recovered, and every operator was correctly typed. The language's arithmetic stratum self-decodes.

Round one's conviction. Offered a vacant slot in an additive frame — three plate emissions then carried a blank fused as an addend — the reader introduced a null object, performing exactly the category collapse the typing charge indicts. The layout, not the reader, was convicted: the emissions were repaired, and the stricter Blank control of the current stratum is the enactment. The experiment thereby served as the register's first external audit instrument.

Round two: the primes. The membership rule of the index family was recovered exactly — membership above one admitting only the unit factorization, with the square-root stopping rule derived from the reflected pairing of divisors: the mirror law's arithmetic shadow, surfacing unprompted. The reader generated correct unattested members from the decoded rule: the grammar is generative in foreign hands.

Round two: the retraction. Tested distributionally, the null-object hypothesis was formally retracted: the empty enclosure is never added, multiplied, exponentiated, indexed, or oriented; it stands only as a balance side or within an enclosure. The reader concluded that it marks a well-typed place whose content is absent — the blank-as-judgment doctrine, reached from evidence alone by a classically trained mind, with the distinction between an unfinished syntax and an inscribed absence drawn without prompting. The sponsored seals were read as meta-level provenance marks, as designed.

Round three: the mirror and the naming. The reader corrected its own earlier census, reformulated the reflection as an involutive order-reversing operation under which the notation is closed — legality preserved, statements carried to equivalent or dual statements — and identified this closure as the structural law, with pointwise symmetry its fixed-point case: the mirror theorem, recovered blind at language level. Then, holding the prime index, the reciprocal ladders, the privileged half with its fixed-point property, and the reflection law jointly, the reader named the object: the Riemann zeta function and its Euler product, at a self-reported confidence of ninety percent; the completed descent with its reflection about one half, seventy; an approach to the critical line and the hypothesis, sixty. The figures the reader specified as settling the remainder are, item for item, the categoricity ingredients of Section and the axis statement of the Riemann architecture: the reader requested exactly the plates the volume contains.

What the trial establishes, and what it does not

The exhibition claim — that the notation carries arithmetic, generative grammar, and structural law to an independent mind without one word of any human language — gains empirical support. The reference clauses gain their trial: the categoricity ingredients, jointly held, moved a blind reader to the intended object by name. And the register gained an instrument: the one violation surviving fourteen internal audits was found by external eyes in one round.

Status, recorded exactly. The trial had sample size one; the reader was a single language model; confidence figures are self-reported; the protocol was not a blinded human-subject experiment. The record is an exploratory audit observation and supports the exhibition and reference claims at evidence grade; it is not a theorem of semantic legibility or of reference, and no clause of this volume's assertion of record rests on it. Within those limits the finding stands as stated: reference travels in the strokes; the keeping, as ever, is the cell.

Typed Algebra and Geometry

The First Junction Model and Its Failure

The junction algebra was first proposed with a surcharge cost law, distribution of intersection over fusion, a residue endomorphism, and a Recoverability theorem. This chapter states that model exactly and refutes it; the typed successor is defined in the next chapter, and every later use is governed by the successor.

Carriers

Axioms

The recoverability theorem

Proof.

(\(\Leftarrow\)) In the transverse case the residue is \((A\fuse B)\meet\pproj\) with \(A,B\) the separate traces (Axioma); by Axiom the genealogy of a fused pair is the product of genealogies, and in the transverse case the two factors have independent constraint paths, so the factorization of \(\trace(A\fuse B)\) into its two coprime paths is unique and each factor, together with its cost, determines its sweep. (\(\Rightarrow\)) In the tangential case the merged trace of Axiomb identifies the overlapping constraint once; the surcharge \(\defect\) is exactly the inscription of what the merge forgot, and distinct pairs sharing the same overlap and the same complements precipitate identical residues, so no inverse exists. Formally, in the blade model of § the tangential fiber of the junction map over a fixed residue has positive dimension equal to \(\dim\) of the overlap, while the transverse fiber is a single point; the model computation is Theorem(iv).

The blade model and soundness

Proof.

(i)–(iii) are elementary linear geometry: intersection of subspaces is commutative; codimensions add under transverse intersection and exceed additivity by the overlap dimension otherwise, which is exactly Axiom with \(\defect\) = excess; the cone conditioning is an idempotent operation commuting with direct sum on independent supports, giving Axiom. (iv): in the transverse case two planes in general position through a common line are determined by their traces on that line together with their codimension data, so the junction map is injective on transverse pairs with fixed costs; in the tangential case one may rotate each plane within the overlap without changing either the intersection or the costs, producing the positive-dimensional fiber.

The Zeno instance computed

The Typed Algebra \(\mathsf{MJA}_2\)

From the failed model to the typed algebra

The surcharge law, the distributivity axiom, and Recoverability fail in the blade model; the counterexamples of the preceding chapter close that route. The algebra of record is the typed system defined here.

The assertion is the smaller typed algebra \(\mathsf{MJA}_{2}\).

Signature of \(\mathsf{MJA}_{2}\)

The partial operations are:

\[\fuse:\Sw\times\Sw\rightharpoonup\Sw,\] \[\meetJ:\Sw\times\Sw\rightharpoonup\Res,\] \[\kappa:\Sw\to\Cost, \qquad \trace:\Sw\to\mathcal T,\]

and

\[c_{+}:\Res\rightharpoonup\mathsf{Obs}.\]

Fusion is defined only when the fused sweep remains proper. Junction is defined only when the intersection residue is proper and nontrivial. Undefinedness is a metalanguage fact about the partial operation; no null residue is returned.

Axioms

Distribution of \(\meetJ\) over \(\fuse\), Recoverability of inputs from a residue, and conditioning as a residue endomorphism are not axioms of \(\mathsf{MJA}_{2}\).

Conditioning

Let \(E\) be an ambient classical carrier and \(C_{+}\subset E\) a fixed positive cone. In the metalanguage define

\[P_{+}(X)=X\cap C_{+}.\]

The operator \(P_{+}\) is monotone and idempotent on its set-valued domain:

\[P_{+}(P_{+}(X))=P_{+}(X).\]

The observation sort contains the presented nonempty cone sections of residues. The map

\[c_{+}(R)=P_{+}(R)\]

is a partial corestriction, defined only when the section is observation-typed. The classical metalanguage may state that another section is empty; the strict object language receives no empty observation.

Idempotence belongs to \(P_{+}\). The expression \(c_{+}\circ c_{+}\) is not used when its codomain and domain do not match.

Finite-dimensional model

Proof.

Commutativity and associativity follow from subspace sum on the declared domain. The dimension formula

\[\dim(A+B)+\dim(A\cap B)=\dim A+\dim B\]

is equivalent to

\[\operatorname{codim}(A\cap B) +\operatorname{codim}(A+B) = \operatorname{codim}A+\operatorname{codim}B,\]

which gives the modular cost law whenever both partial outputs belong to their native carriers. Genealogy holds by the definition of the presented generator record under fusion. The absorber for subspace sum would be the ambient space, which is excluded as improper.

The Reading Group: Folding the Page

Fixed-function formulation

Proof.

For page reflection \(x\mapsto-x\), an invariant polynomial contains only even powers of \(x\), giving \(\mathbb R[x^{2},y]\). The real reflection group \(C_{3v}\), acting as the dihedral group of order six, has polynomial invariants generated by \(r^{2}=x^{2}+y^{2}\) and \(\operatorname{Re}(z^{3})=x^{3}-3xy^{2}\). The \(O(2)\)-invariant polynomials are radial and therefore polynomials in \(r^{2}\). These are standard fixed-ring computations; see.

An orbit span decomposes into isotypic components and need not be irreducible. In particular, the span of a two-element chiral orbit under \(\mathbb Z/2\) decomposes as trivial plus sign. The older claim that every orbit span is itself an irreducible chirality is superseded.

The tent, corner, and cone are geometric realizations of the relevant actions. They are not asserted to be literal models of every quotient space carrying the same group.

The page, tent, corner, and cone

The page carries the reflection group \(\mathbb Z/2\). A tent adds a second commuting reflection and realizes \(C_{2v}\). A three-face corner realizes \(C_{3v}\). A rotational cone carries an \(O(2)\) reading action.

These geometric carriers are interpretations of the strict syntax. The structural Mirror theorem itself is the recursive statement of Chapter; it does not depend on physically folding paper.

Right-face defect

Proof.

If \(n\) right face angles meet, strict convexity requires

\[n\frac{\pi}{2}<2\pi.\]

Hence \(n<4\), so \(n\le3\).

At four right angles the angular defect is zero, so no strictly convex positive-curvature vertex forms. This does not imply that every defect-free fold is physically identical to an unfolded page; nontrivial flat-fold configurations may remain. Any dimensional interpretation of the bound is therefore an interpretation, not part of the convexity theorem.

Page, Tent, Corner, and Cone

The reading correspondence, exact form (definitive)

Lawful scalar carriers on a reading surface \(\Sigma\) with reading group \(G\) are the \(G\)-fixed functions — equivalently, functions on \(\Sigma/G\) — and the fixed algebra (classically, the fixed algebra — the import named once here) is computed per action: for the page reflection, \(\mathbb R[x,y]^{\mathbb Z/2}=\mathbb R[x^{2},y]\) (height and squared offset); for the planar \(C_{3v}\) action, generators \(r^{2}\) and \(\operatorname{Re}(z^{3})\); for \(O(2)\), \(\mathbb R[r^{2}]\). The linear span of a \(G\)-orbit of marks decomposes isotypically and is in general reducible: the chiral pair's span is trivial \(\oplus\) sign. The narrative realization that follows (tent, corner, cone) is a family of geometric models of these actions, and its claims are read through this section.

From one mirror to a group

Parts A–B fixed the reading symmetry as a single reflection: \(G=\mathbb{Z}/2\) acting on the plane of the page, with Theorem the statement that semantics descends to the quotient. Folding the sheet changes \(G\). Join two sheets at a ridge (the tent): the isometry group is \(C_{2v}\cong\mathbb{Z}/2\times\mathbb{Z}/2\) (face-swap and end-swap), and the face-swap realizes the reflection functor \(\refl\) as a literal isometry of a three-dimensional object: a term \(t\) and its reflection \(\refl t\) inscribed on the two faces produce a tent that closes — faces coinciding under the fold — precisely when \(t\) is mirror-coherent. Join three sheets at a corner: \(G=C_{3v}\). Roll the sheet and glue its vertical edges: the cone, with \(G=C_{\infty v}=O(2)\), rotations about the axis together with reflections through every axial plane. Horizontal position, which on the page carried no kept meaning, becomes angle; a \(\mathsf{Row}\) wrapped around the cone becomes a cyclic word, and WF3's commutativity discipline strengthens to cyclic keeping.

The classification theorem

Proof.

(i) A coordinate can carry meaning readable from every \(G\)-position iff it is constant on \(G\)-orbits of reading frames, i.e. \(G\)-kept; for the listed groups the fixed algebras are generated by the stated distance functions. (ii) Descent of semantics to \(\Sigma/G\) is keeping of denotation under \(G\), which on the linear span of glyph-content is projection to the trivial isotype. (iii)–(iv) Decompose the glyph space into irreducibles; a \(G\)-orbit of marks denoting converse-related content is exactly a copy of a nontrivial irreducible, and for \(\mathbb{Z}/2\) the only one is the sign.

Roots, Resolvents, and Folding Towers

Quadratic and cubic readings

For a real depressed quadratic

\[y^{2}=D\]

with \(D\) nonnegative, the two real roots may be read as one magnitude with two vertical orientations. If \(D\) is negative, the roots require the rotational complex carrier; the real page reading does not apply.

The generic cubic has Galois group \(S_{3}\cong C_{3v}\). The corner therefore supplies a geometric realization of its permutation action. This is a classical group-theoretic fact together with a geometric interpretation; it is not a derivation of the cubic formula from the shape of a corner.

Quartic resolvent

The separate subgroup picture \(S_{4}\supset S_{3}\) describes the stabilizer of one root. It is not the construction of the resolvent cubic.

Vieta and discriminants

The classical fixed-ring theorem gives

\[k[r_1,\ldots,r_n]^{S_n} = k[e_1,\ldots,e_n],\]

where \(e_1,\ldots,e_n\) are the elementary symmetric functions. Coefficients are therefore invariant functions of the roots. The present program reads solving as passage from the fixed coefficient data to a genealogy carrying individual roots. That reading is an interpretation of the classical theorem, not an additional representation theorem.

The discriminant detects collision of roots. At a repeated root the classical discriminant equals zero; under a presence interpretation, the positively presented data are the parameter and the collision certificate, while the failed distinction is a metalinguistic nonseparation judgment. No Blank term is substituted for the discriminant value inside the strict language.

Right-folding

Proof.

If the group has such a composition series, the product of the orders of its factors is \(2^{a}3^{b}\). Conversely, Burnside's \(p^{\alpha}q^{\beta}\) theorem implies that every finite group of order \(2^{a}3^{b}\) is solvable. Every composition factor of a finite solvable group is cyclic of prime order. Since only the primes \(2\) and \(3\) divide the group order, all factors are \(C_2\) or \(C_3\).

The generic quintic

The generic quintic has Galois group \(S_{5}\), whose composition series contains the nonabelian simple factor \(A_{5}\). That factor is the decisive obstruction to solvability by radicals. The obstruction is not the prime five by itself: cyclic \(C_{5}\)-extensions are solvable by radicals.

Right-folding and radical solvability are therefore compared only as an explicitly defined structural analogy. Theorem classifies the right-folding family; classical Galois theory supplies the distinct \(A_{5}\) obstruction. No general equivalence between physical folding constructions and all radical towers is asserted.

Counting by Positive Analytic Data

This chapter records classical realizations used by the program. Each result remains classical and transfers only through its stated interface.

Meromorphic counting kernel

Proof.

This is the residue theorem under the displayed hypotheses. The presence interpretation concerns the roster of poles and their multiplicity records; it does not alter the classical theorem.

The contour-free-of-poles hypothesis and the residue-equals- multiplicity hypothesis are both essential. A merely meromorphic function is not automatically an admissible counting kernel.

Cyclic factorization and partial fractions

Let \(\zeta_m=e^{2\pi i/m}\). The degree-\(m\) factorization is

\[n^{m}-l^{m} = \prod_{j=1}^{m} \bigl(n-\zeta_m^{\,j}l\bigr).\]

For presented \(l\) and away from the poles, the corresponding partial fraction identity in the \(n\)-variable is

\[\frac{1}{n^{m}-l^{m}} = \frac{1}{m\,l^{m-1}} \sum_{j=1}^{m} \frac{\zeta_m^{\,j}} {n-\zeta_m^{\,j}l}.\]

Proof.

At the pole \(n=\zeta_m^{\,j}l\), the derivative of \(n^{m}-l^{m}\) is

\[m(\zeta_m^{\,j}l)^{m-1} = m\zeta_m^{-j}l^{m-1}.\]

The residue is therefore \(\zeta_m^{\,j}/(m l^{m-1})\), which gives the displayed decomposition.

If one sheet is presented and labelled \(n_1\), the deck orbit is generated genealogically:

\[n_{j+1}=\zeta_m\,n_j \quad(j=1,\dots,m-1), \qquad \zeta_m\,n_m=n_1.\]

This orbit supplies a local labelled roster only after a sheet label has been presented.

Digamma comb

The digamma function \(\psi(w)=\Gamma'(w)/\Gamma(w)\) has simple poles at \(w=0,-1,-2,\ldots\), each with residue \(-1\). Consequently

\[\psi(\rho-z)\]

has poles at

\[z=\rho,\rho+1,\rho+2,\ldots\]

with positive unit residues in the \(z\)-variable.

Indeed, near \(z_0=\rho+k\),

\[\rho-z=-k-(z-z_0),\]

and hence

\[\psi(\rho-z) \sim -\frac{1}{\rho-z+k} = \frac{1}{z-z_0}.\]

The sign depends on the variable. Statements that assign negative unit residues to this comb in the \(z\)-variable are superseded.

Monodromy and labelled rosters

A covering map may have globally constant fiber cardinality while admitting no global labelled trivialization. Monodromy obstructs the latter, not the former.

For example,

\[z\longmapsto z^{2}:S^{1}\to S^{1}\]

has fiber cardinality two over every point. The classical degree is globally defined. Traversing the base circle exchanges the two local labels, so there is no global continuous enumeration preserving the chosen sheet identities.

The program calls a roster retaining witness identity a genealogical roster. Nontrivial monodromy may prevent such a global labelled roster even though the unlabeled cardinality remains constant. Two lawful responses are available: forget the labels and retain the degree, or pull back to a cover on which a trivialization is presented. Neither response licenses the claim that monodromy destroys global fiber cardinality.

Planar Dirichlet heat trace

This is a classical heat-kernel result under the stated smooth, bounded, planar, Euclidean, and Dirichlet hypotheses. Other dimensions, boundary conditions, corners, singular metrics, or non-Euclidean geometries require their own formulas.

The Dagger Identity: the Root Algebra Returned

The referent of the program's deep logic connections is recorded here at adjudicated strength. The provenance verdict stands: the cross-domain schema is interpretive. This chapter therefore asserts its two internal columns as theorems of the present volume, imports its third column as classical mathematics named at the point of use, and declares the identification of pattern as a named reading with its instances tabulated exactly — not as a theorem.

The schema

Status by column. The geometric column is Theorem: lawful carriers on a reading surface are the fixed functions of the reading group, computed per action. The analytic column is the reflection metatheory of the strict grammar: involutivity (Theorem), preservation of well-formedness (Theorem), and renderer equivariance (Theorem). The arithmetic column is classical Galois theory, imported: the fixed field of the Galois group is the base field, and the fixed ring of the symmetric action on roots is the ring of coefficients. The identification of the three factorizations as one schema is the reading declared above; it is exact on every instance tabulated in this volume and is asserted at no greater strength.

Vieta re-read

The classical fixed-ring theorem of Chapter,

\[k[r_1,\ldots,r_n]^{S_n}=k[e_1,\ldots,e_n],\]

acquires its reading here. Coefficients are the mirror-coherent content of roots: a balance-form equation, which inscribes coefficients, is an achiral inscription, and solving it is a controlled descent into chirality. The moment an orientation glyph appears is the moment the notation reaches past the fixed component; a single root is never inscribable without exhibited orientation, only the achiral pair or an oriented member carried by \(\mathsf{Up}\)/\(\mathsf{Dn}\). Solving is breaking mirror-coherence in a licensed way. Status: this is the fixed-ring theorem re-read as a statement about the language; the mathematics is classical, and the reading is the dagger reading applied to one instance.

The boundary of the reading

The reading is a factorization schema, not a solvability equivalence. Theorem classifies the right-folding family, and classical Galois theory supplies the distinct \(A_{5}\) obstruction for the generic quintic; no general equivalence between physical folding constructions and radical solvability is asserted, exactly as the roots chapter records. The dagger reading survives that boundary because it never crossed it: what is identified is the pattern of keeping, not any transfer of solvability between columns.

Cone-Chain Applications

Closed Planar Cone Chains

Conventions as in the di-cone papers: a sector of fraction \(t interior to the unit interval\) of a circle of radius \(R\) rolls into a right circular cone of slant height \(R\), base radius \(r=Rt\), semi-vertical angle \(\alpha\) with \(\sin\alpha=\kappa=t\). “Material” of a cone family is \(m=\sum_k \sin\alpha_k\), in units of one circle's arc. A planar chain requires consecutive shared generatrices, \(\gamma_k=\alpha_k+\alpha_{k+1}\); a closed chain requires \(\sum_k\gamma_k=2\pi\), i.e. \(\sum_k\alpha_k=\pi\).

The no-go and the two-circle barrier

The minimal symmetric closure

Quantum structure of the closed tri-chain

The root algebra of the di-cone, and the deep connections

Riemann Architecture

Formation of the Native Riemann Question

Classical analytic object

In the classical register define

\[\xi(s) = \frac12 s(s-1)\pi^{-s/2}\Gamma\!\left(\frac{s}{2}\right)\zeta(s).\]

It is entire and satisfies

\[\xi(s)=\xi(1-s)\]

and

\[\xi(\bar s)=\overline{\xi(s)}.\]

The standard analytic background is given in.

Let

\[\Xi(t)=\xi\!\left(\frac12+it\right).\]

For real \(t\), \(\Xi(t)\) is real.

Presence retyping

The symbol \(\uparrow\) is a judgment about the partial evaluation. It is not an element of \(\Ctimes\), a third truth value, or an object-language term.

The certificate is positive data. The parameter is positive data. The withheld value is not converted into an object.

Nonformation of the literal zero-locus sentence

Proof.

For all \(m,n\in T\),

\[m\oplus n=m+n>m.\]

Thus no \(n\in T\) satisfies \(m\oplus n=m\) for every \(m\).

Proof.

Inspect the atom registry and the twelve constructors of Definition. No zero atom occurs, and no constructor introduces one. The result follows by closure of the term grammar.

This is a theorem about \(\GP\). It is not a claim that \(\xi(s)=0\) is ill formed in classical complex analysis.

The native sentence

Every term quantified over in this sentence is positive: the record, parameter, certificate, completed descent, and involution. Nonemission remains a metalanguage condition attached to the definition of the record.

Proof.

The sentence quantifies over formed exit-locus records and uses only presented parameters, certificates, the mirror involution, and the symmetric balance relation. It requires no Blank control and no zero term.

The tent group

Let

\[\sigma(s)=1-s, \qquad \tau(s)=\bar s.\]

Then \(\sigma\) and \(\tau\) commute and generate

\[G=\{1,\sigma,\tau,\sigma\tau\} \cong C_2\times C_2.\]

The fixed locus of \(\tau\) is the real axis, and the fixed locus of \(\sigma\tau\) is the critical line.

A generic orbit has four points:

\[\{s,1-s,\bar s,1-\bar s\}.\]

An orbit on either fixed axis has at most two points. The orbit has one point only at \(s=1/2\).

Three exact classical forms

Proof.

R1 says exactly that every classical zero of \(\xi\) has the form \(1/2+it\) with real \(t\), which is the critical-line statement. A point is fixed by \(s\mapsto1-\bar s\) exactly when its real part is \(1/2\), giving R2. A generic non-real off-axis point has a four-element Klein orbit. A non-real point has an orbit of size at most two precisely when it lies on the critical line. Real points also have orbits of size at most two, which is why R3 includes the separate classical fact that \(\xi\) has no real zeros.

Proof.

Write

\[\Xi(t)=(t-t_0)^m u(t)\]

with \(u(t_0)\ne0\). The factor \((t-t_0)^m\) changes sign exactly when \(m\) is odd.

Sign-change detection is therefore not a fourth unconditional equivalence.

The completed function and the so-called trivial zeros

For every positive integer \(n\), the pole of \(\Gamma(s/2)\) at \(s=-2n\) is cancelled by the classical zero of \(\zeta(s)\) there. The completed function is regular and

\[\xi(-2n)=\xi(1+2n)\ne0.\]

Thus the negative even zeros belong to the uncompleted zeta factorization and are not exit loci of the completed \(\xi\). This is ordinary classical cancellation under the displayed normalization.

The foundational interpretation may describe the completion factor as an interface cost. The cancellation theorem itself remains a classical analytic fact.

Class-wide and zeta-specific Admission

The two sentences are not interchangeable.

• \(\AdmClass\) ranges over an abstract class and is separated by the finite models of Chapter.
• \(\AdmZeta\) concerns one completed prime-fused descent and is fixed only after the zeta reference conditions are supplied.
• Class-wide independence does not imply zeta-specific independence.
• A finite polynomial witness to \(\CounterAdmClass\) is not thereby a model of the zeta reference conditions.

Explicit sponsorship and native derivation

Let \(\alpha_\zeta\) name the recorded adoption event

\[\mathsf{Sponsor}(\alpha_\zeta,\AdmZeta).\]

Proof.

Let \(\mathsf{Exit}_{\xi}(s;c)\) be an arbitrary native exit-locus record for the completed descent fixed by the zeta reference interface. Instantiating \(\AdmZeta\) at that record yields

\[s=1-\bar s.\]

Since the record was arbitrary, universal introduction gives \(\RHMirror\).

The theorem is intentionally transparent. Its content is that the native axis sentence follows from the explicitly adopted zeta-specific Admission law. It is not a derivation of that law from the unextended base theory, and it is not advertised as an unpriced classical proof.

Reference interface

The zeta-specific instance is fixed through three interpretive conditions:

1. the genealogy is the full prime genealogy associated with the Euler product in its convergent region;
2. the plenum normalization is the harmonic/pole normalization of the zeta Dirichlet series;
3. the completed descent has the zeta functional equation and the standard gamma factor.

Proof.

This is the relevant application of Hamburger's converse theorem under its named hypotheses. The reference result is conditional on those analytic hypotheses; the glyph grammar alone does not establish them.

Analytic interface

Proof.

By Definition, the exit-locus records of the zeta-specific descent correspond to the classical zeros of \(\xi\), and the native mirror axis corresponds to \(\operatorname{Re}s=1/2\). Therefore the interpreted Admission law says exactly that every nontrivial classical zero lies on the critical line.

A second expression of the same classical price is Weil positivity. For the admissible test class in Weil's criterion, with the involution

\[\widetilde f(x)=\overline{f(-x)},\]

the criterion has the form

\[W(f*\widetilde f)\ge0 \qquad \text{for every admissible }f.\]

Under the standard analytic hypotheses and normalization, Weil's criterion is equivalent to \(\RHClass\). The criterion is a classical theorem used at the interface, not a consequence of reflection symmetry or the renderer.

Symmetry No-Go

Proof.

The substitution \(s\mapsto1-s\) sends \(s-\tfrac12\) to its negative, so it fixes \((s-\tfrac12)^2\) and hence \(F\).

The root set is

\[\left\{ \frac12+a,\frac12-a, \frac12+\bar a,\frac12-\bar a \right\},\]

which is closed under complex conjugation; consequently the coefficients are real and \(F(\bar s)=\overline{F(s)}\).

One root is

\[\frac12+a=\frac45+7i,\]

whose real part is \(4/5\), not \(1/2\). The roots form a complete off-axis Klein-four orbit while satisfying both displayed symmetries.

The theorem identifies the precise limit of symmetry arguments. A zeta-specific proof obligation must use arithmetic or analytic information not shared by \(F\), such as the prime genealogy, completed growth structure, or an equivalent Admission law.

Relative Independence of Class-Wide Admission

The symmetric route, attempted and closed

An earlier development attempted to derive axis occupation from the junction algebra and the reflection symmetry alone: the spend-covering argument ran the algebra axiom by axiom against the completed function's reading group and concluded occupation from symmetry bookkeeping. The route fails, and the failure is exact: the polynomial witness of the controlling architecture, \(F(s)=((s-\tfrac12)^2-a^2)((s-\tfrac12)^2-\bar a^{\,2})\) with \(a=\tfrac3{10}+7i\), satisfies every symmetry the argument uses while carrying an off-axis quartet. The Symmetry No-Go above is the theorem this witness proves, and the repaired route is the one this part follows: class-wide relative independence, explicit adoption of \(\AdmZeta\), and the native axis theorem in \(\Pdag\). The development record of the attempted route is preserved in the project archive.

Declared base scope

The theorem in this chapter concerns the native base theory \(\Pbase\), not PA, ZFC, or another external proof theory.

The relevant descent fragment of \(\Pbase\) has:

1. nonempty finite root multisets;
2. closure under nonempty multiset fusion;
3. closure under the declared mirror and conjugation actions;
4. a polynomial carrier \[ F_D(s)=\prod_{\rho\in D}(s-\rho); \]
5. a conditioned field \[ \Phi_D(s) = \operatorname{Re}\frac{F_D'(s)}{F_D(s)}; \]
6. presented rational test points away from the roots;
7. no class-wide Admission axiom.

The grammar and \(\mathsf{MJA}_2\) modules receive one common interpretation in both models. The models differ only in the descent carrier. The independence theorem is relative to this exact many-sorted base.

Model A

Let the descents of Model A be the nonempty finite multisets of roots on the seam

\[\rho=\frac12+i\gamma,\]

closed under the required conjugation and fusion operations.

For

\[s=\sigma+it, \qquad \sigma>\frac12,\]

one has

\[\operatorname{Re} \frac1{s-(\frac12+i\gamma)} = \frac{\sigma-\frac12} {|s-(\frac12+i\gamma)|^2} >0.\]

Every term in \(\Phi_D(s)\) is therefore positive.

Proof.

Sum the strictly positive displayed contribution over the nonempty finite root multiset.

Model B

Let Model B be generated under nonempty fusion by the Klein-symmetric quadruple

\[D_B= \left\{ \frac45+5i,\frac45-5i, \frac15+5i,\frac15-5i \right\}.\]

Evaluate at the presented rational point

\[s_0=\frac35+5i.\]

The four real contributions are:

\[-5, \qquad -\frac5{2501}, \qquad \frac52, \qquad \frac5{1252}.\]

Using

\[1252\cdot2501=3131252,\]

their sum is

\[\begin{aligned} \Phi_{D_B}(s_0) &= \frac{-15656260-6260+7828130+12505} {3131252}\\ &= -\frac{7821885}{3131252}\\ &<0. \end{aligned}\]

Proof.

The descent \(D_B\) and the presented point \(s_0\) witness the existential sentence, by the exact calculation above.

Independence theorem

Proof.

Model A is a model of the base theory in which \(\AdmClass\) holds. Model B is a model of the same base theory in which \(\CounterAdmClass\) holds. By soundness of the declared proof calculus for these interpretations, a sentence derivable from \(\Pbase\) must hold in every model of \(\Pbase\). Model B therefore refutes derivability of \(\AdmClass\), and Model A refutes derivability of \(\CounterAdmClass\).

Exact-arithmetic artifact scope

The displayed fraction can be checked directly in rational arithmetic. An accompanying script may reproduce it, but the script does not by itself verify:

• the grammar axioms;
• the shared \(\mathsf{MJA}_2\) interpretation;
• closure of the model carriers;
• the soundness theorem;
• any zeta-specific statement.

No script execution is asserted by this TeX source.

Omega Formation and the Selection Jump

Kept stages

Fix a decidable address sort and a decidable negative verifier. Write

\[\mathsf{Reject}(w,r)\]

when \(r\) is a positively presented rejecting trace for address \(w\).

The metalanguage natural numbers in this definition index stages. They are not strict object-language numerals and do not install a zero term in \(\GP\).

Omega-Seal rule

The premise of the rule is a presented completed object. It is stronger than separately stated stagewise availability. The formation-rule study behind this chapter is the corpus manuscript The Selection Jump.

Proof.

The formation rules contain constructors for the three listed events. They contain no rule whose premise is merely \(\forall n\,\exists k_n\,\mathsf{Keep}(n,k_n)\) and whose conclusion is a selector or coherent family. Closure under the declared rules therefore leaves the stagewise statement without a family-forming derivation. The result is a theorem about this formation system, not a theorem that no external classical choice principle can be adopted.

Explicit witnessed completion

Let \(K_\zeta\) be a name introduced at the metalanguage level for the completed family required by the witnessed omega semantics. The assertion includes the explicit adoption event

\[\mathsf{Sponsor} (\alpha_\omega,\mathsf{OmegaKeep}(K_\zeta)).\]

This is a completion postulate. It does not provide:

• a program computing \(k_n\) from \(n\);
• the component records \(k_n\);
• an analytic proof that every component is kept;
• a proof internal to the unextended base theory;
• an interval-certified verification of all addresses.

The sponsorship records occupation in the witnessed semantics, at exactly that strength.

Zeno-register consequence

Assume the named negative-channel interface: if an off-axis exit-locus record exists, then some finite address is accepted by the negative verifier; and a kept stage covering that address carries a rejecting trace incompatible with acceptance.

Proof.

Suppose an off-axis exit-locus record were presented. By the negative-channel interface it yields an accepted finite address \(w\). Choose a stage index exceeding \(w\). The corresponding component of the sponsored coherent family contains a rejecting trace for \(w\). Determinism of the verifier supplies a positive clash between the accepted and rejected traces. Hypothesis-discharging rejection therefore rejects the off-axis record. Since the record was arbitrary, the native axis sentence follows in the omega register.

This is not an analytic proof because the completed-family premise is an explicitly adopted completion postulate.

Class-wide independence, arithmetic shadow, and coverage

The two-model theorem concerns \(\AdmClass\), not \(\AdmZeta\). Its direct consequence is that the unextended native base does not select a side of the class-wide fork.

A separate arithmetic interpretation may assign a standard \(\Pi_1\) sentence \(\varphi_{\mathrm{RH}}\) to the classical arithmetic shadow of the Riemann question.

Proof.

If \(\varphi_{\mathrm{RH}}\) were false in the standard arithmetic interpretation, then \(\neg\varphi_{\mathrm{RH}}\) would be a true \(\Sigma_1\) sentence with a finite standard witness. The declared \(\Sigma_1\)-completeness clause would give

\[T\vdash\neg\varphi_{\mathrm{RH}},\]

contrary to the assumed independence. Therefore the arithmetic shadow is true.

The theorem establishes the standard arithmetic shadow only. A further coverage theorem is required before that truth is transferred to every formation admitted by the full presence foundation.

Proof.

Under \(C_{\mathrm{cov}}\), every relevant exit formation is in the image of the standard coding. The arithmetic truth excludes every coded counterexample, so coverage excludes every relevant counterexample.

Without coverage, a formation outside the image is not addressed by the arithmetic quantifier. No transfer follows for that formation.

Conservative independence transfer

The arithmetic shadow of the independence theorem is governed by a transfer schema whose proof is immediate but whose statement fixes exactly what any classical relabeling of the native theorem must supply.

Proof.

Contraposition of each displayed hypothesis.

The theorem composes with the one-sided route into a single chain: native independence, under a proof-reflecting translation, yields classical arithmetic independence; a \(\Pi_1\) representative together with \(\Sigma_1\)-completeness of a sound \(T\) converts that independence into arithmetic truth; and the analytic equivalence converts truth into \(\RHClass\). Independence is therefore not an evasion of the Riemann question: at the appropriate arithmetic strength it is an affirmative proof method. The chain's antecedent is a zeta-specific independence theorem under a proof-reflecting translation; the theorem proved in this book is class-wide, over \(\Pbase\), and the two are connected only by an instance-separation theorem that the reference clauses do not yet supply. That connection is stated as an open problem.

What licenses the adoption

The Sponsorship Declaration of \(\AdmZeta\) is a foundational act, and a foundational act invites the question of what makes it lawful rather than arbitrary. The answer is not an analogy to any historical foundational choice. It is a theorem about routes.

Four steps, each already proved.

Presence-only formation. The verdict language records positive presentations and contains no constructor for absence: no witness-not-found, no counterexample-not-seen, no checker-returned-nothing. Nonpresentation is therefore never converted into a present verdict. This is the no-free-sign theorem, and it is the grammar of this volume applied to sign formation itself.

Nullity of the selected architecture. Consider the enriched exact selected package of the completed zeta descent: exact finite negative channels, exact all-stage positive channels, trace predicates, and a \(\Pi_1\) arithmetic representative. Every sound resolver that is fully invariant under replacement of one exact selected package by another is identically empty. Equivalent criteria are absorbed as fibres of one package, and absorption forms no verdict: availability of an exact criterion is not occupation of a sign. Criterion splitting, replay, arithmetization, realizer indexing, and finite-stage verification raise complexity without raising sign.

The forgetful boundary. A resolver is a-priori selected exactly when it factors through the map that discards package-specific coordinates while retaining exact selected structure. No sound sign selector factors through selected architecture alone. Consequently every sound route that does form a sign must expose the point at which it stops so factoring, and that point is an occupation, a derivation, a coordinate theorem, a stream, or an oracle. Every sound route is exposed.

The declaration is the exposure. The adoption recorded here is that exposed point, named in advance rather than discovered by audit. It constitutes the theory \(\Pdag=\Pbase+\AdmZeta\), it carries a sponsor \(\alpha_\zeta\), it is marked at its stratum, and its classical price is stated exactly by Interface Theorem. Every verdict it sponsors is formed carrying that trace, which is what formation means in this volume: every verdict here names what presented it, and that naming is the whole of what is sought.

The license follows. A route that forms a sign without exposing its non-invariant effect is convicted by the hypothesis-tethering theorem, which admits no untethered premise into a sign derivation. A route whose formation withholds every inscription is already absorbed into the maximal selected closure. There is no third class. The adopted law is therefore not one option among many equally available foundational choices: it is the disclosed form of the only kind of act that can form a sign at all, made visible at the moment of adoption instead of recovered later from a proof that quietly used it.

The declaration answers the independence theorem rather than evading it. That \(\AdmZeta\) is underivable from \(\Pbase\) is what makes a declaration the required act; a derivation would have made it superfluous, and a refutation would have made it unavailable.

What is formed

It remains to say what verdict this forms, and in what terms.

The interface \(I\) is defined in Definition and the equivalence

\[I(\AdmZeta)\Longleftrightarrow\RHClass\]

is proved from that definition by Interface Theorem. The proof is carried out in the classical metatheory, which is where a statement about the object language is stated and proved: standing outside a language is the condition of speaking about it, and the register separation of this book is accordingly the instrument of reach, not a limit on it. The theorem is a proved reaching, and it grips \(\RHClass\) exactly. It requires no prior construction: the faithfulness condition belongs to Corollary, which constrains classical realizations of \(\Pdag\), and is not a hypothesis of the interface theorem.

\(\AdmZeta\) is present in \(\Pdag\) by the Sponsorship Declaration, sponsored by \(\alpha_\zeta\). Therefore, under \(I\), \(\RHClass\) holds, and the verdict that forms carries its trace: the adopted theory \(\Pdag\), the native derivation of \(\RHMirror\), and the sponsor \(\alpha_\zeta\) that presented the law.

That trace is not a qualification on the verdict. It is what a verdict is here: the naming exhausts the verdict. Every formed verdict of this book names what presented it — a certificate, a derivation, a coordinate theorem, a completed stream, or a declaration — and the classical register's sponsorless verdict is, in this grammar's diagnosis, one more reification of non-presentation, the analysis of which occupies this volume throughout. The record is complete and the seeking is performed: what presented this one is a declaration, made at a fork proved inhabited on both sides, displayed at the moment of adoption rather than recovered afterward from a proof that used it silently.

Riemann result by register

The Riemann architecture has five positive components.

• Grammar. The literal sentence \(\RHClassZero\) is not in \(\Sent(\GP)\), while the certified native axis sentence \(\RHMirror\) is.
• Adopted native theory. The explicitly sponsored theory \[ \Pdag=\Pbase+\AdmZeta \] derives \(\RHMirror\).
• Relative native metatheory. The declared class-wide base has models on both sides of the Admission fork: \[ \Pbase\nvdash\AdmClass, \qquad \Pbase\nvdash\CounterAdmClass. \]
• Omega completion. The witnessed semantics explicitly sponsors a coherent omega-kept family as a completion postulate. The Omega-Seal rule yields the native axis conclusion relative to that completed family and the negative-channel interface.
• Classical analytic interface. The named interpretation satisfies \[ I(\AdmZeta)\Longleftrightarrow\RHClass. \] Thus the classical strength of the zeta-specific native adoption is stated exactly.

The Symmetry No-Go proves that reflection and functional-equation symmetry do not alone select the axis configuration.

Explicit Formula and Computation

The Explicit-Formula Ledger

Normalization

Let \(g\) be a real even test function in the declared Weil class and define

\[h(r) = \int_{-\infty}^{\infty} g(u)e^{iru}\,du,\]

with inverse convention

\[g(u) = \frac1{2\pi} \int_{-\infty}^{\infty} h(r)e^{-iru}\,dr.\]

For a nontrivial classical zero \(\rho\), write

\[\gamma_\rho=\frac{\rho-\frac12}{i}.\]

On the Riemann hypothesis these parameters are real. Without that hypothesis the spectral side is read in complete Klein-symmetric quartet form.

Under the normalization used by the supplied ledger, the explicit formula is

\[\begin{aligned} \sum_{\rho} h(\gamma_\rho) ={}& h\!\left(\frac i2\right) + h\!\left(-\frac i2\right) - g(0)\log\pi\\ &+ \frac1{2\pi} \int_{-\infty}^{\infty} h(r) \operatorname{Re} \psi\!\left(\frac14+\frac{ir}{2}\right)\,dr\\ &- 2\sum_{n\ge2} \frac{\Lambda(n)}{\sqrt n} g(\log n). \end{aligned}\]

The formula is classical and depends on its test-class and normalization hypotheses.

Moving the prime term to the other side gives a balance interpretation, but the signs remain those of the displayed classical formula. The phrase “four unsigned blocks” is not used.

Assurance classification

The supplied source records numerical evaluations using a finite zero roster, a finite prime-power cutoff, and multiprecision arithmetic. Those evaluations are not analytic tail certificates.

The current assertion is limited to:

The ledger values are computations at their stated truncations, with the independent-precision stability information recorded by the underlying numerical artifact when such a comparison was actually performed.

The following remain:

• a repaired and independently checked zero-count tail lemma;
• a complete analytic spectral-tail budget;
• a complete prime-power tail budget;
• outward-rounded interval evaluation of every component;
• a rerun tied to the final frozen source and artifact hashes.

No theorem in the assertion-of-record stratum uses the former unit-interval zero-count lemma or the former extremely small tail budgets.

Gaussian rows

For the reported Gaussian family

\[h(r)=\sqrt{2\pi s_2}\,e^{-s_2r^2/2},\]

the supplied source records the following finite computations. The table is retained as numerical data at the stated truncations, not as a proof of global positivity.

\(s_2\)	spend \(+\) plenum	prime bill	reported margin	bill/spend	margin divided by \(2h(\gamma_1)\)
\(0.01\)	\(0.26930811\)	\(3.6\times10^{-11}\)	\(0.26930811\)	\(1.3\times10^{-10}\)	\(1.4587\)
\(0.04\)	\(0.02100690\)	\(0.00241645\)	\(0.01859045\)	\(0.11503\)	\(1.00809\)
\(0.09\)	\(0.06969797\)	\(0.06951061\)	\(1.874\times10^{-4}\)	\(0.99731\)	\(1.0000185\)
\(0.16\)	\(0.24976826\)	\(0.24976803\)	\(2.295\times10^{-7}\)	\(0.9999991\)	\(1.0000000\)
\(0.25\)	\(0.51233559\)	\(0.51233559\)	\(3.574\times10^{-11}\)	\(1.0000000\)	\(1.0000000\)
\(0.36\)	\(0.83816961\)	\(0.83816961\)	\(7.245\times10^{-16}\)	\(1.0000000\)	\(1.0000000\)

The finite parameters reported by the supplied source were a roster of eighty positive ordinates, prime powers through \(10^7\), and multiprecision arithmetic. This TeX source does not claim that those parameters have been rerun or independently confirmed for the final distribution.

Because a Gaussian has full support, its prime bill is never grammatically absent merely because it is numerically small. The exact empty-bill statement belongs only to a compactly supported test whose support is contained in

\[(-\log2,\log2).\]

Proof.

For \(n\ge2\),

\[\log n\ge\log2,\]

which lies outside the open support interval.

The absence of a contributing term is stated here in the metalanguage. A renderer may display a withheld prime-bill slot as a diagnostic, but that display is not a strict empty object.

Lowest-ordinate asymptotic, conditional form

If all relevant spectral parameters are real and ordered by positive ordinate, then for the Gaussian family the finite spectral sum has leading behavior

\[2m_1\sqrt{2\pi s_2} e^{-s_2\gamma_1^2/2}\]

as \(s_2\) increases, provided the remaining terms are controlled so that their ratio to the first term tends to zero. This is a conditional asymptotic statement under the stated spectral and tail hypotheses. The displayed finite ratios in the table are numerical observations, not a completed proof of the global tail condition.

Detector status

A one-parameter test family may reveal oscillation caused by a specified off-axis quartet, but absence of observed oscillation over a finite range does not exclude all off-axis configurations. Different contributions may be too small, lie beyond the tested scale, or partially mask one another. The proposed Faithfulness Detector is therefore exploratory and partial. It is not a decision procedure for the Riemann hypothesis.

No analytic-budget theorem

Earlier source strata asserted a unit-interval zero-count lemma, spectral tails hundreds of orders below the displayed margins, and unconditional positivity of selected Gaussian rows. Those claims are not assertions of record. They require a repaired zero-count argument, verified constants, complete truncation accounting, and an outward-rounded interval rerun. Until those tasks are completed, the ledger remains.

The Kept Register: Speaking Only of Presence

The quarantine convention licenses the metatheory to speak classically. This chapter records a stricter declared discipline and what the corpus looks like from inside it. Call the discipline \(\mathsf D_{+}\): speech records performed acts and presented objects, and the record is exhausted by them. \(\mathsf D_{+}\) is here a sponsored perspective, declared as such; the register convention of the front matter stands, and every claim of this chapter is relative to the declaration. The chapter adds a perspective and keeps the others.

The survival roster

Read under \(\mathsf D_{+}\), the volume's principal results appear in the following forms, each a performed act or a presented object.

Formation of the flagship. The formation checker, run on the zero-normalized string, terminates in a fired rejection at the clause where an equation demands a formed term; the rejection certificate, with its trace, is the theorem. Refusals are events, and this one is performed.

Independence as two rejections. The reformed reductio runs twice. Assume a base derivation of class-wide Admission; soundness transports it into Model B, a presented finite object, where it meets the counter-inscription that B witnesses — a clash, exhibited in exact rationals — and the clash rule fires \(\mathrm{Reject}(\ulcorner \Pbase\vdash\AdmClass\urcorner;\kappa_B)\). Symmetrically through Model A for the counter-law. Two rejection inscriptions, each finite, each carrying its witness, jointly constitute the independence theorem in kept form.

Consistency as a presented model. Model B presents the base; Model A presents it again. A presented model is a positive consistency certificate, and the semantic route is the one this volume travels.

The record as roster. The emission ledger lists performed emissions, and the roster is the entire record. Sponsorship appears as a totality: every formed verdict names its presenter, and the presenters are exhausted by occupation, derivation, coordinate theorem, completed stream, oracle, and declaration.

The kept form of the axis law

A law is an act performed at every stage, not a stasis — the idiom convention says so, and under \(\mathsf D_{+}\) that sentence carries the resolution. The native axis law, spoken in kept form:

At every stage of the kept ledger there is a next stage, and the stage is kept: the ascent is performed, the keeping is witnessed, \(\mathrm{Keep}(n,k_n)\) with \(k_n\preceq k_{n+1}\) presented, stage by stage; the sponsored coherent family seals the ledger under the registered Omega-Seal rule; and the clash channel stands ready — a presented off-axis exit record meets the covering stage in a witnessed clash and fires a rejection.

That is the theorem in presence-only speech. It asserts acts: keeping performed at every stage, a family sponsored, a seal formed, a channel armed. Its verdict carries its sponsors — the stage witnesses, the family's declaration, the interface's price — and the carrying exhausts the verdict. What the classical register compresses into a quantifier over an open domain, the kept register performs, stage by verified stage, in exactly the posture this volume holds toward its one open axiom.

The same posture carries the limitative results. Universal claims over open domains are kept laws under \(\mathsf D_{+}\): held stage by stage, each stage certified. Incompleteness itself appears in kept form as the ascent of the ledger — at every stage there is a next stage — which the omega chapter already formalizes as the refusal of the Selection Jump and the sponsorship of the seal.

The discipline polices its expositors

Drafting audit, recorded in house style: an early exposition of this chapter summarized the survival roster with an absence idiom (“almost nothing dies”). The eliminability test convicted the phrase; the conviction fired; the repaired form is the roster above, which speaks of what each result becomes and of the machinery it lands on. The specimen is retained because it exhibits the discipline's edge: \(\mathsf D_{+}\) is kept the way every law here is kept, act by act, and its audits are among the acts.

Research Directions and Engineering Consequences

Directions Beyond the Axis

The research program of the founding stratum was executed in many directions, and only its axis-facing third matured into the Riemann architecture of the preceding part. The remaining directions are recorded here at exact current strength: what is proved is asserted, what is computed is dated to its truncations, what is open is named open, and every full historical construction remains readable verbatim in the strata. This chapter is where the program's concepts meet one another.

The founding fold: tent and cone-three algebra rooted i

the primes

For a cone rolled from a sector of share \(\rho\) of the full turn with slant height \(\ell\), the base radius is \(r=\rho\ell\) and the height satisfies

\[h^{2}=(\ell-r)(\ell+r).\]

For the prime shares \(\rho=1/p\) the normalized height \(x=h/\ell\) satisfies

\[p^{2}x^{2}=(p-1)(p+1),\]

with the tent case \(4x^{2}=3\) and the one-third case \(9x^{2}=8\). Status: the identities are exact elementary geometry and are asserted. Their reading — the third dimension of the folded page rooted, share by share, in the primes — is a declared reading in the sense of Chapter, and the fixed-function discipline governing what the folded forms may carry is Theorem.

The di-cone system and the variational silhouette

With complementary radii \(r_{1}+r_{2}=\ell\) on a common slant, the heights satisfy

\[h_{i}^{2}=\ell^{2}-r_{i}^{2}, \qquad h_{1}^{2}=r_{2}(\ell+r_{1}), \qquad h_{2}^{2}=r_{1}(\ell+r_{2}),\]

and

\[h_{1}^{2}-h_{2}^{2}=\ell\,(r_{2}-r_{1}).\]

The di-cone volume stationarity polynomial factorizes exactly as

\[(2\rho-1) \left( 18\rho^{6}-54\rho^{5}+24\rho^{4}+42\rho^{3}-42\rho^{2}+12\rho-1 \right),\]

with the seam factor \(2\rho-1\) exhibiting the mirror-symmetric critical share and the sextic carrying the paired off-seam critical ratios. Status: the identities and the factorization are exact and asserted. The comparison of seam and off-seam occupations against a computed prime-fused field is a computed observation at its recorded truncations, and the silhouette reading built on it is open.

Reference and the categoricity clauses

The reference question is whether the notation, held jointly, determines its intended object. Three categoricity clauses are proposed:

1. a full prime genealogy;
2. a harmonic-plenum or pole normalization;
3. a zeta-type mirror completion.

Status: these are proposed identification criteria. Their joint sufficiency is not a theorem of this volume. One external trial is on record — the blind reading of Chapter — in which the clauses' ingredients, jointly held, produced the intended identification by name; a trial supports and does not prove.

Positivity in the di-cone: the orbifold examination

The critical strip may be read as a reflection orbifold and a self-convolution test as a mirror fusion. On the critical line a real spectral parameter contributes a nonnegative square-type Gaussian weight; an off-line pair contributes oscillatory terms of indefinite sign. Status: this is a heuristic frame, consistent with the classical Gaussian ledger of Chapter, and no positivity theorem is asserted from it.

The Zeno completion and the generator

The witness channel admits a decidable rejection judgment \(\mathsf{Rej}(w,r)\) and finite kept stages \(\mathsf{Keep}(n,k_{n})\), assembled into coherent families \(K=(k_{n})\). Status: the definitions are sound and retained. The historical witness-exhaustion claim is superseded; its corrected descendant is the omega-completion postulate and Selection Jump of the Riemann architecture, where the completed coherent family is explicitly sponsored rather than derived. The generator direction is retained with its recorded distinction: totality of a stage-extending verifier at each input is distinct from uniform production of a completed family, and only the former is claimed.

The stiffness field and the harmonic face

The stiffness field is

\[\Phi(\sigma,t)=\operatorname{Re}\frac{\xi'}{\xi}(\sigma+it).\]

By the functional equation the appropriately completed field is odd about the critical line away from singularities; away from zeros and poles it is harmonic, and the minimum principle applies on compact subdomains with controlled boundary data. Status: these facts are classical, imported and exact. The historical unconditional positivity wedge and the kept-region assembly are open: they require exact lower bounds on the relevant boundary data and a verified zero roster below the cited height, and neither is asserted here.

The de Branges test

Status: a scope statement at interface strength, with its classical input cited; it sharpens the target of the Admission law and leaves the law's status to the adoption that decides it.

The Selberg-class generalization

Under the classical interface, the two admission filters correspond exactly: distinct genealogy to the functional-equation axiom, and prime-fused trace to the Euler-product axiom. The trace typing thus recovers the Selberg axioms from inside the calculus, and Admission over the class reads, classically, as the class-wide Riemann hypothesis. Status: the axiom recovery is a structural comparison at interface strength. The class-wide sentence of the present volume, \(\AdmClass\), is this direction matured: the independence chapter separates it from its counter-inscription by finite models, so the class-wide hypothesis itself is neither asserted nor refuted here — that separation is the content of Theorem. The survey observation that every known off-axis family fails a filter is recorded at survey strength.

The mining protocol

Candidate implications over the \(\mathsf{MJA}_{2}\) signature are triaged in order: well-formedness; survival in the blade model; survival against the polynomial witness; survival against the Davenport–Heilbronn descent; non-equivalence to Admission, with any candidate implying full-cone positivity set aside at conjecture strength. Survivors are conjecture-grade lemmas ranked by detector sensitivity. Status: the protocol is specified, and its filters now have exact instruments in the current stratum — the polynomial witness is the descent of Model B, and the genealogy filter is the Davenport–Heilbronn exclusion. No run is claimed.

Open problems

The following problems are stated as mathematics. (1) Prove or refute the coverage theorem: that the standard analytic roster represents every exit-locus formation of the completed descent, i.e. \(C_{\mathrm{cov}}\) holds for \(\zeta\). (2) Determine whether the di-cone sextic's paired critical ratios admit a spectral interpretation under the prime-fused field, and prove or refute the silhouette comparison at all truncations. (3) Prove the unconditional stiffness wedge: exhibit exact boundary bounds under which \(\Phi>0\) on a right neighborhood of the line, or show no such bounds exist. (4) Extend the kernel formalization from \(\mathsf G_{\mathrm K}\) to the full strict grammar — eliminating the implementation blank variant, which the discipline of record excludes at every layer — and machine-check numeral canonicality. (5) Characterize the class for which the Selberg-axiom recovery of the trace typing is exact, and decide class-wide Admission for a nontrivial finitely axiomatized subclass. (6) Give a formation-faithful interpretation of a zero-based foundation into \(\Pdag\) and compute its price on the explicit-formula ledger. (7) Construct an admitting model of the referenced theory \(\Pbase+\mathrm{RefClauses}\) — a model of the reference clauses whose referent admits — or prove that the referenced theory does not derive \(\CounterAdmZeta\) by other means. Either, together with membership of the referent in the class and internalization of a finite contrary witness, yields \(\RHClass\); with the converse adequacy of the analytic interpretation, the three statements \(\RHClass\), non-derivability of \(\CounterAdmZeta\) over the referenced theory, and existence of an admitting model are equivalent. Model B separates the class-wide schema precisely by evading the reference clauses, so the proved class-wide theorem neither supplies nor is supplied by this instance; the two are related by an existential introduction in the easy direction only.

Appendices

Finite Presentations for the Class-Wide Independence Theorem

This appendix preserves the finite presentation associated with the class-wide relative independence theorem. Its models concern \(\AdmClass\), not \(\AdmZeta\), the full coverage interface, or an external arithmetic independence claim.

Signature

module	symbol	type	domain or role
grammar	\(\mathsf{Term}(\mathsf G)\)	inductive sort	implementation or strict term carrier as separately declared
grammar	\(\mu\)	\(\mathsf{Term}\to\mathsf{Term}\)	mirror involution
grammar	\(\mathsf{WF}\)	predicate	well-formedness discipline
grammar	\(\mathsf{Em}\)	term to emission	renderer map
\(\mathsf{MJA}_2\)	\(\Sw\)	sort	proper sweeps
\(\mathsf{MJA}_2\)	\(\Res\subseteq\Sw\)	subsort	proper nontrivial residues
\(\mathsf{MJA}_2\)	\(\mathcal K,\mathcal T\)	sorts	costs and traces
\(\mathsf{MJA}_2\)	\(\fuse\)	\(\Sw\times\Sw\rightharpoonup\Sw\)	partial proper fusion
\(\mathsf{MJA}_2\)	\(\meetJ\)	\(\Sw\times\Sw\rightharpoonup\Res\)	partial proper nontrivial intersection
\(\mathsf{MJA}_2\)	\(\kappa\)	\(\Sw\to\mathcal K\)	cost
\(\mathsf{MJA}_2\)	\(\trace\)	\(\Sw\to\mathcal T\)	genealogy trace
\(\mathsf{MJA}_2\)	\(c_+\)	\(\Res\rightharpoonup\mathsf{Obs}\)	partial positive-cone observation
descent	\(\mathsf D\)	sort	nonempty finite class-wide descents
descent	\(\mathrm{gen}\)	\(\mathsf D\to\mathcal T\)	root or genealogy multiset
descent	\(\mathrm{ev}\)	\(\mathsf D\times\mathsf{Pt} \rightharpoonup\mathsf F\)	field evaluation at presented points
descent	\(\mathrm{sec}^+\)	predicate	right-of-seam conditioning
descent	\(\mathrm{Asc}\)	predicate	formation of the positive-sector observation of the conditioned fieldClassical gloss: \(\Phi_D(s)>0\) at the conditioned point.

No Admission sentence is built into the base signature.

Base axioms

label	base requirement
A1–A6	the declared implementation or strict well-formedness rules, read at their separately scoped levels
A7	renderer-control positions do not become strict semantic operands
A8	mirror involutivity and the applicable emission-equivariance theorem
A9	the modular cost identity wherever both partial operations are defined
A10	fusion genealogy \[ \trace(X\fuse Y)=\trace(X)\sqcup\trace(Y) \]
A11	no absorber among proper sweeps
A12	trace compatibility on fusion
A13	conditioning is the partial corestriction of the ambient positive-cone section
A14	descent fusion is nonempty multiset concatenation
A15	finite products of nonzero classical factors remain nonzero
A16	the conditioned field is evaluated only at presented points in its declared domain

Shared grammar and algebra interpretation

Both independence models use the same interpretation of the grammar and \(\mathsf{MJA}_2\) modules. Their separation occurs only in the descent carrier.

The current mathematical proof of the separation requires only that the shared modules have at least one common model and that the descent axioms below are satisfied. A checker run or Lean theorem is not substituted for that model-theoretic requirement.

Descent field

For a nonempty finite root multiset

\[D=\{\rho_1,\ldots,\rho_k\},\]

define

\[F_D(s) = \prod_{j=1}^{k}(s-\rho_j)\]

and

\[\Phi_D(s) = \operatorname{Re}\frac{F_D'(s)}{F_D(s)} = \sum_{j=1}^{k} \operatorname{Re}\frac1{s-\rho_j}.\]

Fusion is multiset concatenation. The field is evaluated away from the roots at presented rational points.

Model A

The Model A carrier consists of nonempty finite multisets of roots

\[\rho_j=\frac12+i\gamma_j\]

on the seam, closed under the declared conjugation, mirror, and fusion operations.

For

\[s=\sigma+it, \qquad \sigma>\frac12,\]

one has

\[\operatorname{Re} \frac1{s-(\frac12+i\gamma_j)} = \frac{\sigma-\frac12} {|s-(\frac12+i\gamma_j)|^2} >0.\]

Hence

\[\Phi_D(s)>0\]

for every Model A descent and every presented conditioned point.

Model A satisfies \(\AdmClass\).

Model B

The Model B carrier is generated under nonempty multiset fusion by

\[D_B = \left\{ \frac45+5i, \frac45-5i, \frac15+5i, \frac15-5i \right\}.\]

At

\[s_0=\frac35+5i,\]

the four contributions are

\[-5, \qquad -\frac5{2501}, \qquad \frac52, \qquad \frac5{1252}.\]

Since

\[1252\cdot2501=3131252,\]

the exact sum is

\[\begin{aligned} \Phi_{D_B}(s_0) &= \frac{ -15656260 -6260 +7828130 +12505 }{3131252}\\ &= -\frac{7821885}{3131252}\\ &<0. \end{aligned}\]

The exact field value is machine-checked by the exact-rational script verify_independence.py supplied with the artifacts: the four terms evaluate to \(-5,\ -\tfrac{5}{2501},\ \tfrac{5}{2},\ \tfrac{5}{1252}\) and sum to \(-\tfrac{7821885}{3131252}<0\).

Model B satisfies \(\CounterAdmClass\).

Axiom-by-axiom table

axiom	Model A	Model B
A1–A8	shared grammar interpretation	shared grammar interpretation
A9–A13	shared typed \(\mathsf{MJA}_2\) interpretation	shared typed \(\mathsf{MJA}_2\) interpretation
A14	nonempty seam-multiset concatenation	nonempty witness-multiset concatenation
A15	finite nonzero products remain nonzero	finite nonzero products remain nonzero
A16	right-half-strip field evaluation	right-half-strip field evaluation
Admission	holds term by term	fails at \(s_0\) by the exact fraction

Separation

Model A satisfies the class-wide Admission sentence. Model B satisfies its class-wide counter-inscription. Both interpret the declared base. Therefore

\[\Pbase\nvdash\AdmClass\]

and

\[\Pbase\nvdash\CounterAdmClass.\]

No zeta-specific or higher-cardinality coverage conclusion follows without another interface theorem.

Kernel-Source Transcriptions

Scope

The following listings reproduce the supplied Lean transcriptions. They are retained for inspection. The source of record in a final distribution is the separate .lean file, not this typeset copy.

The implementation datatype contains a variant named blank, for which the strict discipline of record has no counterpart at any layer. It also differs from the exact strict twelve-constructor inventory. Any successful kernel result is therefore scoped to \(\GK\).

No compiler result or checksum is asserted by this transcription.

Mirror.lean

/- The Mirror Calculus: implementation-fragment proof-assistant port.
   The datatype includes implementation control syntax.
   It is not the complete strict PreTerm/Term split. -/

namespace MirrorCalculus

def mir : Nat -> Nat
  | 0 => 1
  | 1 => 0
  | 2 => 3
  | 3 => 2
  | 4 => 5
  | 5 => 4
  | 6 => 7
  | 7 => 6
  | n + 8 => n + 8

theorem mir_invol : forall c, mir (mir c) = c
  | 0 => rfl
  | 1 => rfl
  | 2 => rfl
  | 3 => rfl
  | 4 => rfl
  | 5 => rfl
  | 6 => rfl
  | 7 => rfl
  | _ + 8 => rfl

@[simp] theorem mir_shift (n : Nat) :
    mir (n + 8) = n + 8 := rfl

@[simp] theorem mir_dig (d : Nat) :
    mir (d + 100) = d + 100 := rfl

@[simp] theorem mir_bal :
    mir 50 = 50 := rfl

@[simp] theorem mir_link :
    mir 51 = 51 := rfl

@[simp] theorem mir_fbar :
    mir 52 = 52 := rfl

def bTag : Bool -> Nat
  | true => 60
  | false => 61

@[simp] theorem mir_tag (u : Bool) :
    mir (bTag u) = bTag u := by
  cases u <;> rfl

inductive Term where
  | atom (c : Nat)
  | dig (d : Nat)
  | blank
  | row (l : Term) (op : Nat) (r : Term)
  | bal (l r : Term)
  | jux (l r : Term)
  | ovl (l r : Term)
  | adh (host mark : Term) (up : Bool)
  | box (t : Term)
  | obox (t : Term)
  | lk (l r : Term)
  | frac (n d : Term)
deriving Repr, DecidableEq

open Term

def rho : Term -> Term
  | atom c => atom (mir c)
  | dig d => dig d
  | blank => blank
  | row l op r => row (rho r) (mir op) (rho l)
  | bal l r => bal (rho r) (rho l)
  | jux l r => jux (rho r) (rho l)
  | ovl l r => ovl (rho l) (rho r)
  | adh h m u => adh (rho h) (rho m) u
  | box t => box (rho t)
  | obox t => obox (rho t)
  | lk l r => lk (rho r) (rho l)
  | frac n d => frac (rho n) (rho d)

theorem rho_invol :
    forall t, rho (rho t) = t := by
  intro t
  induction t <;> simp [rho, mir_invol, *]

@[simp] theorem rho_blank_iff :
    forall t, rho t = blank <-> t = blank := by
  intro t
  cases t <;> simp [rho]

def isBlank : Term -> Bool
  | blank => true
  | _ => false

@[simp] theorem isBlank_rho :
    forall t, isBlank (rho t) = isBlank t := by
  intro t
  cases t <;> rfl

def wfb : Term -> Bool
  | atom _ => true
  | dig d => decide (1 <= d) && decide (d <= 10)
  | blank => false
  | row l _ r => wfb l && wfb r
  | bal l r =>
      (isBlank l || wfb l) &&
      (isBlank r || wfb r)
  | jux l r => wfb l && wfb r
  | ovl l r => wfb l && wfb r
  | adh h m _ => wfb h && wfb m
  | box t => isBlank t || wfb t
  | obox t => isBlank t || wfb t
  | lk l r => wfb l && wfb r
  | frac n d => wfb n && wfb d

def sideb (t : Term) : Bool :=
  isBlank t || wfb t

theorem wf5 (m : Term) (u : Bool) :
    wfb (adh blank m u) = false := by
  simp [wfb]

theorem clause_viii (op : Nat) (r : Term) :
    wfb (row blank op r) = false := by
  simp [wfb]

theorem wf_rho :
    forall t, wfb (rho t) = wfb t := by
  intro t
  induction t <;>
    simp [rho, wfb, isBlank_rho, *] <;>
    exact Bool.and_comm _ _

inductive Emis where
  | prim (c : Nat)
  | eblank
  | h2 (a b : Emis)
  | h3 (a b c : Emis)
  | v2 (a b : Emis)
  | v3 (a b c : Emis)
  | ov (a b : Emis)
  | encl (k : Nat) (a : Emis)
deriving Repr, DecidableEq

open Emis

def emit : Term -> Emis
  | atom c => prim c
  | dig d => prim (d + 100)
  | blank => eblank
  | row l op r => h3 (emit l) (prim op) (emit r)
  | bal l r => h3 (emit l) (prim 50) (emit r)
  | jux l r => h2 (emit l) (emit r)
  | ovl l r => ov (emit l) (emit r)
  | adh h m u =>
      v2 (emit h) (ov (prim (bTag u)) (emit m))
  | box t => encl 8 (emit t)
  | obox t => encl 9 (emit t)
  | lk l r => h3 (emit l) (prim 51) (emit r)
  | frac n d => v3 (emit n) (prim 52) (emit d)

def mirE : Emis -> Emis
  | prim c => prim (mir c)
  | eblank => eblank
  | h2 a b => h2 (mirE b) (mirE a)
  | h3 a b c => h3 (mirE c) (mirE b) (mirE a)
  | v2 a b => v2 (mirE a) (mirE b)
  | v3 a b c => v3 (mirE a) (mirE b) (mirE c)
  | ov a b => ov (mirE a) (mirE b)
  | encl k a => encl k (mirE a)

theorem mirror_equivariance :
    forall t, emit (rho t) = mirE (emit t) := by
  intro t
  induction t with
  | atom c => rfl
  | dig d => simp [rho, emit, mirE]
  | blank => rfl
  | row l op r ihl ihr =>
      simp [rho, emit, mirE, ihl, ihr]
  | bal l r ihl ihr =>
      simp [rho, emit, mirE, ihl, ihr]
  | jux l r ihl ihr =>
      simp [rho, emit, mirE, ihl, ihr]
  | ovl l r ihl ihr =>
      simp [rho, emit, mirE, ihl, ihr]
  | adh h m u ihh ihm =>
      simp [rho, emit, mirE, ihh, ihm]
  | box t ih =>
      simp [rho, emit, mirE, ih]
  | obox t ih =>
      simp [rho, emit, mirE, ih]
  | lk l r ihl ihr =>
      simp [rho, emit, mirE, ihl, ihr]
  | frac n d ihn ihd =>
      simp [rho, emit, mirE, ihn, ihd]

theorem mirE_invol :
    forall e, mirE (mirE e) = e := by
  intro e
  induction e <;> simp [mirE, mir_invol, *]

def samplePlate : Term :=
  bal (frac (dig 4) (dig 4)) (dig 1)

example : wfb samplePlate = true := by
  decide

example :
    emit (rho samplePlate) =
    mirE (emit samplePlate) := by
  decide

example :
    wfb (adh blank (dig 1) true) = false := by
  decide

end MirrorCalculus

Transport.lean

/- Conditional transport between a certified hierarchy and
   an omega-kept family. -/

namespace Transport

variable {Rec : Type}

structure Interface (Rec : Type) where
  Fib : Nat -> Rec -> Prop
  comp : Nat -> Rec -> Rec -> Prop

structure Atlas (I : Interface Rec) where
  pick : Nat -> Rec
  mem : forall n, I.Fib n (pick n)
  coh : forall n, I.comp n (pick n) (pick (n + 1))

structure ZenoLaws (Rec : Type) where
  Keep : Nat -> Rec -> Prop
  Coh : Nat -> Rec -> Rec -> Prop

structure Family (Rec : Type) where
  K : Nat -> Rec

def OmegaKeep
    (Z : ZenoLaws Rec)
    (F : Family Rec) : Prop :=
  (forall n, Z.Keep n (F.K n)) /\
  (forall n, Z.Coh n (F.K n) (F.K (n + 1)))

def transport
    {I : Interface Rec}
    (A : Atlas I) : Family Rec :=
  (A.pick)

def Dict
    (I : Interface Rec)
    (Z : ZenoLaws Rec) : Prop :=
  (forall n r, I.Fib n r <-> Z.Keep n r) /\
  (forall n a b, I.comp n a b <-> Z.Coh n a b)

theorem transport_keeps
    {I : Interface Rec}
    {Z : ZenoLaws Rec}
    (h : Dict I Z)
    (A : Atlas I) :
    OmegaKeep Z (transport A) :=
  (fun n =>
      (h.1 n (A.pick n)).mp (A.mem n),
   fun n =>
      (h.2 n (A.pick n) (A.pick (n + 1))).mp
        (A.coh n))

def atlasOf
    {I : Interface Rec}
    {Z : ZenoLaws Rec}
    (h : Dict I Z)
    (F : Family Rec)
    (hK : OmegaKeep Z F) :
    Atlas I where
  pick := F.K
  mem :=
    fun n =>
      (h.1 n (F.K n)).mpr (hK.1 n)
  coh :=
    fun n =>
      (h.2 n (F.K n) (F.K (n + 1))).mpr
        (hK.2 n)

theorem round_trip_family
    {I : Interface Rec}
    {Z : ZenoLaws Rec}
    (h : Dict I Z)
    (F : Family Rec)
    (hK : OmegaKeep Z F) :
    transport (atlasOf h F hK) = F :=
  rfl

theorem round_trip_pick
    {I : Interface Rec}
    {Z : ZenoLaws Rec}
    (h : Dict I Z)
    (A : Atlas I) :
    (atlasOf h
      (transport A)
      (transport_keeps h A)).pick = A.pick :=
  rfl

structure ZRec where
  addr : Nat
  count : Nat
  ok : Bool
deriving Repr, DecidableEq

def canonKeep
    (n : Nat)
    (r : ZRec) : Prop :=
  r.addr = n /\
  r.ok = true /\
  r.count = n + 1

def canonCoh
    (_ : Nat)
    (a b : ZRec) : Prop :=
  b.addr = a.addr + 1

def canonI : Interface ZRec :=
  (canonKeep, canonCoh)

def canonZ : ZenoLaws ZRec :=
  (canonKeep, canonCoh)

theorem canon_dict :
    Dict canonI canonZ :=
  (fun _ _ => Iff.rfl,
   fun _ _ _ => Iff.rfl)

theorem canonical_connection
    (A : Atlas canonI) :
    OmegaKeep canonZ (transport A) :=
  transport_keeps canon_dict A

end Transport

Provenance and Revision History

artifact or stratum	status	reason
first chiral linearization	historical	its atom pairs violated the later strict fixed-atom requirement
hand-laid founding plates	historical generated exhibit	the generative renderer replaced per-figure layout as the normative method
Blank-as-object-term Option B	superseded	the discipline of record carries no non-emission mark at any layer; withheld emission is a metalanguage judgment only (WF6)
first MJA surcharge law	refuted	codimension satisfies the modular formula instead
first MJA distribution	refuted	the supplied subspace counterexample invalidates it
first MJA Recoverability	refuted	the \(Q_\theta\)-pencil gives nonunique inputs with identical proposed output data
\(\mathsf{MJA}_2\)	current typed fragment	partial fusion, partial intersection, modular cost, genealogy, and partial conditioning
reading-group irreducibility claim	superseded	orbit spans decompose isotypically and need not be irreducible
right-face “page returns” caption	corrected	zero angular defect does not exclude every nontrivial flat fold
quartic root-stabilizer account	corrected	the resolvent action factors through \(S_4/V_4\cong S_3\)
prime-five quintic caption	corrected	the generic radical obstruction is \(A_5\)
R4	corrected	sign reversal detects odd multiplicity only
P1–P5	historical interpretation	the claimed derivations used an unsound or missing representation
P6	open representation condition	one implication is available only if the representation is supplied
F15–F19 native proof	superseded	the positivity step was assumed and symmetry inheritance was false
Witness–Blank theorem	refuted	a positioned off-axis exit record is well formed
class-wide independence	current relative theorem	the exact two-model calculation separates \(\AdmClass\) and its counter-inscription
zeta-specific Admission	explicitly sponsored law	its classical analytic price is RH
omega-family	explicit completion postulate	the sponsor forms the completed family without supplying computable components
numerical analytic budgets	withdrawn pending certification	the zero-count and outward-rounded tail work was not completed in the supplied record
Lean implementation fragment	scoped artifact	contains implementation blank and does not formalize the complete strict grammar
historical plate checker claims	execution-dependent	a final build record must report the actual commands and results

Bibliography

Imports are named in prose at their points of use; the entries below are their sources, in two parts: external literature, then the program's corpus and data. Published corpus records carry their full metadata, verified against the journal and repository records of record; program manuscripts of the corpus are identified by title and role pending their archival identifiers, which are affixed at deposit.

External bibliography

Program corpus and data

enumiv77

emmerson-buchanan-witness-fibres P. M. D. Emmerson and R. J. Buchanan, Riemann-Hypothesis Witness Fibres, Quantitative \(\Theta\)-Atlas \(\Xi\)-Certificates, Criterion Absorption, Nullity Matching, and Universal Selected Logical Nullity, Preprints.org (2026), DOI 10.20944/preprints202601.2410.v2. [Cited at the Sponsorship Declaration, the irresolvability–independence distinction, and the unification.]

emmerson-bellchsh P. Emmerson (Yaohushuason), Bell–CHSH Under Setting-Dependent Selection: Sharp Total-Variation Bounds and an Experimental Audit Protocol, Quantum Reports 8 (2026), no. 1, article 8, DOI 10.3390/quantum8010008.

emmerson-pv-ijqf P. Emmerson, Phenomenological Velocity and Bell–CHSH: Exceptional-Locus Semantics, Selection Simulations of \(-\cos\), and a Microcausal Realization, International Journal of Quantum Foundations 12 (2026), no. 2, 210–247.

emmerson-buchanan-theta P. Emmerson (Yaohushuason) and R. J. Buchanan, Alternating Slices of the \(A_{2k-1}\) Theta Series (dataset), Zenodo, version v2, 9 July 2026, DOI 10.5281/zenodo.21265022. Version v1 published as Sigma-Adic Numerations (P. Emmerson), 27 March 2024, DOI 10.5281/zenodo.10888345; all versions: DOI 10.5281/zenodo.10888344.

emmerson-witness-fibres P. Emmerson, Riemann-Hypothesis Witness Fibres: Quantitative \(\Theta\)-Atlas \(\Xi\)-Certificates, Criterion Absorption, Nullity Matching, and Universal Selected-Logical Nullity (program manuscript). Archival identifier to be affixed at deposit; cited here as a program manuscript of this corpus.

emmerson-selected-irresolvability P. Emmerson, Maximal A-Priori Selected Irresolvability for the Riemann Hypothesis (program manuscript). Archival identifier to be affixed at deposit; cited here as a program manuscript of this corpus.

emmerson-selection-jump P. Emmerson, The Selection Jump (program manuscript; the formation-rule study of the omega chapter). Archival identifier to be affixed at deposit; cited here as a program manuscript of this corpus.

emmerson-badxi P. Emmerson, BadXi and the witness exclusion computations (program manuscript and computational record).

emmerson-witnessed-semantics P. Emmerson, Witnessed semantics for presence-only verdicts (program manuscript).

emmerson-org-mechanics P. Emmerson, Organizational Mechanics of Effective Cardinality Transitions (program manuscript).

emmerson-dicone P. Emmerson, The di-cone geometry papers (program manuscripts; the stationarity and seam analyses of the folded chapters).

emmerson-companion-ix P. Emmerson, Companion IX (program manuscript of the companion series).

Artifact Availability

The renderer, checker, generated plates, Lean sources, exact-arithmetic checker, numerical scripts, notebook records, and build manifest belong to the publication bundle.

Language-model instruments were used under the author's direction for drafting, restructuring, work, software assistance and technical review; they are cited as sources. Every definition, adopted law, theorem statement, correction, interface and publication claim is the author's.

The mathematical source does not hard-code a compiler result, execution result, short hash, full artifact hash, or archive hash. The final distribution's README.md, execution logs, and build-manifest.json are authoritative for those facts after the archive is frozen.

This edition is deposited at doi:10.5281/zenodo.22002856.

References

1. Anthropic, Claude [large language model], Anthropic PBC, 2026. https://claude.ai. [Drafting, restructuring, and software instrument, used under the author's direction.] find
2. OpenAI, GPT-5.6 SOL [large language model], OpenAI, 2026. https://openai.com. [Drafting, restructuring and technical-review instrument, used under the author's direction.] find
3. L. V. Ahlfors, Complex Analysis, 3rd ed., McGraw–Hill, 1979. find
4. al-Khw\=arizm\=, The Algebra of Mohammed ben Musa, trans. F. Rosen, London, 1831. [The zero-free quadratic case-analysis the machine edition re-enacts.] find
5. Aristotle, Physics, in: The Complete Works, ed. J. Barnes, Princeton, 1984. [Book VI: Zeno.] find
6. D. M. Armstrong, Truth and Truthmakers, Cambridge University Press, 2004. find
7. V. I. Arnold, S. M. Gusein-Zade, and A. N. Varchenko, Singularities of Differentiable Maps I, Birkh\"auser, 1985. [Fold, cusp, swallowtail.] find
8. M. Asorey, A. Ibort, and G. Marmo, Global theory of quantum boundary conditions and topology change, Int. J. Mod. Phys. A 20 (2005), 1001–1025. find
9. E. Bombieri, The Riemann hypothesis, in The Millennium Prize Problems, Clay Mathematics Institute and American Mathematical Society, 2006, 107–124. find
10. G. S. Boolos, J. P. Burgess, and R. C. Jeffrey, Computability and Logic, 5th ed., Cambridge, 2007. find
11. R. Bott and L. W. Tu, Differential Forms in Algebraic Topology, Springer, 1982. [de Rham and Stokes imports.] find
12. W. Burnside, On groups of order \(p^\alpha q^\beta\), Proceedings of the London Mathematical Society, series 2, 1 (1904), 388–392. find
13. L. Carroll, Through the Looking-Glass, Macmillan, 1871. [The Nobody fallacy.] find
14. J. Cheeger, Spectral geometry of singular Riemannian spaces, J. Differential Geom. 18 (1983), 575–657. find
15. K. Claessen and J. Hughes, QuickCheck, Proc. ICFP 2000, ACM, 268–279. [Property-based testing methodology of the engine.] find
16. E. F. Codd, Extending the database relational model to capture more meaning, ACM Transactions on Database Systems 4 (1979), 397–434. find
17. J. B. Conrey and X.-J. Li, A note on some positivity conditions related to zeta and \(L\)-functions, International Mathematics Research Notices 2000, no. 18, 929–940. DOI 10.1155/S1073792800000489 arXiv:math/9812166
18. D. A. Cox, Galois Theory, 2nd ed., Wiley, 2012. find
19. H. S. M. Coxeter, Regular Polytopes, 3rd ed., Dover, 1973; A. D. Alexandrov, Convex Polyhedra, Springer, 2005. [Angular defect and the folded geometry.] find
20. R. C. T. da Costa, Quantum mechanics of a constrained particle, Phys. Rev. A 23 (1981), 1982–1987. find
21. H. Davenport and H. Heilbronn, On the zeros of certain Dirichlet series, Journal of the London Mathematical Society 11 (1936), 181–185. find
22. L. de Branges, Hilbert Spaces of Entire Functions, Prentice-Hall, 1968. find
23. L. de Branges, The convergence of Euler products, J. Funct. Anal. 107 (1992), 122–210. find
24. C.-J. de la Vall\'ee Poussin, Recherches analytiques sur la th\'eorie des nombres premiers, Ann. Soc. Sci. Bruxelles 20 (1896), 183–256. find
25. M. P. do Carmo, Differential Geometry of Curves and Surfaces, Prentice-Hall, 1976. find
26. R. Durrett, Probability: Theory and Examples, 5th ed., Cambridge University Press, 2019. find
27. H. M. Edwards, Riemann's Zeta Function, Academic Press, 1974. find
28. Euclid, The Thirteen Books of Euclid's Elements, trans. T. L. Heath, 2nd ed., Dover, 1956. [Book IX, Prop. 20: the plate of the unfactorables.] find
29. G. B. Folland, Real Analysis, 2nd ed., Wiley, 1999. find
30. P. B. Gilkey, Invariance Theory, the Heat Equation, and the Atiyah–Singer Index Theorem, 2nd ed., CRC Press, 1995. find
31. I. M. Gelfand, M. M. Kapranov, and A. V. Zelevinsky, Discriminants, Resultants, and Multidimensional Determinants, Birkh\"auser, 1994. find
32. K. G\"odel, \"Uber formal unentscheidbare S\"atze der Principia Mathematica und verwandter Systeme I, Monatsh. Math. Phys. 38 (1931), 173–198. find
33. J. P. Gram, Note sur les z\'eros de la fonction \(\zeta(s)\) de Riemann, Acta Math. 27 (1903), 289–304. find
34. J. Hadamard, Sur la distribution des z\'eros de la fonction \(\zeta(s)\), Bull. Soc. Math. France 24 (1896), 199–220. find
35. P. H\'ajek and P. Pudl\'ak, Metamathematics of First-Order Arithmetic, Springer, 1993. [\(\Sigma_1\)-completeness at the one-sided door.] find
36. H. Hamburger, \"Uber die Riemannsche Funktionalgleichung der \(\zeta\)-Funktion, Mathematische Zeitschrift 10 (1921), 240–254; 11 (1921), 224–245; 13 (1922), 283–311. find
37. G. H. Hardy, Sur les z\'eros de la fonction \(\zeta(s)\) de Riemann, C. R. Acad. Sci. Paris 158 (1914), 1012–1014. find
38. A. Hatcher, Algebraic Topology, Cambridge University Press, 2002. find
39. A. Heyting, Intuitionism: An Introduction, 3rd ed., North-Holland, 1971. find
40. Y. Hu, Y. Koren, and C. Volinsky, Collaborative filtering for implicit feedback datasets, in Proceedings of IEEE ICDM 2008, 263–272. find
41. H. Iwaniec and E. Kowalski, Analytic Number Theory, AMS Colloquium Publications 53, Providence, 2004. find
42. T. Jech, Set Theory, 3rd millennium ed., Springer, 2003. [The axiom of infinity as the incumbent omega-closure postulate.] find
43. L. H. Jeffery, The Local Scripts of Archaic Greece, rev. ed., Oxford, 1990. [Boustrophedon.] find
44. M. Kac, Can one hear the shape of a drum?, American Mathematical Monthly 73 (1966), 1–23. find
45. R. Kaplan, The Nothing That Is: A Natural History of Zero, Oxford, 2000. [The incumbency history of the banished numeral.] find
46. S. A. Kripke, Semantical analysis of intuitionistic logic I, in: Formal Systems and Recursive Functions, North-Holland, 1965, 92–130. find
47. P. Kuchment, Floquet Theory for Partial Differential Equations, Birkh\"auser, 1993. find
48. J. C. Lagarias, An elementary problem equivalent to the Riemann Hypothesis, Amer. Math. Monthly 109 (2002), 534–543. [The \(\Pi_1\) form of the one-sided door.] find
49. J. C. Lagarias, On a positivity property of the Riemann \(\xi\)-function, Acta Arithmetica 89 (1999), 217–234; Correction, Acta Arithmetica 116 (2005), 293–294. DOI 10.4064/aa-89-3-217-234
50. A. Hinkkanen, On functions of bounded type, Complex Variables, Theory and Application 34 (1997), 119–139. find
51. E. Goldštein and A. Grigutis, On a positivity property of the real part of the logarithmic derivative of the Riemann \(\xi\)-function, Journal of Mathematical Inequalities 18 (2024), no. 3, 829–845. find
52. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, CADE-28, LNCS 12699, Springer, 2021, 625–635; Lean FRO, Lean 4, version 4.9.0 (2024), github.com/leanprover/lean4. source
53. X.-J. Li, The positivity of a sequence of numbers and the Riemann Hypothesis, J. Number Theory 65 (1997), 325–333. find
54. L. Libkin, Incomplete data: what went wrong, and how to fix it, in Proceedings of ACM PODS 2014, 1–13. find
55. I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Oxford University Press, 1995. find
56. H. P. McKean and I. M. Singer, Curvature and the eigenvalues of the Laplacian, Journal of Differential Geometry 1 (1967), 43–69. find
57. F. Mertens, Ein Beitrag zur analytischen Zahlentheorie, J. reine angew. Math. 78 (1874), 46–62. find
58. H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I, Cambridge University Press, 2007. find
59. K. Mulligan, P. Simons, and B. Smith, Truth-makers, Philos. Phenomenol. Res. 44 (1984), 287–321. find
60. NIST, Digital Library of Mathematical Functions, dlmf.nist.gov. [Bessel and gamma evaluations.] find
61. A. M. Odlyzko, Tables of zeros of the Riemann zeta function, www.dtc.umn.edu/ odlyzko/zeta_tables/ (access date to be fixed at the final numerical run). find
62. D. J. Platt and T. S. Trudgian, The Riemann Hypothesis is true up to \(3\cdot10^{12}\), Bull. London Math. Soc. 53 (2021), 792–797, DOI 10.1112/blms.12460. [The verification height.] DOI 10.1112/blms.12460 arXiv:2004.09765
63. W3C, PROV-DM: The PROV Data Model, W3C Recommendation, 2013. find
64. M. Reed and B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness, Academic Press, 1975. find
65. R. Reiter, On closed world data bases, in H. Gallaire and J. Minker (eds.), Logic and Data Bases, Plenum, 1978, 55–76. find
66. B. Riemann, \"Uber die Anzahl der Primzahlen unter einer gegebenen Größ e, Monatsberichte der K\"oniglich Preuß ischen Akademie der Wissenschaften zu Berlin (1859), 671–680. source
67. J. J. Rotman, An Introduction to the Theory of Groups, 4th ed., Springer, 1995. [Jordan–H\"older.] find
68. W. Rudin, Principles of Mathematical Analysis, 3rd ed., McGraw-Hill, 1976. find
69. A. Selberg, Old and new conjectures and results about a class of Dirichlet series, Proc. Amalfi Conf. (1989), Salerno, 1992, 367–385. find
70. P. Selinger, Dagger compact closed categories and completely positive maps, ENTCS 170 (2007), 139–163. [The dagger terminology.] find
71. A. Speiser, Geometrisches zur Riemannschen Zetafunktion, Math. Ann. 110 (1935), 514–521. find
72. B. Sturmfels, Algorithms in Invariant Theory, 2nd ed., Springer, 2008. find
73. A. Tarski, The concept of truth in formalized languages, in: Logic, Semantics, Metamathematics, Clarendon, 1956, 152–278. find
74. W. P. Thurston, The Geometry and Topology of Three-Manifolds, ch. 13, Princeton lecture notes, 1980. [Orbifolds.] find
75. E. C. Titchmarsh, The Theory of the Riemann Zeta-Function, 2nd ed., revised by D. R. Heath-Brown, Oxford University Press, 1986. find
76. A. S. Troelstra and D. van Dalen, Constructivism in Mathematics I, North-Holland, 1988. find
77. T. S. Trudgian, An improved upper bound for the argument of the Riemann zeta-function on the critical line II, J. Number Theory 134 (2014), 280–292. [Source of the unit-interval count with explicit constants.] find
78. A. M. Turing, Some calculations of the Riemann zeta-function, Proc. London Math. Soc. (3) 3 (1953), 99–117. [The block-count certification method.] find
79. D. V. Vassilevich, Heat kernel expansion: user's manual, Physics Reports 388 (2003), 279–360. find
80. A. Weil, Sur les “formules explicites” de la th\'eorie des nombres premiers, Meddelanden fr n Lunds Universitets Matematiska Seminarium, Tome Suppl\'ementaire d\'edié à Marcel Riesz (1952), 252–265. find
81. A. Zettl, Sturm–Liouville Theory, American Mathematical Society, 2005. find