"""Finite reliability budgets and corrected elementary scalar calculations.

Source/trajectory theorems are manuscript inputs; no Lean build is performed.
All accepted six-term and startup comparisons below use rational enclosures.
"""
from dataclasses import dataclass
from fractions import Fraction as F
from math import ceil, floor
import mpmath as mp

EPS=F(1,500000000)
D=F(1,6*10**20)
C=D*D/(8*10**7)
TOLERANCES=(F(1,8),F(1,80),F(1,100000),F(1,3*10**20),F(1,40),F(1))
COEFFICIENTS=(2,12,4,2,2,2)
NAMES=('nonfood_mass','six_foods','selected_foods','selected_product','export','gross_feed')


def exp_negative_bounds(x):
    x=F(x)
    if x<0:raise ValueError('Nonnegative exponent required.')
    if x>100:
        _,upper=exp_negative_bounds(F(100));return F(0),upper
    # Outward grid rounding bounds the exponent, preventing huge rational
    # denominators from propagating through every power.
    scale=10**12;lo=F(floor(x*scale),scale);hi=F(ceil(x*scale),scale);degree=200
    def sum_tail(z):
        total=term=F(1)
        for k in range(1,degree+1):term*=z/k;total+=term
        return total,term*z/(degree+1)/(1-z/F(degree+2))
    slo,_=sum_tail(lo);shi,tail=sum_tail(hi)
    return 1/(shi+tail),1/slo


def log_upper(x):
    x=F(x)
    if x<=0:raise ValueError('Positive logarithm input required.')
    mp.iv.dps=60;v=mp.iv.ln(mp.iv.mpf(x.numerator)/x.denominator)._mpi_[1]
    sign,mantissa,exponent,_=v
    return F((-1)**sign*mantissa)*F(2)**exponent


@dataclass(frozen=True)
class TwoWindowCertificate:
    n: int = 4
    V: int = 5001*10**46
    tolerance_fraction: F = F(99,100)

    def __post_init__(self):
        object.__setattr__(self,'tolerance_fraction',F(self.tolerance_fraction))
        if type(self.n)!=int or self.n<4 or type(self.V)!=int or self.V<1 or not 0<self.tolerance_fraction<1:raise ValueError('n>=4, integer V>0 and interior tolerance fraction required.')

    def terms(self):
        rows=[]
        for index,(name,limit,b) in enumerate(zip(NAMES,TOLERANCES,COEFFICIENTS)):
            s=self.tolerance_fraction*limit;mass=index in [0,4,5];jump=F(self.n if mass else 2,self.V)
            exponent=s*s*self.V/(4*self.n*(96011*200+s) if mass else 4*(96000*200+2*s))
            rows.append(dict(name=name,tolerance=s,permitted=limit,jump_correction=jump,margin_valid=s+jump<=limit,
                             exponent=exponent,failure_upper=b*exp_negative_bounds(exponent)[1]))
        return rows

    def evaluate(self):
        rows=self.terms();valid=all(r['margin_valid'] for r in rows);error=sum(r['failure_upper'] for r in rows)
        return dict(status='valid conditional bound' if valid else 'not certified',rows=rows,
                    failure_upper=min(F(1),error) if valid else None,reliability_lower=max(F(0),1-error) if valid else None,
                    hypotheses='Food-only start, empty food rows, selected self-incidence, all allowed marks, same path through time 199; imported six-noise theorem')

    def sufficient_scale(self,eta=F(1,100)):
        eta=F(eta)
        if not 0<eta<1:raise ValueError('Interior failure target required.')
        rows=[]
        for index,(name,limit,b) in enumerate(zip(NAMES,TOLERANCES,COEFFICIENTS)):
            s=self.tolerance_fraction*limit;mass=index in [0,4,5];jump=self.n if mass else 2
            deterministic=ceil(jump/(limit-s));factor=4*self.n*(96011*200+s) if mass else 4*(96000*200+2*s)
            stochastic=ceil(factor*log_upper(F(6*b)/eta)/(s*s))
            rows.append(dict(name=name,deterministic_minimum=deterministic,tail_minimum=stochastic))
        V=max(max(r['deterministic_minimum'],r['tail_minimum']) for r in rows)
        # The directed logarithm yields an integer sufficient candidate; replay
        # the actual rational tail bound at that candidate before certifying it.
        evaluated=TwoWindowCertificate(self.n,V,self.tolerance_fraction).evaluate()
        if evaluated['failure_upper']>eta:raise ArithmeticError('Finite enclosure too coarse for proposed sufficient scale.')
        return dict(count_scale=V,dominant_term=max(rows,key=lambda r:r['tail_minimum'])['name'],rows=rows,failure_upper=evaluated['failure_upper'])

    def uniform(self):
        valid=self.V>=2*self.n/D;error=24*exp_negative_bounds(C*self.V/self.n)[1]
        return dict(status='valid conditional bound' if valid else 'not certified',failure_upper=min(F(1),error) if valid else None,
                    envelope_hypothesis=self.V>=10**60*(self.n+1)**2,exponent=C*self.V/self.n)


def first_birth_ceiling(V,t=F(1)):
    t=F(t)
    if type(V)!=int or V<1 or t<0:raise ValueError('Positive integer count scale and nonnegative time required.')
    lo,hi=exp_negative_bounds(F(484,3)*EPS*V*t)
    return dict(lower_evaluation=1-hi,upper_evaluation=1-lo,
                meaning='Ceiling on birth by t before corridor exit, food-silent source only; mission uses t=1')


def necessary_startup_scale(eta=F(1,100)):
    eta=F(eta)
    if not 0<eta<1:raise ValueError('Interior failure target required.')
    lam=F(484,3)*EPS
    candidate=ceil(log_upper(1/eta)/lam)
    # The preceding integer's maximum possible success falls below the target.
    if first_birth_ceiling(candidate-1)['upper_evaluation']>=1-eta:raise ArithmeticError('Cannot resolve exact integer boundary with this enclosure.')
    return dict(necessary_integer_scale=candidate,interpretation='necessary only, not sufficient for first birth or operation')


def deterministic_noise_checks():
    """Correct compensator accounting for two slips in the manuscript prose.

    If L'=10-L plus additive prefix noise bounded by eta, variation of constants
    yields L<=10+2eta, not a constant compensator. For x, the lower forcing is
    epsilon*u_min^2; its equilibrium scale is forcing/1476.
    """
    etaF=F(1,100000);etaP=TOLERANCES[3];floorstock=F(1,3*10**18)
    food=F(1,1358)-2*etaF;forcing=EPS*food*food
    # exp(-1476)<=1/1477 follows from exp(t)>=1+t.
    xlower=(forcing/1476-etaP)*(1-F(1,1477))-etaP
    assert food>0 and xlower>floorstock
    rate=F(19,10)-480*EPS
    window=lambda duration:(duration*rate-54)/640-F(1,20)
    return dict(food_lower=food,product_forcing_lower=forcing,product_equilibrium_lower=forcing/1476,
                product_at_one_lower=xlower,stock_floor=floorstock,mass_upper_from_prefix_noise=10+2*F(1,4),
                interval99_occupation=(99*rate-54)/640,interval99_export_lower=window(99),
                interval78_export_lower=window(78),interval79_export_lower=window(79),material_recovery_lower=F(1,12000),
                corrections='Mass compensator is not identically 10. In Lemma 5.5 the forcing is about 1e-15; about 6.9e-19 is the equilibrium floor, not that forcing.')