Disclosure Without a Predicate

On 10 December 2026, Australian Privacy Principles 1.7 to 1.9 start to apply. I read them wanting to write the compliance test, and I have written it, as far as it goes. It goes less far than the essay I published in August said it would.

APP 1.7 is a rule about a document whose truth lives outside the document. Three claims follow. First, no checker that reads only a published policy can decide whether the policy meets the duty; the answer depends on a private register and on judgments that the statute leaves open. That is a theorem, under stated hypotheses. Second, coverage is monotonic [listing more can never lose], so a regulator's advice to include what you doubt pushes toward a list that tells a reader nothing. Third, and most contestable: the OAIC's model text, printed as compliant, does not say which decisions a program makes alone, which is the one distinction APP 1.8 draws that an affected individual could use. So even the part that looks mechanical contains a choice.

I build AI systems for law firms and I gain if firms pay attention to this. Nothing here is legal advice about what anyone must do. Everything below is the statute and the regulator's guidance as I read them on 2 November 2026.

I also owe a correction. In Make the Safe Harbour Compile I wrote of a published predicate: "A firm can run the predicate before shipping, and know" and "A regulator can run it across every filing rather than a sample." For an obligation shaped like APP 1.7, neither holds as written. The firm knows only what its own judgments imply. The regulator's scan reaches the document and stops. I still hold the essay's other line, that a predicate relocates vagueness to named places. This chapter is what that looks like when the named places hold most of the load.

What the duty says, and to whom

All of this section is Australian law. The text was inserted by Part 15 of Schedule 1 to the Privacy and Other Legislation Amendment Act 2024 (Cth). An APP privacy policy "must contain the information covered by subclause 1.8" if:

• (a) "the entity has arranged for a computer program to make, or do a thing that is substantially and directly related to making, a decision";
• (b) "the decision could reasonably be expected to significantly affect the rights or interests of an individual";
• (c) "personal information about the individual is used in the operation of the computer program" to make the decision or do the related thing.

APP 1.8 then requires "the kinds of personal information used", "the kinds of such decisions made solely by the operation of such computer programs", and the kinds "for which a thing, that is substantially and directly related to making the decision, is done". APP 1.9 adds that refusing or failing to decide counts, that beneficial effects count, and gives three examples: a statutory benefit, contractual rights, and "access to a significant service or support".

Who. The duty binds APP entities, which is the first question on the OAIC's flowchart. Section 6(1) defines an APP entity as "an agency or organisation", so government agencies within that definition are bound as well as businesses, and section 6C leaves a State or Territory authority and a registered political party out of "organisation". An organisation carrying on business in Australia has an Australian link under section 5B(3), which is why a foreign firm with a Sydney office should read on. A business with annual turnover of $3,000,000 or less is generally a small business operator outside the regime, but section 6D(4) takes back health service providers holding health information, credit reporting bodies, those who trade personal information for a benefit, and Commonwealth contractors, among others. I read the Act's sections in the Australian Taxation Office's copy, and I do not claim to have listed every exclusion.

When. Item 89 applies the duty to "decisions made after the commencement", whether the arrangement, the use of the data or the data itself came before or after. Nothing is grandfathered [exempted because it already exists]. A system procured in 2021 making a decision on 11 December 2026 is covered.

What follows a breach. Item 87 adds APP 1.7 to section 13K(1)(b), the civil penalty provision for which infringement and compliance notices can be issued, capped at 200 penalty units for a person. Section 82(5) of the Regulatory Powers Act (as made) sets the cap for a body corporate at five times that, and the Explanatory Memorandum (para 88) says so: 1,000 penalty units. In December 2025 the OAIC described the consequence of a non-compliant policy as notices and penalties of "up to $66,000", which the Memorandum gives as the figure for a person, with $330,000 for a body corporate, at the unit value when the Bill was introduced. A 2026 instrument sets the unit at $364, and its note speaks of offences, so I give the cap in units. The Memorandum (para 91) puts the amount stated in an infringement notice at 12 units for a person, 60 for a body corporate and 200 for a listed corporation.

