The Judge's Impossible Function: Why Section 25 Cannot Be Formalised

10 February 2026

Introduction

In the previous essay, I formalised the O-1A visa criteria in Lean 4 and showed that immigration law, in this particular instance, behaves like a type-checking problem. The criteria are independent, the threshold is explicit, and the boundary between mechanical verification and human judgment is architecturally clean.

This essay attempts the same exercise on a legal system where none of those properties hold. The result is not a working formalisation. It is a proof that no working formalisation is possible — at least, not one that satisfies the fairness properties we would want it to satisfy. The failure is the finding.

The system is Section 25 of the Matrimonial Causes Act 1973, which governs how English courts divide assets in divorce. I chose it because it is a canonical example of judicial discretion in English law, and because the contrast with the O-1A is as sharp as any I have found: where immigration law draws clean boundaries, family law dissolves them. More than that, Section 25 turns out to be an impossibility result in disguise, and that is what makes it worth formalising.

What the formalisation reveals is that the discretion is not a malfunction. It is the system working as designed, and the system is designed to do something that is mathematically impossible to do consistently.

The Statutory Structure

Section 25(2) of the Matrimonial Causes Act 1973 requires the court to have regard to "all the circumstances of the case" and in particular to seven factors:

(a) The income, earning capacity, property, and other financial resources of each party

(b) The financial needs, obligations, and responsibilities of each party

(c) The standard of living enjoyed by the family before the breakdown of the marriage

(d) The age of each party and the duration of the marriage

(e) Any physical or mental disability of either party

(f) The contributions which each party has made or is likely in the foreseeable future to make to the welfare of the family, including any contribution by looking after the home or caring for the family

(g) The conduct of each of the parties, if that conduct is such that it would in the opinion of the court be inequitable to disregard it

The statute then requires the court to exercise its powers "so as to place the parties, so far as it is practicable and, having regard to their conduct, just to do so, in the financial position in which they would have been if the marriage had not broken down."

Notice what is absent. There is no weighting function. There is no formula for combining the seven factors into a decision. There is no threshold, no ordering, no specification of which factor takes priority when they conflict. The statute says: consider these things. Then decide.

In White v White [2001] 1 AC 596, the House of Lords introduced a "yardstick of equality" — a check against discrimination, not a presumption of equal division. In Miller v Miller; McFarlane v McFarlane [2006] UKHL 24, the Lords identified three principles — needs, compensation, and sharing — but explicitly declined to specify how they should be weighted against each other. And in Piglowska v Piglowski [1999] UKHL 27, the House of Lords held that appellate courts should not interfere with how trial judges exercise Section 25 discretion unless the outcome is "plainly wrong."

"Plainly wrong" is doing enormous load-bearing work in that sentence.

Attempting the Formalisation

The Types

I model each party's financial profile as a structure containing the Section 25 factors, and the judicial input as a pair of profiles plus context.

structure GBP where
  val : Int
  deriving Repr, BEq, Ord

instance : LE GBP where le a b := a.val ≤ b.val
instance : LT GBP where lt a b := a.val < b.val
instance : Add GBP where add a b := ⟨a.val + b.val⟩
instance : Sub GBP where sub a b := ⟨a.val - b.val⟩

structure Needs where
  housing   : GBP
  income    : GBP
  childcare : GBP
  medical   : GBP
  deriving Repr

structure Contributions where
  financial    : GBP
  nonFinancial : Nat   -- inherently lossy; see discussion below
  deriving Repr

structure PartyProfile where
  income           : GBP
  earningCapacity  : GBP
  assets           : GBP
  needs            : Needs
  contributions    : Contributions
  age              : Nat
  marriageDuration : Nat
  deriving Repr

structure Section25Input where
  party1   : PartyProfile
  party2   : PartyProfile
  totalPot : GBP
  children : Nat
  deriving Repr

structure Outcome where
  party1Allocation : GBP
  deriving Repr

So far, this looks similar to the O-1A formalisation. Types for the domain. Structures for the data. Nothing controversial.

