MDPI Axioms: axioms-15-090 · published 2026-01-26 · 🧮 math.GM · math-ph· quant-ph

Recognition: 8 theorem links

· Lean Theorem

Recognition Geometry

Elshad Allahyarov, Jonathan Washburn, Milan Zlatanović

Authors on Pith 2 claimed

Jonathan Washburn ORCID verified
Elshad Allahyarov name match

Pith reviewed 2026-05-06 00:32 UTC · model claude-opus-4-7

classification 🧮 math.GM math-phquant-ph MSC <parameter name="0">03B30

keywords <parameter name="0">axiomatic foundations

0 comments

The pith

Geometry is reconstructed from scratch as the quotient of configurations by what measurements can distinguish, with the observable map proved injective.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to derive geometric structure from operational measurement rather than assume it. A configuration space is paired with "recognizers" — functions sending configurations to observable outcomes — and two configurations are deemed equivalent whenever no recognizer separates them. The observable space is then defined as that quotient. The main results are an injectivity theorem (distinct observable classes correspond to distinct outcome patterns) and a universal property (every map respecting measurement-indistinguishability factors uniquely through the quotient). Locality enters through neighborhood systems with a finite local-resolution axiom, and quantitative distinguishability appears as pseudometrics built from comparative recognizers. The authors then study composition of recognizers (which can only refine the quotient), gauge symmetries (gauge-equivalent configurations are always observationally indistinguishable, but not conversely), and worked examples on R^n, lattices, and qubit measurements. A portion of the framework and proofs is formalized in Lean 4.

Core claim

The paper proposes a small set of axioms (RG0–RG4) under which an "observable space" is not posited but constructed: one starts with a configuration space and a family of recognizers (maps from configurations to outcomes), declares two configurations equivalent when no recognizer can tell them apart, and takes the quotient. The central theorem is that the induced map from this quotient to the space of observable events is injective, so observable states are exactly equivalence classes of measurements with no hidden remainder. A second universality result says any map that respects measurement-indistinguishability factors through this quotient uniquely. Locality is then layered on via neighbo

What carries the argument

The recognition quotient C_R = C/~_R, where ~_R identifies configurations on which every recognizer agrees, together with the induced observable map R̄: C_R → E. Theorem 1 establishes injectivity of R̄; Theorem 2 establishes universality of the quotient among maps that respect ~_R. Neighborhood systems plus a finite-resolution axiom carry locality without metric or topological input, and pseudometric "recognition distances" carry quantitative distinguishability when comparative recognizers are available.

If this is right

<parameter name="0">If the axioms suffice
"hidden variables" beyond measurement outcomes are categorically excluded by Theorem 1: two configurations that no recognizer separates are literally the same observable state.

Load-bearing premise

The whole edifice rests on treating "what a recognizer outputs" as a primitive that already captures everything physically meaningful — so the set-theoretic quotient is taken to encode the content normally carried by algebraic, probabilistic, or causal structure in the theories it claims to unify.

What would settle it

Exhibit a recognizer family and configuration pair where the proposed observable map R̄ fails to be injective under axioms RG0–RG4, or show that the universal factorization in Theorem 2 admits a second, non-equal factoring map; alternatively, demonstrate a working physical theory (e.g., a piece of C*-algebraic QM or causal set dynamics) whose essential content provably cannot be reconstructed from any recognizer family on its configuration space.

read the original abstract