What does not follow. Part 15 gives the individual nothing beyond the policy text. The older machinery remains: a breach of an APP in relation to personal information about an individual is an interference with that individual's privacy (section 13(1)), and the individual may complain to the Commissioner (section 36). That is a complaint about the policy, not a right to be told about a decision. In 2023 the Government agreed that individuals "should have a right to request meaningful information" about such decisions (proposal 19.3). That right is not in Part 15. The Guidelines (para 1.69) ask that information be "framed in a way that allows the information and the decision to be challenged or contested", but a perfect APP 1.7 policy still tells nobody that a program refused their loan. Compare the EU, on the CJEU's press release in C-203/22 under GDPR Article 15(1)(h): the controller must describe "the procedure and principles actually applied", to the data subject, so that they can understand and challenge it. The EU's Article 22(1) (a reproduction; EUR-Lex refused my fetch) reaches decisions "based solely on automated processing", which the Court has held can include a credit score where a lender attributes to it "a determining role" (press release in C-634/21), and the OAIC's text reaches further: a decision "may be within scope ... even where a computer program output does not replace the entire decision-making process or is subject to human review". Wider trigger and shallower content, against narrower trigger and deeper content. The UK has replaced its Article 22 (Data (Use and Access) Act 2025, s 80), and I do not analyse it here.

Four questions that look like one

"Is the disclosure true?" is four questions, with four different answerers.

H.L.A. Hart's formulation fits question 4 exactly. There is "a core of settled meaning, but there will be, as well, a penumbra of debatable cases in which words are neither obviously applicable nor obviously ruled out" (Hart, 1958). A program approving loans is core; the OAIC's fact sheet lists it. A word processor used to type a decision up is out (Guidelines, para 1.40). Between them sit its own examples, and they are harder than the statute's words suggest:

• A spreadsheet is enough. Example 1 puts in scope a spreadsheet formula that ranks people for care.
• Significance varies by person. Suspending an account at Glowride, its rideshare example, "will depend on the individual's circumstances" (Guidelines, Example A). A policy is one document per entity.
• Scope can move with no deployment. Machine learning or generative outputs are generally in scope "unless subject to extensive human oversight and control" (fact sheet), and reliance and likelihood of override are listed factors (para 1.53). If reviewers drift into rubber-stamping, a row can cross the line with no code change. The policy must meanwhile stay "up-to-date" (para 1.11), which is the problem of Yesterday's Permission in a statutory coat.

The predicate, and its declared parameters

The block below compiles, copied from lean/BuildingInSteel/Disclosure.lean, on Lean v4.29.1 with no libraries beyond the book's case file. J is a record of seven judgment functions: arranged, solely, related, significant, exempt, confidentialPI and confidentialDecision. Lean takes them as inputs, says nothing about their right values, and the general theorems below quantify over all of them.

def inScope (J : Judgments) (u : ProgramUse) : Bool :=
  J.arranged u && (J.solely u || J.related u) && J.significant u &&
  !u.piUsed.isEmpty && !J.exempt u

def coversStrict (J : Judgments) (R : List ProgramUse) (p : Policy) : Bool :=
  R.all (fun u => !inScope J u || (piOK J p u && decisionOKStrict J p u))

coversStrict is not compliance. It is one reading of APP 1.8 as a Boolean, conditional on a register R that nothing here shows is complete and on J. Only one conjunct of inScope comes from the record alone, piUsed being non-empty, and what counts as personal information is a further question I leave out. In August I wrote that a predicate which fails "gives you a line number". Here the line number will often name a field of J, and that is the honest result: the formalisation does not settle "significantly", it says where "significantly" sits. This follows the shape of FormalisationBoundary in LegalLean, and The Translator Writes the Rule takes up who chooses the reading.

The answer is not in the document