But notice the field nonFinancial : Nat in Contributions. Section 25(2)(f) requires the court to consider contributions "by looking after the home or caring for the family." This is a qualitative assessment — how much did each party contribute through childcare, emotional support, household management? — that must be encoded as a number.

Any encoding is lossy. A natural number on an arbitrary scale is obviously inadequate. But so is any other representation. There is no principled unit of measurement for "looking after the home." The type signature is not imprecise because I made a bad design choice. It is imprecise because the underlying concept resists quantification. The type system is showing me something about the domain.

The Decision Function

def DecisionFn := Section25Input → Outcome

This is where the O-1A comparison breaks down entirely. For the O-1A, the decision function was well-specified: count the satisfied criteria, check the threshold. For Section 25, the decision function is the entire point of the statute, and the statute does not define it.

The type signature Section25Input → Outcome says: given the facts, produce a division of assets. Every judge implements this function. But different judges implement different functions. Judge A might weight needs heavily. Judge B might weight contributions. Both are lawful. Both are "correct."

In Lean 4, a function is a single, deterministic mapping. The legal system is a family of functions, and the statute does not specify which one is the right one. This is not a bug. As I will show, it cannot be otherwise.

Three Properties We Would Want

If we were to design a decision function for Section 25, what properties would we want it to satisfy? I propose three that seem minimal and reasonable.

Property 1: System Consistency

The same facts should produce the same outcome, regardless of which judge hears the case.

def systemConsistency (fs : List DecisionFn) : Prop :=
  ∀ f g : DecisionFn, f ∈ fs → g ∈ fs →
    ∀ x : Section25Input, f x = g x

This is the property the current system explicitly violates. Different judges, presented with identical Section 25 facts, will reach different outcomes. Piglowska blesses this by requiring appellate courts to defer to trial judges' discretion unless the result is "plainly wrong." The system is designed to tolerate inconsistency.