We introduce Recognition Geometry (RG), an axiomatic framework in which geometric structure is not assumed a priori but derived. The starting point of the theory is a configuration space together with recognizers that map configurations to observable events. Observational indistinguishability induces an equivalence relation, and the observable space is obtained as a recognition quotient. Locality is introduced through a neighborhood system, without assuming any metric or topological structure. A finite local resolution axiom formalizes the fact that any observer can distinguish only finitely many outcomes within a local region. We prove that the induced observable map R-bar : C_R -> E is injective, establishing that observable states are uniquely determined by measurement outcomes with no hidden structure. The framework connects deeply with existing approaches: C*-algebraic quantum theory, information geometry, categorical physics, causal set theory, noncommutative geometry, and topos-theoretic foundations all share the measurement-first philosophy, yet RG provides a unified axiomatic foundation synthesizing these perspectives. Comparative recognizers allow us to define order-type relations based on operational comparison. Under additional assumptions, quantitative notions of distinguishability can be introduced in the form of recognition distances, defined as pseudometrics. Several examples are provided, including threshold recognizers on R^n, discrete lattice models, quantum spin measurements, and an example motivated by Recognition Science. In the last part, we develop the composition of recognizers, proving that composite recognizers refine quotient structures and increase distinguishing power. We introduce symmetries and gauge equivalence, showing that gauge-equivalent configurations are necessarily observationally indistinguishable, though the converse does not hold in general. A significant part of the axiomatic framework and the main constructions are formalized in the Lean 4 proof assistant, providing an independent verification of logical consistency.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Correct but mostly a renaming exercise dressed up as a unification; the Lean claim and the "Recognition Science" example are the parts to scrutinize.

read the letter

Quick read for you on the Washburn–Zlatanović–Allahyarov "Recognition Geometry" paper.

The math is fine. RG0–RG4 set up a configuration space, a neighborhood base, and a family of maps to an event space. Theorem 1 (the induced map on the quotient by the fiber relation is injective) is one line. Theorem 2 is the universal property of the quotient. Propositions 2–4 are the standard final-topology lemmas. Theorem 4 (composition refines the partition) and Theorem 6 (gauge ⇒ indistinguishable) follow immediately from the definitions. Nothing is wrong, but nothing here is hard either.

What the paper does well: it is clean, self-aware about its own scope, and §2.6 honestly says the construction is "mathematically equivalent" to orbit spaces, level sets, measurable partitions, and the relational-QM picture. The §1.3 positioning section is the right kind of literature work — it acknowledges sheaves, coarse-graining, RG flow, NCG, etc. Examples 1–3 (threshold recognizers, Z³ parity, spin) are pedagogically useful. The Lean 4 claim, if real, is a genuine plus.

Soft spots, in order of how much they actually matter:

1. The abstract sells "a unified axiomatic foundation synthesizing" C*-algebraic QM, information geometry, causal sets, NCG, and topos theory. The body delivers nothing of the kind — there are no reduction theorems recovering algebraic, probabilistic, or causal content. Only the set-theoretic quotient skeleton is shared. This is the main thing to push back on: tone the abstract down, or supply actual reduction results.

2. The Lean 4 formalization is mentioned but I see no repository URL, commit, or file manifest in the supplied text. For a paper whose novelty rests largely on exposition + machine-checked status, that needs to be public and pinned.

3. Example 4 ("Recognition Science instantiation," ledger states L) imports a non-standard paradigm by citation [19] without operational definition, and the same [19] is used in §2.6 for Rovelli's relational QM. That's a citation collision, and the Recognition Science framing is doing no mathematical work — drop it or ground it.

4. Minor: "no hidden structure remains" (§2.6) overstates what Theorem 1 says. Injectivity onto Im(R) does not preclude additional structure; the paper itself notes this two paragraphs later.

Who benefits: someone teaching operational/measurement-first foundations who wants a clean toy axiom system. Not a working researcher in C*-algebras, info-geometry, or causal sets — they have these tools already.

Recommendation: send to review, conditional on the abstract being detuned, the Lean repo being shipped with a commit hash, and Example 4 / the [19] collision being fixed. Don't desk-reject — the mathematics is honest and the formalization angle deserves a referee — but the unification framing as written shouldn't pass.

Referee Report

5 major / 8 minor

Summary. The paper proposes "Recognition Geometry" (RG), an axiomatic framework (RG0–RG4) starting from a configuration space C, an event space E, a primitive locality structure N, and a set Σ of "recognizers" R: C → E with |Im(R)| ≥ 2. The central construction is the recognition quotient C_R = C/∼_R, where c_1 ∼_R c_2 iff R(c_1) = R(c_2). The main results are (i) Theorem 1: the induced map R̄: C_R → E is injective; (ii) Theorem 2: the universal property of the quotient; (iii) Propositions 2–4: N induces a topology τ_N, the quotient topology τ_R is the final topology making π_R continuous, and continuity descends to R̄; (iv) Theorems 3–4: composition of recognizers refines the partition; (v) Theorem 6: gauge equivalence implies observational indistinguishability. Examples include threshold recognizers on R^n, Z^3 parity, Bloch-sphere spin measurements, and a "Recognition Science" ledger example. A Lean 4 formalization is claimed.