The theorem I wanted, and could not get, was a test on the published policy. Here is why not; the block is the statement only, proof in the same file.

theorem no_test_on_policy_alone (J : Judgments) (u : ProgramUse)
    (hs : inScope J u = true) (hd : J.confidentialDecision u.decision = false)
    (f : Policy → Bool) :
    ∃ R, f {} ≠ coversStrict J R {} ∧ f {} ≠ coversGrouped J R {} := by

For every function f that sees only the policy, given one row the judgments put in scope and do not withhold, some register makes f wrong about the empty policy, on both readings of APP 1.8. An empty register passes, and that one row fails. A blank section is fine for a firm with no in-scope program. Nor is blankness special: no_test_at_any_policy_missing_a_row proves the same on the two-list reading at any policy that misses one row, under any judgments. listEverything escapes only because it misses none.

This is what separates APP 1.7 from most of APP 1.4. The OAIC's first sweep reviewed approximately 60 entities against APP 1.4 and, in the Commissioner's words, "found instances of non-compliance in a significant proportion" (Kind, 18/06/2026). A duty such as APP 1.4(e), how to complain, binds every policy, so a missing paragraph is visible on the page. APP 1.7 is conditional on private facts, so its absence is not. The Explanatory Memorandum, on section 13K generally, describes obligations "where a contravention can be easily established, such as an APP entity failing to include the requisite information in a privacy policy" (para 89), determinable "through straightforward, factual circumstances" (para 90). For APP 1.4 I agree. Item 87 puts APP 1.7 on the same list, and what APP 1.7 makes requisite depends on the seven fields above. I think that sentence is wrong for this subclause, and the notice regime will test it.

The document alone can refute something narrower. decisions_without_information_refuted proves that, with nothing withheld, a policy stating a decision kind and no kind of personal information cannot both cover the register and be free of phantom listings, for any register. That is the kind of thing question 1 can do: catch incoherence, and never establish coverage.

Outside evidence does better, in one direction. witness_refutes proves that if part of the register fails the check, the whole fails. So a complainant or journalist who shows one undisclosed program can refute, under given judgments, and no quantity of passing rows confirms. unregistered_stays_green shows the other side on one fixture: leave a row off and the check goes green. Whoever declares the register sets the exam.

Listing more never loses

The fact sheet says entities in doubt "should take a cautious approach and include information". Sensible as advice, and formally it has one direction. covers_mono_policy proves that widening a policy preserves coverage. list_everything_passes proves that a policy listing every kind passes the stricter reading, for every judgment and every register in the model.

The OAIC knows this, and asks for more: detail "must be meaningful to a reasonable person" (fact sheet) and entities must avoid "excessive detail that obscures the purpose of transparency" (para 1.67). Those are standards, and rightly. The check cannot see them. The two-sided check I can write, noPhantom, requires a row behind each listed decision kind, and widening_breaks_faithfulness shows on the Ashdown fixture that widening a faithful policy breaks it. But noPhantom needs the private register too, it looks at decision kinds only, and the Act's text has no phantom limb. Whether over-listing is itself misleading is a question for the standard below.

Goodhart. Machine-readable privacy disclosure has been tried, and the record is not encouraging. W3C's P3P became a Recommendation in April 2002 so that sites could "express their privacy practices in a standard format that can be retrieved automatically", and the specification is now marked obsolete. Its compact policies carried a browser incentive. Leon, Cranor, McDonald and McGuire (2010) studied the result; I could not obtain the paper's text, so the figures are from Cranor's lecture slides: "34% of 33,139 analyzed CPs had errors (11,176)", "Many CPs have been crafted to avoid IE cookie filtering", and 2,756 sites used one policy suggested by Microsoft. The target was the browser's filter, so the tokens were written for the browser. A public APP 1.7 scanner would attract the same behaviour: boilerplate that passes, carried between firms. Perfect Compliance, Defeated Purpose takes up gaming in general. My own defence is narrow: publish no score, and keep the standard behind any check.

