05 — Formal Theorems and Proofs

Core claim: 7 theorems are derivable from the 3 axioms and the source texts. These theorems show that several “exceptions” are actually forced consequences of the axiom system, and that the fraction set has a rigid algebraic structure.

Theorem 1 — Eligibility is Decidable

Statement: For any heir vector $\vec{h} = (g, j, d, q, c)$, the chain validity $c$ is computable from the BFS path by exactly three axis-specific predicates.

Notation: Let $\text{path} = [p_0, p_1, \ldots, p_n]$ where $p_0$ = deceased, $p_n$ = heir, and each $p_i \in {M, F}$.

Predicates:

$$c_{\text{desc}}(j=1): \quad c = 1 \iff p_1, \ldots, p_{n-1} \in M^* \quad \text{(all intermediaries are male)}$$

$$c_{\text{asc}}(j=2): \quad c = 1 \iff [p_1, \ldots, p_n] \in M^F^ \quad \text{(no male may follow a female)}$$

$$c_{\text{coll}}(j \in {3,4}): \quad c = 1 \iff p_1, \ldots, p_{\pi-1} \in M^* ;\wedge; p_{\pi+1}, \ldots, p_{n-1} \in M^*$$

where $\pi$ is the pivot index (shared ancestor) in the collateral path.

Correction note: An earlier draft characterised $c_{\text{asc}}$ as “no male between two females” (i.e., no $(F,M,F)$ subsequence). This is strictly weaker and incorrect. The path $[\text{deceased}, \text{mother}(F), \text{maternal-grandfather}(M)]$ contains no $(F,M,F)$ yet the maternal grandfather is dhawī al-arḥām ($c=0$). The correct rule is $M^F^$: once any female appears on the ascending chain, no male may follow. This matches the classical restriction that a “true grandfather” (جد صحيح) admits no female on his path to the deceased, while a “true grandmother” (جدة صحيحة) may follow an earlier female. The implementation in eligibility.ts (ascendantEligible) correctly enforces $M^F^$.

Proof sketch: Exhaustive verification against the classical list of 25 heir types in faraid/reference.txt. Every valid heir satisfies exactly one predicate; every dhawī al-arḥām fails all three. $\square$

Corollary 1.1 — Direction-Parametric Unification and Impossibility of Directionless Unification

Unified formula. Let $\pi$ be the pivot index (0 for pure descendants, $n$ for pure ascendants). Then:

$$c = 1 \iff \underbrace{[p_1, \ldots, p_\pi] \in M^F^}{\text{upward leg}} ;\wedge; \underbrace{p{\pi+1}, \ldots, p_{n-1} \in M^*}_{\text{downward leg}}$$

Verification by case:

$j=1$ ($\pi=0$): Upward leg is empty — $M^F^$ trivially. Downward condition = $p_1,\ldots,p_{n-1}\in M^*$. Matches $c_{\text{desc}}$. $\checkmark$
$j=2$ ($\pi=n$): Downward leg is empty — $M^*$ trivially. Upward condition = $[p_1,\ldots,p_n]\in M^F^$. Matches $c_{\text{asc}}$. $\checkmark$
$j\in{3,4}$: Both conditions apply at the pivot split. Matches $c_{\text{coll}}$. $\checkmark$

The three predicates are one formula specialised by the pivot index.

Impossibility theorem. No predicate $f$ that takes only the raw suffix $[p_1,\ldots,p_n]$ (without $\pi$) can correctly compute $c$ in all cases.

Proof. Counterexample: let $[p_1, p_2] = [F, F]$.

Case A — $j=2$, maternal grandmother: path $= [\text{deceased}, \text{mother}(F), \text{maternal-grandmother}(F)]$. $[F,F]\in M^F^$. Correct $c=1$.
Case B — $j=1$, granddaughter via daughter: path $= [\text{deceased}, \text{daughter}(F), \text{granddaughter}(F)]$. $p_1=F\notin M^*$. Correct $c=0$.