Significance. The mathematical statements are correct and the construction is well-organized. Strengths to credit explicitly: (a) the manuscript provides a clean, self-contained presentation of measurement-induced quotient structure that may be pedagogically useful, (b) the explicit link to a Lean 4 formalization (if made verifiable) is a positive feature uncommon in math.GM submissions, and (c) the comparison list of related programs in §1.3 is useful. However, the substantive significance is limited: every theorem is a one- or two-line consequence of the definition c_1 ∼_R c_2 ⇔ R(c_1) = R(c_2) or a standard fact about final topologies (cf. Munkres ch. 22; Mac Lane–Moerdijk for the universal property). The framework recovers only the set-theoretic skeleton of the programs it claims to unify (C*-algebras, information geometry, causal sets, NCG, topoi); none of the algebraic, probabilistic, or causal content of those theories is reproduced. The contribution is therefore primarily expository/foundational rather than a new technical result, and the "unification" claim should be calibrated accordingly.

major comments (5)

[Abstract, §1.3, §2.6] The 'unification' claim is overstated relative to what is proved. §2.6 itself acknowledges that the recognition quotient is 'mathematically equivalent' to orbit spaces, level sets, and measurable partitions (Examples 5–7). What is recovered from C*-algebraic QM, information geometry, causal sets, NCG, and topoi is only the set-theoretic quotient skeleton — not the algebraic product, the Fisher metric, the causal order, the spectral triple, or the internal logic. A theorem 'unifying' these frameworks would, at minimum, exhibit functors from each into a category of recognition triples and recover the relevant native structure on the image. Either weaken the claim to 'a common set-theoretic substrate' throughout the abstract and §1.3, or supply the missing functorial statements (Remark 7 currently defers this to future work, which is incompatible with the strength of the abstract).
[Example 4 and reference [19]] Example 4 invokes 'Recognition Science' and the 'space L of all ledger states' as motivating context, citing [19]. Two issues: (i) 'Recognition Science' is not an established framework in the peer-reviewed literature on measurement foundations; presenting it on equal footing with C*-algebraic QM and causal sets requires a defining citation to a peer-reviewed source and a self-contained mathematical definition of L. (ii) Reference [19] is used in §1.2 and Example 8 as the citation for Rovelli's relational QM, and in Example 4 as the citation for 'Recognition Science' — these appear to be different bodies of work and should not share a reference number. Please disambiguate the citations and either remove Example 4 or replace it with a self-contained mathematical instantiation.
[Abstract / Lean 4 claim] The abstract states that 'a significant part of the axiomatic framework and the main constructions are formalized in the Lean 4 proof assistant, providing an independent verification of logical consistency.' The body contains no pointer to the repository, no list of which theorems (RG0–RG4, Theorems 1–6, Propositions 1–4) are formalized, and no statement of which mathlib version is used. Since this claim supports consistency of the framework, please add (a) a public archived link (Zenodo/GitHub commit hash), (b) a table mapping each numbered theorem/proposition to a Lean lemma name, and (c) a note on which axioms are assumed in Lean (classical, choice). Without this the formalization claim cannot be checked.
[§2.1, Axiom 3 (RG2) and Definition 1] RG2 is stated as a neighborhood-base-style structure but with an unusual non-monotonicity: N(c) is not assumed to be upward closed. Remark 2 acknowledges that consequently 'we do not claim that every topological neighborhood of c in τ_N is in N(c).' This has a load-bearing consequence: the τ_N in Definition 1 may not recover N(c) as its neighborhood filter, which weakens the operational meaning of N. In Remark 10 and Example 9 the authors stress that different N can yield different observable topologies on C_R; one would like a clear statement of when two locality structures N, N' generate the same τ_N (i.e., a characterization of which locality data the framework actually distinguishes). Please add such a statement or a clarifying remark.
[§3.2, Definition 14 and Theorem 6] Theorem 6 (gauge equivalence ⇒ observational indistinguishability) is a one-line consequence of Definition 12. The remark following Theorem 6 promises a counterexample to the converse 'with restricted gauge group' but the manuscript text appears truncated mid-sentence ('Let us construct counterexample with restricted gauge group.') without supplying it. Since the gauge-vs-indistinguishability gap is one of the few non-tautological structural points in §3, the counterexample should be given explicitly, with C, R, and G_R written out.