The model text and the missing distinction

APP 1.8 has two decision limbs: kinds made solely by the program, and kinds where it does a related thing. That split is the only thing in the provision telling an individual whether a person was involved. Now read the OAIC's examples of compliant text.

Example 6: Banksia "details the following information which is compliant", naming kinds of information, then: "This information is used to make the following kinds of decisions by Banksia", listing three. The section is headed "Decisions made by computer programs", which could be taken for limb (b). Example 7 prints the same heading over decisions its narrative says staff finally make, so I do not read it as a label, and I encode the lists as unlabelled. Nothing else says which are solely automated. I am also reading these examples against their purpose: the fact sheet offers Examples 6 and 7 as "illustrations on the extent of technical information required", and Example 6 is titled "Meaning of commercial-in-confidence". It still prints the text as "compliant with the transparency obligation", without reserving the limbs. Example 7: the agency "demonstrates compliance" with information used "to support decision-making and administrative action, workflow automation, and service delivery", then lists decisions including "approve or deny government support payments", though its narrative says staff "make the final decision". "Support" may be doing the labelling there; "workflow automation" blurs it. The Guidelines' fraud illustration (para 1.73) lists "permit, flag or deny" with no split.

Encode that as banksiaPolicy, a record holding Example 6's lists in my enumerations, with two register rows I built from its narrative, and write the two obvious readings. The one-list reading accepts a decision stated anywhere. The two-list reading wants it on the right limb.

So the most literal predicate I can write from the Act refuses the regulator's model. I do not conclude the OAIC is wrong. Para 1.70 allows entities to "group information about the categories of decisions", and para 1.72 says that where all decisions use the same type of information they need not "separate out each decision on a granular basis". Grouping by category is not obviously grouping across limbs, and neither paragraph mentions them, so I read the examples as a tolerance the regulator has chosen, whether or not it chose it deliberately. The Act is what a court would read, and I have seen no decision on it.

It matters beyond tidiness. A person refused housing wants to know whether anyone looked. If the common form of disclosure is the one-list form, the statute's distinction exists and nobody can read it. And anyone writing the compliance test must pick a reading: the pick is a legal act performed in a function definition.

Who holds the parameter

judgment_flips_verdict is computed on the Ashdown instruction, the book's invented intake matter, which I extend here. Ashdown Ltd is a company, so a row about it alone has no personal information, and no_personal_information_out_of_scope removes it under every judgment. The firm's intake agent also screens the individual who signs for Ashdown, which is a different row. Assume, for the fixture only, that the firm is an APP entity. Its policy discloses the conflict check and not the intake score. Under a cautious J the check fails. Under partnerReviews, which holds that a partner's review stops the score being "substantially" related, it passes. Same document, same register. The OAIC's Example 3 says how much that reading would take: interrogating outputs, further review, additional evidence and documented divergence "could indicate" the output was not substantially related. A signature is not on that list.

narrower_scope_preserves gives the direction in general: if a reading puts in scope only rows another also does, and they agree on solely and withholding, coverage carries over from the wider to the narrower. And the party who picks the reading first is the party regulated. That is a normal feature of ex post law [settled after the event]. I am not calling it a scandal. I am saying it is the fact a checker has to be honest about.

Two parameters deserve naming because the text is quieter on them than the guidance.

Confidentiality. The fact sheet says commercial-in-confidence information is "explicitly excluded from APP 1.7 requirements", citing paragraph 38 of the Addendum to the Explanatory Memorandum. That paragraph inserts a sentence saying the obligation "is not expected to include commercial-in-confidence information about automated decision-making systems". "Not expected", in extrinsic material, has become "explicitly excluded" in the regulator's sheet. The words of Part 15 contain no such exclusion. The entity applies the factors itself. In the EU the Court went the other way on Article 15: allegedly protected information goes "to the competent supervisory authority or court", which balances. Different duty, different level of detail, so this is a contrast and no more.