Both cases present the identical raw suffix $[F,F]$ but require opposite outputs. Any deterministic function of the raw suffix alone must fail one. Contradiction. $\square$

Consequence. The pivot index $\pi$ (equivalently, jiha $j$ or path direction) is a necessary and irreducible input to the eligibility test. The direction-parametric formula above is the unique minimal unification.

Theorem 2 — The 5-Tuple is a Complete Invariant

Statement: Two heirs with identical $(g, j, d, q, c)$ vectors receive identical treatment under all axioms and exceptions.

Proof sketch: The axioms reference only $g$, $j$, $d$, $q$, $c$:

Axiom $\alpha$ uses $(1-c, j, d, q)$ — all from the tuple.
Axiom $\beta$ uses $j$, $g$, $d$, $q$ for share table lookup and pressure evaluation.
Axiom $\gamma$ is a function of the shares, which are themselves functions of the tuple.
All exceptions ($\epsilon_1$–$\epsilon_8$) reference only tuple components.

No external information (name, age, path history beyond what’s encoded in $c$) enters the computation. $\square$

Caveat: Within the ascendant axis ($j=2$), maternal vs. paternal grandmother have the same tuple $(0, 2, 2, 9, 1)$. They are distinguished by path origin for the purpose of pool-sharing (both share the $\frac{1}{6}$), but their individual shares are computed identically. The tuple determines eligibility and share quantum; the path origin determines which pool they share within.

Theorem 3 — Fraction Generation

Statement: The complete set of farḍ shares $\mathcal{F} = \left{\frac{1}{2}, \frac{1}{3}, \frac{2}{3}, \frac{1}{4}, \frac{1}{6}, \frac{1}{8}\right}$ is generated from exactly two seeds under two operations.

Seeds: $\frac{1}{2}$ and $\frac{1}{3}$

Operations:

Halving: $x \mapsto \frac{x}{2}$
Ceiling (doubling the numerator and adding $\frac{1}{6}$): Maps solo share to plural ceiling — effectively $\frac{1}{2} \mapsto \frac{2}{3}$

Derivation:

$$\frac{1}{2} \xrightarrow{\text{halve}} \frac{1}{4} \xrightarrow{\text{halve}} \frac{1}{8}$$

$$\frac{1}{3} \xrightarrow{\text{halve}} \frac{1}{6}$$

$$\frac{1}{2} \xrightarrow{\text{ceiling}} \frac{2}{3} \quad \left(\text{i.e., } \frac{1}{2} + \frac{1}{6} = \frac{2}{3}\right)$$

Corollary: All denominators lie in the set ${2^a \times 3^b : 0 \le a \le 3, ; 0 \le b \le 1}$, i.e., the fraction field $\mathbb{Q}_{(2,3)}$.

Proof: Exhaustive. The six fractions listed are exactly the Qurʾānic shares. The two seeds and two operations produce exactly this set and nothing more. The identity $\text{LCM}(2, 3, 4, 6, 8) = 24 = 2^3 \times 3$ confirms the prime structure. $\square$

Theorem 4 — The $\frac{2}{3}$ Cap is Forced

Statement: The group ceiling for female farḍ groups (daughters, sisters) must be exactly $\frac{2}{3}$. No other value is consistent with the axiom system.

Proof:

Let $C$ be the ceiling for a female group (e.g., 2+ daughters).

Constraint 1 (Parental guarantee): Both father and mother are guaranteed at least $\frac{1}{6}$ each when descendants exist. Therefore:

$$\text{parental floor} = \frac{1}{6} + \frac{1}{6} = \frac{1}{3}$$

Constraint 2 (Conservation): $\sum \le 1$.

Therefore:

$$C + \frac{1}{3} \le 1 \implies C \le \frac{2}{3}$$