minor comments (8)

[§1.3] The bullet list contrasting RG with QBism, information geometry, causal sets, NCG, topoi, and sheaf theory paraphrases the cited programs in broad strokes. Short, precise statements (e.g., 'NCG replaces commutative C(M) by a possibly noncommutative C*-algebra A; RG does not reproduce the multiplicative structure of A') would help.
[Theorem 1] The proof is omitted; given that it is one line, it should be written out for completeness, since the abstract highlights this theorem.
[Definition 11 / Theorem 4] The notation R_1 ⊗ R_2 for the product map (R_1, R_2): C → E_1 × E_2 conflicts with standard tensor-product usage and may mislead readers expecting a monoidal structure. Consider R_1 × R_2 or ⟨R_1, R_2⟩.
[Remark 5] 'R_Σ separates points (any two distinct points are separated by some half-space)' is correct for the full family of threshold recognizers on R^n but should be stated as a lemma with a one-line justification (use coordinate functionals).
[Front matter] The Keywords field is empty in the version shown. Please supply keywords.
[Throughout] Several typographical/stylistic issues (e.g., 'We let' used in place of 'Let'; some mid-sentence math display breaks). A careful copy-edit pass is warranted.
[§2.3] The discussion of stochastic and partial recognizers is useful scope-setting but should be moved to a 'Limitations and extensions' subsection so §2.3 stays focused on the deterministic case actually used in the theorems.
[§2.6, Example 8] The claim that RG 'formalizes' Rovelli's relational QM via [c]_R is strong; relational QM is about probabilistic content relative to an observer, which deterministic recognizers do not capture. Please soften to 'provides a set-theoretic analogue of'.

Simulated Author's Rebuttal

5 responses · 0 unresolved

We thank the referee for a careful and constructive report. We accept the central editorial point: in its current form the manuscript proves a clean set-theoretic/topological skeleton, while the abstract and §1.3 use the stronger word "unification" that would require functorial statements we have not yet proved. We will recalibrate the language accordingly throughout. We also accept that the Lean 4 claim must be made verifiable, that Example 4 / reference [19] need disambiguation, that the truncated counterexample after Theorem 6 must be supplied in full, and that the role of non-monotone N relative to τ_N deserves an explicit characterization. Below we respond point by point, indicating where the next revision will incorporate the referee's requests and where we wish to defend the current presentation. We are grateful for the explicit acknowledgement of the manuscript's pedagogical value, the comparative §1.3 list, and the Lean component, and we will work to make the latter two genuinely useful to readers.

read point-by-point responses

Referee: The 'unification' claim is overstated; only the set-theoretic quotient skeleton of C*-algebraic QM, information geometry, causal sets, NCG, and topoi is recovered. Either weaken the claim throughout, or supply functorial statements (Remark 7 defers this).

Authors: We agree. Remark 7 already concedes that a categorical/functorial treatment is deferred, and §2.6 explicitly notes that the recognition quotient is mathematically equivalent to orbit spaces, level sets, and measurable partitions. The abstract and §1.3 should match this honesty. In the revision we will: (i) replace 'unified axiomatic foundation synthesizing these perspectives' in the abstract with language such as 'a common set-theoretic and topological substrate underlying these measurement-first programs'; (ii) rewrite §1.3 so each bullet states explicitly which native structure (C*-product, Fisher metric, causal order, spectral triple, internal logic) is *not* recovered by RG alone; (iii) reframe the contribution as expository/foundational, with the technical novelty being the minimal axiom system (RG0–RG4), the finite-resolution axiom, and the Lean formalization, rather than a unification theorem. We will also add a sentence to Remark 7 making clear that any genuine unification claim awaits the construction of functors from each target framework into a category of recognition triples that recover the relevant native structure on the image. revision: yes
Referee: Example 4 invokes 'Recognition Science' citing [19], which is also used for Rovelli's relational QM. Disambiguate the citations; either remove Example 4 or replace it with a self-contained mathematical instantiation, and provide a peer-reviewed defining citation for L.