Employee records. The fact sheet's Note 1 lists AI reports used to "rank employee performance, determine promotions, or decide bonus/remuneration outcomes" as generally in scope, and Example 3 applies that to a private employer. Section 7B(3) exempts an employer's act "directly related to" a current or former employment relationship and an employee record. Neither the fact sheet nor the APP 1.7 passage of the Guidelines reconciles the two, on my reading. The Explanatory Memorandum does not help: its notes on Part 15 (paras 332 to 343) are silent on the exemption, as is the Addendum, and it cites section 7B(3) only in the provisions on codes. It is a clean example of a declared parameter with real money on it.

None of this makes the vagueness a defect. Writing about constitutional law, Cass Sunstein argues that agreements on "abstract formulations" and on "particular doctrines" let people work together amidst disagreement (Sunstein, 2007, abstract read). The drafting record shows the cost was seen: the Tech Council called these provisions "alarmingly vague and uncertain" (Submission 49, 2024). Parliament passed them anyway. "Significantly" can reach a practice the Act's examples do not list; the OAIC already applies it to differential pricing (fact sheet, Example 4). I would not replace it with a threshold. I would make whoever relies on it say so.

What I would actually do: sign the parameters

Proposed, not existing, and not a legal requirement. A firm keeps a register of programs touching decisions about individuals, and for each row a scope note: what was held, by whom, as of when. APP 1.2 already asks for "reasonable steps" on practices and systems, and para 1.45 says entities should "actively identify, assess and keep oversight over" third-party programs, so this is a form for work the guidance already expects. ScopeNote and notesCurrent model it. note_needs_person_and_date is computed: a note signed by an agent fails, the same note signed by the partner passes, and it fails again past its review age. note_check_ignores_answer states the limit: opposite answers pass alike. The check attributes a judgment. It cannot validate one.

This is the book's authority question, in a modest place. A program must not sign its own scope.

Here is the split, since this is a compliance topic.

What exists and what does not

Proved generally in lean/BuildingInSteel/Disclosure.lean, for every judgment, register and policy within the stated hypotheses, with no sorry, and #print axioms listing at most propext and Quot.sound on the main results: no_test_on_policy_alone, no_test_at_any_policy_missing_a_row, decisions_without_information_refuted, strict_implies_grouped, unlabelled_fails_strict, covers_mono_policy, list_everything_passes, covers_antitone_register, witness_refutes, narrower_scope_preserves, no_personal_information_out_of_scope.

Proved for one fixture, over all qualifying J: banksia_passes_grouped, banksia_fails_strict.

Computed on fixed values: judgment_flips_verdict, unregistered_stays_green, list_everything_not_faithful, faithful_passes_both, widening_breaks_faithfulness, grouped_does_not_imply_strict, note_needs_person_and_date, note_check_ignores_answer.

Sketched: that a real policy can be extracted into Policy. Nothing here reads English. Nothing has been run on a real policy. Banksia is the OAIC's hypothetical and Ashdown is mine.

Does not exist, as far as I have read: a published machine-readable format for APP 1.7 disclosures, or a decision construing APP 1.8(b) and (c).

Prior art, and the specialist's first objection

A hostile privacy engineer's first words will be: policy truth has been machine-checked for over a decade. Correct. Sen et al. (2014) reported a system in Bing with a policy language and a data inventory which "checks compliance daily of millions of lines of ever-changing source code". MAPS compared code and policies across 1,035,853 Android apps and found, for example, that "12.1% of apps have at least one location-related potential compliance issue". PoliCheck studied 13,796 apps and found that "up to 42.4%" incorrectly disclose or omit data flows. So question 3 is not hopeless, and witness_refutes is simply the logical form of what such outside-in tools do.

Where they stop is my point. They check data flows, which have a fact of the matter at the code level. They do not decide whether output is a "key factor" for a human or whether a suspension is significant. Bing's checker ran inside the company, on its own code, and a regulator has no such access by default. If someone shows a tool extracting reliance and override rates from workflow logs across firms, questions 3 and 4 narrow, and I would welcome it. Catala and its relatives are further off: APP 1.7 computes nothing, so there is little for a statute-execution language to execute.