Is this a problem? Most lawyers would say no — each family is different, and judicial discretion allows the outcome to reflect the unique circumstances of the case. But this defence conflates two things: variation in outcomes due to variation in facts (which is appropriate) and variation in outcomes due to variation in judges (which is arbitrary from the parties' perspective). The current system permits both and does not distinguish between them.

Property 2: Strict Monotonicity in Financial Contributions

If Party 1 contributed more financially, all else being equal, Party 1's allocation should strictly increase.

def isStrictlyMonotonic (f : DecisionFn) : Prop :=
  ∀ x x' : Section25Input,
    -- x' is identical to x except party1 contributed more
    x'.party2 = x.party2 →
    x'.totalPot = x.totalPot →
    x'.children = x.children →
    x'.party1.income = x.party1.income →
    x'.party1.earningCapacity = x.party1.earningCapacity →
    x'.party1.assets = x.party1.assets →
    x'.party1.needs = x.party1.needs →
    x'.party1.age = x.party1.age →
    x'.party1.marriageDuration = x.party1.marriageDuration →
    x'.party1.contributions.financial > x.party1.contributions.financial →
    (f x').party1Allocation > (f x).party1Allocation

This seems obviously fair: if you put more in, you should get more out. It is also the property that the current system most conspicuously fails to guarantee. A spouse who contributed 85% of the financial assets may receive less than 50% of the pot if the other party's needs are deemed to require it. This is not a hypothetical edge case; it is the predictable outcome whenever the lower-contributing party's housing need is large relative to the total pot.

Property 3: Needs-Based Fairness

If the total assets are sufficient to meet both parties' housing needs, then neither party's allocation should fall below their housing need.

def satisfiesNeedsFairness (f : DecisionFn) : Prop :=
  ∀ x : Section25Input,
    let needs1 := x.party1.needs.housing
    let needs2 := x.party2.needs.housing
    x.totalPot ≥ needs1 + needs2 →
    (f x).party1Allocation ≥ needs1 ∧
    (x.totalPot - (f x).party1Allocation) ≥ needs2

This also seems obviously fair. If there is enough money for both parties to rehouse, both parties should be able to rehouse. No one should be made homeless when the assets exist to prevent it.

The Impossibility

These three properties — consistency, strict monotonicity, and needs-based fairness — are not exotic. They are the minimum conditions that most people would consider fair. And they cannot all hold simultaneously.

The Conflict

The conflict between strict monotonicity and needs-based fairness can be demonstrated with a single example.

Consider a case with the following facts:

Total matrimonial pot: £470,000
Party 1 contributed £400,000 financially
Party 2 contributed £70,000 financially
Party 2's housing need: £300,000 (to rehouse in the area where the children attend school)
Party 1's housing need: £250,000

Needs-based fairness requires that Party 2 receives at least £300,000. This means Party 1 receives at most £170,000.

Now consider a variation where everything is identical except Party 1 contributed £450,000 instead of £400,000. All else equal — same needs, same pot, same everything.

Strict monotonicity requires that Party 1's allocation strictly increases relative to the first case. But needs-based fairness still requires that Party 2 receives at least £300,000, which still caps Party 1 at £170,000. There is no room for the strict increase that monotonicity demands.

theorem no_strict_monotonic_and_needs_fair :
    ¬ ∃ f : DecisionFn,
      isStrictlyMonotonic f ∧ satisfiesNeedsFairness f := by
  sorry  -- Proof by constructing the witness above

The sorry is a placeholder for the formal proof, which would construct the two Section25Input values described above and derive a contradiction. The argument is straightforward: needs-fairness imposes a ceiling on Party 1's allocation that strict monotonicity requires be exceeded. The ceiling does not move when contributions change because it is determined by Party 2's needs, not Party 1's contributions.

What This Means

The impossibility is not a technical curiosity. It is a structural fact about what fairness means when resources are finite and needs are independent of contributions.

Strict monotonicity says: contributions matter. The more you put in, the more you should get out.

Needs-based fairness says: needs matter. No one should fall below the threshold when the resources exist to prevent it.

When the needs of the lower-contributing party exceed what would remain after rewarding the higher-contributing party's contributions proportionally, these two principles are in direct conflict. No function can satisfy both. No formula, no algorithm, no weighting scheme.

This is why the statute does not specify one.

The Escape Valves

The English legal system has developed three mechanisms for living with this impossibility, none of which resolve it.

Judicial Discretion

By allowing each judge to implement their own implicit weighting function, the system avoids commitment to any single function that would visibly violate one of the properties. Judge A can prioritise needs in cases where needs dominate, and Judge B can prioritise contributions in cases where the pot is large enough to satisfy both. Neither judge's approach is "wrong" because there is no specified standard to violate.

The cost is consistency. Different judges, same facts, different outcomes. The system tolerates this because the alternative — specifying a function — would make the impossibility visible.

Before proceeding, it is worth pausing on the strongest counterargument to this analysis. The argument so far treats discretion as a workaround — the system reaching for an escape valve because it cannot solve the underlying problem. But a legal theorist steeped in Cass Sunstein's work on incompletely theorised agreements would push back hard at this point.

Sunstein's argument, developed in Legal Reasoning and Political Conflict (1996), is that legal systems function precisely because they do NOT specify a complete value ordering. Judges with deeply different moral views — utilitarian, Kantian, communitarian — can agree on specific outcomes in specific cases without ever resolving their foundational disagreements. The under-specification in Section 25 is not a bug that forces judges to muddle through; it is a feature that allows a pluralistic legal system to reach decisions that are acceptable across otherwise incompatible normative frameworks.

On this view, the "escape valve" framing has it backwards. Discretion is not what remains when specification fails. Specification is what discretion makes unnecessary in most cases, at the cost of visible inconsistency in hard cases.

I think this objection is largely correct as a descriptive account of why the current system is stable, and it changes how the impossibility result should be interpreted. The result does not show that the system is malfunctioning. It shows precisely why incompletely theorised agreements are necessary: because any fully specified alternative would hit the impossibility. Sunstein gives a sociological explanation for why discretion persists; the formal result gives a mathematical explanation for why it must persist. The two accounts are complementary, not competing.

What the formal result adds that Sunstein's account lacks is specificity about the structure of the trade-off. We can say: when Party 2's housing need exceeds what would remain after proportionally rewarding Party 1's contributions, needs-based fairness and strict monotonicity cannot both be satisfied, and some function will sacrifice one. Discretion allows the sacrifice to be made contextually. But it does not make the sacrifice disappear, and it does not make it visible to the parties.

The "Plainly Wrong" Standard

Piglowska holds that appellate courts should not interfere with Section 25 discretion unless the outcome is "plainly wrong." This is not a standard; it is the absence of one. It says: we will not tell you what the right answer is, but we will tell you if your answer is so far from what any reasonable judge would produce that it cannot stand.

In formal terms, this defines not a function but a set of acceptable functions. A decision is "plainly wrong" if it falls outside this set. But the set is never specified. Its boundary is discovered case by case, through appellate decisions that say "this one went too far."

The "Yardstick of Equality"

White v White introduced equal division as a cross-check — not a presumption, but a reference point. If a proposed outcome departs significantly from equality, the judge must articulate why. This is a weak consistency mechanism: it constrains the space of acceptable functions without specifying a single one. But it does not resolve the underlying impossibility. An equal split (£235,000 each on a £470,000 pot) violates strict monotonicity when contributions are unequal, and may violate needs-based fairness if one party's housing need exceeds £235,000.

The Parallel to AI Alignment

I promised in the previous essay that the failure of this formalisation would reveal something about AI alignment. Here it is.

The problem of specifying "fair division" in Section 25 is structurally identical to the problem of specifying "aligned behaviour" in AI systems. Consider:

"Be helpful" and "be safe" are in tension. A maximally helpful AI would execute any instruction, including harmful ones. A maximally safe AI would refuse every instruction that carries risk, which is nearly all of them. No fixed weighting of helpfulness and safety satisfies both properties at their limits.

"Follow instructions" and "refuse harmful requests" are in tension. An AI that always follows instructions will sometimes comply with harmful requests. An AI that always refuses potentially harmful requests will sometimes refuse legitimate ones. The boundary depends on context that no fixed specification can anticipate.

"Be honest" and "be kind" are in tension. Sometimes the truth is cruel. Sometimes kindness requires omission. No fixed specification resolves this in all cases.

These are the same impossibility, instantiated in different domains. The fairness properties conflict. No single function satisfies all of them. Discretion — whether exercised by a judge or by an AI system — is the escape valve.

The AI alignment community has been searching for the right specification: the correct set of values, the right constitutional principles, the optimal reward function. The Section 25 impossibility result suggests this search may be fundamentally misguided. Not because values do not matter, but because no fixed specification of values can simultaneously satisfy all the properties we want.

Emmett Shear and the team at Softmax have arrived at a similar conclusion from a different direction. Their concept of "organic alignment" — where alignment emerges from ongoing negotiation between agents rather than being specified in advance — is, in formal terms, a response to exactly this impossibility. If you cannot specify a single decision function that satisfies all fairness properties, you need a process that can adapt which properties to prioritise in each case.

The judge in a Section 25 hearing is performing organic alignment in miniature. They are negotiating — within the constraints of the statute, precedent, and the specific facts — which fairness property to sacrifice in this particular case. The problem is that this negotiation is opaque, inconsistent across judges, and experienced as arbitrary by the parties inside the system.

The question, which I will take up in subsequent essays, is whether this negotiation can be made explicit, consistent, and verifiable — without collapsing it back into a fixed function that hits the impossibility result again.

What Would Have to Be True

For a formal approach to work on systems like Section 25, several things would need to change:

The properties would need to be explicitly ranked or traded off. Not "consider needs and contributions" but "in cases where needs exceed X relative to the pot, needs-based fairness takes priority over monotonicity, and here is the exchange rate." The current system hides this trade-off inside judicial discretion. A formalised system would need to make it visible.

The trade-off function would need to be negotiated, not specified. A fixed trade-off function is just another decision function, and it will hit its own impossibility at the boundaries. What is needed is a meta-level protocol for negotiating which trade-offs to make in each case — and that protocol itself must satisfy some formal properties (fairness of the negotiation process, if not fairness of the outcome).

The system would need to distinguish between "we chose to sacrifice this property" and "we failed to notice this property was being sacrificed." The current system does not distinguish between a judge who deliberately prioritised needs over contributions and a judge who forgot to consider contributions. Both outcomes look the same. A formal system could make the trade-off explicit: "In this case, strict monotonicity was relaxed by £X to satisfy needs-based fairness. Here is the calculation."

These are not small changes. They would require a fundamental redesign of how family law works — and, by analogy, how AI alignment works. But the Section 25 impossibility result at least clarifies what the challenge is. It is not finding the right formula. It is designing a process for negotiating which formula to use, case by case, with the trade-offs made visible.

Conclusion

The O-1A visa is a system that cooperates with formal specification. Its criteria are independent, its threshold is explicit, and the type checker can do most of the work.

Section 25 is a system that resists formal specification — not because the law is poorly written, but because the fairness properties it is trying to satisfy are in mathematical conflict. No fixed function can simultaneously guarantee that contributions always matter, that needs are always met, and that identical cases produce identical outcomes. The statute's silence on weighting is not an oversight. It is a necessary consequence of asking a system to do something impossible.

Judicial discretion is the escape valve. It allows each judge to resolve the impossibility locally, case by case, by implicitly choosing which property to sacrifice. The cost is consistency: different judges, same facts, different outcomes.

For anyone inside a Section 25 proceeding who came with evidence and contributions and still felt the outcome was arbitrary, this analysis offers something different from vindication. The system did not malfunction. It resolved an impossibility, locally and opaquely, by choosing which fairness property to sacrifice. That choice is experienced as injustice by the party on the losing side of the trade-off. But the injustice is not random. It is the necessary consequence of asking a finite system to satisfy mutually incompatible guarantees. Understanding that does not change the outcome, but it does change what the right question is.

The next essay asks: if a fixed function cannot work, what kind of process could? If the fairness properties must be traded off case by case, what properties should the trade-off process satisfy? And can those meta-properties be formalised, even when the object-level properties cannot?

Technical Notes

On what exists versus what is proposed. To be precise about the state of the formalisation: the type definitions (GBP, Needs, Contributions, PartyProfile, Section25Input, Outcome) are complete Lean 4 code that would compile. The property definitions (systemConsistency, isStrictlyMonotonic, satisfiesNeedsFairness) are well-typed. The theorem no_strict_monotonic_and_needs_fair has a correct type signature but is marked sorry — it is a statement, not a proof. The prose argument in the essay is the actual argument; the Lean 4 is a type-checked formulation of the premises, not a machine-verified proof of the conclusion. What does not yet exist: a complete Lean 4 proof that eliminates the sorry. Constructing it would require building the two concrete Section25Input witnesses and guiding Lean 4's unifier through the arithmetic inequality chain.

On the impossibility proof. The argument as presented is a sketch, not a complete Lean 4 proof. Completing the proof requires constructing two concrete Section25Input values and deriving a contradiction from the conjunction of strict monotonicity and needs-based fairness. The construction is conceptually straightforward: instantiate the two cases from the £470,000 example, apply both properties to the same function f, and derive 170000 > 170000, which is a contradiction. The mechanical details of working within Lean 4's type system involve producing terms of the correct types for each hypothesis, which is routine but verbose. The Lean 4 source file with the type signatures and the sorry-marked theorem is intended to accompany this essay once the proof is completed.

On weak monotonicity. The impossibility result uses strict monotonicity (more contributions → strictly more allocation). Weak monotonicity (more contributions → allocation does not decrease) is technically compatible with needs-based fairness, but only vacuously: the needs constraint can dominate completely, making contributions irrelevant to the outcome. The spirit of monotonicity — that contributions should matter — is violated even when the letter is satisfied. Whether this weaker version is worth formalising is a judgment call.

On the scope of the formalisation. The three fairness properties as stated concern only the financial contribution field (contributions.financial) and the housing component of needs (needs.housing). The nonFinancial : Nat field in the Contributions structure is present in the type definition and discussed in the text, but it does not appear in the property definitions. This is deliberate but requires explicit acknowledgement: the impossibility result as formally stated applies to a simplified model that considers only financial contributions. The full Section 25 model, which requires the court to weigh non-financial contributions (childcare, household management, emotional support) against financial ones, would require nonFinancial to appear in the monotonicity property. A richer formalisation might encode non-financial contributions as a weighted combination of financial equivalents — but any such encoding inherits the quantification problem discussed above. The impossibility result almost certainly extends to the richer model, because the ceiling imposed by one party's housing need is independent of how contributions are measured. But "almost certainly" is not a proof, and the formal statement here does not cover it.

On the scope of "needs." I have used housing need as the operand for needs-based fairness, because it is the most concrete and measurable component. The statute's concept of "needs" is broader and vaguer: it includes income needs, childcare needs, and the maintenance of the pre-divorce standard of living. A richer formalisation would decompose needs further, but each decomposition introduces new parameters and new opportunities for disagreement. The impossibility holds regardless of how needs are defined, provided the need of one party can exceed what remains after proportionally rewarding the other party's contributions.

On Arrow's Impossibility Theorem. The impossibility result in this essay is related to, but distinct from, Arrow's theorem. Arrow proves that no preference aggregation rule satisfies unanimity, independence of irrelevant alternatives, and non-dictatorship simultaneously. The Section 25 result is narrower: it concerns the aggregation of competing fairness properties over a fixed set of inputs, not the aggregation of preferences across individuals. The structural similarity — fairness properties that cannot all be satisfied — is real, but the technical details differ.

The closer relatives in the literature are Sen's liberal paradox (1970) and the impossibility results in fair division theory. Sen proved that no social welfare function can simultaneously satisfy the Pareto principle and a weak form of individual liberty. The structure is similar: two reasonable-sounding properties entail a contradiction when applied to the same set of inputs. In fair division theory, the incompatibility of envy-freeness and Pareto efficiency in indivisible good allocation (Foley 1967; Moulin 1988) is structurally identical to the Section 25 result: two fairness criteria cannot be simultaneously satisfied when resources are discrete or constrained. The Section 25 case is distinctive in that the "indivisibility" is not of goods but of housing needs — a continuous quantity that creates a hard floor on one party's allocation.

On novelty relative to existing family law scholarship. Legal scholars have long observed that Section 25 is indeterminate: John Eekelaar, Mavis Maclean, and others in the Oxford socio-legal tradition documented the unpredictability of ancillary relief outcomes in empirical studies from the 1980s and 1990s. What the formalisation here adds is not the observation of indeterminacy — that is well-known — but a precise characterisation of why indeterminacy is unavoidable. The claim is not that Section 25 produces inconsistent outcomes (that is documented). The claim is that any decision function satisfying both strict monotonicity and needs-based fairness is formally inconsistent. This is a structural result, not an empirical finding, and it explains why empirical indeterminacy is the norm rather than an implementation failure.

On proportionality and balancing. Robert Alexy's weight formula (developed in A Theory of Constitutional Rights, 2002) provides a formalisation of proportionality balancing that is used in German constitutional law and the European Court of Human Rights. Alexy proposes W(i,j) = I(i) · W(i) · R(i) / I(j) · W(j) · R(j), where I is the intensity of interference, W is the abstract weight, and R is the reliability of the empirical premises. This is a specification of a trade-off function, not a way around the impossibility. The Section 25 result implies that any such formula will, at some input values, produce outcomes that violate one of the fairness properties — which is precisely what the English courts have avoided committing to.

This is the second essay in a series on formal methods, legal reasoning, and AI alignment. Previous: When the Law Is a Type Checker: Formalising O-1 Visa Criteria in Lean 4. Next: "From Fixed Functions to Negotiation Protocols: What Mechanism Design Offers AI Alignment."