Authors: The collision of reference [19] between Rovelli's relational QM (used in §1.2 and Example 8) and the 'Recognition Science' citation in Example 4 is an editorial error and will be corrected: the two will be split into distinct numbered references. On the substantive point we agree with the referee that 'Recognition Science' is not an established framework in the peer-reviewed measurement-foundations literature and should not be presented on equal footing with C*-algebraic QM or causal sets. In the revision we will (a) demote Example 4 from a motivating example to a brief remark explicitly labelled as a non-standard, illustrative instantiation, and (b) provide a self-contained mathematical definition of the ledger space L as an abstract set of records with a position-projection map, so the example stands as pure mathematics independently of the 'Recognition Science' label. If the editor prefers, we are willing to remove Example 4 entirely; the structural content of §2.6 does not depend on it. revision: yes
Referee: The Lean 4 claim in the abstract is unsupported by the body: no repository link, no theorem-to-lemma mapping, no mathlib version, no statement of which Lean axioms (classical, choice) are assumed.

Authors: Accepted in full. The current text does not allow a reader to verify the formalization claim, which undermines the very purpose of mentioning it. In the revision we will add an appendix titled 'Lean 4 Formalization' containing: (a) a public archived link with a fixed commit hash (Zenodo DOI plus GitHub URL); (b) the mathlib version and Lean toolchain version; (c) a table mapping each item RG0–RG4, Theorems 1–6, and Propositions 1–4 to the corresponding Lean definition or lemma name, with a clear indication of which items are *not yet* formalized; (d) an explicit note on the logical foundations used in Lean (Lean's underlying CIC, classical logic via `Classical.em`, and choice via `Classical.choice` where invoked). The abstract will be softened from 'a significant part ... is formalized' to a precise statement matching the table (e.g., 'RG0–RG2 and Theorems 1–3 are formalized; the remaining items are stated but not yet proved in Lean'). revision: yes
Referee: RG2 is non-monotone, so τ_N may not recover N(c) as its neighborhood filter (Remark 2). Since Remark 10 / Example 9 emphasize that different N yield different observable topologies, please characterize when two locality structures N, N' generate the same τ_N.

Authors: This is a fair request and points to an asymmetry we should make explicit. The simple characterization is: τ_N = τ_{N'} iff for every c ∈ C and every U ⊆ C, U contains some V ∈ N(c) with c ∈ V iff U contains some V' ∈ N'(c) with c ∈ V'; equivalently, the upward closures (filters generated by) N(c) and N'(c) coincide for every c. Thus τ_N depends only on the filter generated by N(c) at each point, and the framework genuinely distinguishes locality structures only up to this filter-equivalence. In the revision we will: (i) state and prove this characterization as a new proposition immediately after Definition 1; (ii) add a remark distinguishing 'filter-equivalent' locality structures from genuinely distinct ones; (iii) clarify in Remark 2 that the operational content of N beyond τ_N lies in which specific subsets are taken as primitive accessibility data, not in the topology. We thank the referee for prompting this clarification. revision: yes
Referee: The text following Theorem 6 is truncated mid-sentence: 'Let us construct counterexample with restricted gauge group.' Please provide the explicit counterexample with C, R, and G_R written out.

Authors: The referee is correct; the manuscript is truncated at exactly that point and the counterexample was inadvertently dropped during preparation. We will supply it in full. A concrete instance to be included: take C = {a,b,c,d}, E = {0,1}, and R(a)=R(b)=0, R(c)=R(d)=1. Then the full Aut_R(C) is the group of all bijections preserving the partition {{a,b},{c,d}}, namely (Z/2 × Z/2) ⋊ Z/2. Now restrict the admissible gauge group to G_R = ⟨(a b)⟩ (only swapping a and b is physically implementable). Then a ∼_gauge b and c ∼_gauge c, but although c ∼_R d (same event), there is no T ∈ G_R with T(c)=d. Hence c and d are observationally indistinguishable but not gauge equivalent under G_R, exhibiting the strict gap. We will write this out fully in the revision, with the group action and orbit structure displayed explicitly, and add a brief remark on why such restrictions arise naturally (locality, regularity, or implementability constraints). revision: yes

Circularity Check

2 steps flagged

No load-bearing circularity: theorems are standard quotient-construction results derivable from definitions; "Recognition Science" appears only as a non-load-bearing motivating example.

specific steps

self citation load bearing [Example 4 (§2.6) and reference [19]]
"This example illustrates the RG framework applied to the Recognition Science paradigm [19], showing how the mathematical formalism relates ontological states (ledger) to observable spatial structure."

Author Washburn is associated with the 'Recognition Science' program, and Example 4 invokes ledger states L as a motivating instantiation via citation [19]. Reference [19] also appears to be used in §2.6/Example 8 for Rovelli's relational QM, indicating overlapping/duplicated numbering. This is a minor self-citation: Example 4 is illustrative only and not load-bearing for any theorem (Theorems 1–6 hold without it), so it does not make the derivation circular — it is flagged here for completeness as the only citational issue.
renaming known result [§2.6, Theorem 2 and surrounding text]
"Theorem 2 is the standard universal property of quotient spaces (see [47,61]). ... The recognition quotient construction is mathematically equivalent to several well-known structures in differential geometry, probability theory, and physics. The conceptual contribution lies in the reinterpretation..."

The paper openly acknowledges that its main structural theorem is the standard universal property of quotients and that the C_R construction is 'mathematically equivalent' to orbit spaces, level sets, and measurable partitions. This is a renaming/repackaging of known mathematics under new vocabulary, which the paper itself states. Because the paper is transparent about this and presents the contribution as 'reinterpretation' rather than new theorems, it does not constitute hidden circularity — but it does mean the 'unification' claim in the abstract is rhetorical rather than mathematical.

full rationale

This is a definitional/axiomatic paper in pure mathematics. The chain is: axioms RG0–RG4 → definition of recognizer R: C→E → indistinguishability ∼_R defined as R(c1)=R(c2) → quotient C_R := C/∼_R → induced map R̄: C_R → E. Theorem 1 (R̄ injective) and Theorem 2 (universal property) are standard, immediate consequences of how quotients by kernel relations work; the paper itself flags Theorem 2 as "the standard universal property of quotient spaces (see [47,61])" and §2.6 admits the construction is "mathematically equivalent" to orbit spaces, level sets, and measurable partitions. That is honest restatement, not hidden circularity. Crucially, no quantities are fitted and no empirical "prediction" is being claimed to follow from data that itself defined the prediction — the patterns 1, 2 (self-definitional / fitted-input-as-prediction) simply don't apply, because the paper produces no numerical predictions at all. The abstract reports Lean 4 formalization, which (per the rules) provides independent machine-checked verification of the logical content. The only mild concern is rhetorical/citational, not derivational: Example 4 invokes "Recognition Science [19]" and the space of "ledger states L" as if a known paradigm, and reference [19] is also used in §2.6/Example 8 for Rovelli's relational QM, suggesting overlapping or misnumbered citations. Author Washburn is publicly associated with the "Recognition Science" program, so this could constitute self-citation. However, Example 4 is not load-bearing: it is one of four illustrative examples (alongside threshold recognizers, Z^3 lattice, and S^2 spin), and removing it leaves all axioms, definitions, and theorems intact. None of Theorems 1–6 or Propositions 1–6 depend on the ledger example. Pattern 6 (renaming a known result) has partial applicability — the paper essentially repackages standard quotient-by-fiber constructions under new vocabulary ("recognizers," "resolution cells," "recognition quotient") and the paper transparently acknowledges this in §2.6. Calling this "unification" of C*-algebra/info-geometry/causal sets/NCG/topos is overreach in scope, but that is a correctness/novelty concern, not equational circularity. Score: 1. Self-contained derivation, one minor non-load-bearing self-citation in Example 4.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 2 invented entities

The framework rests on five named axioms plus background ZF. RG0, RG1, and RG2 are domain or standard-math assumptions of negligible cost. RG3 (finite local resolution) and RG4 (comparative recognizers) are introduced specifically for this paper but do no load-bearing work in the visible theorems. No numerical free parameters appear. Two invented entities are present: 'recognizer' (a renaming of a total function with non-trivial image) and 'ledger states' L from Example 4, the latter imported from a separate self-cited paradigm without independent operational grounding.

axioms (6)

domain assumption RG0: a nonempty configuration set C with at least two elements exists
Trivial existence axiom; excludes the degenerate single-point case.
domain assumption RG1: an event set E with |E| >= 2 exists
Excludes the trivial constant recognizer.
standard math RG2: neighborhood system N satisfying reflexivity, intersection-closure, and local refinement
Standard neighborhood-base axioms generating a topology.
ad hoc to paper RG3: finite local resolution within any local region
Operationally motivated finiteness condition introduced to encode measurement coarse-graining; does no load-bearing work in the visible theorems.
ad hoc to paper RG4: comparative recognizers enabling order-type relations
Introduced to derive pseudometric/order structure under additional assumptions; details deferred in the supplied text.
standard math Consistency of ordinary (ZF) set theory
Stated as background in Section 2.

invented entities (2)

Recognizer (total function R: C -> E with |Im(R)| >= 2) no independent evidence
purpose: Primitive object replacing 'points' as the foundation of observable structure.
A renamed total function; no new physical entity is postulated.
Ledger states L (Example 4, 'Recognition Science instantiation') no independent evidence
purpose: Configuration space underlying a position recognizer R_pos: L -> R^3.
Imported from a separate self-cited paradigm without independent operational definition or falsifiable handle inside this paper.

pith-pipeline@v0.9.0 · 34575 in / 6342 out tokens · 201974 ms · 2026-05-06T00:32:41.728822+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

Foundation/RecognizerInducesLogic.lean Recognizer.induces_primitive_observer matches
We let C = L be the space of all ledger states (the complete ontological record of all entities and their properties), and let E = R^3. We define the position recognizer R_pos : L → R^3 ... The recognition quotient is then L/∼_{R_pos} ≅ Im(R_pos) ⊆ R^3 ... This example illustrates the RG framework applied to the Recognition Science paradigm
Foundation/RecognitionLatticeFromRecognizer.lean cell_eq_iff_kernel; latticeEquivOfSameKernel matches
Theorem 1: The induced map R̄ : C_R → E is injective. ... distinct observable states correspond to distinct events, and no further distinctions exist within C_R beyond those encoded by R
Foundation/ObserverFromRecognition.lean PrimitiveInterface (observe : K → Fin n); nontrivial_recognition_forces_interface matches
A finite local resolution axiom formalizes the fact that any observer can distinguish only finitely many outcomes within a local region.
Foundation/MultiplicativeRecognizerL4.lean MultiplicativeRecognizer.RecognizerComposition; multiplicativeRecognizer_satisfies_L4 echoes
Theorem 4: The recognition quotient of the composite refines the quotients of its components ... π_1 : C_{R_1⊗R_2} ↠ C_{R_1} and π_2 : C_{R_1⊗R_2} ↠ C_{R_2}
Foundation/UniversalForcing/NaturalNumberObject.lean IsNaturalNumberObject.recursor_unique; IsNaturalNumberObject.equiv (uniqueness up to canonical iso) echoes
Theorem 2 (universal property): for any function f : C → X constant on resolution cells, there exists a unique f̄ : C_R → X with f = f̄ ∘ π_R
Foundation/RecognitionLatticeFromRecognizer.lean interfaceSetoid; SameKernel; latticeEquivOfSameKernel matches
Theorem 6: gauge equivalent ⇒ observationally indistinguishable; converse fails. Aut_R(C) forms a group of recognition-preserving automorphisms.
Foundation/PrimitiveDistinction.lean equalityCost; identity_from_equality; non_contradiction_from_equality matches
Definition 4 (Indistinguishability): c_1 ∼_R c_2 iff R(c_1) = R(c_2), an equivalence relation on C induced by equality in E.
Foundation/RealityTerminalCategory.lean RealityTerminalCert; every_distinguished_carrier_maps_uniquely_to_reality refines
RG is intentionally positioned at the intersection of several measurement-first programs ... a minimal axiom system for recognition-first models, a canonical quotient construction for observable space, a finite-resolution axiom (RG3), and comparative recognizers (RG4) as a route toward emergent order and distance.