TEXT-LEVELThesis. Classical welfare economics evaluates a projection of total recognition value that is structurally blind to the cross-party coupling term C; the obstruction is the informational non-representability of C from private profiles, not a mechanism-design impossibility.
Every substantive sentence below is status-tagged. The machine-checked core is deliberately small; the load-bearing economic interpretation is labeled TEXT-LEVEL, not PROVED.
CONTEXTThis page is a status-tagged claim register for the settlement-layer economics of Recognition Science: an account, not an argument.
CONTEXTEach claim carries one status tag, links its evidence — a Lean theorem identifier when machine-checked, a paper section otherwise — and, where it is not machine-checked, names a concrete falsifier.
CONTEXTIt is not a manifesto, a policy program, a welfare criterion, or an impossibility theorem for mechanism design.
CONTEXTThe primary reader is a skeptical research economist in welfare theory, social choice, or mechanism design; the secondary reader is a Lean / formal-methods reviewer checking that the certified core says what this page says it says.
CONTEXTThe certified core is mostly finite-graph combinatorics; the economic weight rests on a single interpretive step tagged TEXT-LEVEL and MODEL, and that boundary is marked, not hidden (§6).
A value-bearing economy is a finite graph; its value is the number of independent closed loops.
TEXT-LEVELClassical welfare economics evaluates a projection of total recognition value that is structurally blind to the cross-party coupling term C; the obstruction is informational non-representability of C from private profiles, not a mechanism-design impossibility.
PROVEDAny welfare objective whose only inputs are the private values b₁(A) and b₁(B) cannot determine Z, because equal private profiles can sit on unequal Z, and no decentralized internalization acting on agents' own private records recovers C.
The figure. Two loci A and B joined by a settlement seam carrying s cross-party postings, forming the joined graph G:
propext, Classical.choice,
Quot.sound, with zero domain axioms.Structural rule 1. No PROVED or TEXT-LEVEL row appears without an evidence link.
Structural rule 2. No MODEL, HYPOTHESIS, or PREDICTED row appears without a stated falsifier.
Banded by status, PROVED first. Lean identifiers refer to
IndisputableMonolith/Economics/Recognition/CBlindProjectionPublic.lean. For every PROVED row the
operative falsifier is uniform: a clean lake build fails, the named theorem is absent or its
statement differs from the row, or #print axioms reports an axiom outside propext,
Classical.choice, Quot.sound.
| Claim | Evidence | Assumptions | Falsifier | Depends-on |
|---|---|---|---|---|
| C = b₁(A∪B) − b₁(A) − b₁(B) = max(s−1, 0). | couplingC_eq |
A, B each single-component; finite graph; s a formal seam count. | Build / theorem-statement / axiom check fails. | — |
| Z decomposes super-additively as Z = b₁(A) + b₁(B) + C. | Z_eq_sum_plus_coupling |
Finite settlement graph. | Build / axiom check fails. | couplingC_eq |
| b₁ is additive over disjoint union; the s = 0 baseline has C = 0. | disjoint_additive |
Disjoint finite union; no seam postings. | Build / axiom check fails. | — |
| Any settled trade with s ≥ 2 yields strictly positive coupling, C > 0. | coupling_economy_pos |
Single-component A, B; s ≥ 2. | Build / axiom check fails. | couplingC_eq |
| The private profile (b₁(A), b₁(B)) does not determine Z: equal profiles can carry unequal Z. | Z_not_function_of_profile |
Profile contains only the two private Betti values. | Build / axiom check fails. | Z_eq_sum_plus_coupling |
| At a fixed private profile, Z varies with the seam count s. | Z_depends_on_seam |
Fixed b₁(A), b₁(B); varying s. | Build / axiom check fails. | couplingC_eq |
| Under any split of the s postings between the two agents, the decentralized total of the two enlarged private values equals the autarkic total and recovers none of C. | agent_local_internalization_impotent, agent_local_misses_coupling,
agent_local_gap_pos
|
Each agent acts on its own private record only; no joint object. | Build / axiom check fails. | Z_eq_sum_plus_coupling |
| A settlement posting has exactly two faithful fates — relocated to a dangling edge that closes no loop, or held jointly so it closes a loop only inside a single supra-agent object (the seam glue = the conceded center) — and no third faithful option. | seam_dichotomy |
Faithful posting representation; finite graph. | Build / axiom check fails. | — |
| Any joint-ownership arrangement that recovers C reconstructs the conceded center. | coalition_is_central |
As in seam_dichotomy. |
Build / axiom check fails. | seam_dichotomy |
| A profile-Pareto move — no private value falls, some rises — can strictly lower Z. | pareto_permits_Z_loss |
Pareto comparison uses only private profile values. | Build / axiom check fails. | Z_not_function_of_profile |
| Conditional on gains from trade (wseam > 2·wint), a strict profile-Pareto improvement strictly lowers Z. | pareto_dissolution, pareto_improvement_globally_negative |
wseam > 2·wint; stated payoff weights. | Build / axiom check fails. | pareto_permits_Z_loss |
| Seam funding has a unique interior optimum q* = arsinh((wseam − wint)/(2k))/k, with first-order condition and strict monotonicity against carrying cost 2(cosh(kq) − 1). | z_optimal_economy, qStar_pos, deriv_netZ_strictAnti,
seam_funding_margin
|
k > 0; wseam > wint; stated cost function. | Build / axiom check fails. | Z_eq_sum_plus_coupling |
| Claim | Evidence | Assumptions | Falsifier | Depends-on |
|---|---|---|---|---|
| C equals the rank of the cokernel of the canonical inclusion H₁(A) ⊕ H₁(B) → H₁(G), a basis-independent invariant. | Paper, "Homological reading" | Finite-graph homology over a field. | Exhibit a finite-graph seam in the stated setup where C differs from that cokernel rank, or where the quantity is basis-dependent. | couplingC_eq |
| q* is the unique global maximizer of net Z, by strict concavity. | Paper, "Analytic packaging" | Stated carrying cost; k > 0. | Exhibit a second interior critical point, or a non-concave net-Z under the stated cost. | z_optimal_economy |
| Claim | Evidence | Assumptions | Falsifier | Depends-on |
|---|---|---|---|---|
| A settlement economy is a finite graph, and a subsystem's economic value is its first Betti number b₁ — its count of independent closed recognition loops. | Paper, "The model"; §9 (Recognition Science) | Recognition accounting of value; finite-graph encoding that preserves loop-closure. | Exhibit a settlement economy whose welfare-relevant value is not captured by loop-closure — e.g. value strictly created by an acyclic transfer — shown independent of the graph encoding. | — |
| Claim | Evidence | Assumptions | Falsifier (satisfied) | Depends-on |
|---|---|---|---|---|
| Myerson–Satterthwaite inefficiency equals the unrealized coupling defect C priced at wseam. | Paper, "MS test"; closed-form + 2×2 LP sweep | Canonical MS: uniform types, d = v − c, triangular density. | First-best S₁ = 1/6, second-best S₂ = 9/64, MS loss = 5/192; expected foregone trades E[Clost] = 7/32. Equating loss = w·E[Clost] forces w = (5/192)/(7/32) = 5/42 ≈ 0.119, a number with no independent reading as a seam premium; the 2×2 LP sweep found no interpretable weighting equating dual information rent with priced C. MS inefficiency is mathematically distinct from the topological obstruction. Reopened only by a derivation in which w = 5/42 carries an independent seam-premium interpretation. | couplingC_eq |
CONTEXTDo not trust the table; build it. The full reproduction
is a turnkey bundle: one Mathlib-only Lean file, a lakefile, a lean-toolchain, and a
README.
git clone https://github.com/jonwashburn/c-blind-projection cd c-blind-projection lake exe cache get # fetch the pinned Mathlib build cache lake build # builds CBlindProjection.lean # then inspect the axiom footprint of any cited theorem, e.g.: # #print axioms couplingC_eq
PROVEDAxiom footprint: propext,
Classical.choice, Quot.sound. No domain axioms.
CONTEXTIf the build fails, a named theorem is absent or its
statement differs from its row, or #print axioms reports anything else, a PROVED row above is false —
treat the PROVED band as unresolved and report it (§7).
CONTEXTWhat an opponent correctly concedes is open — stated first. The machine-checked theorems are, taken alone, finite integer and graph combinatorics. An honest critic will say: the certified core is light, and the economic content lives in the unverified TEXT-LEVEL and MODEL bridge, so the Lean certificate proves nothing economically interesting.
CONTEXTThat objection is accepted as the structure of the page. The certified core is small and exact on purpose; the load-bearing interpretive step — that b₁ is the right measure of value, and that the settlement graph is the right object — is TEXT-LEVEL/MODEL on purpose.
PROVEDThe Lean core's job is narrow: given the model, the combinatorial consequences are exactly as stated, with no hidden assumption smuggled in as a domain axiom. It discharges that and no more.
CONTEXTWhat is explicitly not claimed. This is not an impossibility theorem for welfare analysis.
TEXT-LEVELA central observer who treats the seam count s as an observable commodity represents Z = b₁(A∪B) exactly, because Z is a closed-form function of s.
TEXT-LEVELCooperative game theory can impute C as a coalition surplus; a Shapley split exists. Neither is contested.
CONTEXTWhere the content actually sits — one level beneath that fix:
PROVED(1) Measurement: the private profile does not determine Z
(Z_not_function_of_profile), so any objective taking only private values is blind to C.
PROVED(2) Internalization dichotomy: C is representable by a
central commodity price on s and by no agent acting on its own private record (agent_local_*); the
seam has
no third faithful fate (seam_dichotomy), and recovering C jointly reconstructs the center
(coalition_is_central). What is impossible is non-cooperative, private-record internalization — not
welfare analysis, and not cooperative imputation.
MODELThe open seam is the TEXT-LEVEL/MODEL bridge of §4: whether b₁-loop-closure is the right measure of value, and whether the finite settlement graph is the right object for the economies one wants to model. Close it or break it.
CONTEXTThis is the contract. Each non-PROVED claim names a condition that would refute it; each PROVED claim is refuted by a failing build or an unexpected axiom.
lake build fails on the bundle, a named theorem is absent or its statement differs from its row, or
#print axioms reports an axiom outside propext, Classical.choice,
Quot.sound.
CONTEXTSubmission. Falsifications, counterexamples, theorem-statement discrepancies, build logs, and failed reproductions go to the issue tracker at github.com/jonwashburn/c-blind-projection; a refuted row will be re-tagged KILLED with the test attached.
No result yet. This section describes a pre-registered instrument and a prediction under test. There is no measured outcome. Do not cite it as evidence.
INSTRUMENTA pre-registered, anti-cheat protocol measures the Betti-1 closed-loop value Z on a non-human public transaction network — a DeFi / blockchain transaction graph — where the full graph is observable and posting histories cannot be selectively withheld.
PREDICTEDLow-closure divergence — high transaction flow combined with low loop-closure — predicts liquidity stress better than flow and volume baselines.
PREDICTEDBaseline it must beat: standard flow- and volume-based liquidity-stress indicators on the same network and window. The prediction is recorded as failed unless the loop-closure signal yields a measurable, pre-registered, out-of-sample improvement over those baselines.
INSTRUMENTThe instrument is invalidated if the protocol permits post-hoc changes to data selection, graph construction, stress labels, baselines, or scoring metrics after outcomes are known. Status remains INSTRUMENT / PREDICTED until a result is posted here.
CONTEXTThis work uses the same finite-graph machinery as Recognition Science, which derives mathematics and physics from one primitive (distinction / the J-cost balance law) and has appeared in the peer-reviewed venues Axioms and Mathematics (MDPI). Economics here is that machinery applied at the settlement layer.
CONTEXTExplicit no-halo caveat: provenance is context, not evidence. The Lean core is checkable without accepting Recognition Science and without endorsing any of its physics.
CONTEXTTwo points, plainly: peer review at MDPI is not load-bearing here — provenance is context, not proof, and nothing in the certified core depends on it; and the build in §5 stands or falls on its own axiom footprint, so if you reject Recognition Science wholesale, the PROVED rows are unaffected.
CONTEXTPaper: The C-Blind Projection: A Topological Obstruction to Welfare Aggregation (PDF).
CONTEXTCode: turnkey Lean bundle, github.com/jonwashburn/c-blind-projection.
Next action, by reader:
lake build, and #print axioms the theorems in §4; report any deviation from the
three-axiom footprint.