Invitation
Track the claim. Inspect the receipts. Bring an exact failure, and let the record change.
This instrument invites the reader to examine how a description becomes a determination. Navier-Stokes supplies the main case: public resolution claims, formal certificates, competing interpretations, and audiences deciding what those artifacts warrant. The question concerns the conditions carrying a verdict, including the conditions through which the verdict itself receives assessment.
The invitation applies to this paper. Name the assertion you challenge, the scope in which you read it, the evidence you supply, and the inference that evidence defeats. A successful challenge may retract a theorem, replace a bridge, narrow an application, or change the adopted registry. The response belongs in the record with its reason and its effect. Agreement carries the same obligation.
Consideration therefore has a double role. It may assess the claims below; when represented with its actual criterion, it also instantiates their account of scoped adjudication. That second role follows from the specified relation between a consideration, its inputs, and its disposition. It does not depend on the reader agreeing with the author, and it does not protect an erroneous assertion from correction.
Abstract and standing
This paper consolidates the Λ program around one operational premise: a determination carried by a description depends on what that description retains and on the rules used to assess it. The foundational issue begins with distinctions, admissibility, reference, and calibration. It continues through proof construction, translation, checking, and the decision to stop. Λ names this investigative relation across frames; this edition assigns it no metaphysical priority over the domains it describes.
The central theorem characterizes exact target recovery by constancy on observation fibres. Its one-sided counterpart states the precise obligation for a sufficient certificate. These results permit both obstruction and closure. Six Clay case studies display different quantifier arrangements around that obligation. Navier-Stokes receives an additional audit of forcing, the word singularity, existential proof, and the reversal of adjudicative burden. The π and e examples distinguish exact representational exclusion from approximation and show how a theorem can close an infinite class.
The packet contains 278 checked theorem
declarations, all freshly run for R4: 212 originating in R1, 36
in R2, 26 in R3, and four new conditional results on institutional
signals and observational non-identification. Five completed executions
reported zero errors and zero warnings. Exact
source-to-receipt correspondence was checked for every run, and no
reported theorem depends on sorryAx or
Lean.trustCompiler. Definitions, structures, and inductive
types support these theorems and are excluded from the theorem count.
Sources, complete printed statements, dependency reports, hashes, and
reproduction recipes accompany this edition. The count includes examples
and specializations; it does not count independent discoveries.
Empirical, cognitive, biological, and universal conveyance bridges
remain separately identified.
The mathematical claims certified here have their encoded hypotheses. The six case contracts expose, rather than assume, the further bridges needed to connect generic predicates to complete subject-specific formalizations. This paper assigns no Clay verdict to any resolution claimant. Lu Semita’s NS investigation retains OPEN at the unresolved application coordinates specified below. A later proof of a fixed NS statement could close that statement without erasing the scoped character of its proof.
Attribution
This successor edition draws on Lu Semita’s laboratory corpus, the newest Lambda Dictionary, Lambda Part III, and its supplement, the six TOE Arena papers, the subsequent NS bridge, and recovered Lean artifacts. Established mathematics remains attributed to its sources. Jenny Lorraine Nielsen’s TUFT work remains independent. The supplied NS paper prints the authors as “Jennifer Lorraine Nielsen and Lucis Semita”; this paper uses “the Nielsen-Semita claim” when identifying that artifact. Its presence supplies a known comparator and preserves provenance. It does not make that paper’s stronger NS conclusion a premise of the present instrument or imply its author’s endorsement of this edition.
The mathematical ingredients used centrally here are established results: factorization by constancy on fibres, well-defined transitions on equivalence classes, and finite pigeonhole counting. R4 makes these imports explicit at §§2, 1.4, and 1.5. The proposed contribution concerns their assembly into a scope-preserving, self-applying adjudication instrument and its applications; renaming an ingredient does not establish its novelty.
1. The foundation begins before the default
A registry does more than collect already settled facts. Its construction draws distinctions, selects marks, defines admissibility, names transformations, and establishes which comparisons count. A readout may then retain some relationships and omit others. Even a completely successful calculation takes place through those commitments.
The original handoff dictionary supplies twenty-five entries in dependency order. The following compact map retains their roles without creating another competing glossary. The complete supplied dictionary accompanies the packet unchanged; its R4 successor retains the accumulator, carried conditions, access and intervention, and persistence entries, and adds institutional recognition.
| Entries | Dependency and use here |
|---|---|
| Distinction, mark, criterion | A difference receives a representation and a condition of recognition. |
| Registry, admissible | The representation and the objects over which it ranges receive scope. |
| Transport, projection, recoverability | A map carries information; a target may or may not factor through it. |
| Collision, symmetry, fibre | Equal readouts may hide unequal target values; symmetry can supply the witness. |
| Residue, enlargement | What a representation does not carry receives an index; a successor can add resources. |
| Operator, spectrum, invariant | Declared operations yield relations whose preservation needs proof. |
| Calibration, ratio | Relations and absolute scales require different data. |
| Scope index, bridge, receipt | Transported claims retain their assumptions and verification records. |
| Stop, will, cost, holder | The record locates termination, unresolved selection, resources, and the situated registry. |
These entries do not establish a preferred ontology merely by receiving names. Their mathematical content lies in the maps, predicates, and hypotheses supplied in a particular use. For example, the Part III calibration results recover a family of values from gaps only up to an additive shift, or recover an affine calibration when enough distinct anchors have been supplied. The missing anchor belongs to the construction of a numerical description. It need not appear as a downstream computational error.
The same point applies to successful spectral description. Part II and Part III study the readout
Inversion preserves this readout. A collision has the two branches or ; the fibre reduces to a singleton at the corresponding fixed points. The readout carries a real relationship while omitting a distinction that phase recovery may require. “Residue” here names an indexed relation between what a representation carries and what a target requests. It does not mean that the representation has achieved nothing.
Five uses of residue
The dictionary separates residual selection, an infimum of representational costs, positional counts, unrecovered target sets, and directional translation loss. These objects have different types. An infimum need not attain a minimum; an unrecovered set need not come with a numerical norm; different permitted selections need not mean that every target remains undecidable.
This edition preserves those distinctions. Part III proves that enlarging a representation class cannot raise an infimum taken over the enlarged class, given the same cost function. It also supplies examples where enlargement strictly lowers that cost and where it does not. Those examples make successor discipline substantive: enlargement may help, but its label alone does not prove improvement.
The formalization employs Lean’s dependent type theory, with classical principles where reported by the axiom ledger. Some examples use Boolean classifications. This choice gives the present receipt a definite formal scope. It does not establish Boolean logic, the real continuum, or this dictionary as an absolute foundation for every possible description.
1.1 Conveyance already has a boundary
The present extension starts where a description becomes shareable. Within the adopted model, conveying an account requires distinctions through which a recipient can recover what the account distinguishes. Moving to an account of that account relocates the descriptive boundary. It does not, by that move alone, supply access to what the first account omitted.
This formulation makes no claim that an encounter outside every model cannot occur. Even if such an encounter occurred, conveying it through a description would again involve a representation and conditions of interpretation. The research question concerns fidelity through that conveyance. It does not demand an account of what cannot be conveyed before allowing finite work to proceed.
The kernel models source and target as different positions. One carrier can occupy both positions. Consequently self-reference need not collapse the distinction between the roles, and distinct roles need not imply different persons or objects. The role construction neither posits consciousness nor proves a particular account of individuality.
The stronger proposition that every meaningful reference requires this construction, or a functionally equivalent discrimination, remains a declared conveyance bridge. Its proposed challenge coordinate asks for meaningful reference whose content remains recoverable without such discrimination. Classifying an exhibit against that condition would itself require an account and a criterion. That reflexive feature makes the bridge available for self-examination; it supplies no exemption from the task of defending the bridge. “No exception has been constructed in this record” gives a stopping status, not a theorem that no exception exists.
The formal consequence starts after a message map has been supplied. If two admitted states yield the same message but require different target values, no interpreter using only that message can recover the target on both states. Applying a metadescription to the same message cannot split the collision. Additional observation or an enlarged representation may change the situation. These statements locate the limitation in the specified map rather than in an asserted inability of every possible model.
theorem conveyance_collision_blocks_target {X Y Z : Type*}
(message : X → Y) (target : X → Z) {a b : X}
(same : message a = message b) (split : target a ≠ target b) :
¬ ∃ interpret : Y → Z, ∀ x, interpret (message x) = target x
This connects the new foundation directly to §2. The recovery theorem governs the description of an axiom, a calibration, a proof receipt, and an adjudicator’s decision as readily as it governs a downstream numerical readout. Λ need not wait for a conspicuous singularity to enter the account.
1.2 The constitutive pharmakon: make the protocol explicit
Tail call optimization supplies an inspectable comparison. Proper tail recursion permits unbounded chains of tail calls without retaining a fresh continuation for every call. An implementation may reuse a frame; the language-level requirement concerns continuation-space behavior, not a compulsory physical frame layout. Explicit arguments, accumulators, external logs, and other retained data can survive. R6RS, proper tail recursion.
In the selected projection that retains only one identical frame marker, depth has no decoder. Threading the depth as data restores that query. A current argument can already encode depth, so the loss cannot be attributed to frame reuse without inspecting the retained state. Constant continuation space also does not imply constant total memory or termination.
Here constitutive pharmakon names the paired consequences of a declared operational requirement: continue using a carried representation while omitting some construction history. The same omission reduces what must be carried and removes the omitted distinctions from that readout. For a target that needs one of those distinctions, the loss follows from the specified projection. The effect needs no claim that every terminating reflexive model must overwrite its history.
Role polarity makes another descriptive act available. A rule requiring that act to be completed before every current act could produce indefinite regress. The requirement belongs to the protocol; the existence of source and target positions alone does not impose it. Similarly, a protocol may stop expansion, retain a finite trace, or keep selected state. These operations have distinct consequences that the registry should preserve.
The successor kernel includes two useful countermodels to the initial
proposed dichotomy. A structurally recursive countdown terminates for
each natural-number input and returns a trace of that input’s length; no
uniform trace bound covers all inputs. Conversely, a process on the
single state Unit, with a never-satisfied halt predicate,
can continue indefinitely. These checked examples replace the proposed
implication from termination to bounded state. They leave the
substantive issue intact: which distinctions must survive the chosen
compression for the next assessment?
1.3 The accumulator carries two tasks
An accumulator can support recognition, by retaining enough to detect a return, and continuation, by retaining a result so the next step need not reconstruct its derivation. These requests differ. The kernel gives a two-field example: a cached numerical result does not determine whether a return occurred; a return flag does not determine the cached result. Carrying both answers both selected queries.
This gives the accumulator the same double character as the compression it accompanies. What permits continued work can carry earlier commitments beyond the occasion that justified them. Reopening every commitment at every step consumes resources; treating every carried commitment as newly established hides its basis. The storage choice therefore has a declared query class, a cost, and a reopening policy. No universal minimum size settles that choice.
The discipline concerns marked, warranted reuse:
Carry the result with the scope and basis under which it received support. Preserve them during unchanged reuse. When a translation, new observation, or choice changes them, record the transition and its warrant. Keep missing provenance visible as missing.
A bare “forced” or “declared” label cannot carry all of this. A conclusion may follow by derivation from premises whose adoption was declared. The origin of the premises and the warrant for the conclusion occupy different coordinates. An inherited entry may have unknown origin. That uncertainty concerns our record of its origin; it does not supply a third truth value or retrospectively establish a voluntary choice.
The Lean Entry stores holder, scope, basis, claim, and
origin. Reuse requires each of those fields to remain
unchanged. The separate Warrant type carries a proof of the
scoped predicate. Lean verifies both same-scope reuse and transport
across an explicitly supplied bridge. It also verifies that a
derived tag alone cannot prove an arbitrary proposition.
These distinctions prevent the marking convention from becoming another
label that conceals its construction.
theorem warranted_translation_needs_a_bridge {S T C D : Type*}
{holds : S → C → Prop} {nextHolds : T → D → Prop}
(scopeMap : S → T) (claimMap : C → D)
(bridge : ∀ s c, holds s c → nextHolds (scopeMap s) (claimMap c))
(w : Warrant S C holds) : nextHolds (scopeMap w.scope) (claimMap w.claim)
Recognition does not itself provide revision. The instrument therefore records a successor when a carried conclusion gets reopened, disputed, narrowed, or retracted. The prior entry remains available; the newer entry identifies what changed and who made the disposition. This affords an actual revision path without requiring that every old derivation run again during every ordinary use.
1.4 A theorem for an accumulator that keeps working
Standard mathematical ingredient. The condition below makes a transition well-defined on classes of histories: equality of retained states must be preserved by appending the same event. This is the right-congruence principle used in the Myhill-Nerode construction. The present statement does not assert the full finite-index or minimal-automaton theorem. See the University of Pennsylvania notes, Regular Languages; the Myhill-Nerode Approach, Definition 6.3 and Proposition 6.3. Right-invariant equivalence and induced transitions.
A snapshot can contain enough information for a query yet fail to contain enough for the next update. Let range over finite event histories, let denote the retained state, and append an event as . An update using only the retained state must satisfy
Online accumulator theorem. Such an update exists precisely when histories identified by the accumulator remain identified after the same appended event:
The existence direction uses a default state off the image and classical selection of a representative history. It establishes existence, not an executable or efficient update for an arbitrary encoding. Given an actual update satisfying the displayed equation, induction proves that running it from maintains the history encoding for every finite history. If a decoder recovers the requested target from , it consequently recovers that target after every run.
theorem online_target_recovery {E S Z : Type*}
(encode : List E → S) (update : S → E → S) (decode : S → Z)
(target : List E → Z)
(commutes : ∀ h e, update (encode h) e = encode (h ++ [e]))
(exactness : ∀ h, decode (encode h) = target h) :
∀ h, decode (run update (encode []) h) = target h
The counterexample fits in one bit. Retain only whether at least two
events have occurred. This bit answers the current query exactly, but
both zero events and one event read false. Appending one
event must yield false in the first case and
true in the second. No deterministic update from that bit
and the appended event can satisfy both requirements. The current
query’s smallest representation therefore need not support future use.
Retaining the capped count 0, 1, or 2 would repair this example.
This theorem gives the proposed compendium a temporal obligation. It must preserve the distinctions needed by the next permitted operation, not merely display a faithful label for the current snapshot. A rule that changes what future queries may ask declares a successor scope.
1.5 Bounded cost means a stated unit and query
The kernel applies the standard pigeonhole principle, in its finite
injectivity/cardinality form. The library ingredient is
Fintype.card_le_of_injective; exact recovery makes the
encoding injective. Mathlib
cardinality documentation. The resulting bound states: exact
recovery of every element of a finite class requires at least as many
distinguishable stored states as the class contains. Two applications
state the cost without confusing a register with a bit:
| Query, with all listed possibilities admitted | Necessary distinguishable states |
|---|---|
| Which subset of named stops has occurred? | At least |
| What exact depth from 0 through occurred? | At least |
For a fixed binary encoding, these state counts give the corresponding bit requirements: at least bits for arbitrary subsets and at least bits for the stated depth range. The directly checked contracts use cardinalities. Exact unbounded natural-number depth cannot be recovered from a single fixed finite state space. An arbitrary-precision natural-number accumulator can represent depth, while its bit storage grows.
A designated “ever encountered this stop?” flag has only two target values. Recording arbitrary named distinctions, their full textual scopes, or complete order can demand much more. “Constant size per distinction” must consequently specify whether identifiers, contents, receipts, and the referenced store contribute to the cost. The manuscript’s earlier phrase “minimum record of declared stops” becomes a design question under a selected query class, rather than a universal sufficient memory prescription.
1.6 A shared compendium preserves holders and translations
The proposed compendium allows each holder to keep a registry. Its shared element consists of inspectable records and translation contracts. Participants can compare a derivation, carry a result, or disagree about a basis while retaining the differences in what they adopted. The convention governing participation has its own holder, version, scope, and revision record.
For a translation , the contract means that holds exactly when holds. When a second translation preserves that same middle predicate to a third one, composition preserves the end-to-end target. The theorem requires no identity of the carriers and no agreement about every property of their elements.
theorem translation_composes {X Y Z : Type*} (f : X → Y) (g : Y → Z)
(p : X → Prop) (q : Y → Prop) (r : Z → Prop)
(first : Preserves f p q) (second : Preserves g q r) :
Preserves (g ∘ f) p r
A checked Boolean counterexample shows why two individually successful translations can fail to establish the desired end-to-end correspondence: they may certify different predicates at their common station. Thus the label “both translations checked” omits a material condition. The shared registry carries the middle predicate, its interpretation, and any change to it.
“Babel” names the author’s structural reading of translation failure at scale. It functions here as an invitation to preserve compatible meanings across locally workable vocabularies, without claiming a historical or linguistic theorem about the story. “Shared TCO” likewise names a design analogy: participants continue from local state while preserving selected provenance in a common format. A shared depth record exists only to the extent the chosen schema and its actual updates retain the requested depth information.
Origins can be compared under declared criteria: consistency, resource cost, predictive performance, suitability for a target, or another supplied relation. The compendium does not acquire a criterion-independent ranking by registering those comparisons. Lean checks a small example in which two rankings order the same alternatives oppositely. A disagreement about ranking therefore opens the criterion coordinate rather than forcing conversion to one holder’s origin.
Choosing a stance toward a carried frame also differs from having chosen every condition that produced it. Accountability can begin with the present adoption, revision, or acknowledgment of an inherited condition. This distinction preserves the proposed agency without treating involuntary experience as a deliberate premise selection.
1.7 Human analogies and their application boundaries
The trauma comparison motivates a precise question: can a carried response remain active while its origin or present suitability remains difficult to inspect and revise? Clinical descriptions report that reminders can evoke distress and physical reactions. Prolonged exposure involves gradual engagement with trauma memories and safe situations a person has avoided. These descriptions support inquiry into persistence and revision; they do not identify PTSD with a software accumulator or characterize treatment as deleting a stored axiom. NIMH, PTSD, VA, prolonged exposure.
The account of distinction and conveyance also remains distinct from a solution to the hard problem of consciousness. Chalmers formulates that problem around why processing accompanies experience. The present construction examines conditions under which an explanation can be represented and shared. Connecting that constraint to experience would require another argument. The kernel supplies no theorem that tail call optimization produces individuality, or that individuated agents must implement it. Chalmers, Facing Up to the Problem of Consciousness.
These examples stay within the corpus as declared application bridges. They can motivate an investigation without borrowing the proof status of the formal contracts. The same boundary applies to claims about trusting an AI system. A hidden basis can obstruct a particular audit, while a defined behavior can still receive evidence under a specified test. Trust needs the task, warrant, exposure, and revision conditions recorded; the mere presence or absence of a black box does not decide every trust question.
1.8 Carried conditions exceed the declared registry
R2 located accountable reuse in marked entries. The present extension distinguishes those entries from the conditions a holder carries. A condition may influence an act before it is represented in an inspectable registry, and its present carrier need not have selected its origin. The two-mode stop rule has a narrower jurisdiction: it records how an adjudicative act stops under a declared protocol. It does not classify the causal origin of everything that makes that act possible.
Three profiles make the difference visible. They are relative to a holder, a time, and an available access route. They need not partition all things into exclusive kinds.
| Profile | What is being carried | What acknowledgment can establish |
|---|---|---|
| Encoded | A condition inherited or established without the present holder’s declaration | The holder may later describe it through an observation route; declaration alone need not change it. |
| Installed | An acquired condition that can continue operating without present examination | Its effects or provenance may become accessible; revision requires an appropriate intervention. |
| Declared | A commitment explicitly represented with scope and basis | Its recorded adoption can be reopened; any corresponding change in implementation has a separate obligation. |
An encoded condition can acquire a declared description while remaining inherited. An installed response can be recognized while continuing to operate. A declared commitment can change while its implementation remains unchanged. The record therefore carries origin, access, and intervention separately. Its origin field concerns the history of a condition; its stop-mode field concerns the present adjudication. Neither field substitutes for the other.
The new Lean carrier makes that separation literal:
Carried C R has a condition of type C, a
record of type R, and an origin tag. remark
changes only the record. Theorems show that a single remark and any
finite list of such remarks preserve the condition, and that recording
an inherited condition does not rewrite its origin. These are contracts
of the declared operation. They do not assert that all real acts of
speaking or recording lack causal effects. Where an act also changes the
condition, the model must include that intervention.
theorem repeated_remarking_preserves_condition {C R : Type*}
(fs : List (R → R)) (s : Carried C R) :
(fs.foldl (fun st f => remark f st) s).condition = s.condition
The extension also exhibits two collisions. Identical records can accompany different underlying conditions; identical content can accompany different origins. A decoder from that record alone cannot recover the omitted coordinate. Adding an observation of the condition can repair the first target. Whether an actual observation supplies that information, and with what error and cost, remains an application obligation.
The genetic example motivates the profile without defining its mathematical scope. Genetic testing can reveal variations in genes, chromosomes, or proteins; absence of an original choice does not imply permanent absence of access. Gene regulation also involves processes affecting how DNA instructions are used. Thus the word executes expresses a proposed functional comparison, not an assertion that a genome is a consciously declared program or a complete determinant of a person’s response. MedlinePlus, genetic testing, NHGRI, epigenomics.
The useful distinction is not reopenable by declaration alone. It neither certifies an intervention nor declares the condition unamendable. A condition’s history does not become a voluntary selection merely because a holder can now name it. Accountability can register present acknowledgment without assigning that holder authorship of the entire causal history.
1.9 Access and intervention have different proof obligations
Let an observation map determine what a holder can recover, and let an action family determine which state transitions are available. Their relation requires an argument. The kernel supplies countermodels in both directions: exact observation can coexist with only identity actions, while a state-changing action can coexist with an observation that hides the state. These examples establish logical independence in the specified model. They do not measure a person’s awareness or control.
A revision path is a finite sequence of available actions. If every permitted action preserves a predicate, every such path preserves it. A target state violating that predicate is unreachable by those paths. The restriction belongs to the action family: enlarging that family may remove the obstruction. “Not reachable by these actions” must retain the word these.
theorem invariant_obstructs_revision_path {X A : Type*}
(act : A → X → X) (p : X → Prop)
(preserved : ∀ a x, p x → p (act a x)) (x y : X)
(initial : p x) (excluded : ¬ p y) :
¬ ∃ as, applyActions act x as = y
This gives reopening a practical test. The record can distinguish a proposed revision, an attempted intervention, an observed change, and a warranted assertion that the target has changed. Naming an intervention does not establish that it occurred or worked. Naming awareness does not supply an intervention. A missing path remains missing, rather than being attributed to an unexplained act of will.
“Attention is a narrow band on carried state” remains the author’s cognitive bridge: current accessible description can occupy only part of what influences continuation. The source/target primitives do not by themselves prove an infinite cognitive recursion, a numerical attention capacity, or a universal need to overwrite history. The TCO analogy identifies a question about retained information and viable continuation; its actual cognitive realization requires its own evidence. The distinction between record and condition strengthens that bridge’s discipline without converting it into a neuroscience theorem.
1.10 Persistence is recovery under conditions through time
The persistence burden applies to the living holder, the shared compendium, the receipt, and every successor carrier. Moving to a more durable carrier changes that burden; it does not supply permanence merely through the label durable. This edition adopts a conservation practice: specify which distinction remains recoverable, by whom, through which carrier and interpretation, for what horizon, and under which maintenance and transfer conditions.
For admitted histories or source states , let denote the retained representation at time , its decoder, and the selected target. Exact recovery at a station means
Through E D q N requires this relation at each
natural-number station from 0 through
.
A shorter horizon follows from a longer one. No longer horizon follows
just from shortening. The decoder may vary with the station: continuity
concerns the selected meaning, not identity of every representation or
interpretation procedure.
A transfer from a carrier S to a carrier T
preserves the target if the new representation follows that route and
the new decoder agrees with the old decoder on the transferred admitted
states. Together with exact old recovery, those premises imply exact
successor recovery. Neither the full state nor the original medium needs
to be recovered. The obligation names the target actually promised.
theorem target_preserving_transfer_gives_successor_recovery {X S T Z : Type*}
(old : X → S) (next : X → T) (transfer : S → T)
(oldDecode : S → Z) (nextDecode : T → Z) (q : X → Z)
(route : ∀ x, next x = transfer (old x))
(faithful : ∀ x, nextDecode (transfer (old x)) = oldDecode (old x))
(exactness : ∀ x, oldDecode (old x) = q x) :
∀ x, nextDecode (next x) = q x
Induction then supplies conditional continuity. Exact recovery at the first station, plus a preservation implication at every successor, proves recovery at every modeled station. The accompanying maintenance theorem retains the premise that the maintenance condition holds at every step. A universal maintenance premise is substantive evidence still owed in a physical application; it is not generated by induction. The time-indexed formulation uses a common carrier type, which can encode multiple formats; the one-step transfer theorem permits different carrier types directly.
The countermodel marks the other boundary. For any finite
,
one Boolean representation preserves its input through station
and then collapses both inputs to false. It agrees with an
ideal forever-preserving representation throughout the observed prefix.
At
,
no replacement decoder from the collapsed value can recover both
original values. Thus even allowing a new interpretation cannot repair
this particular lost distinction without another information source.
The preceding no-replacement-decoder sentence is supported by the
following companion theorem. Here Recovers observe target
means ∃ decode, ∀ x, decode (observe x) = target x. The
identity function names the target, while the decoder is existentially
quantified and then excluded.
theorem loss_after_horizon_has_no_replacement_decoder (N : Nat) :
¬ Recovers (expiresAfter N (N+1)) id
The next theorem separately states the finite-prefix counterexample with its displayed identity decoder family. Together they establish the two claims made in this paragraph.
theorem no_finite_prefix_certificate_of_permanence (N : Nat) :
¬ (∀ encode : Nat → Bool → Bool,
Through encode (fun _ => id) id N →
∀ t, ExactAt encode (fun _ => id) id t)
This proves the failure of an unrestricted inference from finite successful recovery to all future recovery. It does not prove that a specified physical carrier must fail, that mathematical permanence is inconsistent, or that induction cannot establish a universal conditional result. The kernel also includes the forever-preserving ideal model. Finite observations alone distinguish neither that continuation nor the later-loss continuation. A narrower admitted class, with a proved transition law, may settle the future claim.
That is how the user’s persistence point enters the corpus rigorously: observed durability is a supported history, not an unconditional permanence receipt. Treating all practical carriers as requiring a declared continuity path is a design commitment. A universal empirical assertion that every medium eventually fails would require a physical model and assumptions beyond the present kernel.
A receipt documenting a transfer is itself carried information. The next reader needs access to its statement, interpretation, source identity, and warrant. Copying its badge while losing those coordinates creates another projection problem. The compendium can distribute or relocate the dependency, but its own records inherit the same recovery obligations. A checksum can establish agreement with a retained reference under its assumptions; it cannot alone reconstruct unavailable content or restore a lost interpretation.
1.11 Budgets constrain preservation; they do not supply priority
For a finite-lived holder, allocation occurs over time: retaining content, keeping it accessible, maintaining its fidelity, and transferring it can draw on different resources. This remains a resource question for nonliving carriers and for chains of successors. A budget need not have a conscious budgeter. The holder may encounter the effects of allocations they did not choose.
The formal budget contract states its units. With one unit per retained commitment, a feasible retained set has cardinality at most . If the required set has more than elements, at least one required commitment is omitted. The statement does not choose which commitment to omit, and it does not assert that every physical resource can be measured by counting entries.
theorem budget_forces_an_omitted_commitment {I : Type*} [DecidableEq I]
(required retained : Finset I) (B : Nat)
(feasible : retained.card ≤ B) (overBudget : B < required.card) :
∃ i ∈ required, i ∉ retained
A two-choice example then exhibits different retained sets satisfying the same budget. Feasibility alone does not rank them. A priority relation, utility, risk criterion, or preservation target must be supplied. The resulting selection belongs in the declared record when it is an adjudicative choice. Where its origin is unknown or inherited, the record should say so instead of inventing deliberation.
Part III already supplies the weighted natural-number contract
LambdaIII.finite_budget_forces_tradeoff_n: a budget below
the sum of required costs cannot fund every requirement. R3’s unit-cost
set version locates an omitted named commitment. Storage, maintenance,
interpretation, and transfer costs still need units, a horizon, and an
aggregation rule. Neither contract selects an optimized resource policy
or gives a quantitative model of biological memory. Additional
constraints can produce a unique feasible selection, so the two-choice
example does not assert that every budget always leaves a choice.
A finite carrier can still preserve a selected target exactly: one Boolean coordinate can be retained while an arbitrary companion coordinate is omitted. Consequently a finite budget is not a universal certificate of target failure. The essential question remains whether the distinctions promised to the user survive the particular allocation. If arbitrary exact recovery of a finite class is promised, its distinguishable states supply a necessary capacity bound.
The accumulator therefore carries three connected obligations: continuation, recognition, and persistence. The third asks how long and through which conditions the first two remain available. Its storage size is a declared tradeoff under those obligations. Marking provides an address for reconsideration, while observation and intervention determine what that address can actually reach.
For the instrument, an assessment may now carry a condition profile: its reported origin, access route, available intervention, carrier, target, horizon, maintenance or transfer route, and budget or priority. Unspecified values remain explicit. Unchanged reuse preserves these fields along with the original scope and basis; a change becomes a successor. These are inspectable reports, not automatically executed interventions or independent certifications of the user’s text.
1.12 How this changes the Navier-Stokes instrument
The new layer makes visible what must persist through the existing comparison. Carrying “Lean checked” retains a result while potentially omitting its statement, assumptions, environment, and application bridge. Carrying “singularity” retains a word while potentially omitting the predicate it named. Carrying “still open” retains a status while potentially omitting which search, obstruction, or unproved bridge supports that status. Each instance invokes the same requirement to preserve the selected target-relevant information through reuse.
The full six-case survey remains below. Their tail predicates do not establish a common physical or ontological cause merely by sharing a logical form. They give named sites at which to inspect whether a class-level theorem closes the required family, whether an actual counterexample defeats it, or whether the retained description lacks a warranted bridge. This foundation explains why the scope and receipt matter before a favorite claimant enters the comparison.
The reader’s challenge has the same opportunity. An inspectable response can supply new information, expose a failed update, change a translation, or demonstrate closure. Its registration instantiates the declared recording protocol; its mathematical force comes from its content and warrant. It may require changing this paper. The accumulator then preserves both the earlier claim and the reason for revision, allowing continued work without silently turning the revision into an ahistorical default.
2. What can a description determine?
Standard mathematical ingredient. Exact recovery is the elementary criterion for a target function to factor through the observation map: it is constant on observation fibres. Equivalently, it descends to the quotient by equal observations. Theorem 1 in Cornell’s Universal Mapping Properties states this quotient property. Extension from the image to the entire readout type uses the nonemptiness/default-value assumptions printed in the Lean statements. Universal mapping property of a quotient.
Let carry the admitted states, the retained descriptions, and the target values. Write
An exact decoder would satisfy for every admitted . The requirement concerns the target, not recovery of the whole state.
Recovery theorem. If is nonempty, an exact decoder exists if and only if takes the same value on every fibre of :
The forward proof substitutes equal inputs into . The reverse proof chooses the common target value on each nonempty fibre and a default value off the image. The choice step appears in the axiom receipt. This theorem asserts existence of a decoder; it does not assert its computability or its cost.
theorem recovery_iff_fibre_constancy {X Y Z : Type*} [Nonempty Z]
(read : X → Y) (target : X → Z) :
Recoverable read target ↔
∀ x y, read x = read y → target x = target y
Collision theorem. One exhibited pair with equal readout and unequal target defeats exact decoding from that readout. Pure postprocessing preserves the equality of the inputs. Adding new target-relevant information can remove the obstruction; appending the target itself gives an immediate, deliberately explicit example of the price of such enrichment.
For a sufficient certificate, the obligation differs. If a certificate fires on descriptions in , soundness means
A sufficient certificate may fire on only part of a target class. It need not classify the whole domain. The packet verifies this one-sided contract separately. This distinction corrects an overly broad invariant-sufficiency statement in the earlier NS paper: a non-invariant sufficient condition can prove an invariant conclusion. An exact classifier must preserve the target’s invariance.
Dimensional enlargement and the continuum
The later Arena NS bridge supplies the relevant methodological correction. Its finite geometric exemplar contains an actual mixed fibre: reflection can preserve metric data while reversing orientation. One extra selector can resolve the orientation. This provides a concrete obstruction and a concrete enlargement.
For NS, an analogous pair of admissible PDE data with the same specified readout and opposite regularity outcomes has not been supplied by this edition. That application coordinate remains OPEN. No number of generic collision lemmas substitutes for that witness or for another valid PDE obstruction.
A continuum without a terminal grain leaves arbitrarily fine descriptions available. This feature alone neither establishes nor defeats a target decoder. An all-scale estimate could show the target independent of distinctions a finite measurement drops. Conversely, omission of a distinction does not prove that distinction irrelevant. The recovery theorem states precisely which bridge would settle the question.
3. Freeze the target and expose a change
Use the registry
where gives admissible objects, the language and its meanings, the quantifiers, the target, the admitted witnesses, and the checking relation. This declaration records the game being assessed. It does not gain evidentiary privilege from who declares it.
Suppose acceptance under the current registry means . A later condition has two possible effects. If already follows throughout the admitted class, then has the same extension. Otherwise an exhibited state accepted by and excluded by proves that the strengthened predicate differs. The packet proves both statements.
This test applies equally to a claimant and a critic. A claimant may silently change a domain or witness requirement; a critic may impose a stronger burden after inspecting a candidate. Neither receives immunity by calling the change an interpretation. Where entailment remains unsettled, the record says OPEN rather than asserting either equivalence or a proved change.
Publication, prize eligibility, mathematical derivation, and a reader’s confidence have different predicates. Their relationships require bridges. A refusal supplies no mathematical counterexample merely by occurring; an award supplies no missing inference merely by being granted. This edition uses the official Clay text as a specified target, not as an authority that renders an inference valid.
4. Navier-Stokes: the live comparison
4.1 The source statements
For the whole-space and periodic alternatives respectively, A and B ask for global smooth unforced solutions for every admitted datum. C and D ask for admitted data and forcing with no qualifying global solution. The zero force belongs to the permitted forcing class. The official conditions use smooth real-variable fields and include spatial decay or periodicity requirements; a numerical cutoff does not replace those conditions. Fefferman’s problem statement.
On 8 September 2026, OpenAI announced a forced NS construction and explicitly claimed both Fefferman alternatives C (whole space) and D (periodic space). Its linked paper’s Theorem 1.1 asserts smooth compactly supported forcing, a solution starting from rest, and finite-time velocity blowup. The announcement also makes a separate unforced Euler claim. Its public repository supplies formalization sources. This edition identifies these as imported claims; it does not rerun that repository or adjudicate its full analytic argument. Announcement, paper, repository.
The supplied Nielsen-Semita PDF states a first-draft date in September 2025 and a revision in May 2026. It claims real-time blowup with zero forcing, through its own lemma sequence, while also discussing a complex-time continuation. These constitute claims to examine. The printed dates establish what the supplied artifact reports; this edition makes no independently archived day-level priority finding.
| Coordinate | Nielsen-Semita artifact | OpenAI artifact | Present Λ instrument |
|---|---|---|---|
| Public posture | Claims a resolution | Claims a resolution | Offers scoped adjudication results |
| Relevant NS construction | Claimed unforced real-time blowup | Claimed forced real-time blowup from rest | No PDE witness constructed here |
| Logical proof form | Existential breakdown claim with supporting lemmas | Existential breakdown claim with supporting estimates | Contracts governing evidence and inference |
| Required comparison | The exact theorem, hypotheses, and bridges | The exact theorem, hypotheses, and bridges | The same obligation for every assertion here |
| Disposition in this edition | Merits not adjudicated | Merits not adjudicated | Checked encoded theorems; application coordinates retained |
This comparison establishes a common proof-form question without preloading the verdict. It also preserves a difference that the sources themselves declare. Permitting forcing does not require the force to be nonzero. Consequently, the two breakdown claims need not contradict one another simply because one specializes to zero forcing.
4.1a Public record, institutional recognition, and lineage
Dated import: 13 September 2026. Clay’s 11 September statement describes the problem as having “apparently been settled” and says evaluation and allocation of credit remain ongoing. This is a favorable institutional statement, not a completed prize decision. Its content must be recorded alongside its possible role in shaping reception. Clay announcement.
Clay’s published rules require qualifying publication, at least two years afterward, and general mathematical acceptance. A qualifying outlet ordinarily has a refereeing process; §6 also provides for approved exceptions. Section 7 separates community examination from subsequent detailed institutional consideration. These rules and the announcement do not establish that a waiting requirement was waived. The mere absence of a conventional journal publication does not settle whether an approved outlet exception exists. Clay rules, §§4, 6, 7.
The announced construction has a mathematical lineage. OpenAI’s paper cites Córdoba and Martínez-Zoroa’s forced Euler work and Córdoba, Martínez-Zoroa, and Zheng’s hypodissipative NS work in its introduction. Their actual technical contributions should be compared through the constructions and estimates; a lineage citation alone establishes neither appropriation nor independence. OpenAI paper, introduction and references.
Buckmaster’s public statement credits the Córdoba-Martínez-Zoroa program, describes his collaboration with Alpöge, and reports disputed publication and authorship proposals during contacts with OpenAI. It also expressly leaves unknown whether their data were used. These are his attributed account and stated limits, not findings of this instrument. Buckmaster statement. OpenAI recognizes their priority on forced Euler, distinguishes its own unforced Euler claim, and in its 10 September update says its investigation excluded influence from Buckmaster’s preceding two months of Codex prompts, including through training. This is OpenAI’s attributed response; it does not resolve every conduct allegation. OpenAI, concurrent-work update.
| Coordinate | What this edition records | What remains to establish |
|---|---|---|
| Mathematical validity | Published claims, exact cited statements, and offered formalizations | Full analytic and encoding audit of each NS claimant |
| Prize eligibility | Published criteria and dated institutional statement | Applicable outlet determination, elapsed interval, and formal decision |
| Public recognition | Clay’s favorable statement and its date | The selection criteria for such recognition |
| Lineage and priority | Named antecedents, attributed chronology, and disagreements | Detailed dependency and priority assessment |
| Reception and influence | The statement is available as an institutional signal | Its actual effect on attention, confidence, or consensus |
4.1b Recognition can participate in the evaluation it describes
The concern about equal treatment concerns the process through which claims receive attention as well as its final verdict. Public recognition can become an input to later assessments: readers may redistribute attention, confidence, or their willingness to reopen a claim. An institution may subsequently observe a community whose reception it has helped shape. This is a proposed feedback mechanism, not a measured causal finding about Clay.
The distinction matters even if the formal waiting interval remains intact. The rule’s temporal gate and an earlier public signal are different operations. A record of the latter should identify its issuer, date, declared basis, and the decision in which it is being reused. Comparing treatment requires a defined class of other attempts and evidence of how each was handled. This edition does not assert that every other attempt was ignored or that misconduct follows from recognition.
The formal companion supplies a deliberately small model. Let a declared decision accept when a natural-number evidence score plus a signal weight meets a threshold. If the evidence alone lies below the threshold but the enriched score reaches it, the signal changes that model’s decision:
theorem signal_crosses_declared_threshold (evidence signal threshold : Nat)
(below : evidence < threshold) (enough : threshold ≤ evidence + signal) :
¬ thresholdAccepts evidence 0 threshold ∧
thresholdAccepts evidence signal threshold
This does not estimate any person’s response or assign a numerical influence to Clay. It makes the required behavioral premise visible. An assessment that actually disregards the signal need not change at all.
A second pair of results shows why acceptance observed after a signal cannot by itself establish influence. The identity response accepts only when the Boolean signal is present. The constant-true response accepts with or without it. Both yield the same observed acceptance with the signal present, but only one depends on it.
theorem observed_acceptance_does_not_identify_dependence :
∃ f g : Bool → Bool,
observedAcceptance f = observedAcceptance g ∧
SignalDependent f ∧ ¬ SignalDependent g
theorem no_dependence_decoder_from_observed_acceptance :
¬ ∃ decode : Bool → Bool, ∀ response : Bool → Bool,
decode (observedAcceptance response) =
decide (response true ≠ response false)
The last theorem quantifies over all Boolean response functions. No decoder using just the one observed acceptance value can recover dependence across that admitted family. Additional counterfactual assumptions, interventions, or observations may distinguish the models; the theorem does not deny those routes.
The fourth result keeps public recognition, eligibility, and claim
truth as separate Boolean coordinates and exhibits equal recognition
with different values of the other two. This proves independence within
that unconstrained record type. It supplies no empirical verdict about
any institution. All four full statements and their freshly checked
proofs appear in LambdaInstitutionalSignals.lean and the
theorem catalogue.
This is self-application in a concrete form: this instrument’s own favorable descriptions, proof counts, citations, and presentation can influence its readers. Their actual effect remains a question for evidence. A receipt certifies its stated execution; it does not certify the independence of the audience that later cites it.
4.2 The forcing relation, fully exposed
For an abstract carrier of data , forces , and a global-solution predicate , define
If zero force is admitted, . The reverse implication fails as a general logical rule. The packet supplies a finite countermodel with equivalent to : global success at zero force coexists with failure at an admitted nonzero force. This model proves a quantifier relation, not an NS behavior.
theorem unforced_failure_is_admitted_forced_failure {D F : Type*}
(admD : D → Prop) (admF : F → Prop) (global : D → F → Prop)
(zeroForce : F) (zeroAdmitted : admF zeroForce)
(failure : ¬ NSGlobal admD global zeroForce) :
NSForcedFailure admD admF global
theorem forced_failure_can_coexist_with_unforced_global :
∃ global : Unit → Bool → Prop,
NSGlobal (fun _ => True) global false ∧
NSForcedFailure (fun _ => True) (fun _ => True) global
Thus A/C and B/D do not form primitive pairs of logical negations as written. For a fixed datum, fixed force convention, and an admitted maximal-solution theory, a separate regularity/breakdown dichotomy may be available. Its use must retain those reductions.
4.3 Which “singularity”?
The existing semantic-deflation module already proves the core requested in this discussion. Let an old use exclude a trait , while an extended use admits an actual instance with :
Then
does not imply
throughout its domain, and no single predicate can be extensionally
equivalent to both. A nonempty two-state example gives both uses the
public label singularity. Lean checks both scoped branches and
checks their failure of extensional identification. The exact
declarations include SemanticDeflation.deflation,
constraint_loss, no_shared_definition, and
two_checked_branches_one_label.
This theorem does not say that no object can satisfy two different predicates. In the supplied example the old class lies inside the extended class, so overlap occurs. What fails concerns identification of the whole definitions while retaining the incompatible constraints. The corresponding application burden asks which trait the first source excludes, which actual instance the second admits, and where the disputed argument treats the uses as interchangeable.
Part III’s additional force-scope example distinguishes “requires zero forcing” from “allows forcing.” Lean checks the metadata distinction. The allowed solution classes can nevertheless overlap at zero. This edition therefore does not promote those metadata flags into a proof of incompatible mathematical notions of singularity.
In the contemporary NS comparison, the relevant analytic usage concerns failure of regularity or unboundedness under stated solution conditions. It does not require an object outside all mathematical description. Shared spelling cannot settle the predicate; the theorem and its hypotheses must do that work.
4.4 The residual-force construction
For a sufficiently differentiable pair , rearranging the PDE suggests a force
Defining this residual establishes an equation by construction. Its compliance with the required force class remains a further proposition. The packet isolates the exact logical relationship:
theorem residual_admissibility_is_the_obligation {X F : Type*}
(residual : X → F) (admitted : F → Prop) (x : X) :
(∃ f, f = residual x ∧ admitted f) ↔ admitted (residual x)
The OpenAI paper expressly attempts to establish smoothness and localization through estimates and correction. Merely calling its residual a tautology does not address those obligations. Equally, naming a residual supplies none of them for free. Apply this separation to every claimant: identify the equation made true by definition, then inspect the independent admissibility and blowup claims. Construction and estimates in the linked paper.
4.5 Two reversals that must retain separate names
An existential witness legitimately defeats a universal assertion on the same domain. A proof of existence can carry that witness obligation without a closed-form formula suitable for direct numerical substitution. This permission applies equally to both resolution claimants and to this paper.
An adjudicative reversal has a different form: “You have not supplied a certified refutation; therefore the claim follows.” That rule fails even for a sound certification relation. Take a relation that certifies nothing and a false target. Soundness holds vacuously, no refutation receives certification, and the target remains false.
theorem no_refutation_is_not_a_general_proof :
¬ (∀ (certified : Prop → Prop) (P : Prop),
(∀ Q, certified Q → Q) → ¬ certified (¬ P) → P)
The packet also identifies a premise that can license the inference: completeness at the negation. If every actual falsity of would yield a certified , absence of such a certificate rules out in the classical logic used by this theorem.
theorem completeness_licenses_reversal
(certified : Prop → Prop) (P : Prop)
(completeAtNegation : (¬ P) → certified (¬ P))
(noRefutation : ¬ certified (¬ P)) : P
The exact standard therefore travels in both directions. Neither “produce a counterexample or concede” nor “produce a closed-form configuration or concede” has unrestricted force. The first needs a closure/completeness bridge; the second needs an adopted witness restriction. The Equal Standard seed already distinguishes an existential construction from an accusation that the OpenAI paper literally uses absence of refutation as its proof. This successor preserves that distinction. Structural parity does not itself demonstrate that either paper committed the invalid inference.
4.6 What equality of standard actually proves
If a judgment factors through specified comparison fields, equal values in those fields force equal judgments. Different judgments require a distinction in the declared inputs or failure of the factorization premise. This is the exact theorem behind procedural parity.
It does not require the judge to ignore a relevant force condition, an invalid estimate, or a missing bridge. It requires that the distinction doing the work appear in the record and receive the same application to each candidate. A coarse comparison of public claim form cannot substitute for the richer evidence needed to judge validity.
The repaired Part III lemma L82 fixes its comparison projection to
the three fields named in its statement. The submitted version
accidentally quantified over an arbitrary projection while attempting to
infer equality from only those three fields. The successor removes that
mismatch. Its coded estimatesClose field remains reported
metadata; setting the bit to true does not verify an
estimate.
5. Six cases, six precise tail contracts
“Tail” in this instrument describes a quantified obligation extending beyond a chosen station of examination. It does not mean a probability-theoretic tail event unless a separate application establishes that meaning. It does not mean that a finite proof cannot discharge the obligation.
The recovered Arena supplies six extensive case papers. Its embedded Lean artifact contains five generic declarations, not six complete subject-specific formalizations. This successor adds the contracts below and includes all six original case texts in the evidence packet. The statements use abstract carriers where the corresponding full mathematical objects have not been formalized here.
The common control theorem constructs two predicates agreeing on every test below any fixed , one true at every stage and one failing at . It proves a limitation of unrestricted finite testing. Applying it to a restricted scientific or mathematical class requires showing that the competing extensions actually belong to that class.
theorem finite_window_has_opposite_extensions (N : ℕ) :
∃ good bad : ℕ → Prop,
Window N good ∧ Window N bad ∧ AllStages good ∧ ¬ AllStages bad
An all-stage theorem closes the infinite test family at once. The
same file proves universal_proof_closes_all_windows,
all_windows_iff_all_stages, and
actual_failure_refutes_tail. The green-socks example
therefore has both legitimate exits: a quantified proof and an actual
counterexample. The mere possibility of an unexamined sock supplies
neither.
5.1 Navier-Stokes: lifespan, bounds, and a fixed endpoint
For a fixed datum and an explicitly selected local-solution setup, let mean that the required smooth solution exists through the th bounded time window. The regularity contract reads . For a selected endpoint and scalar size observable, the blowup contract reads
Here before must carry the endpoint and the applicable
time restrictions; size must name the actual norm or
observable. Establishing equivalence to a particular PDE continuation
criterion remains an explicit bridge.
theorem ns_regularity_requires_each_window {D : Type*}
(window : D → ℕ → Prop) (d : D) :
NSRegular window d ↔ ∀ N, Window N (window d)
theorem ns_uniform_bound_excludes_encoded_blowup {D Time : Type*}
(before : D → Time → Prop) (size : D → Time → ℝ) (d : D)
(bound : ∃ K, ∀ t, before d t → size d t ≤ K) :
¬ NSBlowup before size d
The second theorem provides positive closure: one uniform bound over the declared pre-endpoint domain contradicts the encoded blowup property. A bounded simulation does not supply that universal bound automatically. A valid analytic theorem could supply it. Conversely, a genuine blowup construction could close the existential direction.
The earlier T1 orbit argument receives an exact repair here.
invariant_exact_classifier transfers invariance through a
biconditional. sufficient_condition_need_not_be_invariant
supplies a finite countermodel to the stronger claim that every
sufficient condition must be invariant. This preserves the distinction
the later BE1 bridge already requires.
Open coordinate. Exhibit a target-relevant mixed fibre for a named NS observation class, prove a sound one-sided exclusion, or provide an all-scale closure on the fixed PDE target. The existence of arbitrarily finer scales does not itself perform any of those tasks.
5.2 Riemann: one counterexample and a universal zero condition
The direct target asks that every nontrivial zeta zero lie on the
critical line. The Lean carrier Zero and predicates
nontrivial and onLine retain that quantifier
form. Bombieri’s
statement.
theorem rh_counterexample_duality {Zero : Type*} (nontrivial onLine : Zero → Prop) :
¬ RHForm nontrivial onLine ↔ ∃ z, nontrivial z ∧ ¬ onLine z
To use a natural-number test stream, provide an equivalence between that stream’s all-stage property and the actual zero statement. The formal theorem leaves this bridge visible:
theorem rh_tail_transport {Zero : Type*} (nontrivial onLine : Zero → Prop)
(test : ℕ → Prop) (bridge : RHForm nontrivial onLine ↔ AllStages test)
(closure : ∀ n, test n) : RHForm nontrivial onLine
A verified off-line zero would refute the universal target. Passing finitely many checks is weaker than the universal target unless a theorem proves that those checks suffice. A countable reformulation may organize the burden without shortening it. Its syntactic quantifiers alone do not prove a strict arithmetical-hierarchy lower bound, undecidability, or independence.
The earlier RH paper’s control against the Prime Number Theorem matters: an unindexed principle that declares every infinite prime-related obligation unclosable would also attack existing class-level theorems. This edition retains the control and keeps the actual RH verdict open.
Open coordinate. Supply the chosen formal zeta carrier and the exact equivalence for any test coding, then prove the target or exhibit its counterexample. Generic stream countermodels establish no actual off-line zeta zero.
5.3 Yang-Mills: existence, positivity, and uniformity
The case has two coupled obligations: construct an admitted
nontrivial quantum theory for the required gauge groups, and prove a
positive mass gap for that theory. The packet’s YMForm
keeps theory validity separate from UniformGap; a gap
requires one positive lower bound shared by all admitted excited states.
Jaffe-Witten’s
statement.
theorem uniform_gap_implies_pointwise_positive {State : Type*}
(excited : State → Prop) (energy : State → ℝ)
(h : UniformGap excited energy) : ∀ s, excited s → 0 < energy s
theorem pointwise_positive_need_not_have_uniform_gap :
(∀ x : {r : ℝ // 0 < r}, 0 < x.val) ∧
¬ UniformGap (fun _ : {r : ℝ // 0 < r} => True) (fun x => x.val)
The countermodel uses the positive real numbers as states and their values as energies. Every state has positive energy, but any proposed positive lower bound fails at half its value. The missing uniform quantifier therefore has an actual mathematical witness.
theorem common_gap_survives_order_limit {State : Type*}
(excited : State → Prop) (energy : State → ℝ) (approx : ℕ → State → ℝ)
(δ : ℝ) (positive : 0 < δ)
(bounds : ∀ n s, excited s → δ ≤ approx n s)
(passToLimit : ∀ s, (∀ n, δ ≤ approx n s) → δ ≤ energy s) :
UniformGap excited energy
The limit theorem explicitly asks for a passage-to-the-limit premise. That premise would need support from the actual topology, construction, and convergence arguments in a Yang-Mills application. A scale-dependent lattice gap does not become a continuum mass gap by retaining the same name.
Open coordinate. Formalize the admissible continuum theory and prove the common bound together with its limiting bridge. This edition does not infer impossibility of that construction from the presence of infinitely many scales.
5.4 Hodge: a cycle witness and an all-cycle exclusion
The target concerns rational Hodge classes on smooth projective
complex varieties and representation by rational linear combinations of
algebraic cycle classes. HodgeForm quantifies over admitted
instances and asks for a representing cycle. The cycle carrier can
encode a finite rational combination; the representation predicate must
include the exact class equality. Deligne’s
statement.
theorem hodge_actual_cycle_closes_instance {Instance Cycle : Type*}
(represents : Cycle → Instance → Prop) (i : Instance) (c : Cycle)
(certificate : represents c i) : ∃ w, represents w i
theorem hodge_nonmembership_requires_all_cycles {Instance Cycle : Type*}
(represents : Cycle → Instance → Prop) (i : Instance) :
(¬ ∃ c, represents c i) ↔ ∀ c, ¬ represents c i
A finite search without a witness does not prove nonmembership over an unrestricted enumeration. The packet constructs a witness outside any supplied finite set. A sound separating invariant can nevertheless prove nonmembership throughout the class:
theorem hodge_separating_invariant_closes_nonmembership {Instance Cycle : Type*}
(represents : Cycle → Instance → Prop) (invariant : Instance → Prop)
(sound : ∀ c i, represents c i → invariant i) {i : Instance}
(separates : ¬ invariant i) : ¬ ∃ c, represents c i
This gives the proper reading of the filter discussion in T4. Necessary conditions passed by every member of a locus cannot separate members inside that locus by those values alone. A stronger invariant, an exact cycle, or a theorem covering a stratum may settle the relevant target. The phrase “finite witness” includes its exact mathematical certification, not just a picture or an approximate class comparison.
Open coordinate. Supply the host geometry and cycle-class map. If an effective enumeration or reduction to a smaller field is invoked, provide that bridge too. The additional Hodge traversal documents cited in T4 were not recovered in this bounded consolidation; their claims remain cited predecessor claims, not newly checked geometry.
5.5 P versus NP: a candidate contains another universal burden
A candidate combines a machine with a polynomial clock;
correct c x means that the bounded computation answers
input
correctly for the chosen complete problem. The candidate’s mere finite
description does not certify that universal property. A proof of
correctness and its bound can certify it. Cook’s
formulation.
theorem pnp_quantifier_duality {Candidate Input : Type*}
(correct : Candidate → Input → Prop) :
¬ PolyCandidateForm correct ↔ ∀ c, ∃ x, ¬ correct c x
theorem pnp_candidate_with_all_input_proof_closes {Candidate Input : Type*}
(correct : Candidate → Input → Prop) (c : Candidate)
(allInputs : ∀ x, correct c x) : PolyCandidateForm correct
theorem bounded_tests_do_not_prove_candidate (N : ℕ) :
∃ correct : Unit → ℕ → Prop,
(∀ n, n < N → correct () n) ∧ ¬ PolyCandidateForm correct
The contrast concerns tests versus a theorem over all inputs. The packet does not claim that either answer to P versus NP lacks a possible finite proof. It also does not promote a displayed formula into proof that no equivalent simpler formula can exist. Such a hierarchy claim requires additional work.
The earlier T5 paper itself rejects assuming an unindexed Λ obstruction as a shortcut to . Within the polynomial comparator class, asserting that SAT has irreducible construction cost already asserts the difficult separation. Naming that residue cannot supply the missing proof. The present case preserves that self-correction.
Open coordinate. Formalize the machine/clock/SAT bridge and prove a globally correct polynomial candidate or a failure for every such candidate. Finite testing remains a bounded record, with the possibility of structural closure kept open.
5.6 Birch-Swinnerton-Dyer: two quantities and the bridges between them
For an elliptic curve, the rank clause compares algebraic rank with the analytic order at one. The refined formula also contains arithmetic and analytic factors. This edition isolates rank comparison, exact order, and factor recovery as different targets. Wiles’s statement.
theorem bsd_matching_bounds_close_rank (rank lower upper : ℕ)
(hl : lower ≤ rank) (hu : rank ≤ upper) (meet : lower = upper) :
rank = lower
theorem bsd_matching_certificates_close_instance (alg an lower upper : ℕ)
(hl : lower ≤ alg) (hu : alg ≤ upper) (meet : lower = upper)
(analytic : an = lower) : alg = an
These are affirmative stopping theorems: lower and upper rank certificates that meet determine the rank. Relating that value to a certified analytic order closes the encoded instance. The fact that another search station could be attempted does not invalidate such closure.
For coefficients
of the appropriate expansion, ExactOrder a r requires every
earlier coefficient to vanish and the coefficient at
to be nonzero. The packet proves uniqueness of this order and constructs
a case showing that a nonzero coefficient alone does not establish
it.
theorem exact_order_unique (a : ℕ → ℝ) {r s : ℕ}
(hr : ExactOrder a r) (hs : ExactOrder a s) : r = s
The product example captures a separate loss of information. Pairs and share their product but differ in the first factor. Product recovery needs an anchor if the separate factor matters.
theorem product_readout_loses_factor :
¬ Recoverable (fun p : ℝ × ℝ => p.1 * p.2) Prod.fst
theorem anchored_product_recovers_factor (a b c : ℝ) (ha : a ≠ 0)
(h : a * b = a * c) : b = c
The example motivates careful treatment of regulator and Tate-Shafarevich factors; it does not formalize those objects or establish their independence in a particular elliptic-curve family. The earlier T6 claims about general descent termination and exact analytic decidability require their own number-theoretic hypotheses. They are not consequences of the elementary sandwich and product lemmas.
Open coordinate. Provide the exact rank, analytic-order, finiteness, and leading-term bridges needed for the selected BSD clause. These contracts locate the obligations without asserting a resolution or an impossibility theorem.
The common shape and its limit
| Case | Global obligation retained | What can legitimately close it |
|---|---|---|
| NS | Continuation through every required time window, or an actual finite-time breakdown construction | A continuation estimate, a valid construction, or an equivalent all-scale theorem |
| RH | Every nontrivial zero, or an equivalent complete test family | A class theorem or a certified counterexample |
| Yang-Mills | Theory existence and one gap bound uniform over admitted excitations | A constructed theory with the required uniform and limiting estimates |
| Hodge | Every admitted class has a representing algebraic cycle | Exact cycle certificates, a class theorem, or a separating counterexample |
| P vs NP | One candidate correct for every input, or failure for every candidate | A global algorithm proof or a general separation proof |
| BSD | Rank/order agreement and any additional selected refined clauses | Matching exact certificates and the required arithmetic-analytic bridges |
All six admit the tail-contract lens. Their different carriers and bridges retain mathematical content. This common representation does not prove that all six share a single unsolvability mechanism. The Λ research claim invites investigation of these indexed residues and of what survives translation between descriptions. It does not replace the missing bridges by a universal name.
6. π and e: residue with genuine closure
The constants play a substantive role. A restricted representation class may exclude an exact value while arbitrarily accurate approximations remain available. A richer mathematical description can establish the exclusion for the whole restricted class. The relation among those facts gives a precise example of frame-indexed residue.
The packet directly imports and checks Mathlib’s irrationality result for π, then proves that π lies outside the rational image and differs from every finite integer-base fraction. This reaches the representation itself, not just a description of the proof’s shape. Mathlib’s π theorem and analytic proof outline.
theorem pi_no_finite_base_fraction (a : ℤ) (b n : ℕ) :
Real.pi ≠ (a : ℝ) / (b : ℝ) ^ n
For , the packet proves that every finite factorial-series partial sum falls strictly below . One positive next term, together with the established exponential bound, proves the strict inequality for every finite truncation. Mathlib exponential source.
theorem e_exceeds_every_finite_factorial_sum (n : ℕ) :
(∑ i ∈ Finset.range n, (1 : ℝ) / i.factorial) < Real.exp 1
The stronger classical transcendence results for π and e exclude every nonzero rational polynomial root. This packet verifies the closure contract conditional on transcendence, including the e specialization. It does not contain a new complete Lean proof of the Hermite-Lindemann theorems. The inspected Mathlib environment supplies an analytic component of Lindemann-Weierstrass; the attempted full theorem identifiers were unavailable. That boundary appears in the receipt ledger rather than becoming a hidden axiom. Mathlib’s analytic component.
theorem e_algebraic_class_closure_contract (h : Transcendental ℚ (Real.exp 1)) :
∀ p : Polynomial ℚ, p ≠ 0 → Polynomial.aeval (Real.exp 1) p ≠ 0
Enlarging the coefficient field to all reals immediately gives the polynomial for any real . Lean checks that this polynomial is nonzero and vanishes at . The rational-polynomial exclusion survives on its original coefficient class; the enlarged class contains a new exact representation. The transition changes the admitted resources and makes the price visible.
“Outside” therefore refers to resources excluded by the compared representation class. It need not mean outside mathematics, outside every axiom system, or a metaphysically privileged observer. The symbol π already gives a finite exact description in a suitable language. Transcendence limits algebraic representation over the stated field; it does not imply indescribability.
Nonzero residue need not have a positive numerical floor
For every real and every , a rational number can lie strictly between and . The packet verifies this approximation property. Thus an irrational number can differ from every rational number while the infimum of approximation error equals zero. Exact non-attainment and a uniform positive lower bound have different quantifiers.
The distinction also corrects an unnormalized polynomial-residual reading: arbitrarily small nonzero rational constants already make arbitrarily small. A positive lower bound needs a constrained or normalized comparator class and an appropriate cost. An exact exclusion indicator can remain nonzero while a metric approximation cost tends to zero. Λ must carry the comparator and cost index if the statement is to preserve its meaning.
7. The reader’s consideration as an instance of the proof
The instrument represents an assessment with a claim, a scope, evidence, a rule, a verdict, and a receipt that the rule applied to those inputs yields the recorded verdict. These fields let the consideration itself enter the same analysis as any other mathematical description.
theorem consideration_has_an_applied_rule {C S E : Type*}
(a : Assessment C S E) :
∃ rule : S → E → Status, rule a.scope a.evidence = a.verdict
theorem challenge_is_an_instance {C S E : Type*}
(a : Assessment C S E) (rejects : a.verdict = Status.rejected) :
a.rule a.scope a.evidence = Status.rejected
The second theorem is the requested self-application. A recorded rejection has the same structural obligations as another recorded judgment. Its role follows from the assessment relation; it need not be staged as a demonstration for the author’s benefit.
The formalization also proves that shared evidence can receive different verdicts under different declared rules. Equal evidence does not determine a verdict without the rule. Conversely, equal rules, equal scopes, and equal evidence force the same recorded status. This gives a concrete coordinate at which to inspect a disagreement.
An application bridge remains explicit: a human or machine consideration must be represented faithfully enough by these fields for the theorem to describe it. Merely reading a page supplies no automatic proof that this encoding captures every feature of thought. A critic may challenge that bridge. Once that challenge has an inspectable criterion and disposition, it too can receive a scoped record. This recursive availability provides accountability; it does not prove termination of every debate.
Falsification that can change the work
A receipt that a rule produced “accepted” does not certify the rule’s soundness. The packet constructs an assessment of a false proposition with an always-accepting rule and a valid execution receipt. This is an intentional countermodel. It exposes the difference between checking an operation and proving that operation warrants its target.
theorem receipt_does_not_certify_rule_soundness :
∃ a : Assessment Prop Unit Unit,
a.claim = False ∧ a.verdict = Status.accepted
Someone can decline to accept a criticism. That choice does not make a sound counterargument mathematically disappear. This instrument records the refusal, its stated criterion, and the resulting dispute. A decision to strengthen the registry receives a successor entry rather than rewriting the predecessor result. The author retains responsibility for the choice and for its explanation.
An exact criticism can affect this edition in several ways:
| Receipt supplied | Consequence under the stated protocol |
|---|---|
| A failure to check the delivered source in the reported environment | Reopen the build claim; reproduce and repair or retract it |
| A countermodel to a displayed implication under its actual hypotheses | Retract or correct that implication |
| A premise used in prose but absent from the cited theorem | Narrow the prose or prove the missing bridge |
| A demonstrated target-changing interpretation | Record the changed registry and reassess there |
| A theorem that closes a named observation family | Mark that coordinate closed within its scope |
| An objection to the assessment encoding | Examine and, if warranted, revise the encoding bridge |
| A bare possibility or a disagreement without an inspectable coordinate | Preserve the comment; leave its mathematical disposition OPEN |
The last row supplies no immunity from criticism. It preserves information while distinguishing a registered objection from a demonstrated refutation. A more informative successor can later replace the provisional status.
Infinite registry, finite records
Every finite textual comment fits into a record. Appending a record preserves earlier records and increases the history length by one. Lean checks those properties. They give an unbounded extensible registry: no fixed maximum number of entries appears in the datatype.
They do not give an oracle that understands every comment, decides
its truth, or anticipates every future distinction. The
open status makes that limitation part of the interface.
Raw text remains available even when its interpretation has not been
settled. The supplied feedback schema asks for the exact claim, scope,
reason, actor, parent record, and desired change.
The two stop modes in the packet form an adopted taxonomy. An effective stop records a completed test; a declared stop records an actor. Exhaustiveness follows for this datatype. It does not prove that every possible process in the world must enter one of its constructors. A theorem checked at an effective stop retains its mathematical scope; the choice of what to formalize and the fidelity of its translation remain separately inspectable.
8. What the Lean receipts carry
All 278 theorem declarations were freshly checked
for R4 in five executions of the public Lean web interface, project
MathlibDemo / “Latest Mathlib,” reporting Lean
4.34.0-rc2. Each final capture contains every expected theorem
report and an R4 end marker, with zero reported errors and warnings. The
encoded-source URL in each capture decodes to the exact delivered source
bytes. VERIFICATION_SUMMARY.json records the run time,
source hash, report count, and receipt path. Historical receipts remain
dated historical records; none is relabeled as a fresh run.
| Origin of theorem declarations | New in that edition | R4 executions covering them |
|---|---|---|
| R1 | 212 | PartIII (89), Companion (123) |
| R2 | 36 | Constitutive |
| R3 | 26 | CarriedState |
| R4 | 4 | InstitutionalSignals |
| Total | 278 | Five fresh executions |
R2 contained three captures: two originating in R1 and one new in R2. R3 added a fourth. R4 now supplies a fresh execution for every theorem while preserving that origin history. This separates the edition carrying a receipt from the edition in which the theorem entered the packet.
The permitted transitive axiom reports contain only the standard
dependencies actually printed: propext,
Classical.choice, and Quot.sound, or no
axioms. The counts by dependency set appear in
VERIFICATION_SUMMARY.json. A theorem with no reported
axioms still inhabits Lean’s underlying type theory and definitions; “no
reported axioms” does not mean “without a formal framework.”
#print axioms helps identify admitted proof
dependencies. A sorryAx dependency would indicate an
unfinished proof; compiler-trust mechanisms have a distinct trust scope.
The final sources used neither in their theorem reports. These checks
follow Lean’s documented distinction between proof artifacts and the
trusted components used to validate them. Lean:
validating proofs.
The web project did not expose a complete immutable package manifest through the observed interface. The reproduction files therefore distinguish the captured execution from a future fresh run against a supplied Mathlib checkout. This is a successful browser verification record, not a claim that a clean local hermetic build was executed. The toolchain version alone does not pin every imported dependency.
Certification parity
The same evidentiary question applies to every Lean-backed claim: which proposition checked, from which assumptions, and how does that proposition connect to the public claim? A certificate does not recover a forgotten basis simply by carrying the label “verified.” Part III makes that information-loss statement explicit.
The 278 theorem declarations include elementary logical examples, substantive algebraic results, and conditional case contracts. A larger count does not turn a conditional contract into a solution of its host problem. It increases the inspectable surface only when its statements and dependencies remain visible. That standard applies to OpenAI’s artifact, the earlier corpus, and this consolidation alike.
Human and machine contributions remain complementary in this packet. Mechanized checking tests formal derivations. Human and AI-assisted work still selects meanings, identifies targets, proposes bridges, locates errors, and judges whether the encoding addresses the intended problem. The artifact demonstrates that division of labor. It supplies no quantitative theorem about employment, intelligence, or the universal superiority of one kind of agent.
9. Conclusion: bring the coordinate
This instrument offers a determinate body of scoped results and an open invitation to revise their applications. The recovery theorem says exactly when retained information can carry an exact target. Its collision and one-sided variants say what defeats a decoder and what can support a certificate. The six cases make their remaining quantifiers visible. The π and e examples preserve both irreducible exact exclusion in a restricted representation class and genuine mathematical closure.
The NS moment gives these questions public force. A reader who grants credibility to formal verification can now inspect the same kind of evidence for the adjudication claims themselves. Doing so does not require choosing a favorite resolution claimant. It requires tracking what each receipt supports.
Inspect this paper by its own rule. If an inference fails, identify it. If a translation loses a required distinction, exhibit it. If a theorem closes a class the record leaves open, bring it. If the scope must change, state the change. Each response can sharpen the record, including a response that requires retracting something printed here.
The constitutive extension makes the continuity of this work inspectable: a carried result retains its scope and warrant, an online update preserves its declared encoding, and a successor records what changes. The shared compendium can retain distinct holders while requiring compatible predicates along a translation path. R3 further separates a carried condition from its record, access from intervention, and a successful preservation history from a guarantee of permanence. Continued recoverability has a target, horizon, route, and resource burden, including for this paper and its receipts.
The invitation makes no claim to hand down an absolute standpoint. It asks the reader to participate in an accountable determination and to preserve the conditions that make that determination possible.
Appendix A. Successor corrections and unrecovered bridges
This appendix records corrections consequential enough to affect interpretation. The source archive remains unchanged. The complete line-level Part III diff accompanies the packet.
| Coordinate | Submitted or predecessor issue | Treatment in R1 |
|---|---|---|
| Part III L03 | Rewrite failed under a function application | Use congruence on the inverse-function identity; statement retained |
| Finite metadata lemma | Finite-set API no longer supplied the cited helper | Exhibit sup + 1 and prove it lies outside the set |
| Spectral fibre lemma | Sign in a linear-combination step did not close the goal | Correct the sign; statement retained |
| Set/ENNReal and finite-set proofs | Outdated names or argument forms | Port to the checked environment; statements retained |
| L82 parity projection | Default argument still left the projection arbitrary | Fix the projection to the stated three fields; this changes the theorem’s hypotheses |
| Force-scope flags | Distinct tags risked being read as disjoint force classes | Retain tag theorem; separately prove zero-force inclusion and the correct quantifier relation |
| L85-86 A-D classifier | A function assigning tags risked being read as a PDE entailment | Treat it as a classifier only; use the new NSGlobal /
NSForcedFailure contract for logical consequences |
| Dated claim example | Hardcoded dates risked asserting verified public priority | Retain the numeric example; restrict prose to dates printed on the supplied artifact |
| T1 sufficient-condition invariance | An invariant target does not force every sufficient condition to be invariant | Supply an explicit countermodel and prove the corrected biconditional version |
| PNP tail classification | A quantifier presentation alone does not prove absence of simpler equivalents or finite proofs | Keep the duality and bounded-test obstruction; do not carry the hierarchy overclaim |
| Positive residual infimum | Pointwise nonzero error need not give a uniform positive lower bound | Keep exact exclusion distinct from metric infimum; require a specified comparator and cost |
| Dictionary stop and execution prose | Claimed global exhaustiveness and stale “not executed” status | Formalize a declared stop datatype and replace execution status with captured receipts |
| Critique/estimate Boolean flags | An asserted flag does not prove its semantic interpretation | State their metadata role and expose the soundness bridge |
| Hodge/BSD specialized predecessor claims | Additional geometry, descent, and analytic-certification dependencies not rebuilt here | Preserve original papers; state only the checked contracts as results of this edition |
The dictionary contains broader mappings into physics, language, music, and metrology. This edition uses the recovered algebraic and semantic results relevant to the present premise. It does not certify every physical identification or every historical assertion in the supplied corpus. That boundary prevents a successful small theorem from being used as a receipt for an unexamined larger claim.
Appendix B. Evidence inventory
| Packet location | Contents |
|---|---|
sources/ |
The predecessor Lean modules, the new institutional-signal module, and the exact combined companion source checked online |
receipts/ |
Complete final browser captures, plain messages, and theorem/axiom ledger |
originals/ |
The three Claude handoff documents, submitted Part III source, recovered earlier evidence packet, and relevant supplied PDFs |
case_sources/ |
All six recovered Arena case papers and the later NS bridge |
provenance/ |
Source hashes, coverage and correction records, and Part III diff |
reproduction/ |
Exact encoded-source URLs, checked toolchain version, and fresh-run instructions |
FEEDBACK_TEMPLATE.json |
A concrete record for a claim, scope, evidence, disposition, and successor request |
verify_receipts.py |
Checks source/capture identity, theorem counts, and disallowed axiom dependencies |
The originals and earlier receipts preserve the path into this successor. Earlier runs remain separately dated. The R4 summary identifies five fresh captures covering all 278 theorem declarations. Their origins are 212 in R1, 36 in R2, 26 in R3, and four in R4. Supporting definitions are excluded from that count. The R1-R3 captures remain separately named historical evidence.
Appendix C. How to submit an inspectable response
- Identify a theorem by its fully qualified Lean name, or quote the exact prose assertion.
- State the scope and definitions under which you read it.
- Attach the derivation, counterexample, failed build, missing bridge, or source correction.
- State the requested disposition: accept, reject, keep open, or record a scope change.
- Identify whether the response targets a theorem, an encoding bridge, an empirical attribution, or a stopping decision.
- Preserve the prior record and link the successor, including a retraction where warranted.
The response form accepts a comment before its interpretation has been resolved. Registration records receipt of the comment. Mathematical acceptance or rejection requires the further reason. Applying that distinction to this instrument itself completes the requested self-application.
Appendix D. Full Lean carrier definitions for the displayed contracts
These definitions occur in LambdaInstrument.lean. Each
displayed theorem uses these exact carriers. Full proofs for every
declaration appear in the source packet.
def Recoverable {X Y Z : Type*} (read : X → Y) (target : X → Z) : Prop :=
∃ decode : Y → Z, ∀ x, decode (read x) = target x
def AllStages (P : ℕ → Prop) : Prop := ∀ n, P n
def Window (N : ℕ) (P : ℕ → Prop) : Prop := ∀ n, n < N → P n
def NSGlobal {D F : Type*} (admD : D → Prop) (global : D → F → Prop)
(zeroForce : F) : Prop := ∀ d, admD d → global d zeroForce
def NSForcedFailure {D F : Type*} (admD : D → Prop) (admF : F → Prop)
(global : D → F → Prop) : Prop :=
∃ d f, admD d ∧ admF f ∧ ¬ global d f
def NSRegular {D : Type*} (regularWindow : D → ℕ → Prop) (d : D) : Prop :=
∀ n, regularWindow d n
def NSBlowup {D Time : Type*} (before : D → Time → Prop)
(size : D → Time → ℝ) (d : D) : Prop :=
∀ M : ℝ, ∃ t, before d t ∧ M < size d t
def RHForm {Zero : Type*} (nontrivial onLine : Zero → Prop) : Prop :=
∀ z, nontrivial z → onLine z
def UniformGap {State : Type*} (excited : State → Prop) (energy : State → ℝ) : Prop :=
∃ δ : ℝ, 0 < δ ∧ ∀ s, excited s → δ ≤ energy s
def YMForm {Group Theory State : Type*} (admissibleGroup : Group → Prop)
(validTheory : Group → Theory → Prop)
(excited : Theory → State → Prop) (energy : Theory → State → ℝ) : Prop :=
∀ g, admissibleGroup g → ∃ t, validTheory g t ∧ UniformGap (excited t) (energy t)
def HodgeForm {Instance Cycle : Type*} (admitted : Instance → Prop)
(represents : Cycle → Instance → Prop) : Prop :=
∀ i, admitted i → ∃ c, represents c i
def PolyCandidateForm {Candidate Input : Type*} (correct : Candidate → Input → Prop) : Prop :=
∃ c, ∀ x, correct c x
def BSDRankForm {Curve : Type*} (algRank anRank : Curve → ℕ) : Prop :=
∀ E, algRank E = anRank E
def ExactOrder (coefficient : ℕ → ℝ) (r : ℕ) : Prop :=
(∀ n, n < r → coefficient n = 0) ∧ coefficient r ≠ 0
inductive Status where
| accepted | rejected | open | scopeChange
deriving DecidableEq, Repr
structure Assessment (Claim Scope Evidence : Type*) where
claim : Claim
scope : Scope
evidence : Evidence
rule : Scope → Evidence → Status
verdict : Status
receipt : rule scope evidence = verdict
inductive StopMode (Actor : Type*) where
| effective (testRan : Bool) (checked : testRan = true)
| declared (actor : Actor)
Appendix E. R2 corpus integration record (preserved)
R2 supersedes the reading edition of this instrument while preserving
R1’s sources and dated receipts. It adds one formal module,
LambdaConstitutive.lean, and integrates its foundation into
§1. The six Arena papers and the supplied corpus snapshots remain source
records. Their presence never upgrades an unverified mapping to a
checked result.
Lambda_Dictionary_R2.md retains the supplied dictionary
and adds marked successor paragraphs at the existing entries for
distinction, transport, projection, recoverability, scope, receipt,
stop, will, cost, and holder. It adds one term,
accumulator, whose dependencies already occur in those
entries. This incorporates the extension into the vocabulary without
replacing the older evidence by an unexplained rewrite.
| New coordinate | Formal coverage | Application or interpretive bridge |
|---|---|---|
| Conveyance | Role positions; collision obstruction; unchanged-message postprocessing | Every meaningful reference requires an equivalent discrimination |
| TCO and reflection | Lost-depth and retained-depth models; terminating traces without a uniform bound; finite-state continuation | Literal identification with individuality, mental recursion, or all model use |
| Two accumulator tasks | Result/return countermodels and joint recovery | Which real-world queries and costs a holder should select |
| Online reuse | Append compatibility in both directions; induction; snapshot counterexample | An actual implementation realizes the encoded transition |
| Memory costs | Exact finite-class, subset, and depth cardinality bounds | Physical units, available hardware, practical storage budgets |
| Warranted reuse | Scope equality or a supplied translation bridge; tags insufficient | Fidelity and soundness of real records and their claimed receipts |
| Shared compendium | Predicate-preserving composition; middle-predicate counterexample | Participants agree on a representation and maintain it faithfully |
| Human analogies | No clinical or consciousness theorem supplied | Empirical investigation and philosophical argument remain separate |
The main new correction replaces the proposed termination/bounded-state dichotomy with actual countermodels and an update theorem. It replaces a universal minimal accumulator prescription with an indexed cost and query obligation. It preserves the central contribution: reuse can carry both capability and unexamined commitments, so the record should keep the basis available and the revision path real.
The HTML instrument contains the complete reading edition, the checked-statement catalogue, original case texts, formal sources, and a downloadable copy of the evidence packet. Its interactive records remain device-local until a reader explicitly exports them. Their field-level checks implement the declared recording convention; they do not run Lean or adjudicate the truth of free text.
Appendix F. R3 integration and exact formal scope
R3 integrates the final carried-state and persistence discussion into
§§1.8-1.11 and carries the NS application forward in §1.12. R1 and R2
historical sources and receipts retain their identities in the
predecessor record. R4 run sources add execution markers; their new
hashes and receipts are separately recorded. The complete R2 packet is
preserved under originals/ so the predecessor reading
edition and its dictionary remain recoverable.
| New coordinate | Checked scope | Bridge still owed in an application |
|---|---|---|
| Condition versus record | remark and finite lists of remarks preserve the
separately stored condition and origin |
A real operation acts only on the record, or its additional intervention is modeled |
| Origin and observation | Explicit collisions block recovery; enrichment can recover the selected coordinate | Evidence that an actual observation reveals a condition or its origin |
| Access and intervention | Countermodels separate them; an invariant obstructs specified finite action paths | The actual available actions and their invariant or change mechanism |
| Transfer | Route, decoder agreement, and initial recovery imply successor recovery | Implemented transfer, interpretation, and retained target |
| Persistence | Prefix countermodel; ideal permanent model; induction under maintained premises | Physical preservation law, admissible futures, and actual maintenance |
| Budget and priority | Unit-cost cardinality obstruction and equally feasible alternatives | Costs, units, priorities, and any optimization criterion |
The condition profiles are a declared vocabulary, not a proved
biological taxonomy. The Origin datatype contains
inherited, acquired, declared, and unknown tags. It does not infer those
tags from a person’s condition. A description becoming explicit changes
its access record; it does not retroactively change who established the
condition.
The following definitions give the carriers for the new displayed
contracts. Every theorem’s complete printed statement and proof are
available in the catalogue and
sources/LambdaCarriedState.lean.
inductive Origin where
| inherited | acquired | declared | unknown
deriving DecidableEq, Repr
structure Carried (C R : Type*) where
condition : C
record : R
origin : Origin
-- Updating the descriptive record has an explicitly limited action.
def remark {C R : Type*} (f : R → R) (s : Carried C R) : Carried C R :=
{ s with record := f s.record }
def Recovers {X Y Z : Type*} (observe : X → Y) (target : X → Z) : Prop :=
∃ decode : Y → Z, ∀ x, decode (observe x) = target x
def CanChange {X A : Type*} (act : A → X → X) (x : X) : Prop :=
∃ a, act a x ≠ x
def applyActions {X A : Type*} (act : A → X → X) (x : X) (as : List A) : X :=
as.foldl (fun s a => act a s) x
def ExactAt {X S Z : Type*} (encode : Nat → X → S)
(decode : Nat → S → Z) (target : X → Z) (t : Nat) : Prop :=
∀ x, decode t (encode t x) = target x
def Through {X S Z : Type*} (encode : Nat → X → S)
(decode : Nat → S → Z) (target : X → Z) (N : Nat) : Prop :=
∀ t, t ≤ N → ExactAt encode decode target t
def expiresAfter (N t : Nat) (x : Bool) : Bool :=
if t ≤ N then x else false
The HTML instrument extends the recording convention to retain a condition description, reported condition origin, access route, intervention route, carrier, recovery target, horizon, maintenance route, and budget or priority. Missing fields are explicitly unspecified. R2 imports require an explicit translation: the original record is retained inside the translated entry and the new coordinates are marked unspecified. Nothing reconstructs a past observation or intervention from an absent field.
The self-contained page carries its full paper, dictionary, source texts, cases, theorem catalogue, and downloadable packet. Its assessment ledger stays local to the browser until exported. The page does not run Lean or turn a reported intervention into an actual one. Its own persistence is conditional on retaining readable file bytes and an available interpreter; export and transfer move that obligation to another carrier.
Appendix G. R4 audit disposition and delivery contract
R4 responds to the supplied PDF review and its subsequent retraction. The review itself did not audit Lean sources or execution receipts. This edition performs fresh runs and preserves the exact distinctions the review raised.
| Review item | Disposition | Change in this edition |
|---|---|---|
| Finding 1, holder relation | Withdrawn by the auditor | No substantive change to the attribution relation or the distinct OPEN status |
| Finding 2, replacement decoder | Accepted as a displayed-evidence mismatch | §1.10 now displays the existing quantified decoder theorem beside the finite-prefix theorem |
| Finding 3, mathematical attribution | Accepted | Standard factorization, right-congruence, and pigeonhole ingredients are identified and cited at their use sites |
| Finding 4, public record | Accepted with dated qualification | §§4.1a-b record C/D, separate Euler claims, lineage, attributed dispute, Clay’s rules and statement, and the signal’s possible role in reception |
| Capture origin wording | Clarify | §8 separates origin edition, containing edition, and fresh execution |
| Declaration terminology | Correct | 278 theorem declarations; helper definitions, structures, and inductive types excluded |
| Internal name spelling | Correct | Nielsen replaces the internal misspelling |
The auditor retracted Finding 1 because the comparator’s printed byline and Lu Semita’s own OPEN investigation were distinct recorded coordinates. This withdrawal does not settle the other review items and does not convert the comparator’s claim into a premise of the instrument.
The four new signal results are elementary conditional models. They formalize a possible decision change and an observational limitation; they do not prove institutional favoritism, a waiver of prize rules, a psychological law, or an actual causal effect. The four earlier modules preserve their theorem statements and proofs and receive fresh R4 execution markers and receipts.
The PDF, editable paper, dictionary, theorem catalogue, source files,
current receipts, and reproduction recipes are built from one R4
directory. The portable HTML embeds that exact PDF and proof packet and
carries the matching full reading edition.
DELIVERY_MANIFEST.json and verify_package.py
check correspondence between delivered representations and embedded
downloads. SHA256SUMS.txt covers the packet’s payload.
Neither a hash check nor an HTML interaction test reruns Lean; the
reproduction script names the separate fresh-execution procedure.
The HTML retains the existing R3 ledger protocol because its record fields and validation rules are unchanged. Its edition is R4. R3 ledger exports therefore remain directly compatible; R2 imports still require the explicit translation that preserves the original entries. A new edition label does not imply that the user must discard their accumulated records.