Objections

"APP 1.7 only asks for a statement. Truth belongs to other law." Largely right. In trade or commerce, section 18 of the Australian Consumer Law forbids conduct "that is misleading or deceptive or is likely to mislead or deceive", and APP 1.2 reaches systems. So "no test of truth" would be false as a claim about Australian law. My claim is narrower: there is no test you can run before a tribunal does, which is the title of this chapter. Verdict: the law has a truth standard, ex post, as it should. I would change my mind on seeing the OAIC publish a checkable evidence list for APP 1.7.

"A predicate whose hard parts are all parameters proves nothing." Hart's heirs will say this, and for the law they are right: coversStrict decides no contested case. What the theorems establish is how a verdict moves when inputs move: where it is one-sided, what is monotonic, and which readings differ. Concede also that no firm needs Lean for this; a spreadsheet holds a register. Lean's job here is to make the claims about the structure checkable, for this book's reader. Verdict: thin, and I have labelled it thin. I would drop the formal part if the results above turned out to be obvious to practitioners already, which a survey could show.

"Written scope notes are a liability. Nobody should create that document." The strongest practical objection. A signed note that a partner's review takes a score out of scope is what a regulator asks for first, and it may not be privileged. Verdict: a real cost, and I accept it. The alternative is the same judgment unrecorded, with APP 1.2 still asking what your systems were. A firm could reasonably run this under legal advice, which is a decision for its own lawyers. I would change my mind if regulators were shown to penalise documented reasonable judgments more heavily than undocumented ones.

"Nobody reads privacy policies, so the limb distinction is pedantry." Individuals mostly do not. Advocates, journalists and regulators do, and a limb distinction nobody can read cannot be relied on by anybody. Verdict: disagree, and prediction 2 tests whether the distinction survives in practice at all.

What formalising loses

"Significantly" lets the Glowride case come out differently for a person who needs the ride to reach a doctor. A row with one Boolean cannot do that, and my significant field hides it. The vulnerability guidance (paras 1.64 to 1.66) has no home in the model. A public check would also favour firms able to pay for a register, and I sell to those firms; the people affected gain less from a tidier register than from the right of request the Government agreed to in 2023. The check belongs behind the standard, as evidence of care, and never in place of it.

What to do on Thursday

If you are a partner advising an Australian APP entity, or running one, none of this asks you to code or buy anything. The reason to act is external: 10 December 2026. Ask the person who runs the client's systems three questions, about one business line.

1. Which programs touch a decision about an individual, including spreadsheets and chat tools staff were told they may use?
2. For each, who decided whether it is in scope, and when was that last looked at?
3. For each in-scope kind of decision, does the program decide alone, and can a reader of the policy tell?

You want a list, names and dates, and a yes or no. An hour, perhaps two, of possibly unbillable time; the honest outcome may be disclosure work you cannot charge for, or a finding your client dislikes. Take your own advice on what the answers require. I am only saying where to look.

Predictions

1. By 31/12/2027, no OAIC-published enforcement action under APP 1.7 will rest on the published policy alone. Each will cite information from the entity, a complaint or other outside evidence. Refuted by one such action whose stated evidence is only the policy text, which would mean a document-only test is more useful than no_test_on_policy_alone suggests.
2. On 30/06/2027, in the 30 alphabetically first ASX 50 companies that publish an APP 1.7 section (or all that do, if fewer, with the threshold at a majority), fewer than 16 will state, for each kind of decision, whether a program makes it solely. Refuted if that threshold is met, which would show my reading of the model text overstates how the market will follow it.
3. By 10/12/2027, neither the OAIC nor an Australian court will have said in terms whether APP 1.8(b) and (c) require separately identifiable lists. Refuted by any such statement.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.