Constraint 3 (Maximality): The Qurʾān assigns the largest possible share to the children. Among all fractions $\le \frac{2}{3}$ in $\mathbb{Q}_{(2,3)}$, the value $\frac{2}{3}$ is the maximum.

Therefore $C = \frac{2}{3}$. $\square$

Corollary: The completion gap (the difference between the solo $\frac{1}{2}$ and the share needed by a supplementary heir — e.g., son’s daughter gets $\frac{1}{6}$) is:

$$\frac{2}{3} - \frac{1}{2} = \frac{1}{6}$$

This is the universal quantum of the system — the same value as the minimum parental guarantee.

Theorem 5 — ʿAwl Only Occurs at 2-3 Composite Bases

Statement: ʿAwl (proportional compression) can only occur when the base (أصل المسألة) is divisible by both 2 and 3. Specifically, the ʿawl-capable bases are ${6, 12, 24}$.

Proof:

For ʿawl to occur, $\sum \text{farḍ} > 1$ while all heirs are farḍ (no ʿaṣaba).

Case: Base is a pure power of 2 (${2, 4, 8}$). All fractions have denominators that are powers of 2. The fractions are nested: $\frac{1}{8} \subset \frac{1}{4} \subset \frac{1}{2}$. In any combination where all shares have power-of-2 denominators, the sum cannot exceed 1 without an ʿaṣaba heir absorbing the excess. (The only fractions are $\frac{1}{2}, \frac{1}{4}, \frac{1}{8}$, and these correspond to spousal shares which are always paired with at least an ʿaṣaba.)

Case: Base is a pure power of 3 (${3}$). The fractions are $\frac{1}{3}$ and $\frac{2}{3}$. Sum: $\frac{1}{3} + \frac{2}{3} = 1$ (exact). By Jumhūr consensus, base 3 does not ʿawl (Muʿādh’s dissent is a minority position).

Case: Base has both factors (${6, 12, 24}$). Now fractions from both prime families coexist (e.g., $\frac{1}{2}$ and $\frac{1}{3}$ sum to $\frac{5}{6} < 1$, but $\frac{1}{2} + \frac{1}{2} + \frac{1}{3} = \frac{4}{3} > 1$). ʿAwl is possible and documented.

Source: faraid/awl.md — “ما يعول باتفاق القائلين بالعَوْل… أصل: (٦، ١٢، ٢٤)” and “ما لا يعول بالاتفاق… أصل: (٢، ٤، ٨، ١٨، ٣٦)” $\square$

Theorem 6 — ʿAṣaba maʿa al-Ghayr is an Anti-ʿAwl Optimization

Statement: The rule that sisters become ʿaṣaba in the presence of daughters is the unique assignment that prevents ʿawl while preserving the priority cascade.

Proof:

Consider the case: 1 Daughter, 1 Full Sister.

Option A (both take farḍ): Daughter $\frac{1}{2}$, Sister $\frac{1}{2}$. Sum = 1. ʿAwl doesn’t trigger here, but add any third farḍ heir (e.g., mother $\frac{1}{6}$) and sum $= \frac{1}{2} + \frac{1}{2} + \frac{1}{6} = \frac{7}{6} > 1$. ʿAwl triggers.

Option B (sister becomes ʿaṣaba): Daughter $\frac{1}{2}$, Sister takes remainder $= \frac{1}{2}$. If mother exists: Daughter $\frac{1}{2}$, Mother $\frac{1}{6}$, Sister takes remainder $= \frac{1}{3}$. Sum = 1. No ʿawl.

The critical insight: under Option B, the sister’s share is flexible (it absorbs whatever remains), so adding more farḍ heirs simply reduces the sister’s share rather than triggering compression. Under Option A, the sister’s share is rigid, so any additional heir pushes the system past capacity.

Uniqueness: No other assignment preserves:

The daughter’s farḍ share (Qurʾānically fixed).
The sister’s right to inherit (she’s a valid heir).
The $\sum \le 1$ constraint without ʿawl.

The only degree of freedom is the sister’s inheritance mode (farḍ vs ʿaṣaba), and only ʿaṣaba satisfies all three constraints simultaneously.

Ḥadīth confirmation: The Prophet ﷺ ruled in the case of a daughter and a sister: “give the daughter her half, the sister what remains” — exactly ʿaṣaba treatment.

Therefore $\epsilon_5$ is derived, not exceptional. $\square$

Theorem 7 — The ʿUmariyyatān are Forced

Statement: In the cases {Husband, Mother, Father} and {Wife, Mother, Father}, the mother must receive $\frac{1}{3}$ of the remainder (not $\frac{1}{3}$ of the total) to satisfy the parent constraint father $\ge$ mother.

Proof:

Case 1: Husband $\frac{1}{2}$, Mother, Father.

Standard rule: Mother gets $\frac{1}{3}$ of total.

Husband: $\frac{1}{2}$
Mother: $\frac{1}{3}$
Father (remainder): $1 - \frac{1}{2} - \frac{1}{3} = \frac{1}{6}$

Violation: Father ($\frac{1}{6}$) < Mother ($\frac{1}{3}$). But in the same generation, the male should receive at least as much as the female (the 2:1 rule applied to parents means father $\ge$ mother).

Dynamic baseline: Mother gets $\frac{1}{3}$ of remainder after spouse.

Husband: $\frac{1}{2}$
Remainder: $\frac{1}{2}$
Mother: $\frac{1}{3} \times \frac{1}{2} = \frac{1}{6}$
Father: $\frac{1}{2} - \frac{1}{6} = \frac{1}{3}$

Check: Father ($\frac{1}{3}$) = $2 \times$ Mother ($\frac{1}{6}$). ✓ The 2:1 ratio is restored.

Case 2: Wife $\frac{1}{4}$, Mother, Father.

Standard rule:

Mother: $\frac{1}{3}$, Father: $1 - \frac{1}{4} - \frac{1}{3} = \frac{5}{12}$

Father ($\frac{5}{12}$) > Mother ($\frac{1}{3} = \frac{4}{12}$). No violation — but for consistency (both cases should use the same rule), and because ʿUmar ruled on both cases together:

Dynamic baseline:

Remainder: $\frac{3}{4}$
Mother: $\frac{1}{3} \times \frac{3}{4} = \frac{1}{4}$
Father: $\frac{3}{4} - \frac{1}{4} = \frac{1}{2}$

Check: Father ($\frac{1}{2}$) = $2 \times$ Mother ($\frac{1}{4}$). ✓

Uniqueness: The dynamic baseline is the only modification of the mother’s share that:

Preserves the mother’s entitlement to $\frac{1}{3}$ (just of a different base).
Restores father $\ge$ mother.
Does not alter the spouse’s Qurʾānically fixed share.

Therefore $\epsilon_6$ is forced, not arbitrary. $\square$

Summary Table

#	Theorem	Type	Key Implication
1	Eligibility is decidable	Structural	$c$ computable from 3 predicates
2	5-tuple is complete invariant	Structural	No external data needed
3	Fraction generation	Algebraic	All shares from ${\frac{1}{2}, \frac{1}{3}}$ under halving/ceiling
4	$\frac{2}{3}$ cap is forced	Algebraic	Ceiling value is unique
5	ʿAwl requires 2-3 composites	Algebraic	Only bases 6, 12, 24 can ʿawl
6	ʿAṣaba maʿa al-ghayr is optimization	Derivation	$\epsilon_5$ is not an exception
7	ʿUmariyyatān are forced	Derivation	$\epsilon_6$ is not an exception

References

Grandmother ijmāʿ: faraid/jaddah.md
Fraction bases: faraid/tasil.md
ʿAwl data: faraid/awl.md
ʿAṣaba rules: faraid/asaba.md
Exclusion rules: faraid/hajb.md
Primary reference: faraid/reference.txt